diff options
| -rw-r--r-- | theories/MSets/MSetAVL.v | 4 | ||||
| -rw-r--r-- | theories/MSets/MSetEqProperties.v | 16 | ||||
| -rw-r--r-- | theories/MSets/MSetFacts.v | 21 | ||||
| -rw-r--r-- | theories/MSets/MSetInterface.v | 8 | ||||
| -rw-r--r-- | theories/MSets/MSetList.v | 5 | ||||
| -rw-r--r-- | theories/MSets/MSetProperties.v | 30 | ||||
| -rw-r--r-- | theories/MSets/MSetWeakList.v | 5 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivTrunc.v | 1 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZDiv.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZDomain.v | 18 | ||||
| -rw-r--r-- | theories/Structures/DecidableType2.v | 3 | ||||
| -rw-r--r-- | theories/Structures/DecidableType2Facts.v | 10 | ||||
| -rw-r--r-- | theories/Structures/GenericMinMax.v | 28 | ||||
| -rw-r--r-- | theories/Structures/OrderedType2Alt.v | 6 | ||||
| -rw-r--r-- | theories/Structures/OrderedType2Ex.v | 8 | ||||
| -rw-r--r-- | theories/Structures/OrderedType2Facts.v | 15 | ||||
| -rw-r--r-- | theories/Structures/OrderedType2Lists.v | 6 |
17 files changed, 102 insertions, 88 deletions
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index 56186e623c..c08f46294c 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -581,6 +581,10 @@ Hint Unfold lt_tree gt_tree. Hint Resolve @ok. Hint Constructors Ok. +(* TODO: modify proofs in order to avoid these hints *) +Hint Resolve MX.eq_refl MX.eq_trans. +Hint Immediate MX.eq_sym. + Tactic Notation "factornode" ident(l) ident(x) ident(r) ident(h) "as" ident(s) := set (s:=Node l x r h) in *; clearbody s; clear l x r h. diff --git a/theories/MSets/MSetEqProperties.v b/theories/MSets/MSetEqProperties.v index 49f436a011..fe6c3c79c2 100644 --- a/theories/MSets/MSetEqProperties.v +++ b/theories/MSets/MSetEqProperties.v @@ -89,7 +89,7 @@ Qed. Lemma add_mem_1: mem x (add x s)=true. Proof. -auto with set. +auto with set relations. Qed. Lemma add_mem_2: ~E.eq x y -> mem y (add x s)=mem y s. @@ -99,7 +99,7 @@ Qed. Lemma remove_mem_1: mem x (remove x s)=false. Proof. -rewrite <- not_mem_iff; auto with set. +rewrite <- not_mem_iff; auto with set relations. Qed. Lemma remove_mem_2: ~E.eq x y -> mem y (remove x s)=mem y s. @@ -275,7 +275,7 @@ Qed. Lemma singleton_mem_1: mem x (singleton x)=true. Proof. -auto with set. +auto with set relations. Qed. Lemma singleton_mem_2: ~E.eq x y -> mem y (singleton x)=false. @@ -653,7 +653,7 @@ Lemma filter_add_1 : forall s x, f x = true -> Proof. red; intros; set_iff; do 2 (rewrite filter_iff; auto); set_iff. intuition. -rewrite <- H; apply Comp; auto. +rewrite <- H; apply Comp; auto with relations. Qed. Lemma filter_add_2 : forall s x, f x = false -> @@ -672,7 +672,7 @@ unfold Add, MP.Add; intros. repeat rewrite filter_iff; auto. rewrite H0; clear H0. intuition. -setoid_replace y with x; auto. +setoid_replace y with x; auto with relations. Qed. Lemma add_filter_2 : forall s s' x, @@ -908,9 +908,9 @@ elim (equal_2 H x); auto with set; intros. apply fold_equal with (eqA:=eqA); auto with set. transitivity (f x (fold f s0 i)). apply fold_add with (eqA:=eqA); auto with set. -transitivity (g x (fold f s0 i)); auto with set. -transitivity (g x (fold g s0 i)); auto with set. -apply gc; auto with set. +transitivity (g x (fold f s0 i)); auto with set relations. +transitivity (g x (fold g s0 i)); auto with set relations. +apply gc; auto with set relations. symmetry; apply fold_add with (eqA:=eqA); auto. do 2 rewrite fold_empty; reflexivity. Qed. diff --git a/theories/MSets/MSetFacts.v b/theories/MSets/MSetFacts.v index bd99198f4b..84f6a17055 100644 --- a/theories/MSets/MSetFacts.v +++ b/theories/MSets/MSetFacts.v @@ -59,23 +59,23 @@ Lemma is_empty_2 : is_empty s = true -> Empty s. Proof. intros; apply -> is_empty_spec; auto. Qed. Lemma add_1 : E.eq x y -> In y (add x s). -Proof. intros; apply <- add_spec; auto. Qed. +Proof. intros; apply <- add_spec. auto with relations. Qed. Lemma add_2 : In y s -> In y (add x s). Proof. intros; apply <- add_spec; auto. Qed. Lemma add_3 : ~ E.eq x y -> In y (add x s) -> In y s. -Proof. rewrite add_spec. intros H [H'|H']; auto. elim H; auto. Qed. +Proof. rewrite add_spec. intros H [H'|H']; auto. elim H; auto with relations. Qed. Lemma remove_1 : E.eq x y -> ~ In y (remove x s). Proof. intros; rewrite remove_spec; intuition. Qed. Lemma remove_2 : ~ E.eq x y -> In y s -> In y (remove x s). -Proof. intros; apply <- remove_spec; auto. Qed. +Proof. intros; apply <- remove_spec; auto with relations. Qed. Lemma remove_3 : In y (remove x s) -> In y s. Proof. rewrite remove_spec; intuition. Qed. Lemma singleton_1 : In y (singleton x) -> E.eq x y. -Proof. rewrite singleton_spec; auto. Qed. +Proof. rewrite singleton_spec; auto with relations. Qed. Lemma singleton_2 : E.eq x y -> In y (singleton x). -Proof. rewrite singleton_spec; auto. Qed. +Proof. rewrite singleton_spec; auto with relations. Qed. Lemma union_1 : In x (union s s') -> In x s \/ In x s'. Proof. rewrite union_spec; auto. Qed. @@ -190,7 +190,7 @@ Lemma add_iff : In y (add x s) <-> E.eq x y \/ In y s. Proof. rewrite add_spec; intuition. Qed. Lemma add_neq_iff : ~ E.eq x y -> (In y (add x s) <-> In y s). -Proof. rewrite add_spec; intuition. elim H; auto. Qed. +Proof. rewrite add_spec; intuition. elim H; auto with relations. Qed. Lemma remove_iff : In y (remove x s) <-> In y s /\ ~E.eq x y. Proof. rewrite remove_spec; intuition. Qed. @@ -340,7 +340,7 @@ rewrite H0; intros. destruct H1 as (_,H1). apply H1; auto. rewrite H2. -rewrite InA_alt; eauto. +rewrite InA_alt. exists x0; split; auto with relations. Qed. Lemma exists_b : Proper (E.eq==>Logic.eq) f -> @@ -354,7 +354,7 @@ rewrite <- H1; intros. destruct H0 as (H0,_). destruct H0 as (a,(Ha1,Ha2)); auto. exists a; split; auto. -rewrite H2; rewrite InA_alt; eauto. +rewrite H2; rewrite InA_alt; exists a; auto with relations. symmetry. rewrite H0. destruct H1 as (_,H1). @@ -393,13 +393,12 @@ Instance mem_m : Proper (E.eq==>Equal==>Logic.eq) mem. Proof. intros x x' Hx s s' Hs. generalize (mem_iff s x). rewrite Hs, Hx at 1; rewrite mem_iff. -destruct (mem x s); destruct (mem x' s'); intuition. +destruct (mem x s), (mem x' s'); intuition. Qed. Instance singleton_m : Proper (E.eq==>Equal) singleton. Proof. -intros x y H a. -rewrite !singleton_iff; split; intros; etransitivity; eauto. +intros x y H a. rewrite !singleton_iff, H; intuition. Qed. Instance add_m : Proper (E.eq==>Equal==>Equal) add. diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v index fbaa01c908..b21c00fe2b 100644 --- a/theories/MSets/MSetInterface.v +++ b/theories/MSets/MSetInterface.v @@ -830,7 +830,7 @@ Module MakeSetOrdering (O:OrderedType)(Import M:IN O). rewrite (Ad y) in IN; destruct IN as [EQ|IN]. order. specialize (Ab y IN). order. left; split. - rewrite (Ad x); auto. + rewrite (Ad x). now left. intros y Hy. elim (Em y Hy). Qed. @@ -844,9 +844,9 @@ Module MakeSetOrdering (O:OrderedType)(Import M:IN O). split; intros [U|U]; try order. specialize (Ab1 y U). order. specialize (Ab2 y U). order. - rewrite (Ad1 x1); auto. + rewrite (Ad1 x1); auto with *. exists x2; repeat split; auto. - rewrite (Ad2 x2); auto. + rewrite (Ad2 x2); now left. intros y. rewrite (Ad2 y). intros [U|U]. order. specialize (Ab2 y U). order. Qed. @@ -947,7 +947,7 @@ Module MakeListOrdering (O:OrderedType). Lemma cons_CompSpec : forall c x1 x2 l1 l2, O.eq x1 x2 -> CompSpec eq lt l1 l2 c -> CompSpec eq lt (x1::l1) (x2::l2) c. Proof. - destruct c; simpl; inversion_clear 2; auto. + destruct c; simpl; inversion_clear 2; auto with relations. Qed. Hint Resolve cons_CompSpec. diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v index c5e300cdd4..4292eb9386 100644 --- a/theories/MSets/MSetList.v +++ b/theories/MSets/MSetList.v @@ -218,6 +218,11 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Notation Inf := (lelistA X.lt). Notation In := (InA X.eq). + (* TODO: modify proofs in order to avoid these hints *) + Hint Resolve (@Equivalence_Reflexive _ _ X.eq_equiv). + Hint Immediate (@Equivalence_Symmetric _ _ X.eq_equiv). + Hint Resolve (@Equivalence_Transitive _ _ X.eq_equiv). + Definition IsOk := Sort. Class Ok (s:t) : Prop := { ok : Sort s }. diff --git a/theories/MSets/MSetProperties.v b/theories/MSets/MSetProperties.v index 59fbcf49d8..dc82a14502 100644 --- a/theories/MSets/MSetProperties.v +++ b/theories/MSets/MSetProperties.v @@ -293,7 +293,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E). red; intros. apply (H a). rewrite elements_iff. - rewrite InA_alt; exists a; auto. + rewrite InA_alt; exists a; auto with relations. destruct (elements s); auto. elim (H0 e); simpl; auto. red; intros. @@ -368,7 +368,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E). apply Pempty. intro x. rewrite Hsame, InA_nil; intuition. (* step *) intros s Hsame; simpl. - apply Pstep' with (of_list l); auto. + apply Pstep' with (of_list l); auto with relations. inversion_clear Hdup; rewrite of_list_1; auto. red. intros. rewrite Hsame, of_list_1, InA_cons; intuition. apply IHl. @@ -430,7 +430,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E). assert (Rstep' : forall x a b, InA x l -> R a b -> R (f x a) (g x b)) by (intros; apply Rstep; auto; rewrite elements_iff, <- InA_rev; auto with *). clearbody l; clear Rstep s. - induction l; simpl; auto. + induction l; simpl; auto with relations. Qed. (** From the induction principle on [fold], we can deduce some general @@ -546,7 +546,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E). apply fold_rel with (R:=fun u v => eqA u (f x v)); intros. reflexivity. transitivity (f x0 (f x b)); auto. - apply Comp; auto. + apply Comp; auto with relations. Qed. (** ** Fold is a morphism *) @@ -555,7 +555,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E). eqA (fold f s i) (fold f s i'). Proof. intros. apply fold_rel with (R:=eqA); auto. - intros; apply Comp; auto. + intros; apply Comp; auto with relations. Qed. Lemma fold_equal : @@ -597,7 +597,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E). Proof. intros. symmetry. - apply fold_2 with (eqA:=eqA); auto with set. + apply fold_2 with (eqA:=eqA); auto with set relations. Qed. Lemma remove_fold_2: forall i s x, ~In x s -> @@ -631,18 +631,18 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E). apply equal_sym; apply union_Equal with x; auto with set. transitivity (f x (fold f (union s s') (fold f (inter s s') i))). apply fold_commutes; auto. - apply Comp; auto. + apply Comp; auto with relations. symmetry; apply fold_2 with (eqA:=eqA); auto. (* ~(In x s') *) transitivity (f x (fold f (union s s') (fold f (inter s'' s') i))). apply fold_2 with (eqA:=eqA); auto with set. transitivity (f x (fold f (union s s') (fold f (inter s s') i))). - apply Comp;auto. + apply Comp;auto with relations. apply fold_init;auto. apply fold_equal;auto. apply equal_sym; apply inter_Add_2 with x; auto with set. transitivity (f x (fold f s (fold f s' i))). - apply Comp; auto. + apply Comp; auto with relations. symmetry; apply fold_2 with (eqA:=eqA); auto. Qed. @@ -738,7 +738,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E). intros; rewrite FM.cardinal_1 in H. generalize (elements_2 (s:=s)). destruct (elements s); try discriminate. - exists e; auto. + exists e; auto with relations. Qed. Lemma cardinal_inv_2b : @@ -758,8 +758,10 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E). apply cardinal_1; rewrite <- H; auto. destruct (cardinal_inv_2 Heqn) as (x,H2). revert Heqn. - rewrite (cardinal_2 (s:=remove x s) (s':=s) (x:=x)); auto with set. - rewrite (cardinal_2 (s:=remove x s') (s':=s') (x:=x)); eauto with set. + rewrite (cardinal_2 (s:=remove x s) (s':=s) (x:=x)); + auto with set relations. + rewrite (cardinal_2 (s:=remove x s') (s':=s') (x:=x)); + eauto with set relations. Qed. Instance cardinal_m : Proper (Equal==>Logic.eq) cardinal. @@ -1053,7 +1055,7 @@ Module OrdProperties (M:Sets). apply X0 with (remove e s) e; auto with set. apply IHn. assert (S n = S (cardinal (remove e s))). - rewrite Heqn; apply cardinal_2 with e; auto with set. + rewrite Heqn; apply cardinal_2 with e; auto with set relations. inversion H0; auto. red; intros. rewrite remove_iff in H0; destruct H0. @@ -1074,7 +1076,7 @@ Module OrdProperties (M:Sets). apply X0 with (remove e s) e; auto with set. apply IHn. assert (S n = S (cardinal (remove e s))). - rewrite Heqn; apply cardinal_2 with e; auto with set. + rewrite Heqn; apply cardinal_2 with e; auto with set relations. inversion H0; auto. red; intros. rewrite remove_iff in H0; destruct H0. diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v index c49ab9d95b..feab44f58b 100644 --- a/theories/MSets/MSetWeakList.v +++ b/theories/MSets/MSetWeakList.v @@ -119,6 +119,11 @@ Module MakeRaw (X:DecidableType) <: WRawSets X. Notation NoDup := (NoDupA X.eq). Notation In := (InA X.eq). + (* TODO: modify proofs in order to avoid these hints *) + Hint Resolve (@Equivalence_Reflexive _ _ X.eq_equiv). + Hint Immediate (@Equivalence_Symmetric _ _ X.eq_equiv). + Hint Resolve (@Equivalence_Transitive _ _ X.eq_equiv). + Definition IsOk := NoDup. Class Ok (s:t) : Prop := { ok : NoDup s }. diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v index 15b8a9cd02..b57f8e27fb 100644 --- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v +++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v @@ -498,6 +498,7 @@ Theorem add_mod: forall a b n, n~=0 -> 0 <= a*b -> (a+b) mod n == (a mod n + b mod n) mod n. Proof. intros a b n Hn Hab. rewrite add_mod_idemp_l, add_mod_idemp_r; trivial. +reflexivity. destruct (le_0_mul _ _ Hab) as [(Ha,Hb)|(Ha,Hb)]; destruct (le_0_mul _ _ (mod_sign b n Hn)) as [(Hb',Hm)|(Hb',Hm)]; auto using mul_nonneg_nonneg, mul_nonpos_nonpos. diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v index 12cf01cae8..5b81cadd2d 100644 --- a/theories/Numbers/NatInt/NZDiv.v +++ b/theories/Numbers/NatInt/NZDiv.v @@ -457,7 +457,7 @@ Qed. Theorem mul_mod: forall a b n, 0<=a -> 0<=b -> 0<n -> (a * b) mod n == ((a mod n) * (b mod n)) mod n. Proof. - intros. rewrite mul_mod_idemp_l, mul_mod_idemp_r; trivial. + intros. rewrite mul_mod_idemp_l, mul_mod_idemp_r; trivial. reflexivity. now destruct (mod_bound b n). Qed. @@ -468,7 +468,7 @@ Proof. generalize (add_nonneg_nonneg _ _ Ha Hb). rewrite (div_mod a n) at 1 2; [|order]. rewrite <- add_assoc, add_comm, mul_comm. - intros. rewrite mod_add; trivial. + intros. rewrite mod_add; trivial. reflexivity. apply add_nonneg_nonneg; auto. destruct (mod_bound a n); auto. Qed. @@ -481,7 +481,7 @@ Qed. Theorem add_mod: forall a b n, 0<=a -> 0<=b -> 0<n -> (a+b) mod n == (a mod n + b mod n) mod n. Proof. - intros. rewrite add_mod_idemp_l, add_mod_idemp_r; trivial. + intros. rewrite add_mod_idemp_l, add_mod_idemp_r; trivial. reflexivity. now destruct (mod_bound b n). Qed. diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v index 2d627dbc79..6dcc9e91fe 100644 --- a/theories/Numbers/NatInt/NZDomain.v +++ b/theories/Numbers/NatInt/NZDomain.v @@ -164,8 +164,8 @@ Hypothesis Initial : initial init. Lemma initial_unique : forall m, initial m -> m == init. Proof. intros m Im. destruct (itersucc_or_itersucc init m) as (p,[H|H]). -destruct p; simpl in *; auto. destruct (Initial _ H). -destruct p; simpl in *; auto with *. destruct (Im _ H). +destruct p. now simpl in *. destruct (Initial _ H). +destruct p. now simpl in *. destruct (Im _ H). Qed. (** ... then all other points are descendant of it. *) @@ -287,7 +287,7 @@ Qed. Lemma ofnat_succ : forall n, [Datatypes.S n] == succ [n]. Proof. - unfold ofnat. intros. simpl; auto. + now unfold ofnat. Qed. Lemma ofnat_pred : forall n, n<>O -> [Peano.pred n] == P [n]. @@ -336,7 +336,7 @@ Qed. Lemma ofnat_eq : forall n m, [n]==[m] <-> n = m. Proof. -split. apply ofnat_injective. intros; subst; auto. +split. apply ofnat_injective. intros; now subst. Qed. (* In addition, we can prove that [ofnat] preserves order. *) @@ -382,8 +382,8 @@ Qed. Lemma ofnat_add : forall n m, [n+m] == [n]+[m]. Proof. intros. rewrite ofnat_add_l. - induction n; simpl; auto. - rewrite ofnat_succ. apply succ_wd; auto. + induction n; simpl. reflexivity. + rewrite ofnat_succ. now apply succ_wd. Qed. Lemma ofnat_mul : forall n m, [n*m] == [n]*[m]. @@ -392,21 +392,21 @@ Proof. symmetry. apply mul_0_l. rewrite plus_comm. rewrite ofnat_succ, ofnat_add, mul_succ_l. - apply add_wd; auto. + now apply add_wd. Qed. Lemma ofnat_sub_r : forall n m, n-[m] == (P^m) n. Proof. induction m; simpl; intros. rewrite ofnat_zero. apply sub_0_r. - rewrite ofnat_succ, sub_succ_r. apply pred_wd; auto. + rewrite ofnat_succ, sub_succ_r. now apply pred_wd. Qed. Lemma ofnat_sub : forall n m, m<=n -> [n-m] == [n]-[m]. Proof. intros n m H. rewrite ofnat_sub_r. revert n H. induction m. intros. - rewrite <- minus_n_O. simpl; auto. + rewrite <- minus_n_O. now simpl. intros. destruct n. inversion H. diff --git a/theories/Structures/DecidableType2.v b/theories/Structures/DecidableType2.v index 0957ef2430..585b981366 100644 --- a/theories/Structures/DecidableType2.v +++ b/theories/Structures/DecidableType2.v @@ -24,9 +24,6 @@ End BareEquality. Module Type IsEq (Import E:BareEquality). Declare Instance eq_equiv : Equivalence eq. - Hint Resolve (@Equivalence_Reflexive _ _ eq_equiv). - Hint Resolve (@Equivalence_Transitive _ _ eq_equiv). - Hint Immediate (@Equivalence_Symmetric _ _ eq_equiv). End IsEq. (** * Earlier specification of equality by three separate lemmas. *) diff --git a/theories/Structures/DecidableType2Facts.v b/theories/Structures/DecidableType2Facts.v index 988122b0b5..154a40d872 100644 --- a/theories/Structures/DecidableType2Facts.v +++ b/theories/Structures/DecidableType2Facts.v @@ -49,22 +49,24 @@ Module KeyDecidableType(D:DecidableType). Instance eqk_equiv : Equivalence eqk. Proof. - constructor; eauto. + constructor; unfold eqk; repeat red; intros; + [ reflexivity | symmetry; auto | etransitivity; eauto ]. Qed. Instance eqke_equiv : Equivalence eqke. Proof. - constructor. auto. - red; unfold eqke; intuition. - red; unfold eqke; intuition; [ eauto | congruence ]. + constructor; unfold eqke; repeat red; intuition; simpl; + etransitivity; eauto. Qed. +(* Hint Resolve (@Equivalence_Reflexive _ _ eqk_equiv). Hint Resolve (@Equivalence_Transitive _ _ eqk_equiv). Hint Immediate (@Equivalence_Symmetric _ _ eqk_equiv). Hint Resolve (@Equivalence_Reflexive _ _ eqke_equiv). Hint Resolve (@Equivalence_Transitive _ _ eqke_equiv). Hint Immediate (@Equivalence_Symmetric _ _ eqke_equiv). +*) Lemma InA_eqke_eqk : forall x m, InA eqke x m -> InA eqk x m. diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v index 49daacabda..0650546a5e 100644 --- a/theories/Structures/GenericMinMax.v +++ b/theories/Structures/GenericMinMax.v @@ -47,14 +47,14 @@ Module GenericMinMax (Import O:OrderedTypeFull) <: HasMinMax O. (lt x y /\ eq (max x y) y) \/ (le y x /\ eq (max x y) x). Proof. intros. rewrite le_lteq. unfold max, gmax. - destruct (compare_spec x y); auto. + destruct (compare_spec x y); auto with relations. Qed. Lemma min_spec : forall x y, (lt x y /\ eq (min x y) x) \/ (le y x /\ eq (min x y) y). Proof. intros. rewrite le_lteq. unfold min, gmin. - destruct (compare_spec x y); auto. + destruct (compare_spec x y); auto with relations. Qed. End GenericMinMax. @@ -133,7 +133,7 @@ Defined. Lemma max_dec : forall n m, {max n m == n} + {max n m == m}. Proof. - intros n m. apply max_case; auto. + intros n m. apply max_case; auto with relations. intros x y H [E|E]; [left|right]; order. Defined. @@ -161,21 +161,19 @@ Qed. Lemma max_assoc : forall m n p, max m (max n p) == max (max m n) p. Proof. intros. - destruct (M.max_spec n p) as [(H,Eq)|(H,Eq)]; rewrite Eq; auto. - destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; auto. - destruct (max_spec m p); intuition; order. - destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; auto. + destruct (M.max_spec n p) as [(H,Eq)|(H,Eq)]; rewrite Eq. + destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'. + destruct (max_spec m p); intuition; order. order. + destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'. order. destruct (max_spec m p); intuition; order. Qed. Lemma max_comm : forall n m, max n m == max m n. Proof. intros. - destruct (M.max_spec n m) as [(H,Eq)|(H,Eq)]; rewrite Eq; auto. - destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; auto. - order. - destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; auto. - order. + destruct (M.max_spec n m) as [(H,Eq)|(H,Eq)]; rewrite Eq. + destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; order. + destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; order. Qed. (** *** Least-upper bound properties of [max] *) @@ -434,7 +432,7 @@ Lemma max_min_modular : forall n m p, max n (min m (max n p)) == min (max n m) (max n p). Proof. intros. rewrite <- max_min_distr. - destruct (max_spec n p) as [(C,E)|(C,E)]; rewrite E; auto. + destruct (max_spec n p) as [(C,E)|(C,E)]; rewrite E. reflexivity. destruct (min_spec m n) as [(C',E')|(C',E')]; rewrite E'. rewrite 2 max_l; try OF.order. rewrite min_le_iff; auto. rewrite 2 max_l; try OF.order. rewrite min_le_iff; auto. @@ -444,10 +442,10 @@ Lemma min_max_modular : forall n m p, min n (max m (min n p)) == max (min n m) (min n p). Proof. intros. rewrite <- min_max_distr. - destruct (min_spec n p) as [(C,E)|(C,E)]; rewrite E; auto. + destruct (min_spec n p) as [(C,E)|(C,E)]; rewrite E. destruct (max_spec m n) as [(C',E')|(C',E')]; rewrite E'. rewrite 2 min_l; try OF.order. rewrite max_le_iff; right; OF.order. - rewrite 2 min_l; try OF.order. rewrite max_le_iff; auto. + rewrite 2 min_l; try OF.order. rewrite max_le_iff; auto. reflexivity. Qed. (** Disassociativity *) diff --git a/theories/Structures/OrderedType2Alt.v b/theories/Structures/OrderedType2Alt.v index 43b27553fb..3371977334 100644 --- a/theories/Structures/OrderedType2Alt.v +++ b/theories/Structures/OrderedType2Alt.v @@ -231,10 +231,10 @@ Module OT_to_Alt (Import O:OrderedType) <: OrderedTypeAlt. Proof. intros c x y z. destruct c; unfold compare. - rewrite 3 compare_Eq; eauto. - rewrite 3 compare_Lt. apply StrictOrder_Transitive. + rewrite 3 compare_Eq. etransitivity; eauto. + rewrite 3 compare_Lt. etransitivity; eauto. do 3 (rewrite compare_sym, CompOpp_iff, compare_Lt). - intros; apply StrictOrder_Transitive with y; auto. + etransitivity; eauto. Qed. End OT_to_Alt. diff --git a/theories/Structures/OrderedType2Ex.v b/theories/Structures/OrderedType2Ex.v index c64fb7a97b..1e45a3fbfb 100644 --- a/theories/Structures/OrderedType2Ex.v +++ b/theories/Structures/OrderedType2Ex.v @@ -58,9 +58,9 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType. (* transitive *) intros (x1,x2) (y1,y2) (z1,z2). compute. intuition. left; etransitivity; eauto. - left; rewrite <- H0; auto. - left; rewrite H; auto. - right; split; eauto. etransitivity; eauto. + left. setoid_replace z1 with y1; auto with relations. + left; setoid_replace x1 with y1; auto with relations. + right; split; etransitivity; eauto. Qed. Instance lt_compat : Proper (eq==>eq==>iff) lt. @@ -81,7 +81,7 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType. Proof. intros (x1,x2) (y1,y2); unfold compare; simpl. destruct (O1.compare_spec x1 y1); try (constructor; compute; auto). - destruct (O2.compare_spec x2 y2); constructor; compute; auto. + destruct (O2.compare_spec x2 y2); constructor; compute; auto with relations. Qed. End PairOrderedType. diff --git a/theories/Structures/OrderedType2Facts.v b/theories/Structures/OrderedType2Facts.v index e35c7c651c..9d964d7129 100644 --- a/theories/Structures/OrderedType2Facts.v +++ b/theories/Structures/OrderedType2Facts.v @@ -50,33 +50,34 @@ Module OrderedTypeFullFacts (Import O:OrderedTypeFull). Module Order := OTF_to_OrderTac O. Ltac order := Order.order. + Ltac iorder := intuition order. Instance le_compat : Proper (eq==>eq==>iff) le. - Proof. repeat red; intuition; order. Qed. + Proof. repeat red; iorder. Qed. Instance le_preorder : PreOrder le. Proof. split; red; order. Qed. Instance le_order : PartialOrder eq le. - Proof. compute; intuition; order. Qed. + Proof. compute; iorder. Qed. Instance le_antisym : Antisymmetric _ eq le. Proof. apply partial_order_antisym; auto with *. Qed. Lemma le_not_gt_iff : forall x y, le x y <-> ~lt y x. - Proof. split; order. Qed. + Proof. iorder. Qed. Lemma lt_not_ge_iff : forall x y, lt x y <-> ~le y x. - Proof. split; order. Qed. + Proof. iorder. Qed. Lemma le_or_gt : forall x y, le x y \/ lt y x. Proof. intros. rewrite le_lteq; destruct (O.compare_spec x y); auto. Qed. Lemma lt_or_ge : forall x y, lt x y \/ le y x. - Proof. intros. rewrite le_lteq; destruct (O.compare_spec x y); auto. Qed. + Proof. intros. rewrite le_lteq; destruct (O.compare_spec x y); iorder. Qed. Lemma eq_is_le_ge : forall x y, eq x y <-> le x y /\ le y x. - Proof. intuition; order. Qed. + Proof. iorder. Qed. End OrderedTypeFullFacts. @@ -260,7 +261,7 @@ Definition compare := flip O.compare. Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). Proof. intros; unfold compare, eq, lt, flip. -destruct (O.compare_spec y x); auto. +destruct (O.compare_spec y x); auto with relations. Qed. End OrderedTypeRev. diff --git a/theories/Structures/OrderedType2Lists.v b/theories/Structures/OrderedType2Lists.v index 567cbd9f85..51e7512393 100644 --- a/theories/Structures/OrderedType2Lists.v +++ b/theories/Structures/OrderedType2Lists.v @@ -197,7 +197,7 @@ Module KeyOrderedType(Import O:OrderedType). destruct H1 as [e' H2]. elim (@ltk_not_eqk (k,e) (k,e')). eapply Sort_Inf_In; eauto. - red; simpl; auto. + repeat red; reflexivity. Qed. Lemma Sort_NoDupA: forall l, Sort l -> NoDupA eqk l. @@ -211,8 +211,8 @@ Module KeyOrderedType(Import O:OrderedType). Lemma Sort_In_cons_2 : forall l e e', Sort (e::l) -> InA eqk e' (e::l) -> ltk e e' \/ eqk e e'. Proof. - intros; invlist InA; auto. - left; apply Sort_In_cons_1 with l; auto. + intros; invlist InA; auto with relations. + left; apply Sort_In_cons_1 with l; auto with relations. Qed. Lemma Sort_In_cons_3 : |