diff options
Diffstat (limited to 'theories')
-rw-r--r-- | theories/Arith/Between.v | 4 | ||||
-rw-r--r-- | theories/Compat/Coq87.v | 3 | ||||
-rw-r--r-- | theories/FSets/FSetCompat.v | 44 | ||||
-rw-r--r-- | theories/Init/Tactics.v | 7 | ||||
-rw-r--r-- | theories/Logic/FunctionalExtensionality.v | 3 | ||||
-rw-r--r-- | theories/Program/Combinators.v | 12 | ||||
-rw-r--r-- | theories/Sets/Powerset_facts.v | 91 |
7 files changed, 131 insertions, 33 deletions
diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v index 9b4071085..ead08b3eb 100644 --- a/theories/Arith/Between.v +++ b/theories/Arith/Between.v @@ -16,6 +16,8 @@ Implicit Types k l p q r : nat. Section Between. Variables P Q : nat -> Prop. + (** The [between] type expresses the concept + [forall i: nat, k <= i < l -> P i.]. *) Inductive between k : nat -> Prop := | bet_emp : between k k | bet_S : forall l, between k l -> P l -> between k (S l). @@ -47,6 +49,8 @@ Section Between. induction 1; auto with arith. Qed. + (** The [exists_between] type expresses the concept + [exists i: nat, k <= i < l /\ Q i]. *) Inductive exists_between k : nat -> Prop := | exists_S : forall l, exists_between k l -> exists_between k (S l) | exists_le : forall l, k <= l -> Q l -> exists_between k (S l). diff --git a/theories/Compat/Coq87.v b/theories/Compat/Coq87.v index ef1737bf8..aeef9595d 100644 --- a/theories/Compat/Coq87.v +++ b/theories/Compat/Coq87.v @@ -15,3 +15,6 @@ and breaks at least fiat-crypto. *) Declare ML Module "omega_plugin". Unset Omega UseLocalDefs. + + +Set Typeclasses Axioms Are Instances. diff --git a/theories/FSets/FSetCompat.v b/theories/FSets/FSetCompat.v index b1769da3d..31bc1cc31 100644 --- a/theories/FSets/FSetCompat.v +++ b/theories/FSets/FSetCompat.v @@ -165,13 +165,13 @@ End Backport_WSets. (** * From new Sets to new ones *) Module Backport_Sets - (E:OrderedType.OrderedType) - (M:MSetInterface.Sets with Definition E.t := E.t - with Definition E.eq := E.eq - with Definition E.lt := E.lt) - <: FSetInterface.S with Module E:=E. + (O:OrderedType.OrderedType) + (M:MSetInterface.Sets with Definition E.t := O.t + with Definition E.eq := O.eq + with Definition E.lt := O.lt) + <: FSetInterface.S with Module E:=O. - Include Backport_WSets E M. + Include Backport_WSets O M. Implicit Type s : t. Implicit Type x y : elt. @@ -182,21 +182,21 @@ Module Backport_Sets Definition min_elt_1 : forall s x, min_elt s = Some x -> In x s := M.min_elt_spec1. Definition min_elt_2 : forall s x y, - min_elt s = Some x -> In y s -> ~ E.lt y x + min_elt s = Some x -> In y s -> ~ O.lt y x := M.min_elt_spec2. Definition min_elt_3 : forall s, min_elt s = None -> Empty s := M.min_elt_spec3. Definition max_elt_1 : forall s x, max_elt s = Some x -> In x s := M.max_elt_spec1. Definition max_elt_2 : forall s x y, - max_elt s = Some x -> In y s -> ~ E.lt x y + max_elt s = Some x -> In y s -> ~ O.lt x y := M.max_elt_spec2. Definition max_elt_3 : forall s, max_elt s = None -> Empty s := M.max_elt_spec3. - Definition elements_3 : forall s, sort E.lt (elements s) + Definition elements_3 : forall s, sort O.lt (elements s) := M.elements_spec2. Definition choose_3 : forall s s' x y, - choose s = Some x -> choose s' = Some y -> Equal s s' -> E.eq x y + choose s = Some x -> choose s' = Some y -> Equal s s' -> O.eq x y := M.choose_spec3. Definition lt_trans : forall s s' s'', lt s s' -> lt s' s'' -> lt s s'' := @StrictOrder_Transitive _ _ M.lt_strorder. @@ -211,7 +211,7 @@ Module Backport_Sets [ apply EQ | apply LT | apply GT ]; auto. Defined. - Module E := E. + Module E := O. End Backport_Sets. @@ -342,13 +342,13 @@ End Update_WSets. (** * From old Sets to new ones. *) Module Update_Sets - (E:Orders.OrderedType) - (M:FSetInterface.S with Definition E.t := E.t - with Definition E.eq := E.eq - with Definition E.lt := E.lt) - <: MSetInterface.Sets with Module E:=E. + (O:Orders.OrderedType) + (M:FSetInterface.S with Definition E.t := O.t + with Definition E.eq := O.eq + with Definition E.lt := O.lt) + <: MSetInterface.Sets with Module E:=O. - Include Update_WSets E M. + Include Update_WSets O M. Implicit Type s : t. Implicit Type x y : elt. @@ -359,21 +359,21 @@ Module Update_Sets Definition min_elt_spec1 : forall s x, min_elt s = Some x -> In x s := M.min_elt_1. Definition min_elt_spec2 : forall s x y, - min_elt s = Some x -> In y s -> ~ E.lt y x + min_elt s = Some x -> In y s -> ~ O.lt y x := M.min_elt_2. Definition min_elt_spec3 : forall s, min_elt s = None -> Empty s := M.min_elt_3. Definition max_elt_spec1 : forall s x, max_elt s = Some x -> In x s := M.max_elt_1. Definition max_elt_spec2 : forall s x y, - max_elt s = Some x -> In y s -> ~ E.lt x y + max_elt s = Some x -> In y s -> ~ O.lt x y := M.max_elt_2. Definition max_elt_spec3 : forall s, max_elt s = None -> Empty s := M.max_elt_3. - Definition elements_spec2 : forall s, sort E.lt (elements s) + Definition elements_spec2 : forall s, sort O.lt (elements s) := M.elements_3. Definition choose_spec3 : forall s s' x y, - choose s = Some x -> choose s' = Some y -> Equal s s' -> E.eq x y + choose s = Some x -> choose s' = Some y -> Equal s s' -> O.eq x y := M.choose_3. Instance lt_strorder : StrictOrder lt. @@ -407,6 +407,6 @@ Module Update_Sets Lemma compare_spec : forall s s', CompSpec eq lt s s' (compare s s'). Proof. intros; unfold compare; destruct M.compare; auto. Qed. - Module E := E. + Module E := O. End Update_Sets. diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 5d0e7602a..47a971ef0 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -306,3 +306,10 @@ Ltac inversion_sigma_step := => induction_sigma_in_using H @eq_sigT2_rect end. Ltac inversion_sigma := repeat inversion_sigma_step. + +(** A version of [time] that works for constrs *) +Ltac time_constr tac := + let eval_early := match goal with _ => restart_timer end in + let ret := tac () in + let eval_early := match goal with _ => finish_timing ( "Tactic evaluation" ) end in + ret. diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v index ac95ddd0c..82b04d132 100644 --- a/theories/Logic/FunctionalExtensionality.v +++ b/theories/Logic/FunctionalExtensionality.v @@ -221,13 +221,12 @@ Tactic Notation "extensionality" "in" hyp(H) := (* If we [subst H], things break if we already have another equation of the form [_ = H] *) destruct Heq; rename H_out into H. -(** Eta expansion follows from extensionality. *) +(** Eta expansion is built into Coq. *) Lemma eta_expansion_dep {A} {B : A -> Type} (f : forall x : A, B x) : f = fun x => f x. Proof. intros. - extensionality x. reflexivity. Qed. diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v index 90db10ef1..237d878bf 100644 --- a/theories/Program/Combinators.v +++ b/theories/Program/Combinators.v @@ -22,15 +22,13 @@ Open Scope program_scope. Lemma compose_id_left : forall A B (f : A -> B), id ∘ f = f. Proof. intros. - unfold id, compose. - symmetry. apply eta_expansion. + reflexivity. Qed. Lemma compose_id_right : forall A B (f : A -> B), f ∘ id = f. Proof. intros. - unfold id, compose. - symmetry ; apply eta_expansion. + reflexivity. Qed. Lemma compose_assoc : forall A B C D (f : A -> B) (g : B -> C) (h : C -> D), @@ -47,9 +45,7 @@ Hint Rewrite <- @compose_assoc : core. Lemma flip_flip : forall A B C, @flip A B C ∘ flip = id. Proof. - unfold flip, compose. intros. - extensionality x ; extensionality y ; extensionality z. reflexivity. Qed. @@ -57,9 +53,7 @@ Qed. Lemma prod_uncurry_curry : forall A B C, @prod_uncurry A B C ∘ prod_curry = id. Proof. - simpl ; intros. - unfold prod_uncurry, prod_curry, compose. - extensionality x ; extensionality y ; extensionality z. + intros. reflexivity. Qed. diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v index 2dd559a95..209c22f71 100644 --- a/theories/Sets/Powerset_facts.v +++ b/theories/Sets/Powerset_facts.v @@ -40,6 +40,11 @@ Section Sets_as_an_algebra. auto 6 with sets. Qed. + Theorem Empty_set_zero_right : forall X:Ensemble U, Union U X (Empty_set U) = X. + Proof. + auto 6 with sets. + Qed. + Theorem Empty_set_zero' : forall x:U, Add U (Empty_set U) x = Singleton U x. Proof. unfold Add at 1; auto using Empty_set_zero with sets. @@ -131,6 +136,17 @@ Section Sets_as_an_algebra. elim H'; intros x0 H'0; elim H'0; auto with sets. Qed. + Lemma Distributivity_l + : forall (A B C : Ensemble U), + Intersection U (Union U A B) C = + Union U (Intersection U A C) (Intersection U B C). + Proof. + intros A B C. + rewrite Intersection_commutative. + rewrite Distributivity. + f_equal; apply Intersection_commutative. + Qed. + Theorem Distributivity' : forall A B C:Ensemble U, Union U A (Intersection U B C) = @@ -251,6 +267,81 @@ Section Sets_as_an_algebra. intros; apply Definition_of_covers; auto with sets. Qed. + Lemma Disjoint_Intersection: + forall A s1 s2, Disjoint A s1 s2 -> Intersection A s1 s2 = Empty_set A. + Proof. + intros. apply Extensionality_Ensembles. split. + * destruct H. + intros x H1. unfold In in *. exfalso. intuition. apply (H _ H1). + * intuition. + Qed. + + Lemma Intersection_Empty_set_l: + forall A s, Intersection A (Empty_set A) s = Empty_set A. + Proof. + intros. auto with sets. + Qed. + + Lemma Intersection_Empty_set_r: + forall A s, Intersection A s (Empty_set A) = Empty_set A. + Proof. + intros. auto with sets. + Qed. + + Lemma Seminus_Empty_set_l: + forall A s, Setminus A (Empty_set A) s = Empty_set A. + Proof. + intros. apply Extensionality_Ensembles. split. + * intros x H1. destruct H1. unfold In in *. assumption. + * intuition. + Qed. + + Lemma Seminus_Empty_set_r: + forall A s, Setminus A s (Empty_set A) = s. + Proof. + intros. apply Extensionality_Ensembles. split. + * intros x H1. destruct H1. unfold In in *. assumption. + * intuition. + Qed. + + Lemma Setminus_Union_l: + forall A s1 s2 s3, + Setminus A (Union A s1 s2) s3 = Union A (Setminus A s1 s3) (Setminus A s2 s3). + Proof. + intros. apply Extensionality_Ensembles. split. + * intros x H. inversion H. inversion H0; intuition. + * intros x H. constructor; inversion H; inversion H0; intuition. + Qed. + + Lemma Setminus_Union_r: + forall A s1 s2 s3, + Setminus A s1 (Union A s2 s3) = Setminus A (Setminus A s1 s2) s3. + Proof. + intros. apply Extensionality_Ensembles. split. + * intros x H. inversion H. constructor. intuition. contradict H1. intuition. + * intros x H. inversion H. inversion H0. constructor; intuition. inversion H4; intuition. + Qed. + + Lemma Setminus_Disjoint_noop: + forall A s1 s2, + Intersection A s1 s2 = Empty_set A -> Setminus A s1 s2 = s1. + Proof. + intros. apply Extensionality_Ensembles. split. + * intros x H1. inversion_clear H1. intuition. + * intros x H1. constructor; intuition. contradict H. + apply Inhabited_not_empty. + exists x. intuition. + Qed. + + Lemma Setminus_Included_empty: + forall A s1 s2, + Included A s1 s2 -> Setminus A s1 s2 = Empty_set A. + Proof. + intros. apply Extensionality_Ensembles. split. + * intros x H1. inversion_clear H1. contradiction H2. intuition. + * intuition. + Qed. + End Sets_as_an_algebra. Hint Resolve Empty_set_zero Empty_set_zero' Union_associative Union_add |