diff options
| -rw-r--r-- | doc/changelog/10-standard-library/09772-ordered_type-hint-db.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 3 | ||||
| -rw-r--r-- | test-suite/bugs/opened/bug_1596.v | 7 | ||||
| -rw-r--r-- | theories/FSets/FMapAVL.v | 54 | ||||
| -rw-r--r-- | theories/FSets/FMapFacts.v | 24 | ||||
| -rw-r--r-- | theories/FSets/FMapFullAVL.v | 2 | ||||
| -rw-r--r-- | theories/FSets/FMapList.v | 53 | ||||
| -rw-r--r-- | theories/FSets/FSetBridge.v | 10 | ||||
| -rw-r--r-- | theories/FSets/FSetProperties.v | 8 | ||||
| -rw-r--r-- | theories/Structures/OrderedType.v | 135 | ||||
| -rw-r--r-- | theories/Structures/OrderedTypeEx.v | 10 |
11 files changed, 159 insertions, 151 deletions
diff --git a/doc/changelog/10-standard-library/09772-ordered_type-hint-db.rst b/doc/changelog/10-standard-library/09772-ordered_type-hint-db.rst new file mode 100644 index 0000000000..7babcdb6f1 --- /dev/null +++ b/doc/changelog/10-standard-library/09772-ordered_type-hint-db.rst @@ -0,0 +1,4 @@ +- Moved the `auto` hints of the `OrderedType` module into a new `ordered_type` + database + (`#9772 <https://github.com/coq/coq/pull/9772>`_, + by Vincent Laporte). diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index fa6d62ffa2..85dfe0e5d2 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3960,6 +3960,9 @@ At Coq startup, only the core database is nonempty and can be used. :fset: internal database for the implementation of the ``FSets`` library. +:ordered_type: lemmas about ordered types (as defined in the legacy ``OrderedType`` module), + mainly used in the ``FSets`` and ``FMaps`` libraries. + You are advised not to put your own hints in the core database, but use one or several databases specific to your development. diff --git a/test-suite/bugs/opened/bug_1596.v b/test-suite/bugs/opened/bug_1596.v index 820022d995..27cb731151 100644 --- a/test-suite/bugs/opened/bug_1596.v +++ b/test-suite/bugs/opened/bug_1596.v @@ -69,9 +69,8 @@ Definition t := (X.t * Y.t)%type. elim (X.lt_not_eq H2 H3). elim H0;clear H0;intros. right. - split. - eauto. - eauto. + split; + eauto with ordered_type. Qed. Lemma lt_not_eq : forall (x y:t),(lt x y)->~(eq x y). @@ -97,7 +96,7 @@ Definition t := (X.t * Y.t)%type. apply EQ. split;trivial. apply GT. - right;auto. + right;auto with ordered_type. apply GT. left;trivial. Defined. diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 8627ff7353..7c69350db4 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -593,14 +593,14 @@ Qed. Lemma MapsTo_1 : forall m x y e, X.eq x y -> MapsTo x e m -> MapsTo y e m. Proof. - induction m; simpl; intuition_in; eauto. + induction m; simpl; intuition_in; eauto with ordered_type. Qed. Hint Immediate MapsTo_1 : core. Lemma In_1 : forall m x y, X.eq x y -> In x m -> In y m. Proof. - intros m x y; induction m; simpl; intuition_in; eauto. + intros m x y; induction m; simpl; intuition_in; eauto with ordered_type. Qed. Lemma In_node_iff : @@ -671,7 +671,7 @@ Qed. Lemma lt_tree_trans : forall x y, X.lt x y -> forall m, lt_tree x m -> lt_tree y m. Proof. - eauto. + eauto with ordered_type. Qed. Lemma gt_tree_not_in : @@ -683,7 +683,7 @@ Qed. Lemma gt_tree_trans : forall x y, X.lt y x -> forall m, gt_tree x m -> gt_tree y m. Proof. - eauto. + eauto with ordered_type. Qed. Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans : core. @@ -707,7 +707,7 @@ Qed. Lemma is_empty_1 : forall m, Empty m -> is_empty m = true. Proof. destruct m as [|r x e l h]; simpl; auto. - intro H; elim (H x e); auto. + intro H; elim (H x e); auto with ordered_type. Qed. Lemma is_empty_2 : forall m, is_empty m = true -> Empty m. @@ -732,7 +732,7 @@ Lemma find_1 : forall m x e, bst m -> MapsTo x e m -> find x m = Some e. Proof. intros m x; functional induction (find x m); auto; intros; clearf; inv bst; intuition_in; simpl; auto; - try solve [order | absurd (X.lt x y); eauto | absurd (X.lt y x); eauto]. + try solve [order | absurd (X.lt x y); eauto with ordered_type | absurd (X.lt y x); eauto with ordered_type]. Qed. Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m. @@ -832,8 +832,8 @@ Lemma bal_bst : forall l x e r, bst l -> bst r -> Proof. intros l x e r; functional induction (bal l x e r); intros; clearf; inv bst; repeat apply create_bst; auto; unfold create; try constructor; - (apply lt_tree_node || apply gt_tree_node); auto; - (eapply lt_tree_trans || eapply gt_tree_trans); eauto. + (apply lt_tree_node || apply gt_tree_node); auto with ordered_type; + (eapply lt_tree_trans || eapply gt_tree_trans); eauto with ordered_type. Qed. Hint Resolve bal_bst : core. @@ -865,7 +865,7 @@ Lemma add_in : forall m x y e, Proof. intros m x y e; functional induction (add x e m); auto; intros; try (rewrite bal_in, IHt); intuition_in. - apply In_1 with x; auto. + apply In_1 with x; auto with ordered_type. Qed. Lemma add_bst : forall m x e, bst m -> bst (add x e m). @@ -874,14 +874,14 @@ Proof. inv bst; try apply bal_bst; auto; intro z; rewrite add_in; intuition. apply MX.eq_lt with x; auto. - apply MX.lt_eq with x; auto. + apply MX.lt_eq with x; auto with ordered_type. Qed. Hint Resolve add_bst : core. Lemma add_1 : forall m x y e, X.eq x y -> MapsTo y e (add x e m). Proof. intros m x y e; functional induction (add x e m); - intros; inv bst; try rewrite bal_mapsto; unfold create; eauto. + intros; inv bst; try rewrite bal_mapsto; unfold create; eauto with ordered_type. Qed. Lemma add_2 : forall m x y e e', ~X.eq x y -> @@ -912,7 +912,7 @@ Proof. intros; rewrite find_mapsto_equiv; auto. split; eauto using add_2, add_3. destruct X.compare; try (apply H0; order). - auto using find_1, add_1. + auto using find_1, add_1 with ordered_type. Qed. (** * Extraction of minimum binding *) @@ -971,7 +971,7 @@ Proof. generalize (remove_min_in ll lx ld lr _x m#1). rewrite e0; simpl; intros. rewrite (bal_in l' x d r y) in H. - assert (In m#1 (Node ll lx ld lr _x)) by (rewrite H4; auto); clear H4. + assert (In m#1 (Node ll lx ld lr _x)) by (rewrite H4; auto with ordered_type); clear H4. assert (X.lt m#1 x) by order. decompose [or] H; order. Qed. @@ -1050,7 +1050,7 @@ Proof. (* EQ *) inv bst; clear e0. rewrite merge_in; intuition; [ order | order | intuition_in ]. - elim H4; eauto. + elim H4; eauto with ordered_type. (* GT *) inv bst; clear e0. rewrite bal_in; auto. @@ -1069,7 +1069,7 @@ Proof. destruct H; eauto. (* EQ *) inv bst. - apply merge_bst; eauto. + apply merge_bst; eauto with ordered_type. (* GT *) inv bst. apply bal_bst; auto. @@ -1124,8 +1124,8 @@ Lemma join_bst : forall l x d r, bst l -> bst r -> Proof. join_tac; auto; try (simpl; auto; fail); inv bst; apply bal_bst; auto; clear Hrl Hlr; intro; intros; rewrite join_in in *. - intuition; [ apply MX.lt_eq with x | ]; eauto. - intuition; [ apply MX.eq_lt with x | ]; eauto. + intuition; [ apply MX.lt_eq with x | ]; eauto with ordered_type. + intuition; [ apply MX.eq_lt with x | ]; eauto with ordered_type. Qed. Hint Resolve join_bst : core. @@ -1135,8 +1135,8 @@ Lemma join_find : forall l x d r y, Proof. join_tac; auto; inv bst; simpl (join (Leaf elt)); - try (assert (X.lt lx x) by auto); - try (assert (X.lt x rx) by auto); + try (assert (X.lt lx x) by auto with ordered_type); + try (assert (X.lt x rx) by auto with ordered_type); rewrite ?add_find, ?bal_find; auto. simpl; destruct X.compare; auto. @@ -1260,7 +1260,7 @@ Proof. change (bst (m2',xd)#1). rewrite <-e1; eauto. intros y Hy. apply H1; auto. - rewrite remove_min_in, e1; simpl; auto. + rewrite remove_min_in, e1; simpl; auto with ordered_type. change (gt_tree (m2',xd)#2#1 (m2',xd)#1). rewrite <-e1; eauto. Qed. Hint Resolve concat_bst : core. @@ -1283,9 +1283,9 @@ Proof. simpl; destruct X.compare as [Hlt| |Hlt]; simpl; auto. destruct (find y m2'); auto. symmetry; rewrite not_find_iff; auto; intro. - apply (MX.lt_not_gt Hlt); apply H1; auto; rewrite H3; auto. + apply (MX.lt_not_gt Hlt); apply H1; auto; rewrite H3; auto with ordered_type. - intros z Hz; apply H1; auto; rewrite H3; auto. + intros z Hz; apply H1; auto; rewrite H3; auto with ordered_type. Qed. @@ -1338,12 +1338,12 @@ Proof. apply InA_InfA with (eqA:=eqke); auto with *. intros (y',e') H6. destruct (elements_aux_mapsto r acc y' e'); intuition. red; simpl; eauto. - red; simpl; eauto. - intros. + red; simpl; eauto with ordered_type. + intros x e0 y0 H H6. inversion_clear H. destruct H7; simpl in *. order. - destruct (elements_aux_mapsto r acc x e0); intuition eauto. + destruct (elements_aux_mapsto r acc x e0); intuition eauto with ordered_type. Qed. Lemma elements_sort : forall s : t elt, bst s -> sort ltk (elements s). @@ -1567,7 +1567,7 @@ Lemma mapi_1 : forall (m: tree elt)(x:key)(e:elt), MapsTo x e m -> exists y, X.eq y x /\ MapsTo x (f y e) (mapi f m). Proof. induction m; simpl; inversion_clear 1; auto. -exists k; auto. +exists k; auto with ordered_type. destruct (IHm1 _ _ H0). exists x0; intuition. destruct (IHm2 _ _ H0). @@ -2072,7 +2072,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: X.eq x1 x2 -> D.eq d1 d2 -> Cmp c l1 l2 -> Cmp c ((x1,d1)::l1) ((x2,d2)::l2). Proof. - destruct c; simpl; intros; P.MX.elim_comp; auto. + destruct c; simpl; intros; P.MX.elim_comp; auto with ordered_type. Qed. Hint Resolve cons_Cmp : core. diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 1a531542cc..758f9d41b0 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -1822,7 +1822,7 @@ Module OrdProperties (M:S). destruct (gtb (x,e) (a,e')); destruct (gtb (x,e) (b,e'')); auto. unfold O.ltk in *; simpl in *; intros. symmetry; rewrite H2. - apply ME.eq_lt with a; auto. + apply ME.eq_lt with a; auto with ordered_type. rewrite <- H1; auto. unfold O.ltk in *; simpl in *; intros. rewrite H1. @@ -1869,7 +1869,7 @@ Module OrdProperties (M:S). rewrite <- elements_mapsto_iff in H1. assert (~E.eq x t0). contradict H. - exists e0; apply MapsTo_1 with t0; auto. + exists e0; apply MapsTo_1 with t0; auto with ordered_type. ME.order. apply (@filter_sort _ eqke); auto with *; clean_eauto. intros. @@ -1888,9 +1888,9 @@ Module OrdProperties (M:S). find_mapsto_iff, (H0 t0), <- find_mapsto_iff, add_mapsto_iff by (auto with *). unfold O.eqke, O.ltk; simpl. - destruct (E.compare t0 x); intuition; try fold (~E.eq x t0); auto. + destruct (E.compare t0 x); intuition; try fold (~E.eq x t0); auto with ordered_type. - elim H; exists e0; apply MapsTo_1 with t0; auto. - - fold (~E.lt t0 x); auto. + - fold (~E.lt t0 x); auto with ordered_type. Qed. Lemma elements_Add_Above : forall m m' x e, @@ -1905,7 +1905,7 @@ Module OrdProperties (M:S). destruct x0; destruct y. rewrite <- elements_mapsto_iff in H1. unfold O.eqke, O.ltk in *; simpl in *; destruct H3. - apply ME.lt_eq with x; auto. + apply ME.lt_eq with x; auto with ordered_type. apply H; firstorder. inversion H3. red; intros a; destruct a. @@ -1991,7 +1991,7 @@ Module OrdProperties (M:S). injection H as [= -> ->]. inversion_clear H1. red in H; simpl in *; intuition. - elim H0; eauto. + elim H0; eauto with ordered_type. inversion H. change (max_elt_aux (p::l) = Some (x,e)) in H. generalize (IHl x e H); clear IHl; intros IHl. @@ -2007,9 +2007,9 @@ Module OrdProperties (M:S). inversion_clear H2. inversion_clear H5. red in H2; simpl in H2; ME.order. - eapply IHl; eauto. + eapply IHl; eauto with ordered_type. econstructor; eauto. - red; eauto. + red; eauto with ordered_type. inversion H2; auto. Qed. @@ -2022,7 +2022,7 @@ Module OrdProperties (M:S). induction (elements m). simpl; try discriminate. destruct a; destruct l; simpl in *. - injection H; intros; subst; constructor; red; auto. + injection H; intros; subst; constructor; red; auto with ordered_type. constructor 2; auto. Qed. @@ -2069,7 +2069,7 @@ Module OrdProperties (M:S). destruct (elements m). simpl; try discriminate. destruct p; simpl in *. - injection H; intros; subst; constructor; red; auto. + injection H; intros; subst; constructor; red; auto with ordered_type. Qed. Lemma min_elt_Empty : @@ -2106,7 +2106,7 @@ Module OrdProperties (M:S). apply IHn. assert (S n = S (cardinal (remove k m))). rewrite Heqn. - eapply cardinal_2; eauto with map. + eapply cardinal_2; eauto with map ordered_type. inversion H1; auto. eapply max_elt_Above; eauto. @@ -2133,7 +2133,7 @@ Module OrdProperties (M:S). apply IHn. assert (S n = S (cardinal (remove k m))). rewrite Heqn. - eapply cardinal_2; eauto with map. + eapply cardinal_2; eauto with map ordered_type. inversion H1; auto. eapply min_elt_Below; eauto. diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v index 8ca9401a06..0ef356b582 100644 --- a/theories/FSets/FMapFullAVL.v +++ b/theories/FSets/FMapFullAVL.v @@ -712,7 +712,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: X.eq x1 x2 -> D.eq d1 d2 -> Cmp c l1 l2 -> Cmp c ((x1,d1)::l1) ((x2,d2)::l2). Proof. - destruct c; simpl; intros; MX.elim_comp; auto. + destruct c; simpl; intros; MX.elim_comp; auto with ordered_type. Qed. Hint Resolve cons_Cmp : core. diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v index b21d809059..cad528644a 100644 --- a/theories/FSets/FMapList.v +++ b/theories/FSets/FMapList.v @@ -68,7 +68,7 @@ Proof. intros m. case m;auto. intros (k,e) l inlist. - absurd (InA eqke (k, e) ((k, e) :: l));auto. + absurd (InA eqke (k, e) ((k, e) :: l)); auto with ordered_type. Qed. Lemma is_empty_2 : forall m, is_empty m = true -> Empty m. @@ -106,14 +106,14 @@ Proof. elim (sort_inv sorted);auto. elim (In_inv belong1);auto. intro abs. - absurd (X.eq x k');auto. + absurd (X.eq x k'); auto with ordered_type. Qed. Lemma mem_2 : forall m (Hm:Sort m) x, mem x m = true -> In x m. Proof. intros m Hm x; generalize Hm; clear Hm; unfold PX.In,PX.MapsTo. functional induction (mem x m); intros sorted hyp;try ((inversion hyp);fail). - exists _x; auto. + exists _x; auto with ordered_type. induction IHb; auto. exists x0; auto. inversion_clear sorted; auto. @@ -135,7 +135,7 @@ Function find (k:key) (s: t elt) {struct s} : option elt := Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m. Proof. intros m x. unfold PX.MapsTo. - functional induction (find x m);simpl;intros e' eqfind; inversion eqfind; auto. + functional induction (find x m);simpl;intros e' eqfind; inversion eqfind; auto with ordered_type. Qed. Lemma find_1 : forall m (Hm:Sort m) x e, MapsTo x e m -> find x m = Some e. @@ -174,7 +174,7 @@ Lemma add_1 : forall m x y e, X.eq x y -> MapsTo y e (add x e m). Proof. intros m x y e; generalize y; clear y. unfold PX.MapsTo. - functional induction (add x e m);simpl;auto. + functional induction (add x e m);simpl;auto with ordered_type. Qed. Lemma add_2 : forall m x y e e', @@ -195,12 +195,12 @@ Qed. Lemma add_3 : forall m x y e e', ~ X.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m. -Proof. +Proof with auto with ordered_type. intros m x y e e'. generalize y e; clear y e; unfold PX.MapsTo. functional induction (add x e' m);simpl; intros. - apply (In_inv_3 H0); compute; auto. - apply (In_inv_3 H0); compute; auto. - constructor 2; apply (In_inv_3 H0); compute; auto. + apply (In_inv_3 H0)... + apply (In_inv_3 H0)... + constructor 2; apply (In_inv_3 H0)... inversion_clear H0; auto. Qed. @@ -254,7 +254,7 @@ Proof. clear e0;inversion_clear Hm. apply Sort_Inf_NotIn with x0; auto. - apply Inf_eq with (k',x0);auto; compute; apply X.eq_trans with x; auto. + apply Inf_eq with (k',x0);auto; compute; apply X.eq_trans with x; auto with ordered_type. clear e0;inversion_clear Hm. assert (notin:~ In y (remove x l)) by auto. @@ -374,13 +374,13 @@ Definition Equivb cmp m m' := Lemma equal_1 : forall m (Hm:Sort m) m' (Hm': Sort m') cmp, Equivb cmp m m' -> equal cmp m m' = true. -Proof. +Proof with auto with ordered_type. intros m Hm m' Hm' cmp; generalize Hm Hm'; clear Hm Hm'. functional induction (equal cmp m m'); simpl; subst;auto; unfold Equivb; intuition; subst. match goal with H: X.compare _ _ = _ |- _ => clear H end. assert (cmp_e_e':cmp e e' = true). - apply H1 with x; auto. + apply H1 with x... rewrite cmp_e_e'; simpl. apply IHb; auto. inversion_clear Hm; auto. @@ -388,7 +388,7 @@ Proof. unfold Equivb; intuition. destruct (H0 k). assert (In k ((x,e) ::l)). - destruct H as (e'', hyp); exists e''; auto. + destruct H as (e'', hyp); exists e''... destruct (In_inv (H2 H4)); auto. inversion_clear Hm. elim (Sort_Inf_NotIn H6 H7). @@ -396,20 +396,20 @@ Proof. apply MapsTo_eq with k; auto; order. destruct (H0 k). assert (In k ((x',e') ::l')). - destruct H as (e'', hyp); exists e''; auto. + destruct H as (e'', hyp); exists e''... destruct (In_inv (H3 H4)); auto. inversion_clear Hm'. elim (Sort_Inf_NotIn H6 H7). destruct H as (e'', hyp); exists e''; auto. apply MapsTo_eq with k; auto; order. - apply H1 with k; destruct (X.eq_dec x k); auto. + apply H1 with k; destruct (X.eq_dec x k)... destruct (X.compare x x') as [Hlt|Heq|Hlt]; try contradiction; clear y. destruct (H0 x). assert (In x ((x',e')::l')). apply H; auto. - exists e; auto. + exists e... destruct (In_inv H3). order. inversion_clear Hm'. @@ -420,7 +420,7 @@ Proof. destruct (H0 x'). assert (In x' ((x,e)::l)). apply H2; auto. - exists e'; auto. + exists e'... destruct (In_inv H3). order. inversion_clear Hm. @@ -434,13 +434,13 @@ Proof. clear H1;destruct p as (k,e). destruct (H0 k). destruct H1. - exists e; auto. + exists e... inversion H1. destruct p as (x,e). destruct (H0 x). destruct H. - exists e; auto. + exists e... inversion H. destruct p;destruct p0;contradiction. @@ -449,7 +449,7 @@ Qed. Lemma equal_2 : forall m (Hm:Sort m) m' (Hm:Sort m') cmp, equal cmp m m' = true -> Equivb cmp m m'. -Proof. +Proof with auto with ordered_type. intros m Hm m' Hm' cmp; generalize Hm Hm'; clear Hm Hm'. functional induction (equal cmp m m'); simpl; subst;auto; unfold Equivb; intuition; try discriminate; subst; @@ -464,16 +464,16 @@ Proof. exists e'; constructor; split; trivial; apply X.eq_trans with x; auto. destruct (H k). destruct (H9 H8) as (e'',hyp). - exists e''; auto. + exists e''... inversion_clear Hm;inversion_clear Hm'. destruct (andb_prop _ _ H); clear H. destruct (IHb H1 H3 H6). destruct (In_inv H0). - exists e; constructor; split; trivial; apply X.eq_trans with x'; auto. + exists e; constructor; split; trivial; apply X.eq_trans with x'... destruct (H k). destruct (H10 H8) as (e'',hyp). - exists e''; auto. + exists e''... inversion_clear Hm;inversion_clear Hm'. destruct (andb_prop _ _ H); clear H. @@ -615,7 +615,8 @@ Proof. inversion_clear 1. exists x'. destruct H0; simpl in *. - split; auto. + split. + auto with ordered_type. constructor 1. unfold eqke in *; simpl in *; intuition congruence. destruct IHm as (y, hyp); auto. @@ -946,7 +947,7 @@ Proof. destruct (IHm0 H0) as (_,H4); apply H4; auto. case_eq (find x m0); intros; auto. assert (eqk (elt:=oee') (k,(oo,oo')) (x,(oo,oo'))). - red; auto. + red; auto with ordered_type. destruct (Sort_Inf_NotIn H0 (Inf_eq (eqk_sym H5) H1)). exists p; apply find_2; auto. (* k < x *) @@ -1315,7 +1316,7 @@ Proof. apply (IHm1 H0 (Build_slist H5)); intuition. Qed. -Ltac cmp_solve := unfold eq, lt; simpl; try Raw.MX.elim_comp; auto. +Ltac cmp_solve := unfold eq, lt; simpl; try Raw.MX.elim_comp; auto with ordered_type. Definition compare : forall m1 m2, Compare lt eq m1 m2. Proof. diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v index 6e08c38a49..f0b31e6986 100644 --- a/theories/FSets/FSetBridge.v +++ b/theories/FSets/FSetBridge.v @@ -63,11 +63,11 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. {s' : t | forall y : elt, In y s' <-> ~ E.eq x y /\ In y s}. Proof. intros; exists (remove x s); intuition. - absurd (In x (remove x s)); auto with set. - apply In_1 with y; auto. + absurd (In x (remove x s)); auto with set ordered_type. + apply In_1 with y; auto with ordered_type. elim (E.eq_dec x y); intros; auto. - absurd (In x (remove x s)); auto with set. - apply In_1 with y; auto. + absurd (In x (remove x s)); auto with set ordered_type. + apply In_1 with y; auto with ordered_type. eauto with set. Qed. @@ -470,7 +470,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Hint Resolve elements_3 : core. Lemma elements_3w : forall s : t, NoDupA E.eq (elements s). - Proof. auto. Qed. + Proof. auto with ordered_type. Qed. Definition min_elt (s : t) : option elt := match min_elt s with diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v index c6b2e0a09d..e500debc73 100644 --- a/theories/FSets/FSetProperties.v +++ b/theories/FSets/FSetProperties.v @@ -939,7 +939,7 @@ Module OrdProperties (M:S). generalize (gtb_1 x a)(gtb_1 x b); destruct (gtb x a); destruct (gtb x b); auto. intros. symmetry; rewrite H1. - apply ME.eq_lt with a; auto. + apply ME.eq_lt with a; auto with ordered_type. rewrite <- H0; auto. intros. rewrite H0. @@ -1013,7 +1013,7 @@ Module OrdProperties (M:S). intros. inversion_clear H2. rewrite <- elements_iff in H1. - apply ME.lt_eq with x; auto. + apply ME.lt_eq with x; auto with ordered_type. inversion H3. red; intros a. rewrite InA_app_iff, InA_cons, InA_nil by auto with *. @@ -1052,7 +1052,7 @@ Module OrdProperties (M:S). 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 ordered_type. inversion H0; auto. red; intros. rewrite remove_iff in H0; destruct H0. @@ -1073,7 +1073,7 @@ Module OrdProperties (M:S). 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 ordered_type. inversion H0; auto. red; intros. rewrite remove_iff in H0; destruct H0. diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index 566dd31a9e..a411c5e54e 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -26,6 +26,8 @@ Arguments LT [X lt eq x y] _. Arguments EQ [X lt eq x y] _. Arguments GT [X lt eq x y] _. +Create HintDb ordered_type. + Module Type MiniOrderedType. Parameter Inline t : Type. @@ -42,8 +44,8 @@ Module Type MiniOrderedType. Parameter compare : forall x y : t, Compare lt eq x y. - Hint Immediate eq_sym : core. - Hint Resolve eq_refl eq_trans lt_not_eq lt_trans : core. + Hint Immediate eq_sym : ordered_type. + Hint Resolve eq_refl eq_trans lt_not_eq lt_trans : ordered_type. End MiniOrderedType. @@ -60,9 +62,9 @@ Module MOT_to_OT (Import O : MiniOrderedType) <: OrderedType. Include O. Definition eq_dec : forall x y : t, {eq x y} + {~ eq x y}. - Proof. - intros; elim (compare x y); intro H; [ right | left | right ]; auto. - assert (~ eq y x); auto. + Proof with auto with ordered_type. + intros; elim (compare x y); intro H; [ right | left | right ]... + assert (~ eq y x)... Defined. End MOT_to_OT. @@ -79,31 +81,30 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma lt_antirefl : forall x, ~ lt x x. Proof. - intros; intro; absurd (eq x x); auto. + intros; intro; absurd (eq x x); auto with ordered_type. Qed. Instance lt_strorder : StrictOrder lt. Proof. split; [ exact lt_antirefl | exact lt_trans]. Qed. Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z. - Proof. + Proof with auto with ordered_type. intros; destruct (compare x z) as [Hlt|Heq|Hlt]; auto. - elim (lt_not_eq H); apply eq_trans with z; auto. - elim (lt_not_eq (lt_trans Hlt H)); auto. + elim (lt_not_eq H); apply eq_trans with z... + elim (lt_not_eq (lt_trans Hlt H))... Qed. Lemma eq_lt : forall x y z, eq x y -> lt y z -> lt x z. - Proof. + Proof with auto with ordered_type. intros; destruct (compare x z) as [Hlt|Heq|Hlt]; auto. - elim (lt_not_eq H0); apply eq_trans with x; auto. - elim (lt_not_eq (lt_trans H0 Hlt)); auto. + elim (lt_not_eq H0); apply eq_trans with x... + elim (lt_not_eq (lt_trans H0 Hlt))... Qed. Instance lt_compat : Proper (eq==>eq==>iff) lt. - Proof. apply proper_sym_impl_iff_2; auto with *. intros x x' Hx y y' Hy H. - apply eq_lt with x; auto. + apply eq_lt with x; auto with ordered_type. apply lt_eq with y; auto. Qed. @@ -143,9 +144,9 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma eq_not_gt x y : eq x y -> ~ lt y x. Proof. order. Qed. Lemma lt_not_gt x y : lt x y -> ~ lt y x. Proof. order. Qed. - Hint Resolve gt_not_eq eq_not_lt : core. - Hint Immediate eq_lt lt_eq le_eq eq_le neq_eq eq_neq : core. - Hint Resolve eq_not_gt lt_antirefl lt_not_gt : core. + Hint Resolve gt_not_eq eq_not_lt : ordered_type. + Hint Immediate eq_lt lt_eq le_eq eq_le neq_eq eq_neq : ordered_type. + Hint Resolve eq_not_gt lt_antirefl lt_not_gt : ordered_type. Lemma elim_compare_eq : forall x y : t, @@ -197,7 +198,7 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma lt_dec : forall x y : t, {lt x y} + {~ lt x y}. Proof. - intros; elim (compare x y); [ left | right | right ]; auto. + intros; elim (compare x y); [ left | right | right ]; auto with ordered_type. Defined. Definition eqb x y : bool := if eq_dec x y then true else false. @@ -247,8 +248,8 @@ Proof. exact (SortA_NoDupA eq_equiv lt_strorder lt_compat). Qed. End ForNotations. -Hint Resolve ListIn_In Sort_NoDup Inf_lt : core. -Hint Immediate In_eq Inf_lt : core. +Hint Resolve ListIn_In Sort_NoDup Inf_lt : ordered_type. +Hint Immediate In_eq Inf_lt : ordered_type. End OrderedTypeFacts. @@ -266,8 +267,8 @@ Module KeyOrderedType(O:OrderedType). eq (fst p) (fst p') /\ (snd p) = (snd p'). Definition ltk (p p':key*elt) := lt (fst p) (fst p'). - Hint Unfold eqk eqke ltk : core. - Hint Extern 2 (eqke ?a ?b) => split : core. + Hint Unfold eqk eqke ltk : ordered_type. + Hint Extern 2 (eqke ?a ?b) => split : ordered_type. (* eqke is stricter than eqk *) @@ -283,35 +284,35 @@ Module KeyOrderedType(O:OrderedType). Lemma ltk_right_l : forall x k e e', ltk (k,e) x -> ltk (k,e') x. Proof. auto. Qed. - Hint Immediate ltk_right_r ltk_right_l : core. + Hint Immediate ltk_right_r ltk_right_l : ordered_type. (* eqk, eqke are equalities, ltk is a strict order *) Lemma eqk_refl : forall e, eqk e e. - Proof. auto. Qed. + Proof. auto with ordered_type. Qed. Lemma eqke_refl : forall e, eqke e e. - Proof. auto. Qed. + Proof. auto with ordered_type. Qed. Lemma eqk_sym : forall e e', eqk e e' -> eqk e' e. - Proof. auto. Qed. + Proof. auto with ordered_type. Qed. Lemma eqke_sym : forall e e', eqke e e' -> eqke e' e. Proof. unfold eqke; intuition. Qed. Lemma eqk_trans : forall e e' e'', eqk e e' -> eqk e' e'' -> eqk e e''. - Proof. eauto. Qed. + Proof. eauto with ordered_type. Qed. Lemma eqke_trans : forall e e' e'', eqke e e' -> eqke e' e'' -> eqke e e''. Proof. - unfold eqke; intuition; [ eauto | congruence ]. + unfold eqke; intuition; [ eauto with ordered_type | congruence ]. Qed. Lemma ltk_trans : forall e e' e'', ltk e e' -> ltk e' e'' -> ltk e e''. - Proof. eauto. Qed. + Proof. eauto with ordered_type. Qed. Lemma ltk_not_eqk : forall e e', ltk e e' -> ~ eqk e e'. - Proof. unfold eqk, ltk; auto. Qed. + Proof. unfold eqk, ltk; auto with ordered_type. Qed. Lemma ltk_not_eqke : forall e e', ltk e e' -> ~eqke e e'. Proof. @@ -319,18 +320,18 @@ Module KeyOrderedType(O:OrderedType). exact (lt_not_eq H H1). Qed. - Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core. - Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke : core. - Hint Immediate eqk_sym eqke_sym : core. + Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : ordered_type. + Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke : ordered_type. + Hint Immediate eqk_sym eqke_sym : ordered_type. Global Instance eqk_equiv : Equivalence eqk. - Proof. constructor; eauto. Qed. + Proof. constructor; eauto with ordered_type. Qed. Global Instance eqke_equiv : Equivalence eqke. - Proof. split; eauto. Qed. + Proof. split; eauto with ordered_type. Qed. Global Instance ltk_strorder : StrictOrder ltk. - Proof. constructor; eauto. intros x; apply (irreflexivity (x:=fst x)). Qed. + Proof. constructor; eauto with ordered_type. intros x; apply (irreflexivity (x:=fst x)). Qed. Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk. Proof. @@ -348,45 +349,45 @@ Module KeyOrderedType(O:OrderedType). Lemma eqk_not_ltk : forall x x', eqk x x' -> ~ltk x x'. Proof. - unfold eqk, ltk; simpl; auto. + unfold eqk, ltk; simpl; auto with ordered_type. Qed. Lemma ltk_eqk : forall e e' e'', ltk e e' -> eqk e' e'' -> ltk e e''. - Proof. eauto. Qed. + Proof. eauto with ordered_type. Qed. Lemma eqk_ltk : forall e e' e'', eqk e e' -> ltk e' e'' -> ltk e e''. Proof. intros (k,e) (k',e') (k'',e''). - unfold ltk, eqk; simpl; eauto. + unfold ltk, eqk; simpl; eauto with ordered_type. Qed. - Hint Resolve eqk_not_ltk : core. - Hint Immediate ltk_eqk eqk_ltk : core. + Hint Resolve eqk_not_ltk : ordered_type. + Hint Immediate ltk_eqk eqk_ltk : ordered_type. Lemma InA_eqke_eqk : forall x m, InA eqke x m -> InA eqk x m. Proof. unfold eqke; induction 1; intuition. Qed. - Hint Resolve InA_eqke_eqk : core. + Hint Resolve InA_eqke_eqk : ordered_type. Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). Definition In k m := exists e:elt, MapsTo k e m. Notation Sort := (sort ltk). Notation Inf := (lelistA ltk). - Hint Unfold MapsTo In : core. + Hint Unfold MapsTo In : ordered_type. (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *) Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l. - Proof. + Proof with auto with ordered_type. firstorder. - exists x; auto. + exists x... induction H. - destruct y. - exists e; auto. + destruct y. + exists e... destruct IHInA as [e H0]. - exists e; auto. + exists e... Qed. Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. @@ -405,8 +406,8 @@ Module KeyOrderedType(O:OrderedType). Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l. Proof. exact (InfA_ltA ltk_strorder). Qed. - Hint Immediate Inf_eq : core. - Hint Resolve Inf_lt : core. + Hint Immediate Inf_eq : ordered_type. + Hint Resolve Inf_lt : ordered_type. Lemma Sort_Inf_In : forall l p q, Sort l -> Inf q l -> InA eqk p l -> ltk q p. @@ -420,8 +421,8 @@ Module KeyOrderedType(O:OrderedType). intros; red; intros. destruct H1 as [e' H2]. elim (@ltk_not_eqk (k,e) (k,e')). - eapply Sort_Inf_In; eauto. - red; simpl; auto. + eapply Sort_Inf_In; eauto with ordered_type. + red; simpl; auto with ordered_type. Qed. Lemma Sort_NoDupA: forall l, Sort l -> NoDupA eqk l. @@ -437,7 +438,7 @@ Module KeyOrderedType(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. - inversion_clear 2; auto. + inversion_clear 2; auto with ordered_type. left; apply Sort_In_cons_1 with l; auto. Qed. @@ -451,7 +452,7 @@ Module KeyOrderedType(O:OrderedType). Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l. Proof. inversion 1. - inversion_clear H0; eauto. + inversion_clear H0; eauto with ordered_type. destruct H1; simpl in *; intuition. Qed. @@ -469,19 +470,19 @@ Module KeyOrderedType(O:OrderedType). End Elt. - Hint Unfold eqk eqke ltk : core. - Hint Extern 2 (eqke ?a ?b) => split : core. - Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core. - Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke : core. - Hint Immediate eqk_sym eqke_sym : core. - Hint Resolve eqk_not_ltk : core. - Hint Immediate ltk_eqk eqk_ltk : core. - Hint Resolve InA_eqke_eqk : core. - Hint Unfold MapsTo In : core. - Hint Immediate Inf_eq : core. - Hint Resolve Inf_lt : core. - Hint Resolve Sort_Inf_NotIn : core. - Hint Resolve In_inv_2 In_inv_3 : core. + Hint Unfold eqk eqke ltk : ordered_type. + Hint Extern 2 (eqke ?a ?b) => split : ordered_type. + Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : ordered_type. + Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke : ordered_type. + Hint Immediate eqk_sym eqke_sym : ordered_type. + Hint Resolve eqk_not_ltk : ordered_type. + Hint Immediate ltk_eqk eqk_ltk : ordered_type. + Hint Resolve InA_eqke_eqk : ordered_type. + Hint Unfold MapsTo In : ordered_type. + Hint Immediate Inf_eq : ordered_type. + Hint Resolve Inf_lt : ordered_type. + Hint Resolve Sort_Inf_NotIn : ordered_type. + Hint Resolve In_inv_2 In_inv_3 : ordered_type. End KeyOrderedType. diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v index 9b99fa5de4..a8e6993a63 100644 --- a/theories/Structures/OrderedTypeEx.v +++ b/theories/Structures/OrderedTypeEx.v @@ -178,7 +178,7 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType. Lemma eq_refl : forall x : t, eq x x. Proof. - intros (x1,x2); red; simpl; auto. + intros (x1,x2); red; simpl; auto with ordered_type. Qed. Lemma eq_sym : forall x y : t, eq x y -> eq y x. @@ -188,16 +188,16 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType. Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. Proof. - intros (x1,x2) (y1,y2) (z1,z2); unfold eq; simpl; intuition eauto. + intros (x1,x2) (y1,y2) (z1,z2); unfold eq; simpl; intuition eauto with ordered_type. Qed. Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. Proof. intros (x1,x2) (y1,y2) (z1,z2); unfold eq, lt; simpl; intuition. - left; eauto. + left; eauto with ordered_type. left; eapply MO1.lt_eq; eauto. left; eapply MO1.eq_lt; eauto. - right; split; eauto. + right; split; eauto with ordered_type. Qed. Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. @@ -214,7 +214,7 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType. destruct (O2.compare x2 y2). apply LT; unfold lt; auto. apply EQ; unfold eq; auto. - apply GT; unfold lt; auto. + apply GT; unfold lt; auto with ordered_type. apply GT; unfold lt; auto. Defined. |