diff options
author | 2009-10-19 13:14:18 +0000 | |
---|---|---|
committer | 2009-10-19 13:14:18 +0000 | |
commit | c054cff9fe279c9a0ca45d34b0032692eb676e39 (patch) | |
tree | 1176391cde626256a977076595a27c2c18237da3 /theories/Structures/OrderedType.v | |
parent | 6b391cc61a35d1ef42f88d18f9c428c369180493 (diff) |
Merge SetoidList2 into SetoidList.
This file contains low-level stuff for FSets/FMaps. Switching it to
the new version (the one using Equivalence and so on instead of
eq_refl/eq_sym/eq_trans and so on) only leads to a few changes in
FSets/FMaps that are minor and probably invisible to standard users.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12400 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Structures/OrderedType.v')
-rw-r--r-- | theories/Structures/OrderedType.v | 50 |
1 files changed, 37 insertions, 13 deletions
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index e582db3ea..a8e1ebdd6 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -218,32 +218,32 @@ Notation Sort:=(sort lt). Notation NoDup:=(NoDupA eq). Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. -Proof. exact (InA_eqA eq_sym eq_trans). Qed. +Proof. exact (InA_eqA eq_equiv). Qed. Lemma ListIn_In : forall l x, List.In x l -> In x l. -Proof. exact (In_InA eq_refl). Qed. +Proof. exact (In_InA eq_equiv). Qed. Lemma Inf_lt : forall l x y, lt x y -> Inf y l -> Inf x l. -Proof. exact (InfA_ltA lt_trans). Qed. +Proof. exact (InfA_ltA lt_strorder). Qed. Lemma Inf_eq : forall l x y, eq x y -> Inf y l -> Inf x l. -Proof. exact (InfA_eqA eq_lt). Qed. +Proof. exact (InfA_eqA eq_equiv lt_strorder lt_compat). Qed. Lemma Sort_Inf_In : forall l x a, Sort l -> Inf a l -> In x l -> lt a x. -Proof. exact (SortA_InfA_InA eq_refl eq_sym lt_trans lt_eq eq_lt). Qed. +Proof. exact (SortA_InfA_InA eq_equiv lt_strorder lt_compat). Qed. Lemma ListIn_Inf : forall l x, (forall y, List.In y l -> lt x y) -> Inf x l. Proof. exact (@In_InfA t lt). Qed. Lemma In_Inf : forall l x, (forall y, In y l -> lt x y) -> Inf x l. -Proof. exact (InA_InfA eq_refl (ltA:=lt)). Qed. +Proof. exact (InA_InfA eq_equiv (ltA:=lt)). Qed. Lemma Inf_alt : forall l x, Sort l -> (Inf x l <-> (forall y, In y l -> lt x y)). -Proof. exact (InfA_alt eq_refl eq_sym lt_trans lt_eq eq_lt). Qed. +Proof. exact (InfA_alt eq_equiv lt_strorder lt_compat). Qed. Lemma Sort_NoDup : forall l, Sort l -> NoDup l. -Proof. exact (SortA_NoDupA eq_refl eq_sym lt_trans lt_not_eq lt_eq eq_lt) . Qed. +Proof. exact (SortA_NoDupA eq_equiv lt_strorder lt_compat). Qed. End ForNotations. @@ -323,6 +323,30 @@ Module KeyOrderedType(O:OrderedType). Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke. Hint Immediate eqk_sym eqke_sym. + Global Instance eqk_equiv : Equivalence eqk. + Proof. split; eauto. Qed. + + Global Instance eqke_equiv : Equivalence eqke. + Proof. split; eauto. Qed. + + Global Instance ltk_strorder : StrictOrder ltk. + Proof. + split; eauto. + intros (x,e); compute; apply (StrictOrder_Irreflexive x). + Qed. + + Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk. + Proof. + intros (x,e) (x',e') Hxx' (y,f) (y',f') Hyy'; compute. + compute in Hxx'; compute in Hyy'. rewrite Hxx', Hyy'; auto. + Qed. + + Global Instance ltk_compat' : Proper (eqke==>eqke==>iff) ltk. + Proof. + intros (x,e) (x',e') (Hxx',_) (y,f) (y',f') (Hyy',_); compute. + compute in Hxx'; compute in Hyy'. rewrite Hxx', Hyy'; auto. + Qed. + (* Additionnal facts *) Lemma eqk_not_ltk : forall x x', eqk x x' -> ~ltk x x'. @@ -370,7 +394,7 @@ Module KeyOrderedType(O:OrderedType). Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. Proof. - intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto. + intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto with *. Qed. Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. @@ -379,10 +403,10 @@ Module KeyOrderedType(O:OrderedType). Qed. Lemma Inf_eq : forall l x x', eqk x x' -> Inf x' l -> Inf x l. - Proof. exact (InfA_eqA eqk_ltk). Qed. + Proof. exact (InfA_eqA eqk_equiv ltk_strorder ltk_compat). Qed. Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l. - Proof. exact (InfA_ltA ltk_trans). Qed. + Proof. exact (InfA_ltA ltk_strorder). Qed. Hint Immediate Inf_eq. Hint Resolve Inf_lt. @@ -390,7 +414,7 @@ Module KeyOrderedType(O:OrderedType). Lemma Sort_Inf_In : forall l p q, Sort l -> Inf q l -> InA eqk p l -> ltk q p. Proof. - exact (SortA_InfA_InA eqk_refl eqk_sym ltk_trans ltk_eqk eqk_ltk). + exact (SortA_InfA_InA eqk_equiv ltk_strorder ltk_compat). Qed. Lemma Sort_Inf_NotIn : @@ -405,7 +429,7 @@ Module KeyOrderedType(O:OrderedType). Lemma Sort_NoDupA: forall l, Sort l -> NoDupA eqk l. Proof. - exact (SortA_NoDupA eqk_refl eqk_sym ltk_trans ltk_not_eqk ltk_eqk eqk_ltk). + exact (SortA_NoDupA eqk_equiv ltk_strorder ltk_compat). Qed. Lemma Sort_In_cons_1 : forall e l e', Sort (e::l) -> InA eqk e' l -> ltk e e'. |