From 772ff9dfb10312ecaf2f1f08a9145c9383600300 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 7 Jan 2010 15:32:10 +0000 Subject: misc improvements in some Structures files git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12634 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Structures/DecidableType2Facts.v | 106 ++++++++++++++---------------- theories/Structures/GenericMinMax.v | 7 +- theories/Structures/OrderedType2Alt.v | 13 ++-- theories/Structures/OrderedType2Lists.v | 8 --- 4 files changed, 58 insertions(+), 76 deletions(-) diff --git a/theories/Structures/DecidableType2Facts.v b/theories/Structures/DecidableType2Facts.v index 154a40d87..07a3b8f83 100644 --- a/theories/Structures/DecidableType2Facts.v +++ b/theories/Structures/DecidableType2Facts.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -Require Import DecidableType2 Bool SetoidList. +Require Import DecidableType2 Bool SetoidList RelationPairs. (** In a BooleanEqualityType, [eqb] is compatible with [eq] *) @@ -23,55 +23,35 @@ End BoolEqualityFacts. (** * Keys and datas used in FMap *) - -Module KeyDecidableType(D:DecidableType). - Import D. +Module KeyDecidableType(Import D:DecidableType). Section Elt. Variable elt : Type. Notation key:=t. - Definition eqk (p p':key*elt) := eq (fst p) (fst p'). - Definition eqke (p p':key*elt) := - eq (fst p) (fst p') /\ (snd p) = (snd p'). + Local Open Scope signature_scope. + Definition eqk : relation (key*elt) := eq @@1. + Definition eqke : relation (key*elt) := eq * Logic.eq. Hint Unfold eqk eqke. - Hint Extern 2 (eqke ?a ?b) => split. - (* eqke is stricter than eqk *) + (* eqke is stricter than eqk *) - Lemma eqke_eqk : forall x x', eqke x x' -> eqk x x'. - Proof. - unfold eqk, eqke; intuition. - Qed. + Global Instance eqke_eqk : subrelation eqke eqk. + Proof. firstorder. Qed. - (* eqk, eqke are equalities *) + (* eqk, eqke are equalities, ltk is a strict order *) - Instance eqk_equiv : Equivalence eqk. - Proof. - constructor; unfold eqk; repeat red; intros; - [ reflexivity | symmetry; auto | etransitivity; eauto ]. - Qed. + Global Instance eqk_equiv : Equivalence eqk. - Instance eqke_equiv : Equivalence eqke. - Proof. - constructor; unfold eqke; repeat red; intuition; simpl; - etransitivity; eauto. - Qed. + Global Instance eqke_equiv : Equivalence eqke. -(* - 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). -*) + (* Additionnal facts *) Lemma InA_eqke_eqk : forall x m, InA eqke x m -> InA eqk x m. Proof. - unfold eqke; induction 1; intuition. + unfold eqke, RelProd; induction 1; firstorder. Qed. Hint Resolve InA_eqke_eqk. @@ -92,63 +72,75 @@ Module KeyDecidableType(D:DecidableType). firstorder. exists x; auto. induction H. - destruct y. - exists e; auto. + destruct y; compute in H. + exists e; left; auto. destruct IHInA as [e H0]. exists e; auto. Qed. - Global Instance MapsTo_compat : - Proper (eq==>Logic.eq==>Logic.eq==>iff) MapsTo. + Lemma In_alt2 : forall k l, In k l <-> Exists (fun p => eq k (fst p)) l. Proof. - intros x x' Hxx' e e' Hee' l l' Hll'; subst. - unfold MapsTo. - assert (EQN : eqke (x,e') (x',e')) by (compute;auto). - rewrite EQN; intuition. + unfold In, MapsTo. + setoid_rewrite Exists_exists; setoid_rewrite InA_alt. + firstorder. + exists (snd x), x; auto. Qed. - Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. + Lemma In_nil : forall k, In k nil <-> False. Proof. - intros; rewrite <- H; auto. + intros; rewrite In_alt2; apply Exists_nil. Qed. - Global Instance In_compat : Proper (eq==>Logic.eq==>iff) In. + Lemma In_cons : forall k p l, + In k (p::l) <-> eq k (fst p) \/ In k l. Proof. - intros x x' Hxx' l l' Hll'; subst l. - unfold In. - split; intros (e,He); exists e. - rewrite <- Hxx'; auto. - rewrite Hxx'; auto. + intros; rewrite !In_alt2, Exists_cons; intuition. Qed. - Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. + Global Instance MapsTo_compat : + Proper (eq==>Logic.eq==>equivlistA eqke==>iff) MapsTo. + Proof. + intros x x' Hx e e' He l l' Hl. unfold MapsTo. + rewrite Hx, He, Hl; intuition. + Qed. + + Global Instance In_compat : Proper (eq==>equivlistA eqk==>iff) In. Proof. - intros; rewrite <- H; auto. + intros x x' Hx l l' Hl. rewrite !In_alt. + setoid_rewrite Hl. setoid_rewrite Hx. intuition. Qed. + Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. + Proof. intros l x y e EQ. rewrite <- EQ; auto. Qed. + + Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. + Proof. intros l x y EQ. rewrite <- EQ; auto. Qed. + 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. - destruct H1; simpl in *; intuition. + intros; invlist In; invlist MapsTo. compute in * |- ; intuition. + right; exists x; auto. Qed. Lemma In_inv_2 : forall k k' e e' l, InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l. Proof. - inversion_clear 1; compute in H0; intuition. + intros; invlist InA; intuition. Qed. Lemma In_inv_3 : forall x x' l, InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l. Proof. - inversion_clear 1; compute in H0; intuition. + intros; invlist InA; compute in * |- ; intuition. Qed. End Elt. + Hint Unfold eqk eqke. + Hint Extern 2 (eqke ?a ?b) => split. + Hint Resolve InA_eqke_eqk. + Hint Unfold MapsTo In. Hint Resolve In_inv_2 In_inv_3. - (* TODO: (re-)populate with more hints after failed attempt of Global Hint *) End KeyDecidableType. diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v index 0650546a5..f5ff27888 100644 --- a/theories/Structures/GenericMinMax.v +++ b/theories/Structures/GenericMinMax.v @@ -488,7 +488,7 @@ End MinMaxProperties. -(** Some Remaining questions... +(** TODO: Some Remaining questions... --> Compare with a type-classes version ? @@ -497,9 +497,4 @@ End MinMaxProperties. --> Is it possible to avoid copy-paste about min even more ? ---> Can this modular approach be used for more complex things, - in particular div/mod ? - How can we share common parts between nat and Z in this case ? - How to handle different choices (Zdiv vs. ZOdiv) ? - *) diff --git a/theories/Structures/OrderedType2Alt.v b/theories/Structures/OrderedType2Alt.v index 337197733..b036b50e5 100644 --- a/theories/Structures/OrderedType2Alt.v +++ b/theories/Structures/OrderedType2Alt.v @@ -226,15 +226,18 @@ Module OT_to_Alt (Import O:OrderedType) <: OrderedTypeAlt. rewrite H in H0. elim (StrictOrder_Irreflexive x); auto. Qed. + Lemma compare_Gt : forall x y, compare x y = Gt <-> lt y x. + Proof. + intros x y. rewrite compare_sym, CompOpp_iff. apply compare_Lt. + Qed. + Lemma compare_trans : forall c x y z, (x?=y) = c -> (y?=z) = c -> (x?=z) = c. Proof. intros c x y z. - destruct c; unfold compare. - rewrite 3 compare_Eq. etransitivity; eauto. - rewrite 3 compare_Lt. etransitivity; eauto. - do 3 (rewrite compare_sym, CompOpp_iff, compare_Lt). - etransitivity; eauto. + destruct c; unfold compare; + rewrite ?compare_Eq, ?compare_Lt, ?compare_Gt; + transitivity y; auto. Qed. End OT_to_Alt. diff --git a/theories/Structures/OrderedType2Lists.v b/theories/Structures/OrderedType2Lists.v index 51e751239..79690fb02 100644 --- a/theories/Structures/OrderedType2Lists.v +++ b/theories/Structures/OrderedType2Lists.v @@ -242,14 +242,6 @@ Module KeyOrderedType(Import O:OrderedType). End Elt. - Hint Resolve (fun elt => @Equivalence_Reflexive _ _ (eqk_equiv elt)). - Hint Resolve (fun elt => @Equivalence_Transitive _ _ (eqk_equiv elt)). - Hint Immediate (fun elt => @Equivalence_Symmetric _ _ (eqk_equiv elt)). - Hint Resolve (fun elt => @Equivalence_Reflexive _ _ (eqke_equiv elt)). - Hint Resolve (fun elt => @Equivalence_Transitive _ _ (eqke_equiv elt)). - Hint Immediate (fun elt => @Equivalence_Symmetric _ _ (eqke_equiv elt)). - Hint Resolve (fun elt => @StrictOrder_Transitive _ _ (ltk_strorder elt)). - Hint Unfold eqk eqke ltk. Hint Extern 2 (eqke ?a ?b) => split. Hint Resolve ltk_not_eqk ltk_not_eqke. -- cgit v1.2.3