summaryrefslogtreecommitdiff
path: root/theories/FSets
diff options
context:
space:
mode:
Diffstat (limited to 'theories/FSets')
-rw-r--r--theories/FSets/FMapFacts.v1276
-rw-r--r--theories/FSets/FMapInterface.v10
-rw-r--r--theories/FSets/FMapList.v4
-rw-r--r--theories/FSets/FMapPositive.v86
-rw-r--r--theories/FSets/FSetAVL.v10
-rw-r--r--theories/FSets/FSetBridge.v13
-rw-r--r--theories/FSets/FSetDecide.v49
-rw-r--r--theories/FSets/FSetEqProperties.v47
-rw-r--r--theories/FSets/FSetFacts.v48
-rw-r--r--theories/FSets/FSetFullAVL.v10
-rw-r--r--theories/FSets/FSetInterface.v35
-rw-r--r--theories/FSets/FSetList.v10
-rw-r--r--theories/FSets/FSetProperties.v566
-rw-r--r--theories/FSets/FSetToFiniteSet.v12
-rw-r--r--theories/FSets/FSetWeakList.v57
-rw-r--r--theories/FSets/OrderedType.v35
-rw-r--r--theories/FSets/OrderedTypeAlt.v11
-rw-r--r--theories/FSets/OrderedTypeEx.v24
18 files changed, 1545 insertions, 758 deletions
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 05cd1892..df12166e 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FMapFacts.v 11359 2008-09-04 09:43:36Z notin $ *)
+(* $Id: FMapFacts.v 11720 2008-12-28 07:12:15Z letouzey $ *)
(** * Finite maps library *)
@@ -20,9 +20,14 @@ Require Export FMapInterface.
Set Implicit Arguments.
Unset Strict Implicit.
+Hint Extern 1 (Equivalence _) => constructor; congruence.
+
+Notation Leibniz := (@eq _) (only parsing).
+
+
(** * Facts about weak maps *)
-Module WFacts (E:DecidableType)(Import M:WSfun E).
+Module WFacts_fun (E:DecidableType)(Import M:WSfun E).
Notation eq_dec := E.eq_dec.
Definition eqb x y := if eq_dec x y then true else false.
@@ -32,6 +37,15 @@ Proof.
destruct b; destruct b'; intuition.
Qed.
+Lemma eq_option_alt : forall (elt:Type)(o o':option elt),
+ o=o' <-> (forall e, o=Some e <-> o'=Some e).
+Proof.
+split; intros.
+subst; split; auto.
+destruct o; destruct o'; try rewrite H; auto.
+symmetry; rewrite <- H; auto.
+Qed.
+
Lemma MapsTo_fun : forall (elt:Type) m x (e e':elt),
MapsTo x e m -> MapsTo x e' m -> e=e'.
Proof.
@@ -85,14 +99,10 @@ Qed.
Lemma not_find_in_iff : forall m x, ~In x m <-> find x m = None.
Proof.
-intros.
-generalize (find_mapsto_iff m x); destruct (find x m).
-split; intros; try discriminate.
-destruct H0.
-exists e; rewrite H; auto.
-split; auto.
-intros; intros (e,H1).
-rewrite H in H1; discriminate.
+split; intros.
+rewrite eq_option_alt. intro e. rewrite <- find_mapsto_iff.
+split; intro H'; try discriminate. elim H; exists e; auto.
+intros (e,He); rewrite find_mapsto_iff,H in He; discriminate.
Qed.
Lemma in_find_iff : forall m x, In x m <-> find x m <> None.
@@ -334,21 +344,14 @@ Qed.
Lemma find_o : forall m x y, E.eq x y -> find x m = find y m.
Proof.
-intros.
-generalize (find_mapsto_iff m x) (find_mapsto_iff m y) (fun e => MapsTo_iff m e H).
-destruct (find x m); destruct (find y m); intros.
-rewrite <- H0; rewrite H2; rewrite H1; auto.
-symmetry; rewrite <- H1; rewrite <- H2; rewrite H0; auto.
-rewrite <- H0; rewrite H2; rewrite H1; auto.
-auto.
+intros. rewrite eq_option_alt. intro e. rewrite <- 2 find_mapsto_iff.
+apply MapsTo_iff; auto.
Qed.
Lemma empty_o : forall x, find x (empty elt) = None.
Proof.
-intros.
-case_eq (find x (empty elt)); intros; auto.
-generalize (find_2 H).
-rewrite empty_mapsto_iff; intuition.
+intros. rewrite eq_option_alt. intro e.
+rewrite <- find_mapsto_iff, empty_mapsto_iff; now intuition.
Qed.
Lemma empty_a : forall x, mem x (empty elt) = false.
@@ -368,15 +371,12 @@ Qed.
Lemma add_neq_o : forall m x y e,
~ E.eq x y -> find y (add x e m) = find y m.
Proof.
-intros.
-case_eq (find y m); intros; auto with map.
-case_eq (find y (add x e m)); intros; auto with map.
-rewrite <- H0; symmetry.
-apply find_1; apply add_3 with x e; auto with map.
+intros. rewrite eq_option_alt. intro e'. rewrite <- 2 find_mapsto_iff.
+apply add_neq_mapsto_iff; auto.
Qed.
Hint Resolve add_neq_o : map.
-Lemma add_o : forall m x y e,
+Lemma add_o : forall m x y e,
find y (add x e m) = if eq_dec x y then Some e else find y m.
Proof.
intros; destruct (eq_dec x y); auto with map.
@@ -404,45 +404,38 @@ Qed.
Lemma remove_eq_o : forall m x y,
E.eq x y -> find y (remove x m) = None.
Proof.
-intros.
-generalize (remove_1 (m:=m) H).
-generalize (find_mapsto_iff (remove x m) y).
-destruct (find y (remove x m)); auto.
-destruct 2.
-exists e; rewrite H0; auto.
+intros. rewrite eq_option_alt. intro e.
+rewrite <- find_mapsto_iff, remove_mapsto_iff; now intuition.
Qed.
Hint Resolve remove_eq_o : map.
-Lemma remove_neq_o : forall m x y,
- ~ E.eq x y -> find y (remove x m) = find y m.
+Lemma remove_neq_o : forall m x y,
+ ~ E.eq x y -> find y (remove x m) = find y m.
Proof.
-intros.
-case_eq (find y m); intros; auto with map.
-case_eq (find y (remove x m)); intros; auto with map.
-rewrite <- H0; symmetry.
-apply find_1; apply remove_3 with x; auto with map.
+intros. rewrite eq_option_alt. intro e.
+rewrite <- find_mapsto_iff, remove_neq_mapsto_iff; now intuition.
Qed.
Hint Resolve remove_neq_o : map.
-Lemma remove_o : forall m x y,
+Lemma remove_o : forall m x y,
find y (remove x m) = if eq_dec x y then None else find y m.
Proof.
intros; destruct (eq_dec x y); auto with map.
Qed.
-Lemma remove_eq_b : forall m x y,
+Lemma remove_eq_b : forall m x y,
E.eq x y -> mem y (remove x m) = false.
Proof.
intros; rewrite mem_find_b; rewrite remove_eq_o; auto.
Qed.
-Lemma remove_neq_b : forall m x y,
+Lemma remove_neq_b : forall m x y,
~ E.eq x y -> mem y (remove x m) = mem y m.
Proof.
intros; do 2 rewrite mem_find_b; rewrite remove_neq_o; auto.
Qed.
-Lemma remove_b : forall m x y,
+Lemma remove_b : forall m x y,
mem y (remove x m) = negb (eqb x y) && mem y m.
Proof.
intros; do 2 rewrite mem_find_b; rewrite remove_o; unfold eqb.
@@ -506,7 +499,7 @@ Qed.
Lemma map2_1bis : forall (m: t elt)(m': t elt') x
(f:option elt->option elt'->option elt''),
f None None = None ->
- find x (map2 f m m') = f (find x m) (find x m').
+ find x (map2 f m m') = f (find x m) (find x m').
Proof.
intros.
case_eq (find x m); intros.
@@ -525,23 +518,16 @@ rewrite (find_1 H4) in H0; discriminate.
rewrite (find_1 H4) in H1; discriminate.
Qed.
-Lemma elements_o : forall m x,
+Lemma elements_o : forall m x,
find x m = findA (eqb x) (elements m).
Proof.
-intros.
-assert (forall e, find x m = Some e <-> InA (eq_key_elt (elt:=elt)) (x,e) (elements m)).
- intros; rewrite <- find_mapsto_iff; apply elements_mapsto_iff.
-assert (H0:=elements_3w m).
-generalize (fun e => @findA_NoDupA _ _ _ E.eq_sym E.eq_trans eq_dec (elements m) x e H0).
-fold (eqb x).
-destruct (find x m); destruct (findA (eqb x) (elements m));
- simpl; auto; intros.
-symmetry; rewrite <- H1; rewrite <- H; auto.
-symmetry; rewrite <- H1; rewrite <- H; auto.
-rewrite H; rewrite H1; auto.
-Qed.
-
-Lemma elements_b : forall m x,
+intros. rewrite eq_option_alt. intro e.
+rewrite <- find_mapsto_iff, elements_mapsto_iff.
+unfold eqb.
+rewrite <- findA_NoDupA; intuition; try apply elements_3w; eauto.
+Qed.
+
+Lemma elements_b : forall m x,
mem x m = existsb (fun p => eqb x (fst p)) (elements m).
Proof.
intros.
@@ -568,30 +554,41 @@ Qed.
End BoolSpec.
-Section Equalities.
+Section Equalities.
Variable elt:Type.
+ (** Another characterisation of [Equal] *)
+
+Lemma Equal_mapsto_iff : forall m1 m2 : t elt,
+ Equal m1 m2 <-> (forall k e, MapsTo k e m1 <-> MapsTo k e m2).
+Proof.
+intros m1 m2. split; [intros Heq k e|intros Hiff].
+rewrite 2 find_mapsto_iff, Heq. split; auto.
+intro k. rewrite eq_option_alt. intro e.
+rewrite <- 2 find_mapsto_iff; auto.
+Qed.
+
(** * Relations between [Equal], [Equiv] and [Equivb]. *)
(** First, [Equal] is [Equiv] with Leibniz on elements. *)
-Lemma Equal_Equiv : forall (m m' : t elt),
+Lemma Equal_Equiv : forall (m m' : t elt),
Equal m m' <-> Equiv (@Logic.eq elt) m m'.
Proof.
- unfold Equal, Equiv; split; intros.
- split; intros.
- rewrite in_find_iff, in_find_iff, H; intuition.
- rewrite find_mapsto_iff in H0,H1; congruence.
- destruct H.
- specialize (H y).
- specialize (H0 y).
- do 2 rewrite in_find_iff in H.
- generalize (find_mapsto_iff m y)(find_mapsto_iff m' y).
- do 2 destruct find; auto; intros.
- f_equal; apply H0; [rewrite H1|rewrite H2]; auto.
- destruct H as [H _]; now elim H.
- destruct H as [_ H]; now elim H.
+intros. rewrite Equal_mapsto_iff. split; intros.
+split.
+split; intros (e,Hin); exists e; [rewrite <- H|rewrite H]; auto.
+intros; apply MapsTo_fun with m k; auto; rewrite H; auto.
+split; intros H'.
+destruct H.
+assert (Hin : In k m') by (rewrite <- H; exists e; auto).
+destruct Hin as (e',He').
+rewrite (H0 k e e'); auto.
+destruct H.
+assert (Hin : In k m) by (rewrite H; exists e; auto).
+destruct Hin as (e',He').
+rewrite <- (H0 k e' e); auto.
Qed.
(** [Equivb] and [Equiv] and equivalent when [eq_elt] and [cmp]
@@ -649,8 +646,8 @@ Lemma Equal_trans : forall (elt:Type)(m m' m'' : t elt),
Equal m m' -> Equal m' m'' -> Equal m m''.
Proof. unfold Equal; congruence. Qed.
-Definition Equal_ST : forall elt:Type, Setoid_Theory (t elt) (@Equal _).
-Proof.
+Definition Equal_ST : forall elt:Type, Equivalence (@Equal elt).
+Proof.
constructor; red; [apply Equal_refl | apply Equal_sym | apply Equal_trans].
Qed.
@@ -660,8 +657,6 @@ Add Relation key E.eq
transitivity proved by E.eq_trans
as KeySetoid.
-Typeclasses unfold key.
-
Implicit Arguments Equal [[elt]].
Add Parametric Relation (elt : Type) : (t elt) Equal
@@ -670,52 +665,52 @@ Add Parametric Relation (elt : Type) : (t elt) Equal
transitivity proved by (@Equal_trans elt)
as EqualSetoid.
-Add Parametric Morphism elt : (@In elt) with signature E.eq ==> Equal ==> iff as In_m.
+Add Parametric Morphism elt : (@In elt)
+ with signature E.eq ==> Equal ==> iff as In_m.
Proof.
unfold Equal; intros k k' Hk m m' Hm.
rewrite (In_iff m Hk), in_find_iff, in_find_iff, Hm; intuition.
Qed.
Add Parametric Morphism elt : (@MapsTo elt)
- with signature E.eq ==> @Logic.eq _ ==> Equal ==> iff as MapsTo_m.
+ with signature E.eq ==> Leibniz ==> Equal ==> iff as MapsTo_m.
Proof.
unfold Equal; intros k k' Hk e m m' Hm.
-rewrite (MapsTo_iff m e Hk), find_mapsto_iff, find_mapsto_iff, Hm;
+rewrite (MapsTo_iff m e Hk), find_mapsto_iff, find_mapsto_iff, Hm;
intuition.
Qed.
-Add Parametric Morphism elt : (@Empty elt) with signature Equal ==> iff as Empty_m.
+Add Parametric Morphism elt : (@Empty elt)
+ with signature Equal ==> iff as Empty_m.
Proof.
unfold Empty; intros m m' Hm; intuition.
rewrite <-Hm in H0; eauto.
rewrite Hm in H0; eauto.
Qed.
-Add Parametric Morphism elt : (@is_empty elt) with signature Equal ==> @Logic.eq _ as is_empty_m.
+Add Parametric Morphism elt : (@is_empty elt)
+ with signature Equal ==> Leibniz as is_empty_m.
Proof.
intros m m' Hm.
rewrite eq_bool_alt, <-is_empty_iff, <-is_empty_iff, Hm; intuition.
Qed.
-Add Parametric Morphism elt : (@mem elt) with signature E.eq ==> Equal ==> @Logic.eq _ as mem_m.
+Add Parametric Morphism elt : (@mem elt)
+ with signature E.eq ==> Equal ==> Leibniz as mem_m.
Proof.
intros k k' Hk m m' Hm.
rewrite eq_bool_alt, <- mem_in_iff, <-mem_in_iff, Hk, Hm; intuition.
Qed.
-Add Parametric Morphism elt : (@find elt) with signature E.eq ==> Equal ==> @Logic.eq _ as find_m.
+Add Parametric Morphism elt : (@find elt)
+ with signature E.eq ==> Equal ==> Leibniz as find_m.
Proof.
-intros k k' Hk m m' Hm.
-generalize (find_mapsto_iff m k)(find_mapsto_iff m' k')
- (not_find_in_iff m k)(not_find_in_iff m' k');
-do 2 destruct find; auto; intros.
-rewrite <- H, Hk, Hm, H0; auto.
-rewrite <- H1, Hk, Hm, H2; auto.
-symmetry; rewrite <- H2, <-Hk, <-Hm, H1; auto.
+intros k k' Hk m m' Hm. rewrite eq_option_alt. intro e.
+rewrite <- 2 find_mapsto_iff, Hk, Hm. split; auto.
Qed.
-Add Parametric Morphism elt : (@add elt) with signature
- E.eq ==> @Logic.eq _ ==> Equal ==> Equal as add_m.
+Add Parametric Morphism elt : (@add elt)
+ with signature E.eq ==> Leibniz ==> Equal ==> Equal as add_m.
Proof.
intros k k' Hk e m m' Hm y.
rewrite add_o, add_o; do 2 destruct eq_dec; auto.
@@ -723,8 +718,8 @@ elim n; rewrite <-Hk; auto.
elim n; rewrite Hk; auto.
Qed.
-Add Parametric Morphism elt : (@remove elt) with signature
- E.eq ==> Equal ==> Equal as remove_m.
+Add Parametric Morphism elt : (@remove elt)
+ with signature E.eq ==> Equal ==> Equal as remove_m.
Proof.
intros k k' Hk m m' Hm y.
rewrite remove_o, remove_o; do 2 destruct eq_dec; auto.
@@ -732,7 +727,8 @@ elim n; rewrite <-Hk; auto.
elim n; rewrite Hk; auto.
Qed.
-Add Parametric Morphism elt elt' : (@map elt elt') with signature @Logic.eq _ ==> Equal ==> Equal as map_m.
+Add Parametric Morphism elt elt' : (@map elt elt')
+ with signature Leibniz ==> Equal ==> Equal as map_m.
Proof.
intros f m m' Hm y.
rewrite map_o, map_o, Hm; auto.
@@ -743,25 +739,23 @@ Qed.
(* old name: *)
Notation not_find_mapsto_iff := not_find_in_iff.
-End WFacts.
+End WFacts_fun.
-(** * Same facts for full maps *)
+(** * Same facts for self-contained weak sets and for full maps *)
-Module Facts (M:S).
- Module D := OT_as_DT M.E.
- Include WFacts D M.
-End Facts.
+Module WFacts (M:S) := WFacts_fun M.E M.
+Module Facts := WFacts.
+
+(** * Additional Properties for weak maps
-(** * Additional Properties for weak maps
-
Results about [fold], [elements], induction principles...
*)
-Module WProperties (E:DecidableType)(M:WSfun E).
- Module Import F:=WFacts E M.
+Module WProperties_fun (E:DecidableType)(M:WSfun E).
+ Module Import F:=WFacts_fun E M.
Import M.
- Section Elt.
+ Section Elt.
Variable elt:Type.
Definition Add x (e:elt) m m' := forall y, find y m' = find y (add x e m).
@@ -769,6 +763,44 @@ Module WProperties (E:DecidableType)(M:WSfun E).
Notation eqke := (@eq_key_elt elt).
Notation eqk := (@eq_key elt).
+ (** Complements about InA, NoDupA and findA *)
+
+ Lemma InA_eqke_eqk : forall k1 k2 e1 e2 l,
+ E.eq k1 k2 -> InA eqke (k1,e1) l -> InA eqk (k2,e2) l.
+ Proof.
+ intros k1 k2 e1 e2 l Hk. rewrite 2 InA_alt.
+ intros ((k',e') & (Hk',He') & H); simpl in *.
+ exists (k',e'); split; auto.
+ red; simpl; eauto.
+ Qed.
+
+ Lemma NoDupA_eqk_eqke : forall l, NoDupA eqk l -> NoDupA eqke l.
+ Proof.
+ induction 1; auto.
+ constructor; auto.
+ destruct x as (k,e).
+ eauto using InA_eqke_eqk.
+ Qed.
+
+ Lemma findA_rev : forall l k, NoDupA eqk l ->
+ findA (eqb k) l = findA (eqb k) (rev l).
+ Proof.
+ intros.
+ case_eq (findA (eqb k) l).
+ intros. symmetry.
+ unfold eqb.
+ rewrite <- findA_NoDupA, InA_rev, findA_NoDupA
+ by eauto using NoDupA_rev; eauto.
+ case_eq (findA (eqb k) (rev l)); auto.
+ intros e.
+ unfold eqb.
+ rewrite <- findA_NoDupA, InA_rev, findA_NoDupA
+ by eauto using NoDupA_rev.
+ intro Eq; rewrite Eq; auto.
+ Qed.
+
+ (** * Elements *)
+
Lemma elements_Empty : forall m:t elt, Empty m <-> elements m = nil.
Proof.
intros.
@@ -793,29 +825,268 @@ Module WProperties (E:DecidableType)(M:WSfun E).
rewrite <-elements_Empty; apply empty_1.
Qed.
- Lemma fold_Empty : forall m (A:Type)(f:key->elt->A->A)(i:A),
- Empty m -> fold f m i = i.
+ (** * Conversions between maps and association lists. *)
+
+ Definition of_list (l : list (key*elt)) :=
+ List.fold_right (fun p => add (fst p) (snd p)) (empty _) l.
+
+ Definition to_list := elements.
+
+ Lemma of_list_1 : forall l k e,
+ NoDupA eqk l ->
+ (MapsTo k e (of_list l) <-> InA eqke (k,e) l).
+ Proof.
+ induction l as [|(k',e') l IH]; simpl; intros k e Hnodup.
+ rewrite empty_mapsto_iff, InA_nil; intuition.
+ inversion_clear Hnodup as [| ? ? Hnotin Hnodup'].
+ specialize (IH k e Hnodup'); clear Hnodup'.
+ rewrite add_mapsto_iff, InA_cons, <- IH.
+ unfold eq_key_elt at 1; simpl.
+ split; destruct 1 as [H|H]; try (intuition;fail).
+ destruct (eq_dec k k'); [left|right]; split; auto.
+ contradict Hnotin.
+ apply InA_eqke_eqk with k e; intuition.
+ Qed.
+
+ Lemma of_list_1b : forall l k,
+ NoDupA eqk l ->
+ find k (of_list l) = findA (eqb k) l.
+ Proof.
+ induction l as [|(k',e') l IH]; simpl; intros k Hnodup.
+ apply empty_o.
+ inversion_clear Hnodup as [| ? ? Hnotin Hnodup'].
+ specialize (IH k Hnodup'); clear Hnodup'.
+ rewrite add_o, IH.
+ unfold eqb; do 2 destruct eq_dec; auto; elim n; eauto.
+ Qed.
+
+ Lemma of_list_2 : forall l, NoDupA eqk l ->
+ equivlistA eqke l (to_list (of_list l)).
+ Proof.
+ intros l Hnodup (k,e).
+ rewrite <- elements_mapsto_iff, of_list_1; intuition.
+ Qed.
+
+ Lemma of_list_3 : forall s, Equal (of_list (to_list s)) s.
+ Proof.
+ intros s k.
+ rewrite of_list_1b, elements_o; auto.
+ apply elements_3w.
+ Qed.
+
+ (** * Fold *)
+
+ (** ** Induction principles about fold contributed by S. Lescuyer *)
+
+ (** In the following lemma, the step hypothesis is deliberately restricted
+ to the precise map m we are considering. *)
+
+ Lemma fold_rec :
+ forall (A:Type)(P : t elt -> A -> Type)(f : key -> elt -> A -> A),
+ forall (i:A)(m:t elt),
+ (forall m, Empty m -> P m i) ->
+ (forall k e a m' m'', MapsTo k e m -> ~In k m' ->
+ Add k e m' m'' -> P m' a -> P m'' (f k e a)) ->
+ P m (fold f m i).
+ Proof.
+ intros A P f i m Hempty Hstep.
+ rewrite fold_1, <- fold_left_rev_right.
+ set (F:=fun (y : key * elt) (x : A) => f (fst y) (snd y) x).
+ set (l:=rev (elements m)).
+ assert (Hstep' : forall k e a m' m'', InA eqke (k,e) l -> ~In k m' ->
+ Add k e m' m'' -> P m' a -> P m'' (F (k,e) a)).
+ intros k e a m' m'' H ? ? ?; eapply Hstep; eauto.
+ revert H; unfold l; rewrite InA_rev, elements_mapsto_iff; auto.
+ assert (Hdup : NoDupA eqk l).
+ unfold l. apply NoDupA_rev; try red; eauto. apply elements_3w.
+ assert (Hsame : forall k, find k m = findA (eqb k) l).
+ intros k. unfold l. rewrite elements_o, findA_rev; auto.
+ apply elements_3w.
+ clearbody l. clearbody F. clear Hstep f. revert m Hsame. induction l.
+ (* empty *)
+ intros m Hsame; simpl.
+ apply Hempty. intros k e.
+ rewrite find_mapsto_iff, Hsame; simpl; discriminate.
+ (* step *)
+ intros m Hsame; destruct a as (k,e); simpl.
+ apply Hstep' with (of_list l); auto.
+ rewrite InA_cons; left; red; auto.
+ inversion_clear Hdup. contradict H. destruct H as (e',He').
+ apply InA_eqke_eqk with k e'; auto.
+ rewrite <- of_list_1; auto.
+ intro k'. rewrite Hsame, add_o, of_list_1b. simpl.
+ unfold eqb. do 2 destruct eq_dec; auto; elim n; eauto.
+ inversion_clear Hdup; auto.
+ apply IHl.
+ intros; eapply Hstep'; eauto.
+ inversion_clear Hdup; auto.
+ intros; apply of_list_1b. inversion_clear Hdup; auto.
+ Qed.
+
+ (** Same, with [empty] and [add] instead of [Empty] and [Add]. In this
+ case, [P] must be compatible with equality of sets *)
+
+ Theorem fold_rec_bis :
+ forall (A:Type)(P : t elt -> A -> Type)(f : key -> elt -> A -> A),
+ forall (i:A)(m:t elt),
+ (forall m m' a, Equal m m' -> P m a -> P m' a) ->
+ (P (empty _) i) ->
+ (forall k e a m', MapsTo k e m -> ~In k m' ->
+ P m' a -> P (add k e m') (f k e a)) ->
+ P m (fold f m i).
+ Proof.
+ intros A P f i m Pmorphism Pempty Pstep.
+ apply fold_rec; intros.
+ apply Pmorphism with (empty _); auto. intro k. rewrite empty_o.
+ case_eq (find k m0); auto; intros e'; rewrite <- find_mapsto_iff.
+ intro H'; elim (H k e'); auto.
+ apply Pmorphism with (add k e m'); try intro; auto.
+ Qed.
+
+ Lemma fold_rec_nodep :
+ forall (A:Type)(P : A -> Type)(f : key -> elt -> A -> A)(i:A)(m:t elt),
+ P i -> (forall k e a, MapsTo k e m -> P a -> P (f k e a)) ->
+ P (fold f m i).
+ Proof.
+ intros; apply fold_rec_bis with (P:=fun _ => P); auto.
+ Qed.
+
+ (** [fold_rec_weak] is a weaker principle than [fold_rec_bis] :
+ the step hypothesis must here be applicable anywhere.
+ At the same time, it looks more like an induction principle,
+ and hence can be easier to use. *)
+
+ Lemma fold_rec_weak :
+ forall (A:Type)(P : t elt -> A -> Type)(f : key -> elt -> A -> A)(i:A),
+ (forall m m' a, Equal m m' -> P m a -> P m' a) ->
+ P (empty _) i ->
+ (forall k e a m, ~In k m -> P m a -> P (add k e m) (f k e a)) ->
+ forall m, P m (fold f m i).
+ Proof.
+ intros; apply fold_rec_bis; auto.
+ Qed.
+
+ Lemma fold_rel :
+ forall (A B:Type)(R : A -> B -> Type)
+ (f : key -> elt -> A -> A)(g : key -> elt -> B -> B)(i : A)(j : B)
+ (m : t elt),
+ R i j ->
+ (forall k e a b, MapsTo k e m -> R a b -> R (f k e a) (g k e b)) ->
+ R (fold f m i) (fold g m j).
+ Proof.
+ intros A B R f g i j m Rempty Rstep.
+ do 2 rewrite fold_1, <- fold_left_rev_right.
+ set (l:=rev (elements m)).
+ assert (Rstep' : forall k e a b, InA eqke (k,e) l ->
+ R a b -> R (f k e a) (g k e b)) by
+ (intros; apply Rstep; auto; rewrite elements_mapsto_iff, <- InA_rev; auto).
+ clearbody l; clear Rstep m.
+ induction l; simpl; auto.
+ apply Rstep'; auto.
+ destruct a; simpl; rewrite InA_cons; left; red; auto.
+ Qed.
+
+ (** From the induction principle on [fold], we can deduce some general
+ induction principles on maps. *)
+
+ Lemma map_induction :
+ forall P : t elt -> Type,
+ (forall m, Empty m -> P m) ->
+ (forall m m', P m -> forall x e, ~In x m -> Add x e m m' -> P m') ->
+ forall m, P m.
+ Proof.
+ intros. apply (@fold_rec _ (fun s _ => P s) (fun _ _ _ => tt) tt m); eauto.
+ Qed.
+
+ Lemma map_induction_bis :
+ forall P : t elt -> Type,
+ (forall m m', Equal m m' -> P m -> P m') ->
+ P (empty _) ->
+ (forall x e m, ~In x m -> P m -> P (add x e m)) ->
+ forall m, P m.
Proof.
intros.
- rewrite fold_1.
- rewrite elements_Empty in H; rewrite H; simpl; auto.
+ apply (@fold_rec_bis _ (fun s _ => P s) (fun _ _ _ => tt) tt m); eauto.
Qed.
- Lemma NoDupA_eqk_eqke : forall l, NoDupA eqk l -> NoDupA eqke l.
+ (** [fold] can be used to reconstruct the same initial set. *)
+
+ Lemma fold_identity : forall m : t elt, Equal (fold (@add _) m (empty _)) m.
Proof.
- induction 1; auto.
- constructor; auto.
- contradict H.
- destruct x as (x,y).
- rewrite InA_alt in *; destruct H as ((a,b),((H1,H2),H3)); simpl in *.
- exists (a,b); auto.
+ intros.
+ apply fold_rec with (P:=fun m acc => Equal acc m); auto with map.
+ intros m' Heq k'.
+ rewrite empty_o.
+ case_eq (find k' m'); auto; intros e'; rewrite <- find_mapsto_iff.
+ intro; elim (Heq k' e'); auto.
+ intros k e a m' m'' _ _ Hadd Heq k'.
+ rewrite Hadd, 2 add_o, Heq; auto.
+ Qed.
+
+ Section Fold_More.
+
+ (** ** Additional properties of fold *)
+
+ (** When a function [f] is compatible and allows transpositions, we can
+ compute [fold f] in any order. *)
+
+ Variables (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA)(f:key->elt->A->A).
+
+ (** This is more convenient than a [compat_op eqke ...].
+ In fact, every [compat_op], [compat_bool], etc, should
+ become a [Morphism] someday. *)
+ Hypothesis Comp : Morphism (E.eq==>Leibniz==>eqA==>eqA) f.
+
+ Lemma fold_init :
+ forall m i i', eqA i i' -> eqA (fold f m i) (fold f m i').
+ Proof.
+ intros. apply fold_rel with (R:=eqA); auto.
+ intros. apply Comp; auto.
+ Qed.
+
+ Lemma fold_Empty :
+ forall m i, Empty m -> eqA (fold f m i) i.
+ Proof.
+ intros. apply fold_rec_nodep with (P:=fun a => eqA a i).
+ reflexivity.
+ intros. elim (H k e); auto.
Qed.
- Lemma fold_Equal : forall m1 m2 (A:Type)(eqA:A->A->Prop)(st:Setoid_Theory A eqA)
- (f:key->elt->A->A)(i:A),
- compat_op eqke eqA (fun y =>f (fst y) (snd y)) ->
- transpose eqA (fun y => f (fst y) (snd y)) ->
- Equal m1 m2 ->
+ (** As noticed by P. Casteran, asking for the general [SetoidList.transpose]
+ here is too restrictive. Think for instance of [f] being [M.add] :
+ in general, [M.add k e (M.add k e' m)] is not equivalent to
+ [M.add k e' (M.add k e m)]. Fortunately, we will never encounter this
+ situation during a real [fold], since the keys received by this [fold]
+ are unique. Hence we can ask the transposition property to hold only
+ for non-equal keys.
+
+ This idea could be push slightly further, by asking the transposition
+ property to hold only for (non-equal) keys living in the map given to
+ [fold]. Please contact us if you need such a version.
+
+ FSets could also benefit from a restricted [transpose], but for this
+ case the gain is unclear. *)
+
+ Definition transpose_neqkey :=
+ forall k k' e e' a, ~E.eq k k' ->
+ eqA (f k e (f k' e' a)) (f k' e' (f k e a)).
+
+ Hypothesis Tra : transpose_neqkey.
+
+ Lemma fold_commutes : forall i m k e, ~In k m ->
+ eqA (fold f m (f k e i)) (f k e (fold f m i)).
+ Proof.
+ intros i m k e Hnotin.
+ apply fold_rel with (R:= fun a b => eqA a (f k e b)); auto.
+ reflexivity.
+ intros.
+ transitivity (f k0 e0 (f k e b)).
+ apply Comp; auto.
+ apply Tra; auto.
+ contradict Hnotin; rewrite <- Hnotin; exists e0; auto.
+ Qed.
+
+ Lemma fold_Equal : forall m1 m2 i, Equal m1 m2 ->
eqA (fold f m1 i) (fold f m2 i).
Proof.
assert (eqke_refl : forall p, eqke p p).
@@ -826,22 +1097,26 @@ Module WProperties (E:DecidableType)(M:WSfun E).
intros (x1,x2) (y1,y2) (z1,z2); unfold eq_key_elt; simpl.
intuition; eauto; congruence.
intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right.
- apply fold_right_equivlistA with (eqA:=eqke) (eqB:=eqA); auto.
+ apply fold_right_equivlistA_restr with
+ (R:=fun p p' => ~eqk p p') (eqA:=eqke) (eqB:=eqA); auto.
+ intros (k1,e1) (k2,e2) a1 a2 (Hk,He) Ha; simpl in *; apply Comp; auto.
+ unfold eq_key; auto.
+ intros (k1,e1) (k2,e2) (k3,e3). unfold eq_key_elt, eq_key; simpl.
+ intuition eauto.
+ intros (k,e) (k',e'); unfold eq_key; simpl; auto.
apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
+ apply ForallList2_equiv1 with (eqA:=eqk); try red; eauto.
+ apply NoDupA_rev; try red; eauto. apply elements_3w.
red; intros.
do 2 rewrite InA_rev.
destruct x; do 2 rewrite <- elements_mapsto_iff.
do 2 rewrite find_mapsto_iff.
- rewrite H1; split; auto.
+ rewrite H; split; auto.
Qed.
- Lemma fold_Add : forall m1 m2 x e (A:Type)(eqA:A->A->Prop)(st:Setoid_Theory A eqA)
- (f:key->elt->A->A)(i:A),
- compat_op eqke eqA (fun y =>f (fst y) (snd y)) ->
- transpose eqA (fun y =>f (fst y) (snd y)) ->
- ~In x m1 -> Add x e m1 m2 ->
- eqA (fold f m2 i) (f x e (fold f m1 i)).
+ Lemma fold_Add : forall m1 m2 k e i, ~In k m1 -> Add k e m1 m2 ->
+ eqA (fold f m2 i) (f k e (fold f m1 i)).
Proof.
assert (eqke_refl : forall p, eqke p p).
red; auto.
@@ -852,52 +1127,68 @@ Module WProperties (E:DecidableType)(M:WSfun E).
intuition; eauto; congruence.
intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right.
set (f':=fun y x0 => f (fst y) (snd y) x0) in *.
- change (f x e (fold_right f' i (rev (elements m1))))
- with (f' (x,e) (fold_right f' i (rev (elements m1)))).
- apply fold_right_add with (eqA:=eqke)(eqB:=eqA); auto.
+ change (f k e (fold_right f' i (rev (elements m1))))
+ with (f' (k,e) (fold_right f' i (rev (elements m1)))).
+ apply fold_right_add_restr with
+ (R:=fun p p'=>~eqk p p')(eqA:=eqke)(eqB:=eqA); auto.
+ intros (k1,e1) (k2,e2) a1 a2 (Hk,He) Ha; unfold f'; simpl in *. apply Comp; auto.
+
+ unfold eq_key; auto.
+ intros (k1,e1) (k2,e2) (k3,e3). unfold eq_key_elt, eq_key; simpl.
+ intuition eauto.
+ unfold f'; intros (k1,e1) (k2,e2); unfold eq_key; simpl; auto.
apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
+ apply ForallList2_equiv1 with (eqA:=eqk); try red; eauto.
+ apply NoDupA_rev; try red; eauto. apply elements_3w.
rewrite InA_rev.
- contradict H1.
+ contradict H.
exists e.
rewrite elements_mapsto_iff; auto.
intros a.
- rewrite InA_cons; do 2 rewrite InA_rev;
+ rewrite InA_cons; do 2 rewrite InA_rev;
destruct a as (a,b); do 2 rewrite <- elements_mapsto_iff.
do 2 rewrite find_mapsto_iff; unfold eq_key_elt; simpl.
- rewrite H2.
+ rewrite H0.
rewrite add_o.
- destruct (eq_dec x a); intuition.
- inversion H3; auto.
+ destruct (eq_dec k a); intuition.
+ inversion H1; auto.
f_equal; auto.
- elim H1.
+ elim H.
exists b; apply MapsTo_1 with a; auto with map.
elim n; auto.
Qed.
- Lemma cardinal_fold : forall m : t elt,
+ Lemma fold_add : forall m k e i, ~In k m ->
+ eqA (fold f (add k e m) i) (f k e (fold f m i)).
+ Proof.
+ intros. apply fold_Add; try red; auto.
+ Qed.
+
+ End Fold_More.
+
+ (** * Cardinal *)
+
+ Lemma cardinal_fold : forall m : t elt,
cardinal m = fold (fun _ _ => S) m 0.
Proof.
intros; rewrite cardinal_1, fold_1.
symmetry; apply fold_left_length; auto.
Qed.
- Lemma cardinal_Empty : forall m : t elt,
+ Lemma cardinal_Empty : forall m : t elt,
Empty m <-> cardinal m = 0.
Proof.
intros.
rewrite cardinal_1, elements_Empty.
destruct (elements m); intuition; discriminate.
Qed.
-
- Lemma Equal_cardinal : forall m m' : t elt,
+
+ Lemma Equal_cardinal : forall m m' : t elt,
Equal m m' -> cardinal m = cardinal m'.
Proof.
intros; do 2 rewrite cardinal_fold.
- apply fold_Equal with (eqA:=@eq _); auto.
- constructor; auto; congruence.
- red; auto.
- red; auto.
+ apply fold_Equal with (eqA:=Leibniz); compute; auto.
Qed.
Lemma cardinal_1 : forall m : t elt, Empty m -> cardinal m = 0.
@@ -910,10 +1201,7 @@ Module WProperties (E:DecidableType)(M:WSfun E).
Proof.
intros; do 2 rewrite cardinal_fold.
change S with ((fun _ _ => S) x e).
- apply fold_Add; auto.
- constructor; intros; auto; congruence.
- red; simpl; auto.
- red; simpl; auto.
+ apply fold_Add with (eqA:=Leibniz); compute; auto.
Qed.
Lemma cardinal_inv_1 : forall m : t elt,
@@ -943,27 +1231,16 @@ Module WProperties (E:DecidableType)(M:WSfun E).
eauto.
Qed.
- Lemma map_induction :
- forall P : t elt -> Type,
- (forall m, Empty m -> P m) ->
- (forall m m', P m -> forall x e, ~In x m -> Add x e m m' -> P m') ->
- forall m, P m.
- Proof.
- intros; remember (cardinal m) as n; revert m Heqn; induction n; intros.
- apply X; apply cardinal_inv_1; auto.
+ (** * Additional notions over maps *)
- destruct (cardinal_inv_2 (sym_eq Heqn)) as ((x,e),H0); simpl in *.
- assert (Add x e (remove x m) m).
- red; intros.
- rewrite add_o; rewrite remove_o; destruct (eq_dec x y); eauto with map.
- apply X0 with (remove x m) x e; auto with map.
- apply IHn; auto with map.
- assert (S n = S (cardinal (remove x m))).
- rewrite Heqn; eapply cardinal_2; eauto with map.
- inversion H1; auto with map.
- Qed.
+ Definition Disjoint (m m' : t elt) :=
+ forall k, ~(In k m /\ In k m').
+
+ Definition Partition (m m1 m2 : t elt) :=
+ Disjoint m1 m2 /\
+ (forall k e, MapsTo k e m <-> MapsTo k e m1 \/ MapsTo k e m2).
- (** * Let's emulate some functions not present in the interface *)
+ (** * Emulation of some functions lacking in the interface *)
Definition filter (f : key -> elt -> bool)(m : t elt) :=
fold (fun k e m => if f k e then add k e m else m) m (empty _).
@@ -977,122 +1254,411 @@ Module WProperties (E:DecidableType)(M:WSfun E).
Definition partition (f : key -> elt -> bool)(m : t elt) :=
(filter f m, filter (fun k e => negb (f k e)) m).
+ (** [update] adds to [m1] all the bindings of [m2]. It can be seen as
+ an [union] operator which gives priority to its 2nd argument
+ in case of binding conflit. *)
+
+ Definition update (m1 m2 : t elt) := fold (@add _) m2 m1.
+
+ (** [restrict] keeps from [m1] only the bindings whose key is in [m2].
+ It can be seen as an [inter] operator, with priority to its 1st argument
+ in case of binding conflit. *)
+
+ Definition restrict (m1 m2 : t elt) := filter (fun k _ => mem k m2) m1.
+
+ (** [diff] erases from [m1] all bindings whose key is in [m2]. *)
+
+ Definition diff (m1 m2 : t elt) := filter (fun k _ => negb (mem k m2)) m1.
+
Section Specs.
Variable f : key -> elt -> bool.
- Hypothesis Hf : forall e, compat_bool E.eq (fun k => f k e).
+ Hypothesis Hf : Morphism (E.eq==>Leibniz==>Leibniz) f.
- Lemma filter_iff : forall m k e,
+ Lemma filter_iff : forall m k e,
MapsTo k e (filter f m) <-> MapsTo k e m /\ f k e = true.
Proof.
- unfold filter; intros.
- rewrite fold_1.
- rewrite <- fold_left_rev_right.
- rewrite (elements_mapsto_iff m).
- rewrite <- (InA_rev eqke (k,e) (elements m)).
- assert (NoDupA eqk (rev (elements m))).
- apply NoDupA_rev; auto; try apply elements_3w; auto.
- intros (k1,e1); compute; auto.
- intros (k1,e1)(k2,e2); compute; auto.
- intros (k1,e1)(k2,e2)(k3,e3); compute; eauto.
- induction (rev (elements m)); simpl; auto.
-
- rewrite empty_mapsto_iff.
- intuition.
- inversion H1.
-
- destruct a as (k',e'); simpl.
- inversion_clear H.
- case_eq (f k' e'); intros; simpl;
- try rewrite add_mapsto_iff; rewrite IHl; clear IHl; intuition.
- constructor; red; auto.
- rewrite (Hf e' H2),H4 in H; auto.
- inversion_clear H3.
- compute in H2; destruct H2; auto.
- destruct (E.eq_dec k' k); auto.
- elim H0.
- rewrite InA_alt in *; destruct H2 as (w,Hw); exists w; intuition.
- red in H2; red; simpl in *; intuition.
- rewrite e0; auto.
- inversion_clear H3; auto.
- compute in H2; destruct H2.
- rewrite (Hf e H2),H3,H in H4; discriminate.
+ unfold filter.
+ set (f':=fun k e m => if f k e then add k e m else m).
+ intro m. pattern m, (fold f' m (empty _)). apply fold_rec.
+
+ intros m' Hm' k e. rewrite empty_mapsto_iff. intuition.
+ elim (Hm' k e); auto.
+
+ intros k e acc m1 m2 Hke Hn Hadd IH k' e'.
+ change (Equal m2 (add k e m1)) in Hadd; rewrite Hadd.
+ unfold f'; simpl.
+ case_eq (f k e); intros Hfke; simpl;
+ rewrite !add_mapsto_iff, IH; clear IH; intuition.
+ rewrite <- Hfke; apply Hf; auto.
+ destruct (eq_dec k k') as [Hk|Hk]; [left|right]; auto.
+ elim Hn; exists e'; rewrite Hk; auto.
+ assert (f k e = f k' e') by (apply Hf; auto). congruence.
Qed.
-
+
Lemma for_all_iff : forall m,
for_all f m = true <-> (forall k e, MapsTo k e m -> f k e = true).
Proof.
- cut (forall m : t elt,
- for_all f m = true <->
- (forall k e, InA eqke (k,e) (rev (elements m)) -> f k e = true)).
- intros; rewrite H; split; intros.
- apply H0; rewrite InA_rev, <- elements_mapsto_iff; auto.
- apply H0; rewrite InA_rev, <- elements_mapsto_iff in H1; auto.
-
- unfold for_all; intros.
- rewrite fold_1.
- rewrite <- fold_left_rev_right.
- assert (NoDupA eqk (rev (elements m))).
- apply NoDupA_rev; auto; try apply elements_3w; auto.
- intros (k1,e1); compute; auto.
- intros (k1,e1)(k2,e2); compute; auto.
- intros (k1,e1)(k2,e2)(k3,e3); compute; eauto.
- induction (rev (elements m)); simpl; auto.
-
- intuition.
- inversion H1.
-
- destruct a as (k,e); simpl.
- inversion_clear H.
- case_eq (f k e); intros; simpl;
- try rewrite IHl; clear IHl; intuition.
- inversion_clear H3; auto.
- compute in H4; destruct H4.
- rewrite (Hf e0 H3), H4; auto.
- rewrite <-H, <-(H2 k e); auto.
- constructor; red; auto.
+ unfold for_all.
+ set (f':=fun k e b => if f k e then b else false).
+ intro m. pattern m, (fold f' m true). apply fold_rec.
+
+ intros m' Hm'. split; auto. intros _ k e Hke. elim (Hm' k e); auto.
+
+ intros k e b m1 m2 _ Hn Hadd IH. clear m.
+ change (Equal m2 (add k e m1)) in Hadd.
+ unfold f'; simpl. case_eq (f k e); intros Hfke.
+ (* f k e = true *)
+ rewrite IH. clear IH. split; intros Hmapsto k' e' Hke'.
+ rewrite Hadd, add_mapsto_iff in Hke'.
+ destruct Hke' as [(?,?)|(?,?)]; auto.
+ rewrite <- Hfke; apply Hf; auto.
+ apply Hmapsto. rewrite Hadd, add_mapsto_iff; right; split; auto.
+ contradict Hn; exists e'; rewrite Hn; auto.
+ (* f k e = false *)
+ split; intros H; try discriminate.
+ rewrite <- Hfke. apply H.
+ rewrite Hadd, add_mapsto_iff; auto.
Qed.
-
+
Lemma exists_iff : forall m,
- exists_ f m = true <->
+ exists_ f m = true <->
(exists p, MapsTo (fst p) (snd p) m /\ f (fst p) (snd p) = true).
Proof.
- cut (forall m : t elt,
- exists_ f m = true <->
- (exists p, InA eqke p (rev (elements m))
- /\ f (fst p) (snd p) = true)).
- intros; rewrite H; split; intros.
- destruct H0 as ((k,e),Hke); exists (k,e).
- rewrite InA_rev, <-elements_mapsto_iff in Hke; auto.
- destruct H0 as ((k,e),Hke); exists (k,e).
- rewrite InA_rev, <-elements_mapsto_iff; auto.
- unfold exists_; intros.
- rewrite fold_1.
- rewrite <- fold_left_rev_right.
- assert (NoDupA eqk (rev (elements m))).
- apply NoDupA_rev; auto; try apply elements_3w; auto.
- intros (k1,e1); compute; auto.
- intros (k1,e1)(k2,e2); compute; auto.
- intros (k1,e1)(k2,e2)(k3,e3); compute; eauto.
- induction (rev (elements m)); simpl; auto.
-
- intuition; try discriminate.
- destruct H0 as ((k,e),(Hke,_)); inversion Hke.
-
- destruct a as (k,e); simpl.
- inversion_clear H.
- case_eq (f k e); intros; simpl;
- try rewrite IHl; clear IHl; intuition.
+ unfold exists_.
+ set (f':=fun k e b => if f k e then true else b).
+ intro m. pattern m, (fold f' m false). apply fold_rec.
+
+ intros m' Hm'. split; try (intros; discriminate).
+ intros ((k,e),(Hke,_)); simpl in *. elim (Hm' k e); auto.
+
+ intros k e b m1 m2 _ Hn Hadd IH. clear m.
+ change (Equal m2 (add k e m1)) in Hadd.
+ unfold f'; simpl. case_eq (f k e); intros Hfke.
+ (* f k e = true *)
+ split; [intros _|auto].
exists (k,e); simpl; split; auto.
- constructor; red; auto.
- destruct H2 as ((k',e'),(Hke',Hf')); exists (k',e'); simpl; auto.
- destruct H2 as ((k',e'),(Hke',Hf')); simpl in *.
- inversion_clear Hke'.
- compute in H2; destruct H2.
- rewrite (Hf e' H2), H3,H in Hf'; discriminate.
+ rewrite Hadd, add_mapsto_iff; auto.
+ (* f k e = false *)
+ rewrite IH. clear IH. split; intros ((k',e'),(Hke1,Hke2)); simpl in *.
+ exists (k',e'); simpl; split; auto.
+ rewrite Hadd, add_mapsto_iff; right; split; auto.
+ contradict Hn. exists e'; rewrite Hn; auto.
+ rewrite Hadd, add_mapsto_iff in Hke1. destruct Hke1 as [(?,?)|(?,?)].
+ assert (f k' e' = f k e) by (apply Hf; auto). congruence.
exists (k',e'); auto.
Qed.
+
End Specs.
+ Lemma Disjoint_alt : forall m m',
+ Disjoint m m' <->
+ (forall k e e', MapsTo k e m -> MapsTo k e' m' -> False).
+ Proof.
+ unfold Disjoint; split.
+ intros H k v v' H1 H2.
+ apply H with k; split.
+ exists v; trivial.
+ exists v'; trivial.
+ intros H k ((v,Hv),(v',Hv')).
+ eapply H; eauto.
+ Qed.
+
+ Section Partition.
+ Variable f : key -> elt -> bool.
+ Hypothesis Hf : Morphism (E.eq==>Leibniz==>Leibniz) f.
+
+ Lemma partition_iff_1 : forall m m1 k e,
+ m1 = fst (partition f m) ->
+ (MapsTo k e m1 <-> MapsTo k e m /\ f k e = true).
+ Proof.
+ unfold partition; simpl; intros. subst m1.
+ apply filter_iff; auto.
+ Qed.
+
+ Lemma partition_iff_2 : forall m m2 k e,
+ m2 = snd (partition f m) ->
+ (MapsTo k e m2 <-> MapsTo k e m /\ f k e = false).
+ Proof.
+ unfold partition; simpl; intros. subst m2.
+ rewrite filter_iff.
+ split; intros (H,H'); split; auto.
+ destruct (f k e); simpl in *; auto.
+ rewrite H'; auto.
+ repeat red; intros. f_equal. apply Hf; auto.
+ Qed.
+
+ Lemma partition_Partition : forall m m1 m2,
+ partition f m = (m1,m2) -> Partition m m1 m2.
+ Proof.
+ intros. split.
+ rewrite Disjoint_alt. intros k e e'.
+ rewrite (@partition_iff_1 m m1), (@partition_iff_2 m m2)
+ by (rewrite H; auto).
+ intros (U,V) (W,Z). rewrite <- (MapsTo_fun U W) in Z; congruence.
+ intros k e.
+ rewrite (@partition_iff_1 m m1), (@partition_iff_2 m m2)
+ by (rewrite H; auto).
+ destruct (f k e); intuition.
+ Qed.
+
+ End Partition.
+
+ Lemma Partition_In : forall m m1 m2 k,
+ Partition m m1 m2 -> In k m -> {In k m1}+{In k m2}.
+ Proof.
+ intros m m1 m2 k Hm Hk.
+ destruct (In_dec m1 k) as [H|H]; [left|right]; auto.
+ destruct Hm as (Hm,Hm').
+ destruct Hk as (e,He); rewrite Hm' in He; destruct He.
+ elim H; exists e; auto.
+ exists e; auto.
+ Defined.
+
+ Lemma Disjoint_sym : forall m1 m2, Disjoint m1 m2 -> Disjoint m2 m1.
+ Proof.
+ intros m1 m2 H k (H1,H2). elim (H k); auto.
+ Qed.
+
+ Lemma Partition_sym : forall m m1 m2,
+ Partition m m1 m2 -> Partition m m2 m1.
+ Proof.
+ intros m m1 m2 (H,H'); split.
+ apply Disjoint_sym; auto.
+ intros; rewrite H'; intuition.
+ Qed.
+
+ Lemma Partition_Empty : forall m m1 m2, Partition m m1 m2 ->
+ (Empty m <-> (Empty m1 /\ Empty m2)).
+ Proof.
+ intros m m1 m2 (Hdisj,Heq). split.
+ intro He.
+ split; intros k e Hke; elim (He k e); rewrite Heq; auto.
+ intros (He1,He2) k e Hke. rewrite Heq in Hke. destruct Hke.
+ elim (He1 k e); auto.
+ elim (He2 k e); auto.
+ Qed.
+
+ Lemma Partition_Add :
+ forall m m' x e , ~In x m -> Add x e m m' ->
+ forall m1 m2, Partition m' m1 m2 ->
+ exists m3, (Add x e m3 m1 /\ Partition m m3 m2 \/
+ Add x e m3 m2 /\ Partition m m1 m3).
+ Proof.
+ unfold Partition. intros m m' x e Hn Hadd m1 m2 (Hdisj,Hor).
+ assert (Heq : Equal m (remove x m')).
+ change (Equal m' (add x e m)) in Hadd. rewrite Hadd.
+ intro k. rewrite remove_o, add_o.
+ destruct eq_dec as [He|Hne]; auto.
+ rewrite <- He, <- not_find_in_iff; auto.
+ assert (H : MapsTo x e m').
+ change (Equal m' (add x e m)) in Hadd; rewrite Hadd.
+ apply add_1; auto.
+ rewrite Hor in H; destruct H.
+
+ (* first case : x in m1 *)
+ exists (remove x m1); left. split; [|split].
+ (* add *)
+ change (Equal m1 (add x e (remove x m1))).
+ intro k.
+ rewrite add_o, remove_o.
+ destruct eq_dec as [He|Hne]; auto.
+ rewrite <- He; apply find_1; auto.
+ (* disjoint *)
+ intros k (H1,H2). elim (Hdisj k). split; auto.
+ rewrite remove_in_iff in H1; destruct H1; auto.
+ (* mapsto *)
+ intros k' e'.
+ rewrite Heq, 2 remove_mapsto_iff, Hor.
+ intuition.
+ elim (Hdisj x); split; [exists e|exists e']; auto.
+ apply MapsTo_1 with k'; auto.
+
+ (* second case : x in m2 *)
+ exists (remove x m2); right. split; [|split].
+ (* add *)
+ change (Equal m2 (add x e (remove x m2))).
+ intro k.
+ rewrite add_o, remove_o.
+ destruct eq_dec as [He|Hne]; auto.
+ rewrite <- He; apply find_1; auto.
+ (* disjoint *)
+ intros k (H1,H2). elim (Hdisj k). split; auto.
+ rewrite remove_in_iff in H2; destruct H2; auto.
+ (* mapsto *)
+ intros k' e'.
+ rewrite Heq, 2 remove_mapsto_iff, Hor.
+ intuition.
+ elim (Hdisj x); split; [exists e'|exists e]; auto.
+ apply MapsTo_1 with k'; auto.
+ Qed.
+
+ Lemma Partition_fold :
+ forall (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA)(f:key->elt->A->A),
+ Morphism (E.eq==>Leibniz==>eqA==>eqA) f ->
+ transpose_neqkey eqA f ->
+ forall m m1 m2 i,
+ Partition m m1 m2 ->
+ eqA (fold f m i) (fold f m1 (fold f m2 i)).
+ Proof.
+ intros A eqA st f Comp Tra.
+ induction m as [m Hm|m m' IH k e Hn Hadd] using map_induction.
+
+ intros m1 m2 i Hp. rewrite (fold_Empty (eqA:=eqA)); auto.
+ rewrite (Partition_Empty Hp) in Hm. destruct Hm.
+ rewrite 2 (fold_Empty (eqA:=eqA)); auto. reflexivity.
+
+ intros m1 m2 i Hp.
+ destruct (Partition_Add Hn Hadd Hp) as (m3,[(Hadd',Hp')|(Hadd',Hp')]).
+ (* fst case: m3 is (k,e)::m1 *)
+ assert (~In k m3).
+ contradict Hn. destruct Hn as (e',He').
+ destruct Hp' as (Hp1,Hp2). exists e'. rewrite Hp2; auto.
+ transitivity (f k e (fold f m i)).
+ apply fold_Add with (eqA:=eqA); auto.
+ symmetry.
+ transitivity (f k e (fold f m3 (fold f m2 i))).
+ apply fold_Add with (eqA:=eqA); auto.
+ apply Comp; auto.
+ symmetry; apply IH; auto.
+ (* snd case: m3 is (k,e)::m2 *)
+ assert (~In k m3).
+ contradict Hn. destruct Hn as (e',He').
+ destruct Hp' as (Hp1,Hp2). exists e'. rewrite Hp2; auto.
+ assert (~In k m1).
+ contradict Hn. destruct Hn as (e',He').
+ destruct Hp' as (Hp1,Hp2). exists e'. rewrite Hp2; auto.
+ transitivity (f k e (fold f m i)).
+ apply fold_Add with (eqA:=eqA); auto.
+ transitivity (f k e (fold f m1 (fold f m3 i))).
+ apply Comp; auto using IH.
+ transitivity (fold f m1 (f k e (fold f m3 i))).
+ symmetry.
+ apply fold_commutes with (eqA:=eqA); auto.
+ apply fold_init with (eqA:=eqA); auto.
+ symmetry.
+ apply fold_Add with (eqA:=eqA); auto.
+ Qed.
+
+ Lemma Partition_cardinal : forall m m1 m2, Partition m m1 m2 ->
+ cardinal m = cardinal m1 + cardinal m2.
+ Proof.
+ intros.
+ rewrite (cardinal_fold m), (cardinal_fold m1).
+ set (f:=fun (_:key)(_:elt)=>S).
+ setoid_replace (fold f m 0) with (fold f m1 (fold f m2 0)).
+ rewrite <- cardinal_fold.
+ intros. apply fold_rel with (R:=fun u v => u = v + cardinal m2); simpl; auto.
+ apply Partition_fold with (eqA:=@Logic.eq _); try red; auto.
+ compute; auto.
+ Qed.
+
+ Lemma Partition_partition : forall m m1 m2, Partition m m1 m2 ->
+ let f := fun k (_:elt) => mem k m1 in
+ Equal m1 (fst (partition f m)) /\ Equal m2 (snd (partition f m)).
+ Proof.
+ intros m m1 m2 Hm f.
+ assert (Hf : Morphism (E.eq==>Leibniz==>Leibniz) f).
+ intros k k' Hk e e' _; unfold f; rewrite Hk; auto.
+ set (m1':= fst (partition f m)).
+ set (m2':= snd (partition f m)).
+ split; rewrite Equal_mapsto_iff; intros k e.
+ rewrite (@partition_iff_1 f Hf m m1') by auto.
+ unfold f.
+ rewrite <- mem_in_iff.
+ destruct Hm as (Hm,Hm').
+ rewrite Hm'.
+ intuition.
+ exists e; auto.
+ elim (Hm k); split; auto; exists e; auto.
+ rewrite (@partition_iff_2 f Hf m m2') by auto.
+ unfold f.
+ rewrite <- not_mem_in_iff.
+ destruct Hm as (Hm,Hm').
+ rewrite Hm'.
+ intuition.
+ elim (Hm k); split; auto; exists e; auto.
+ elim H1; exists e; auto.
+ Qed.
+
+ Lemma update_mapsto_iff : forall m m' k e,
+ MapsTo k e (update m m') <->
+ (MapsTo k e m' \/ (MapsTo k e m /\ ~In k m')).
+ Proof.
+ unfold update.
+ intros m m'.
+ pattern m', (fold (@add _) m' m). apply fold_rec.
+
+ intros m0 Hm0 k e.
+ assert (~In k m0) by (intros (e0,He0); apply (Hm0 k e0); auto).
+ intuition.
+ elim (Hm0 k e); auto.
+
+ intros k e m0 m1 m2 _ Hn Hadd IH k' e'.
+ change (Equal m2 (add k e m1)) in Hadd.
+ rewrite Hadd, 2 add_mapsto_iff, IH, add_in_iff. clear IH. intuition.
+ Qed.
+
+ Lemma update_dec : forall m m' k e, MapsTo k e (update m m') ->
+ { MapsTo k e m' } + { MapsTo k e m /\ ~In k m'}.
+ Proof.
+ intros m m' k e H. rewrite update_mapsto_iff in H.
+ destruct (In_dec m' k) as [H'|H']; [left|right]; intuition.
+ elim H'; exists e; auto.
+ Defined.
+
+ Lemma update_in_iff : forall m m' k,
+ In k (update m m') <-> In k m \/ In k m'.
+ Proof.
+ intros m m' k. split.
+ intros (e,H); rewrite update_mapsto_iff in H.
+ destruct H; [right|left]; exists e; intuition.
+ destruct (In_dec m' k) as [H|H].
+ destruct H as (e,H). intros _; exists e.
+ rewrite update_mapsto_iff; left; auto.
+ destruct 1 as [H'|H']; [|elim H; auto].
+ destruct H' as (e,H'). exists e.
+ rewrite update_mapsto_iff; right; auto.
+ Qed.
+
+ Lemma diff_mapsto_iff : forall m m' k e,
+ MapsTo k e (diff m m') <-> MapsTo k e m /\ ~In k m'.
+ Proof.
+ intros m m' k e.
+ unfold diff.
+ rewrite filter_iff.
+ intuition.
+ rewrite mem_1 in *; auto; discriminate.
+ intros ? ? Hk _ _ _; rewrite Hk; auto.
+ Qed.
+
+ Lemma diff_in_iff : forall m m' k,
+ In k (diff m m') <-> In k m /\ ~In k m'.
+ Proof.
+ intros m m' k. split.
+ intros (e,H); rewrite diff_mapsto_iff in H.
+ destruct H; split; auto. exists e; auto.
+ intros ((e,H),H'); exists e; rewrite diff_mapsto_iff; auto.
+ Qed.
+
+ Lemma restrict_mapsto_iff : forall m m' k e,
+ MapsTo k e (restrict m m') <-> MapsTo k e m /\ In k m'.
+ Proof.
+ intros m m' k e.
+ unfold restrict.
+ rewrite filter_iff.
+ intuition.
+ intros ? ? Hk _ _ _; rewrite Hk; auto.
+ Qed.
+
+ Lemma restrict_in_iff : forall m m' k,
+ In k (restrict m m') <-> In k m /\ In k m'.
+ Proof.
+ intros m m' k. split.
+ intros (e,H); rewrite restrict_mapsto_iff in H.
+ destruct H; split; auto. exists e; auto.
+ intros ((e,H),H'); exists e; rewrite restrict_mapsto_iff; auto.
+ Qed.
+
(** specialized versions analyzing only keys (resp. elements) *)
Definition filter_dom (f : key -> bool) := filter (fun k _ => f k).
@@ -1106,17 +1672,85 @@ Module WProperties (E:DecidableType)(M:WSfun E).
End Elt.
- Add Parametric Morphism elt : (@cardinal elt) with signature Equal ==> @Logic.eq _ as cardinal_m.
+ Add Parametric Morphism elt : (@cardinal elt)
+ with signature Equal ==> Leibniz as cardinal_m.
Proof. intros; apply Equal_cardinal; auto. Qed.
-End WProperties.
-
-(** * Same Properties for full maps *)
-
-Module Properties (M:S).
- Module D := OT_as_DT M.E.
- Include WProperties D M.
-End Properties.
+ Add Parametric Morphism elt : (@Disjoint elt)
+ with signature Equal ==> Equal ==> iff as Disjoint_m.
+ Proof.
+ intros m1 m1' Hm1 m2 m2' Hm2. unfold Disjoint. split; intros.
+ rewrite <- Hm1, <- Hm2; auto.
+ rewrite Hm1, Hm2; auto.
+ Qed.
+
+ Add Parametric Morphism elt : (@Partition elt)
+ with signature Equal ==> Equal ==> Equal ==> iff as Partition_m.
+ Proof.
+ intros m1 m1' Hm1 m2 m2' Hm2 m3 m3' Hm3. unfold Partition.
+ rewrite <- Hm2, <- Hm3.
+ split; intros (H,H'); split; auto; intros.
+ rewrite <- Hm1, <- Hm2, <- Hm3; auto.
+ rewrite Hm1, Hm2, Hm3; auto.
+ Qed.
+
+ Add Parametric Morphism elt : (@update elt)
+ with signature Equal ==> Equal ==> Equal as update_m.
+ Proof.
+ intros m1 m1' Hm1 m2 m2' Hm2.
+ setoid_replace (update m1 m2) with (update m1' m2); unfold update.
+ apply fold_Equal with (eqA:=Equal); auto.
+ intros k k' Hk e e' He m m' Hm; rewrite Hk,He,Hm; red; auto.
+ intros k k' e e' i Hneq x.
+ rewrite !add_o; do 2 destruct eq_dec; auto. elim Hneq; eauto.
+ apply fold_init with (eqA:=Equal); auto.
+ intros k k' Hk e e' He m m' Hm; rewrite Hk,He,Hm; red; auto.
+ Qed.
+
+ Add Parametric Morphism elt : (@restrict elt)
+ with signature Equal ==> Equal ==> Equal as restrict_m.
+ Proof.
+ intros m1 m1' Hm1 m2 m2' Hm2.
+ setoid_replace (restrict m1 m2) with (restrict m1' m2);
+ unfold restrict, filter.
+ apply fold_rel with (R:=Equal); try red; auto.
+ intros k e i i' H Hii' x.
+ pattern (mem k m2); rewrite Hm2. (* UGLY, see with Matthieu *)
+ destruct mem; rewrite Hii'; auto.
+ apply fold_Equal with (eqA:=Equal); auto.
+ intros k k' Hk e e' He m m' Hm; simpl in *.
+ pattern (mem k m2); rewrite Hk. (* idem *)
+ destruct mem; rewrite ?Hk,?He,Hm; red; auto.
+ intros k k' e e' i Hneq x.
+ case_eq (mem k m2); case_eq (mem k' m2); intros; auto.
+ rewrite !add_o; do 2 destruct eq_dec; auto. elim Hneq; eauto.
+ Qed.
+
+ Add Parametric Morphism elt : (@diff elt)
+ with signature Equal ==> Equal ==> Equal as diff_m.
+ Proof.
+ intros m1 m1' Hm1 m2 m2' Hm2.
+ setoid_replace (diff m1 m2) with (diff m1' m2);
+ unfold diff, filter.
+ apply fold_rel with (R:=Equal); try red; auto.
+ intros k e i i' H Hii' x.
+ pattern (mem k m2); rewrite Hm2. (* idem *)
+ destruct mem; simpl; rewrite Hii'; auto.
+ apply fold_Equal with (eqA:=Equal); auto.
+ intros k k' Hk e e' He m m' Hm; simpl in *.
+ pattern (mem k m2); rewrite Hk. (* idem *)
+ destruct mem; simpl; rewrite ?Hk,?He,Hm; red; auto.
+ intros k k' e e' i Hneq x.
+ case_eq (mem k m2); case_eq (mem k' m2); intros; simpl; auto.
+ rewrite !add_o; do 2 destruct eq_dec; auto. elim Hneq; eauto.
+ Qed.
+
+End WProperties_fun.
+
+(** * Same Properties for self-contained weak maps and for full maps *)
+
+Module WProperties (M:WS) := WProperties_fun M.E M.
+Module Properties := WProperties.
(** * Properties specific to maps with ordered keys *)
@@ -1151,7 +1785,8 @@ Module OrdProperties (M:S).
Ltac clean_eauto := unfold O.eqke, O.ltk; simpl; intuition; eauto.
- Definition gtb (p p':key*elt) := match E.compare (fst p) (fst p') with GT _ => true | _ => false end.
+ Definition gtb (p p':key*elt) :=
+ match E.compare (fst p) (fst p') with GT _ => true | _ => false end.
Definition leb p := fun p' => negb (gtb p p').
Definition elements_lt p m := List.filter (gtb p) (elements m).
@@ -1275,7 +1910,7 @@ Module OrdProperties (M:S).
rewrite find_mapsto_iff; rewrite (H0 t0); rewrite <- find_mapsto_iff.
rewrite add_mapsto_iff; unfold O.eqke; simpl.
intuition.
- destruct (ME.eq_dec x t0); auto.
+ destruct (E.eq_dec x t0); auto.
elimtype False.
assert (In t0 m).
exists e0; auto.
@@ -1305,7 +1940,7 @@ Module OrdProperties (M:S).
rewrite find_mapsto_iff; rewrite (H0 t0); rewrite <- find_mapsto_iff.
rewrite add_mapsto_iff; unfold O.eqke; simpl.
intuition.
- destruct (ME.eq_dec x t0); auto.
+ destruct (E.eq_dec x t0); auto.
elimtype False.
assert (In t0 m).
exists e0; auto.
@@ -1361,7 +1996,7 @@ Module OrdProperties (M:S).
inversion_clear H1; [ | inversion_clear H2; eauto ].
red in H3; simpl in H3; destruct H3.
destruct p as (p1,p2).
- destruct (ME.eq_dec p1 x).
+ destruct (E.eq_dec p1 x).
apply ME.lt_eq with p1; auto.
inversion_clear H2.
inversion_clear H5.
@@ -1513,74 +2148,53 @@ Module OrdProperties (M:S).
(** The following lemma has already been proved on Weak Maps,
but with one additionnal hypothesis (some [transpose] fact). *)
- Lemma fold_Equal : forall s1 s2 (A:Type)(eqA:A->A->Prop)(st:Setoid_Theory A eqA)
- (f:key->elt->A->A)(i:A),
- compat_op eqke eqA (fun y =>f (fst y) (snd y)) ->
- Equal s1 s2 ->
- eqA (fold f s1 i) (fold f s2 i).
+ Lemma fold_Equal : forall m1 m2 (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA)
+ (f:key->elt->A->A)(i:A),
+ Morphism (E.eq==>Leibniz==>eqA==>eqA) f ->
+ Equal m1 m2 ->
+ eqA (fold f m1 i) (fold f m2 i).
Proof.
- intros.
+ intros m1 m2 A eqA st f i Hf Heq.
do 2 rewrite fold_1.
do 2 rewrite <- fold_left_rev_right.
apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto.
- apply eqlistA_rev.
- apply elements_Equal_eqlistA; auto.
+ intros (k,e) (k',e') a a' (Hk,He) Ha; simpl in *; apply Hf; auto.
+ apply eqlistA_rev. apply elements_Equal_eqlistA. auto.
Qed.
- Lemma fold_Add : forall s1 s2 x e (A:Type)(eqA:A->A->Prop)(st:Setoid_Theory A eqA)
- (f:key->elt->A->A)(i:A),
- compat_op eqke eqA (fun y =>f (fst y) (snd y)) ->
- transpose eqA (fun y =>f (fst y) (snd y)) ->
- ~In x s1 -> Add x e s1 s2 ->
- eqA (fold f s2 i) (f x e (fold f s1 i)).
- Proof.
- intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right.
- set (f':=fun y x0 => f (fst y) (snd y) x0) in *.
- change (f x e (fold_right f' i (rev (elements s1))))
- with (f' (x,e) (fold_right f' i (rev (elements s1)))).
- trans_st (fold_right f' i
- (rev (elements_lt (x, e) s1 ++ (x,e) :: elements_ge (x, e) s1))).
- apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto.
- apply eqlistA_rev.
- apply elements_Add; auto.
- rewrite distr_rev; simpl.
- rewrite app_ass; simpl.
- rewrite (elements_split (x,e) s1).
- rewrite distr_rev; simpl.
- apply fold_right_commutes with (eqA:=eqke) (eqB:=eqA); auto.
- Qed.
-
- Lemma fold_Add_Above : forall s1 s2 x e (A:Type)(eqA:A->A->Prop)(st:Setoid_Theory A eqA)
- (f:key->elt->A->A)(i:A),
- compat_op eqke eqA (fun y =>f (fst y) (snd y)) ->
- Above x s1 -> Add x e s1 s2 ->
- eqA (fold f s2 i) (f x e (fold f s1 i)).
+ Lemma fold_Add_Above : forall m1 m2 x e (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA)
+ (f:key->elt->A->A)(i:A),
+ Morphism (E.eq==>Leibniz==>eqA==>eqA) f ->
+ Above x m1 -> Add x e m1 m2 ->
+ eqA (fold f m2 i) (f x e (fold f m1 i)).
Proof.
intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right.
set (f':=fun y x0 => f (fst y) (snd y) x0) in *.
- trans_st (fold_right f' i (rev (elements s1 ++ (x,e)::nil))).
+ transitivity (fold_right f' i (rev (elements m1 ++ (x,e)::nil))).
apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto.
+ intros (k1,e1) (k2,e2) a1 a2 (Hk,He) Ha; unfold f'; simpl in *; apply H; auto.
apply eqlistA_rev.
apply elements_Add_Above; auto.
rewrite distr_rev; simpl.
- refl_st.
+ reflexivity.
Qed.
- Lemma fold_Add_Below : forall s1 s2 x e (A:Type)(eqA:A->A->Prop)(st:Setoid_Theory A eqA)
- (f:key->elt->A->A)(i:A),
- compat_op eqke eqA (fun y =>f (fst y) (snd y)) ->
- Below x s1 -> Add x e s1 s2 ->
- eqA (fold f s2 i) (fold f s1 (f x e i)).
+ Lemma fold_Add_Below : forall m1 m2 x e (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA)
+ (f:key->elt->A->A)(i:A),
+ Morphism (E.eq==>Leibniz==>eqA==>eqA) f ->
+ Below x m1 -> Add x e m1 m2 ->
+ eqA (fold f m2 i) (fold f m1 (f x e i)).
Proof.
intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right.
set (f':=fun y x0 => f (fst y) (snd y) x0) in *.
- trans_st (fold_right f' i (rev (((x,e)::nil)++elements s1))).
+ transitivity (fold_right f' i (rev (((x,e)::nil)++elements m1))).
apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto.
+ intros (k1,e1) (k2,e2) a1 a2 (Hk,He) Ha; unfold f'; simpl in *; apply H; auto.
apply eqlistA_rev.
simpl; apply elements_Add_Below; auto.
rewrite distr_rev; simpl.
rewrite fold_right_app.
- refl_st.
+ reflexivity.
Qed.
End Fold_properties.
@@ -1589,7 +2203,3 @@ Module OrdProperties (M:S).
End OrdProperties.
-
-
-
-
diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v
index 1e475887..ebdc9c57 100644
--- a/theories/FSets/FMapInterface.v
+++ b/theories/FSets/FMapInterface.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FMapInterface.v 10616 2008-03-04 17:33:35Z letouzey $ *)
+(* $Id: FMapInterface.v 11699 2008-12-18 11:49:08Z letouzey $ *)
(** * Finite map library *)
@@ -55,11 +55,7 @@ Definition Cmp (elt:Type)(cmp:elt->elt->bool) e1 e2 := cmp e1 e2 = true.
No requirements for an ordering on keys nor elements, only decidability
of equality on keys. First, a functorial signature: *)
-Module Type WSfun (E : EqualityType).
-
- (** The module E of base objects is meant to be a [DecidableType]
- (and used to be so). But requiring only an [EqualityType] here
- allows subtyping between weak and ordered maps. *)
+Module Type WSfun (E : DecidableType).
Definition key := E.t.
@@ -261,7 +257,7 @@ End WSfun.
Similar to [WSfun] but expressed in a self-contained way. *)
Module Type WS.
- Declare Module E : EqualityType.
+ Declare Module E : DecidableType.
Include Type WSfun E.
End WS.
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index 23bf8196..0ec5ef36 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FMapList.v 10616 2008-03-04 17:33:35Z letouzey $ *)
+(* $Id: FMapList.v 11699 2008-12-18 11:49:08Z letouzey $ *)
(** * Finite map library *)
@@ -402,7 +402,7 @@ Proof.
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 (eq_dec x k); auto.
+ apply H1 with k; destruct (X.eq_dec x k); auto.
destruct (X.compare x x'); try contradiction; clear y.
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index 9bc2a599..7fbc3d47 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -11,7 +11,7 @@
* Institution: LRI, CNRS UMR 8623 - Université Paris Sud
* 91405 Orsay, France *)
-(* $Id: FMapPositive.v 10739 2008-04-01 14:45:20Z herbelin $ *)
+(* $Id: FMapPositive.v 11699 2008-12-18 11:49:08Z letouzey $ *)
Require Import Bool.
Require Import ZArith.
@@ -111,17 +111,17 @@ Module PositiveOrderedTypeBits <: UsualOrderedType.
apply EQ; red; auto.
Qed.
-End PositiveOrderedTypeBits.
-
-(** Other positive stuff *)
-
-Lemma peq_dec (x y: positive): {x = y} + {x <> y}.
-Proof.
+ Lemma eq_dec (x y: positive): {x = y} + {x <> y}.
+ Proof.
intros. case_eq ((x ?= y) Eq); intros.
left. apply Pcompare_Eq_eq; auto.
right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate.
right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate.
-Qed.
+ Qed.
+
+End PositiveOrderedTypeBits.
+
+(** Other positive stuff *)
Fixpoint append (i j : positive) {struct i} : positive :=
match i with
@@ -717,7 +717,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
Lemma remove_3 : MapsTo y e (remove x m) -> MapsTo y e m.
Proof.
unfold MapsTo.
- destruct (peq_dec x y).
+ destruct (E.eq_dec x y).
subst.
rewrite grs; intros; discriminate.
rewrite gro; auto.
@@ -820,16 +820,21 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
Variable B : Type.
- Fixpoint xmapi (f : positive -> A -> B) (m : t A) (i : positive)
- {struct m} : t B :=
- match m with
- | Leaf => @Leaf B
- | Node l o r => Node (xmapi f l (append i (xO xH)))
- (option_map (f i) o)
- (xmapi f r (append i (xI xH)))
- end.
+ Section Mapi.
+
+ Variable f : positive -> A -> B.
- Definition mapi (f : positive -> A -> B) m := xmapi f m xH.
+ Fixpoint xmapi (m : t A) (i : positive) {struct m} : t B :=
+ match m with
+ | Leaf => @Leaf B
+ | Node l o r => Node (xmapi l (append i (xO xH)))
+ (option_map (f i) o)
+ (xmapi r (append i (xI xH)))
+ end.
+
+ Definition mapi m := xmapi m xH.
+
+ End Mapi.
Definition map (f : A -> B) m := mapi (fun _ => f) m.
@@ -983,14 +988,47 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
Qed.
- Definition fold (A : Type)(B : Type) (f: positive -> A -> B -> B) (tr: t A) (v: B) :=
- List.fold_left (fun a p => f (fst p) (snd p) a) (elements tr) v.
-
+ Section Fold.
+
+ Variables A B : Type.
+ Variable f : positive -> A -> B -> B.
+
+ Fixpoint xfoldi (m : t A) (v : B) (i : positive) :=
+ match m with
+ | Leaf => v
+ | Node l (Some x) r =>
+ xfoldi r (f i x (xfoldi l v (append i 2))) (append i 3)
+ | Node l None r =>
+ xfoldi r (xfoldi l v (append i 2)) (append i 3)
+ end.
+
+ Lemma xfoldi_1 :
+ forall m v i,
+ xfoldi m v i = fold_left (fun a p => f (fst p) (snd p) a) (xelements m i) v.
+ Proof.
+ set (F := fun a p => f (fst p) (snd p) a).
+ induction m; intros; simpl; auto.
+ destruct o.
+ rewrite fold_left_app; simpl.
+ rewrite <- IHm1.
+ rewrite <- IHm2.
+ unfold F; simpl; reflexivity.
+ rewrite fold_left_app; simpl.
+ rewrite <- IHm1.
+ rewrite <- IHm2.
+ reflexivity.
+ Qed.
+
+ Definition fold m i := xfoldi m i 1.
+
+ End Fold.
+
Lemma fold_1 :
forall (A:Type)(m:t A)(B:Type)(i : B) (f : key -> A -> B -> B),
fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
Proof.
- intros; unfold fold; auto.
+ intros; unfold fold, elements.
+ rewrite xfoldi_1; reflexivity.
Qed.
Fixpoint equal (A:Type)(cmp : A -> A -> bool)(m1 m2 : t A) {struct m1} : bool :=
@@ -1128,10 +1166,10 @@ Module PositiveMapAdditionalFacts.
(* Derivable from the Map interface *)
Theorem gsspec:
forall (A:Type)(i j: positive) (x: A) (m: t A),
- find i (add j x m) = if peq_dec i j then Some x else find i m.
+ find i (add j x m) = if E.eq_dec i j then Some x else find i m.
Proof.
intros.
- destruct (peq_dec i j); [ rewrite e; apply gss | apply gso; auto ].
+ destruct (E.eq_dec i j); [ rewrite e; apply gss | apply gso; auto ].
Qed.
(* Not derivable from the Map interface *)
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index faa705f6..cc1c0a76 100644
--- a/theories/FSets/FSetAVL.v
+++ b/theories/FSets/FSetAVL.v
@@ -11,7 +11,7 @@
* Institution: LRI, CNRS UMR 8623 - Université Paris Sud
* 91405 Orsay, France *)
-(* $Id: FSetAVL.v 10811 2008-04-17 16:29:49Z letouzey $ *)
+(* $Id: FSetAVL.v 11699 2008-12-18 11:49:08Z letouzey $ *)
(** * FSetAVL *)
@@ -1881,6 +1881,14 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
destruct Raw.compare; intros; [apply EQ|apply LT|apply GT]; red; auto.
Defined.
+ Definition eq_dec (s s':t) : { eq s s' } + { ~ eq s s' }.
+ Proof.
+ intros (s,b) (s',b'); unfold eq; simpl.
+ case_eq (Raw.equal s s'); intro H; [left|right].
+ apply equal_2; auto.
+ intro H'; rewrite equal_1 in H; auto; discriminate.
+ Defined.
+
(* specs *)
Section Specs.
Variable s s' s'': t.
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index 0622451f..c03fb92e 100644
--- a/theories/FSets/FSetBridge.v
+++ b/theories/FSets/FSetBridge.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FSetBridge.v 10601 2008-02-28 00:20:33Z letouzey $ *)
+(* $Id: FSetBridge.v 11699 2008-12-18 11:49:08Z letouzey $ *)
(** * Finite sets library *)
@@ -20,11 +20,8 @@ Set Firstorder Depth 2.
(** * From non-dependent signature [S] to dependent signature [Sdep]. *)
-Module DepOfNodep (M: S) <: Sdep with Module E := M.E.
- Import M.
+Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E.
- Module ME := OrderedTypeFacts E.
-
Definition empty : {s : t | Empty s}.
Proof.
exists empty; auto with set.
@@ -50,7 +47,7 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E.
Proof.
intros; exists (add x s); auto.
unfold Add in |- *; intuition.
- elim (ME.eq_dec x y); auto.
+ elim (E.eq_dec x y); auto.
intros; right.
eapply add_3; eauto.
Qed.
@@ -68,7 +65,7 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E.
intros; exists (remove x s); intuition.
absurd (In x (remove x s)); auto with set.
apply In_1 with y; auto.
- elim (ME.eq_dec x y); intros; auto.
+ elim (E.eq_dec x y); intros; auto.
absurd (In x (remove x s)); auto with set.
apply In_1 with y; auto.
eauto with set.
@@ -396,6 +393,8 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
intros; discriminate H.
Qed.
+ Definition eq_dec := equal.
+
Definition equal (s s' : t) : bool :=
if equal s s' then true else false.
diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
index 0639c1f1..06b4e028 100644
--- a/theories/FSets/FSetDecide.v
+++ b/theories/FSets/FSetDecide.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FSetDecide.v 11064 2008-06-06 17:00:52Z letouzey $ *)
+(* $Id: FSetDecide.v 11699 2008-12-18 11:49:08Z letouzey $ *)
(**************************************************************)
(* FSetDecide.v *)
@@ -19,10 +19,10 @@
Require Import Decidable DecidableTypeEx FSetFacts.
-(** First, a version for Weak Sets *)
+(** First, a version for Weak Sets in functorial presentation *)
-Module WDecide (E : DecidableType)(Import M : WSfun E).
- Module F := FSetFacts.WFacts E M.
+Module WDecide_fun (E : DecidableType)(Import M : WSfun E).
+ Module F := FSetFacts.WFacts_fun E M.
(** * Overview
This functor defines the tactic [fsetdec], which will
@@ -509,7 +509,14 @@ the above form:
| J : _ |- _ => progress (change T with E.t in J)
| |- _ => progress (change T with E.t)
end )
- end).
+ | H : forall x : ?T, _ |- _ =>
+ progress (change T with E.t in H);
+ repeat (
+ match goal with
+ | J : _ |- _ => progress (change T with E.t in J)
+ | |- _ => progress (change T with E.t)
+ end )
+ end).
(** These two tactics take us from Coq's built-in equality
to [E.eq] (and vice versa) when possible. *)
@@ -747,6 +754,12 @@ the above form:
In x (singleton x).
Proof. fsetdec. Qed.
+ Lemma test_add_In : forall x y s,
+ In x (add y s) ->
+ ~ E.eq x y ->
+ In x s.
+ Proof. fsetdec. Qed.
+
Lemma test_Subset_add_remove : forall x s,
s [<=] (add x (remove x s)).
Proof. fsetdec. Qed.
@@ -825,17 +838,27 @@ the above form:
intros until 3. intros g_eq. rewrite <- g_eq. fsetdec.
Qed.
+ Lemma test_baydemir :
+ forall (f : t -> t),
+ forall (s : t),
+ forall (x y : elt),
+ In x (add y (f s)) ->
+ ~ E.eq x y ->
+ In x (f s).
+ Proof.
+ fsetdec.
+ Qed.
+
End FSetDecideTestCases.
-End WDecide.
+End WDecide_fun.
Require Import FSetInterface.
-(** Now comes a special version dedicated to full sets. For this
- one, only one argument [(M:S)] is necessary. *)
+(** Now comes variants for self-contained weak sets and for full sets.
+ For these variants, only one argument is necessary. Thanks to
+ the subtyping [WS<=S], the [Decide] functor which is meant to be
+ used on modules [(M:S)] can simply be an alias of [WDecide]. *)
-Module Decide (M : S).
- Module D:=OT_as_DT M.E.
- Module WD := WDecide D M.
- Ltac fsetdec := WD.fsetdec.
-End Decide. \ No newline at end of file
+Module WDecide (M:WS) := WDecide_fun M.E M.
+Module Decide := WDecide.
diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index a397cc28..80ab2b2c 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FSetEqProperties.v 11064 2008-06-06 17:00:52Z letouzey $ *)
+(* $Id: FSetEqProperties.v 11720 2008-12-28 07:12:15Z letouzey $ *)
(** * Finite sets library *)
@@ -19,8 +19,8 @@
Require Import FSetProperties Zerob Sumbool Omega DecidableTypeEx.
-Module WEqProperties (Import E:DecidableType)(M:WSfun E).
-Module Import MP := WProperties E M.
+Module WEqProperties_fun (Import E:DecidableType)(M:WSfun E).
+Module Import MP := WProperties_fun E M.
Import FM Dec.F.
Import M.
@@ -73,7 +73,7 @@ Qed.
Lemma is_empty_equal_empty: is_empty s = equal s empty.
Proof.
apply bool_1; split; intros.
-rewrite <- (empty_is_empty_1 (s:=empty)); auto with set.
+auto with set.
rewrite <- is_empty_iff; auto with set.
Qed.
@@ -281,7 +281,7 @@ Qed.
Lemma singleton_mem_2: ~E.eq x y -> mem y (singleton x)=false.
Proof.
intros; rewrite singleton_b.
-unfold eqb; destruct (eq_dec x y); intuition.
+unfold eqb; destruct (E.eq_dec x y); intuition.
Qed.
Lemma singleton_mem_3: mem y (singleton x)=true -> E.eq x y.
@@ -494,7 +494,7 @@ destruct (mem x s); destruct (mem x s'); intuition.
Qed.
Section Fold.
-Variables (A:Type)(eqA:A->A->Prop)(st:Setoid_Theory _ eqA).
+Variables (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA).
Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f)(Ass:transpose eqA f).
Variables (i:A).
Variables (s s':t)(x:elt).
@@ -852,7 +852,7 @@ assert (gc : compat_opL (fun x:elt => plus (g x))). auto.
assert (gt : transposeL (fun x:elt =>plus (g x))). red; intros; omega.
assert (fgc : compat_opL (fun x:elt =>plus ((f x)+(g x)))). auto.
assert (fgt : transposeL (fun x:elt=>plus ((f x)+(g x)))). red; intros; omega.
-assert (st := gen_st nat).
+assert (st : Equivalence (@Logic.eq nat)) by (split; congruence).
intros s;pattern s; apply set_rec.
intros.
rewrite <- (fold_equal _ _ st _ fc ft 0 _ _ H).
@@ -867,7 +867,7 @@ Lemma sum_filter : forall f, (compat_bool E.eq f) ->
forall s, (sum (fun x => if f x then 1 else 0) s) = (cardinal (filter f s)).
Proof.
unfold sum; intros f Hf.
-assert (st := gen_st nat).
+assert (st : Equivalence (@Logic.eq nat)) by (split; congruence).
assert (cc : compat_opL (fun x => plus (if f x then 1 else 0))).
red; intros.
rewrite (Hf x x' H); auto.
@@ -892,7 +892,7 @@ rewrite filter_iff; auto; set_iff; tauto.
Qed.
Lemma fold_compat :
- forall (A:Type)(eqA:A->A->Prop)(st:Setoid_Theory _ eqA)
+ forall (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA)
(f g:elt->A->A),
(compat_op E.eq eqA f) -> (transpose eqA f) ->
(compat_op E.eq eqA g) -> (transpose eqA g) ->
@@ -901,19 +901,19 @@ Lemma fold_compat :
Proof.
intros A eqA st f g fc ft gc gt i.
intro s; pattern s; apply set_rec; intros.
-trans_st (fold f s0 i).
+transitivity (fold f s0 i).
apply fold_equal with (eqA:=eqA); auto.
rewrite equal_sym; auto.
-trans_st (fold g s0 i).
+transitivity (fold g s0 i).
apply H0; intros; apply H1; auto with set.
elim (equal_2 H x); auto with set; intros.
apply fold_equal with (eqA:=eqA); auto with set.
-trans_st (f x (fold f s0 i)).
+transitivity (f x (fold f s0 i)).
apply fold_add with (eqA:=eqA); auto with set.
-trans_st (g x (fold f s0 i)); auto with set.
-trans_st (g x (fold g s0 i)); auto with set.
-sym_st; apply fold_add with (eqA:=eqA); auto.
-do 2 rewrite fold_empty; refl_st.
+transitivity (g x (fold f s0 i)); auto with set.
+transitivity (g x (fold g s0 i)); auto with set.
+symmetry; apply fold_add with (eqA:=eqA); auto.
+do 2 rewrite fold_empty; reflexivity.
Qed.
Lemma sum_compat :
@@ -927,13 +927,12 @@ Qed.
End Sum.
-End WEqProperties.
-
+End WEqProperties_fun.
-(** Now comes a special version dedicated to full sets. For this
- one, only one argument [(M:S)] is necessary. *)
+(** Now comes variants for self-contained weak sets and for full sets.
+ For these variants, only one argument is necessary. Thanks to
+ the subtyping [WS<=S], the [EqProperties] functor which is meant to be
+ used on modules [(M:S)] can simply be an alias of [WEqProperties]. *)
-Module EqProperties (M:S).
- Module D := OT_as_DT M.E.
- Include WEqProperties D M.
-End EqProperties.
+Module WEqProperties (M:WS) := WEqProperties_fun M.E M.
+Module EqProperties := WEqProperties.
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v
index d77d9c60..1e15d3a1 100644
--- a/theories/FSets/FSetFacts.v
+++ b/theories/FSets/FSetFacts.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FSetFacts.v 11282 2008-07-28 11:51:53Z msozeau $ *)
+(* $Id: FSetFacts.v 11720 2008-12-28 07:12:15Z letouzey $ *)
(** * Finite sets library *)
@@ -21,11 +21,9 @@ Require Export FSetInterface.
Set Implicit Arguments.
Unset Strict Implicit.
-(** First, a functor for Weak Sets. Since the signature [WS] includes
- an EqualityType and not a stronger DecidableType, this functor
- should take two arguments in order to compensate this. *)
+(** First, a functor for Weak Sets in functorial version. *)
-Module WFacts (Import E : DecidableType)(Import M : WSfun E).
+Module WFacts_fun (Import E : DecidableType)(Import M : WSfun E).
Notation eq_dec := E.eq_dec.
Definition eqb x y := if eq_dec x y then true else false.
@@ -293,12 +291,12 @@ End BoolSpec.
(** * [E.eq] and [Equal] are setoid equalities *)
-Definition E_ST : Setoid_Theory elt E.eq.
+Definition E_ST : Equivalence E.eq.
Proof.
constructor ; red; [apply E.eq_refl|apply E.eq_sym|apply E.eq_trans].
Qed.
-Definition Equal_ST : Setoid_Theory t Equal.
+Definition Equal_ST : Equivalence Equal.
Proof.
constructor ; red; [apply eq_refl | apply eq_sym | apply eq_trans].
Qed.
@@ -309,8 +307,6 @@ Add Relation elt E.eq
transitivity proved by E.eq_trans
as EltSetoid.
-Typeclasses unfold elt.
-
Add Relation t Equal
reflexivity proved by eq_refl
symmetry proved by eq_sym
@@ -418,18 +414,15 @@ Qed.
(* [Subset] is a setoid order *)
Lemma Subset_refl : forall s, s[<=]s.
-Proof. red; auto. Defined.
+Proof. red; auto. Qed.
Lemma Subset_trans : forall s s' s'', s[<=]s'->s'[<=]s''->s[<=]s''.
-Proof. unfold Subset; eauto. Defined.
+Proof. unfold Subset; eauto. Qed.
-Add Relation t Subset
+Add Relation t Subset
reflexivity proved by Subset_refl
transitivity proved by Subset_trans
as SubsetSetoid.
-(* NB: for the moment, it is important to use Defined and not Qed in
- the two previous lemmas, in order to allow conversion of
- SubsetSetoid coming from separate Facts modules. See bug #1738. *)
Instance In_s_m : Morphism (E.eq ==> Subset ++> impl) In | 1.
Proof.
@@ -480,28 +473,35 @@ Proof.
unfold Equal; intros; repeat rewrite filter_iff; auto; rewrite H0; tauto.
Qed.
+Lemma filter_ext : forall f f', compat_bool E.eq f -> (forall x, f x = f' x) ->
+ forall s s', s[=]s' -> filter f s [=] filter f' s'.
+Proof.
+intros f f' Hf Hff' s s' Hss' x. do 2 (rewrite filter_iff; auto).
+rewrite Hff', Hss'; intuition.
+red; intros; rewrite <- 2 Hff'; auto.
+Qed.
+
Lemma filter_subset : forall f, compat_bool E.eq f ->
forall s s', s[<=]s' -> filter f s [<=] filter f s'.
Proof.
unfold Subset; intros; rewrite filter_iff in *; intuition.
Qed.
-(* For [elements], [min_elt], [max_elt] and [choose], we would need setoid
+(* For [elements], [min_elt], [max_elt] and [choose], we would need setoid
structures on [list elt] and [option elt]. *)
(* Later:
Add Morphism cardinal ; cardinal_m.
*)
-End WFacts.
-
+End WFacts_fun.
-(** Now comes a special version dedicated to full sets. For this
- one, only one argument [(M:S)] is necessary. *)
+(** Now comes variants for self-contained weak sets and for full sets.
+ For these variants, only one argument is necessary. Thanks to
+ the subtyping [WS<=S], the [Facts] functor which is meant to be
+ used on modules [(M:S)] can simply be an alias of [WFacts]. *)
-Module Facts (Import M:S).
- Module D:=OT_as_DT M.E.
- Include WFacts D M.
+Module WFacts (M:WS) := WFacts_fun M.E M.
+Module Facts := WFacts.
-End Facts.
diff --git a/theories/FSets/FSetFullAVL.v b/theories/FSets/FSetFullAVL.v
index 1fc109f3..a2d8e681 100644
--- a/theories/FSets/FSetFullAVL.v
+++ b/theories/FSets/FSetFullAVL.v
@@ -11,7 +11,7 @@
* Institution: LRI, CNRS UMR 8623 - Université Paris Sud
* 91405 Orsay, France *)
-(* $Id: FSetFullAVL.v 10739 2008-04-01 14:45:20Z herbelin $ *)
+(* $Id: FSetFullAVL.v 11699 2008-12-18 11:49:08Z letouzey $ *)
(** * FSetFullAVL
@@ -913,6 +913,14 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
change (Raw.Equal s s'); auto.
Defined.
+ Definition eq_dec (s s':t) : { eq s s' } + { ~ eq s s' }.
+ Proof.
+ intros (s,b,a) (s',b',a'); unfold eq; simpl.
+ case_eq (Raw.equal s s'); intro H; [left|right].
+ apply equal_2; auto.
+ intro H'; rewrite equal_1 in H; auto; discriminate.
+ Defined.
+
(* specs *)
Section Specs.
Variable s s' s'': t.
diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index 1255fcc8..79eea34e 100644
--- a/theories/FSets/FSetInterface.v
+++ b/theories/FSets/FSetInterface.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FSetInterface.v 10616 2008-03-04 17:33:35Z letouzey $ *)
+(* $Id: FSetInterface.v 11701 2008-12-18 11:49:12Z letouzey $ *)
(** * Finite set library *)
@@ -44,11 +44,7 @@ Unset Strict Implicit.
Weak sets are sets without ordering on base elements, only
a decidable equality. *)
-Module Type WSfun (E : EqualityType).
-
- (** The module E of base objects is meant to be a [DecidableType]
- (and used to be so). But requiring only an [EqualityType] here
- allows subtyping between weak and ordered sets *)
+Module Type WSfun (E : DecidableType).
Definition elt := E.t.
@@ -62,8 +58,8 @@ Module Type WSfun (E : EqualityType).
Definition For_all (P : elt -> Prop) s := forall x, In x s -> P x.
Definition Exists (P : elt -> Prop) s := exists x, In x s /\ P x.
- Notation "s [=] t" := (Equal s t) (at level 70, no associativity).
- Notation "s [<=] t" := (Subset s t) (at level 70, no associativity).
+ Notation "s [=] t" := (Equal s t) (at level 70, no associativity).
+ Notation "s [<=] t" := (Subset s t) (at level 70, no associativity).
Parameter empty : t.
(** The empty set. *)
@@ -95,12 +91,8 @@ Module Type WSfun (E : EqualityType).
(** Set difference. *)
Definition eq : t -> t -> Prop := Equal.
- (** In order to have the subtyping WS < S between weak and ordered
- sets, we do not require here an [eq_dec]. This interface is hence
- not compatible with [DecidableType], but only with [EqualityType],
- so in general it may not possible to form weak sets of weak sets.
- Some particular implementations may allow this nonetheless, in
- particular [FSetWeakList.Make]. *)
+
+ Parameter eq_dec : forall s s', { eq s s' } + { ~ eq s s' }.
Parameter equal : t -> t -> bool.
(** [equal s1 s2] tests whether the sets [s1] and [s2] are
@@ -282,7 +274,7 @@ End WSfun.
module [E] of base elements is incorporated in the signature. *)
Module Type WS.
- Declare Module E : EqualityType.
+ Declare Module E : DecidableType.
Include Type WSfun E.
End WS.
@@ -367,17 +359,16 @@ WSfun ---> WS
| |
| |
V V
-Sfun ---> S
-
+Sfun ---> S
-Module S_WS (M : S) <: SW := M.
+Module S_WS (M : S) <: WS := M.
Module Sfun_WSfun (E:OrderedType)(M : Sfun E) <: WSfun E := M.
-Module S_Sfun (E:OrderedType)(M : S with Module E:=E) <: Sfun E := M.
-Module WS_WSfun (E:EqualityType)(M : WS with Module E:=E) <: WSfun E := M.
+Module S_Sfun (M : S) <: Sfun M.E := M.
+Module WS_WSfun (M : WS) <: WSfun M.E := M.
>>
*)
-(** * Dependent signature
+(** * Dependent signature
Signature [Sdep] presents ordered sets using dependent types *)
@@ -402,7 +393,7 @@ Module Type Sdep.
Parameter lt : t -> t -> Prop.
Parameter compare : forall s s' : t, Compare lt eq s s'.
- Parameter eq_refl : forall s : t, eq s s.
+ Parameter eq_refl : forall s : t, eq s s.
Parameter eq_sym : forall s s' : t, eq s s' -> eq s' s.
Parameter eq_trans : forall s s' s'' : t, eq s s' -> eq s' s'' -> eq s s''.
Parameter lt_trans : forall s s' s'' : t, lt s s' -> lt s' s'' -> lt s s''.
diff --git a/theories/FSets/FSetList.v b/theories/FSets/FSetList.v
index a205d5b0..b009e109 100644
--- a/theories/FSets/FSetList.v
+++ b/theories/FSets/FSetList.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FSetList.v 10616 2008-03-04 17:33:35Z letouzey $ *)
+(* $Id: FSetList.v 11866 2009-01-28 19:10:15Z letouzey $ *)
(** * Finite sets library *)
@@ -1263,6 +1263,14 @@ Module Make (X: OrderedType) <: S with Module E := X.
auto.
Defined.
+ Definition eq_dec : { eq s s' } + { ~ eq s s' }.
+ Proof.
+ change eq with Equal.
+ case_eq (equal s s'); intro H; [left | right].
+ apply equal_2; auto.
+ intro H'; rewrite equal_1 in H; auto; discriminate.
+ Defined.
+
End Spec.
End Make.
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index 7413b06b..8dc7fbd9 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FSetProperties.v 11064 2008-06-06 17:00:52Z letouzey $ *)
+(* $Id: FSetProperties.v 11720 2008-12-28 07:12:15Z letouzey $ *)
(** * Finite sets library *)
@@ -22,15 +22,13 @@ Set Implicit Arguments.
Unset Strict Implicit.
Hint Unfold transpose compat_op.
-Hint Extern 1 (Setoid_Theory _ _) => constructor; congruence.
+Hint Extern 1 (Equivalence _) => constructor; congruence.
-(** First, a functor for Weak Sets. Since the signature [WS] includes
- an EqualityType and not a stronger DecidableType, this functor
- should take two arguments in order to compensate this. *)
+(** First, a functor for Weak Sets in functorial version. *)
-Module WProperties (Import E : DecidableType)(M : WSfun E).
- Module Import Dec := WDecide E M.
- Module Import FM := Dec.F (* FSetFacts.WFacts E M *).
+Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
+ Module Import Dec := WDecide_fun E M.
+ Module Import FM := Dec.F (* FSetFacts.WFacts_fun E M *).
Import M.
Lemma In_dec : forall x s, {In x s} + {~ In x s}.
@@ -126,6 +124,10 @@ Module WProperties (Import E : DecidableType)(M : WSfun E).
Lemma singleton_equal_add : singleton x [=] add x empty.
Proof. fsetdec. Qed.
+ Lemma remove_singleton_empty :
+ In x s -> remove x s [=] empty -> singleton x [=] s.
+ Proof. fsetdec. Qed.
+
Lemma union_sym : union s s' [=] union s' s.
Proof. fsetdec. Qed.
@@ -306,21 +308,176 @@ Module WProperties (Import E : DecidableType)(M : WSfun E).
rewrite <-elements_Empty; auto with set.
Qed.
- (** * Alternative (weaker) specifications for [fold] *)
+ (** * Conversions between lists and sets *)
+
+ Definition of_list (l : list elt) := List.fold_right add empty l.
- Section Old_Spec_Now_Properties.
+ Definition to_list := elements.
+
+ Lemma of_list_1 : forall l x, In x (of_list l) <-> InA E.eq x l.
+ Proof.
+ induction l; simpl; intro x.
+ rewrite empty_iff, InA_nil. intuition.
+ rewrite add_iff, InA_cons, IHl. intuition.
+ Qed.
+
+ Lemma of_list_2 : forall l, equivlistA E.eq (to_list (of_list l)) l.
+ Proof.
+ unfold to_list; red; intros.
+ rewrite <- elements_iff; apply of_list_1.
+ Qed.
+
+ Lemma of_list_3 : forall s, of_list (to_list s) [=] s.
+ Proof.
+ unfold to_list; red; intros.
+ rewrite of_list_1; symmetry; apply elements_iff.
+ Qed.
+
+ (** * Fold *)
+
+ Section Fold.
Notation NoDup := (NoDupA E.eq).
+ Notation InA := (InA E.eq).
+
+ (** ** Induction principles for fold (contributed by S. Lescuyer) *)
+
+ (** In the following lemma, the step hypothesis is deliberately restricted
+ to the precise set s we are considering. *)
+
+ Theorem fold_rec :
+ forall (A:Type)(P : t -> A -> Type)(f : elt -> A -> A)(i:A)(s:t),
+ (forall s', Empty s' -> P s' i) ->
+ (forall x a s' s'', In x s -> ~In x s' -> Add x s' s'' ->
+ P s' a -> P s'' (f x a)) ->
+ P s (fold f s i).
+ Proof.
+ intros A P f i s Pempty Pstep.
+ rewrite fold_1, <- fold_left_rev_right.
+ set (l:=rev (elements s)).
+ assert (Pstep' : forall x a s' s'', InA x l -> ~In x s' -> Add x s' s'' ->
+ P s' a -> P s'' (f x a)).
+ intros; eapply Pstep; eauto.
+ rewrite elements_iff, <- InA_rev; auto.
+ assert (Hdup : NoDup l) by
+ (unfold l; eauto using elements_3w, NoDupA_rev).
+ assert (Hsame : forall x, In x s <-> InA x l) by
+ (unfold l; intros; rewrite elements_iff, InA_rev; intuition).
+ clear Pstep; clearbody l; revert s Hsame; induction l.
+ (* empty *)
+ intros s Hsame; simpl.
+ apply Pempty. intro x. rewrite Hsame, InA_nil; intuition.
+ (* step *)
+ intros s Hsame; simpl.
+ apply Pstep' with (of_list l); auto.
+ inversion_clear Hdup; rewrite of_list_1; auto.
+ red. intros. rewrite Hsame, of_list_1, InA_cons; intuition.
+ apply IHl.
+ intros; eapply Pstep'; eauto.
+ inversion_clear Hdup; auto.
+ exact (of_list_1 l).
+ Qed.
+
+ (** Same, with [empty] and [add] instead of [Empty] and [Add]. In this
+ case, [P] must be compatible with equality of sets *)
+
+ Theorem fold_rec_bis :
+ forall (A:Type)(P : t -> A -> Type)(f : elt -> A -> A)(i:A)(s:t),
+ (forall s s' a, s[=]s' -> P s a -> P s' a) ->
+ (P empty i) ->
+ (forall x a s', In x s -> ~In x s' -> P s' a -> P (add x s') (f x a)) ->
+ P s (fold f s i).
+ Proof.
+ intros A P f i s Pmorphism Pempty Pstep.
+ apply fold_rec; intros.
+ apply Pmorphism with empty; auto with set.
+ rewrite Add_Equal in H1; auto with set.
+ apply Pmorphism with (add x s'); auto with set.
+ Qed.
+
+ Lemma fold_rec_nodep :
+ forall (A:Type)(P : A -> Type)(f : elt -> A -> A)(i:A)(s:t),
+ P i -> (forall x a, In x s -> P a -> P (f x a)) ->
+ P (fold f s i).
+ Proof.
+ intros; apply fold_rec_bis with (P:=fun _ => P); auto.
+ Qed.
+
+ (** [fold_rec_weak] is a weaker principle than [fold_rec_bis] :
+ the step hypothesis must here be applicable to any [x].
+ At the same time, it looks more like an induction principle,
+ and hence can be easier to use. *)
+
+ Lemma fold_rec_weak :
+ forall (A:Type)(P : t -> A -> Type)(f : elt -> A -> A)(i:A),
+ (forall s s' a, s[=]s' -> P s a -> P s' a) ->
+ P empty i ->
+ (forall x a s, ~In x s -> P s a -> P (add x s) (f x a)) ->
+ forall s, P s (fold f s i).
+ Proof.
+ intros; apply fold_rec_bis; auto.
+ Qed.
+
+ Lemma fold_rel :
+ forall (A B:Type)(R : A -> B -> Type)
+ (f : elt -> A -> A)(g : elt -> B -> B)(i : A)(j : B)(s : t),
+ R i j ->
+ (forall x a b, In x s -> R a b -> R (f x a) (g x b)) ->
+ R (fold f s i) (fold g s j).
+ Proof.
+ intros A B R f g i j s Rempty Rstep.
+ do 2 rewrite fold_1, <- fold_left_rev_right.
+ set (l:=rev (elements s)).
+ 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).
+ clearbody l; clear Rstep s.
+ induction l; simpl; auto.
+ Qed.
+
+ (** From the induction principle on [fold], we can deduce some general
+ induction principles on sets. *)
+
+ Lemma set_induction :
+ forall P : t -> Type,
+ (forall s, Empty s -> P s) ->
+ (forall s s', P s -> forall x, ~In x s -> Add x s s' -> P s') ->
+ forall s, P s.
+ Proof.
+ intros. apply (@fold_rec _ (fun s _ => P s) (fun _ _ => tt) tt s); eauto.
+ Qed.
+
+ Lemma set_induction_bis :
+ forall P : t -> Type,
+ (forall s s', s [=] s' -> P s -> P s') ->
+ P empty ->
+ (forall x s, ~In x s -> P s -> P (add x s)) ->
+ forall s, P s.
+ Proof.
+ intros.
+ apply (@fold_rec_bis _ (fun s _ => P s) (fun _ _ => tt) tt s); eauto.
+ Qed.
+
+ (** [fold] can be used to reconstruct the same initial set. *)
+
+ Lemma fold_identity : forall s, fold add s empty [=] s.
+ Proof.
+ intros.
+ apply fold_rec with (P:=fun s acc => acc[=]s); auto with set.
+ intros. rewrite H2; rewrite Add_Equal in H1; auto with set.
+ Qed.
+
+ (** ** Alternative (weaker) specifications for [fold] *)
(** When [FSets] was first designed, the order in which Ocaml's [Set.fold]
- takes the set elements was unspecified. This specification reflects this fact:
+ takes the set elements was unspecified. This specification reflects
+ this fact:
*)
- Lemma fold_0 :
+ Lemma fold_0 :
forall s (A : Type) (i : A) (f : elt -> A -> A),
exists l : list elt,
NoDup l /\
- (forall x : elt, In x s <-> InA E.eq x l) /\
+ (forall x : elt, In x s <-> InA x l) /\
fold f s i = fold_right f i l.
Proof.
intros; exists (rev (elements s)); split.
@@ -333,26 +490,26 @@ Module WProperties (Import E : DecidableType)(M : WSfun E).
apply fold_1.
Qed.
- (** An alternate (and previous) specification for [fold] was based on
- the recursive structure of a set. It is now lemmas [fold_1] and
+ (** An alternate (and previous) specification for [fold] was based on
+ the recursive structure of a set. It is now lemmas [fold_1] and
[fold_2]. *)
Lemma fold_1 :
- forall s (A : Type) (eqA : A -> A -> Prop)
- (st : Setoid_Theory A eqA) (i : A) (f : elt -> A -> A),
+ forall s (A : Type) (eqA : A -> A -> Prop)
+ (st : Equivalence eqA) (i : A) (f : elt -> A -> A),
Empty s -> eqA (fold f s i) i.
Proof.
unfold Empty; intros; destruct (fold_0 s i f) as (l,(H1, (H2, H3))).
rewrite H3; clear H3.
generalize H H2; clear H H2; case l; simpl; intros.
- refl_st.
+ reflexivity.
elim (H e).
elim (H2 e); intuition.
Qed.
Lemma fold_2 :
forall s s' x (A : Type) (eqA : A -> A -> Prop)
- (st : Setoid_Theory A eqA) (i : A) (f : elt -> A -> A),
+ (st : Equivalence eqA) (i : A) (f : elt -> A -> A),
compat_op E.eq eqA f ->
transpose eqA f ->
~ In x s -> Add x s s' -> eqA (fold f s' i) (f x (fold f s i)).
@@ -379,283 +536,238 @@ Module WProperties (Import E : DecidableType)(M : WSfun E).
rewrite elements_Empty in H; rewrite H; simpl; auto.
Qed.
- (** Similar specifications for [cardinal]. *)
+ Section Fold_More.
- Lemma cardinal_fold : forall s, cardinal s = fold (fun _ => S) s 0.
- Proof.
- intros; rewrite cardinal_1; rewrite M.fold_1.
- symmetry; apply fold_left_length; auto.
- Qed.
-
- Lemma cardinal_0 :
- forall s, exists l : list elt,
- NoDupA E.eq l /\
- (forall x : elt, In x s <-> InA E.eq x l) /\
- cardinal s = length l.
- Proof.
- intros; exists (elements s); intuition; apply cardinal_1.
- Qed.
-
- Lemma cardinal_1 : forall s, Empty s -> cardinal s = 0.
- Proof.
- intros; rewrite cardinal_fold; apply fold_1; auto.
- Qed.
-
- Lemma cardinal_2 :
- forall s s' x, ~ In x s -> Add x s s' -> cardinal s' = S (cardinal s).
- Proof.
- intros; do 2 rewrite cardinal_fold.
- change S with ((fun _ => S) x).
- apply fold_2; auto.
- Qed.
-
- End Old_Spec_Now_Properties.
-
- (** * Induction principle over sets *)
+ Variables (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA).
+ Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f)(Ass:transpose eqA f).
- Lemma cardinal_Empty : forall s, Empty s <-> cardinal s = 0.
+ Lemma fold_commutes : forall i s x,
+ eqA (fold f s (f x i)) (f x (fold f s i)).
Proof.
intros.
- rewrite elements_Empty, M.cardinal_1.
- destruct (elements s); intuition; discriminate.
- Qed.
-
- Lemma cardinal_inv_1 : forall s, cardinal s = 0 -> Empty s.
- Proof.
- intros; rewrite cardinal_Empty; auto.
- Qed.
- Hint Resolve cardinal_inv_1.
-
- Lemma cardinal_inv_2 :
- forall s n, cardinal s = S n -> { x : elt | In x s }.
- Proof.
- intros; rewrite M.cardinal_1 in H.
- generalize (elements_2 (s:=s)).
- destruct (elements s); try discriminate.
- exists e; auto.
- Qed.
-
- Lemma cardinal_inv_2b :
- forall s, cardinal s <> 0 -> { x : elt | In x s }.
- Proof.
- intro; generalize (@cardinal_inv_2 s); destruct cardinal;
- [intuition|eauto].
- Qed.
-
- Lemma Equal_cardinal : forall s s', s[=]s' -> cardinal s = cardinal s'.
- Proof.
- symmetry.
- remember (cardinal s) as n; symmetry in Heqn; revert s s' Heqn H.
- induction n; intros.
- 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.
- Qed.
-
- Add Morphism cardinal : cardinal_m.
- Proof.
- exact Equal_cardinal.
+ apply fold_rel with (R:=fun u v => eqA u (f x v)); intros.
+ reflexivity.
+ transitivity (f x0 (f x b)); auto.
Qed.
- Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal.
+ (** ** Fold is a morphism *)
- Lemma set_induction :
- forall P : t -> Type,
- (forall s : t, Empty s -> P s) ->
- (forall s s' : t, P s -> forall x : elt, ~In x s -> Add x s s' -> P s') ->
- forall s : t, P s.
+ Lemma fold_init : forall i i' s, eqA i i' ->
+ eqA (fold f s i) (fold f s i').
Proof.
- intros; remember (cardinal s) as n; revert s Heqn; induction n; intros; auto.
- destruct (cardinal_inv_2 (sym_eq Heqn)) as (x,H0).
- apply X0 with (remove x s) x; auto with set.
- apply IHn; auto.
- assert (S n = S (cardinal (remove x s))).
- rewrite Heqn; apply cardinal_2 with x; auto with set.
- inversion H; auto.
- Qed.
-
- (** Other properties of [fold]. *)
-
- Section Fold.
- Variables (A:Type)(eqA:A->A->Prop)(st:Setoid_Theory _ eqA).
- Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f)(Ass:transpose eqA f).
-
- Section Fold_1.
- Variable i i':A.
-
- Lemma fold_empty : (fold f empty i) = i.
- Proof.
- apply fold_1b; auto with set.
+ intros. apply fold_rel with (R:=eqA); auto.
Qed.
Lemma fold_equal :
- forall s s', s[=]s' -> eqA (fold f s i) (fold f s' i).
+ forall i s s', s[=]s' -> eqA (fold f s i) (fold f s' i).
Proof.
- intros s; pattern s; apply set_induction; clear s; intros.
- trans_st i.
+ intros i s; pattern s; apply set_induction; clear s; intros.
+ transitivity i.
apply fold_1; auto.
- sym_st; apply fold_1; auto.
+ symmetry; apply fold_1; auto.
rewrite <- H0; auto.
- trans_st (f x (fold f s i)).
+ transitivity (f x (fold f s i)).
apply fold_2 with (eqA := eqA); auto.
- sym_st; apply fold_2 with (eqA := eqA); auto.
+ symmetry; apply fold_2 with (eqA := eqA); auto.
unfold Add in *; intros.
rewrite <- H2; auto.
Qed.
-
- Lemma fold_add : forall s x, ~In x s ->
+
+ (** ** Fold and other set operators *)
+
+ Lemma fold_empty : forall i, fold f empty i = i.
+ Proof.
+ intros i; apply fold_1b; auto with set.
+ Qed.
+
+ Lemma fold_add : forall i s x, ~In x s ->
eqA (fold f (add x s) i) (f x (fold f s i)).
Proof.
- intros; apply fold_2 with (eqA := eqA); auto.
+ intros; apply fold_2 with (eqA := eqA); auto with set.
Qed.
- Lemma add_fold : forall s x, In x s ->
+ Lemma add_fold : forall i s x, In x s ->
eqA (fold f (add x s) i) (fold f s i).
Proof.
intros; apply fold_equal; auto with set.
Qed.
- Lemma remove_fold_1: forall s x, In x s ->
+ Lemma remove_fold_1: forall i s x, In x s ->
eqA (f x (fold f (remove x s) i)) (fold f s i).
Proof.
intros.
- sym_st.
+ symmetry.
apply fold_2 with (eqA:=eqA); auto with set.
Qed.
- Lemma remove_fold_2: forall s x, ~In x s ->
+ Lemma remove_fold_2: forall i s x, ~In x s ->
eqA (fold f (remove x s) i) (fold f s i).
Proof.
intros.
apply fold_equal; auto with set.
Qed.
- Lemma fold_commutes : forall s x,
- eqA (fold f s (f x i)) (f x (fold f s i)).
- Proof.
- intros; pattern s; apply set_induction; clear s; intros.
- trans_st (f x i).
- apply fold_1; auto.
- sym_st.
- apply Comp; auto.
- apply fold_1; auto.
- trans_st (f x0 (fold f s (f x i))).
- apply fold_2 with (eqA:=eqA); auto.
- trans_st (f x0 (f x (fold f s i))).
- trans_st (f x (f x0 (fold f s i))).
- apply Comp; auto.
- sym_st.
- apply fold_2 with (eqA:=eqA); auto.
- Qed.
-
- Lemma fold_init : forall s, eqA i i' ->
- eqA (fold f s i) (fold f s i').
- Proof.
- intros; pattern s; apply set_induction; clear s; intros.
- trans_st i.
- apply fold_1; auto.
- trans_st i'.
- sym_st; apply fold_1; auto.
- trans_st (f x (fold f s i)).
- apply fold_2 with (eqA:=eqA); auto.
- trans_st (f x (fold f s i')).
- sym_st; apply fold_2 with (eqA:=eqA); auto.
- Qed.
-
- End Fold_1.
- Section Fold_2.
- Variable i:A.
-
- Lemma fold_union_inter : forall s s',
+ Lemma fold_union_inter : forall i s s',
eqA (fold f (union s s') (fold f (inter s s') i))
(fold f s (fold f s' i)).
Proof.
intros; pattern s; apply set_induction; clear s; intros.
- trans_st (fold f s' (fold f (inter s s') i)).
+ transitivity (fold f s' (fold f (inter s s') i)).
apply fold_equal; auto with set.
- trans_st (fold f s' i).
+ transitivity (fold f s' i).
apply fold_init; auto.
apply fold_1; auto with set.
- sym_st; apply fold_1; auto.
+ symmetry; apply fold_1; auto.
rename s'0 into s''.
destruct (In_dec x s').
(* In x s' *)
- trans_st (fold f (union s'' s') (f x (fold f (inter s s') i))); auto with set.
+ transitivity (fold f (union s'' s') (f x (fold f (inter s s') i))); auto with set.
apply fold_init; auto.
apply fold_2 with (eqA:=eqA); auto with set.
rewrite inter_iff; intuition.
- trans_st (f x (fold f s (fold f s' i))).
- trans_st (fold f (union s s') (f x (fold f (inter s s') i))).
+ transitivity (f x (fold f s (fold f s' i))).
+ transitivity (fold f (union s s') (f x (fold f (inter s s') i))).
apply fold_equal; auto.
apply equal_sym; apply union_Equal with x; auto with set.
- trans_st (f x (fold f (union s s') (fold f (inter s s') i))).
+ transitivity (f x (fold f (union s s') (fold f (inter s s') i))).
apply fold_commutes; auto.
- sym_st; apply fold_2 with (eqA:=eqA); auto.
+ apply Comp; auto.
+ symmetry; apply fold_2 with (eqA:=eqA); auto.
(* ~(In x s') *)
- trans_st (f x (fold f (union s s') (fold f (inter s'' s') i))).
+ transitivity (f x (fold f (union s s') (fold f (inter s'' s') i))).
apply fold_2 with (eqA:=eqA); auto with set.
- trans_st (f x (fold f (union s s') (fold f (inter s s') i))).
+ transitivity (f x (fold f (union s s') (fold f (inter s s') i))).
apply Comp;auto.
apply fold_init;auto.
apply fold_equal;auto.
apply equal_sym; apply inter_Add_2 with x; auto with set.
- trans_st (f x (fold f s (fold f s' i))).
- sym_st; apply fold_2 with (eqA:=eqA); auto.
+ transitivity (f x (fold f s (fold f s' i))).
+ apply Comp; auto.
+ symmetry; apply fold_2 with (eqA:=eqA); auto.
Qed.
- End Fold_2.
- Section Fold_3.
- Variable i:A.
-
- Lemma fold_diff_inter : forall s s',
+ Lemma fold_diff_inter : forall i s s',
eqA (fold f (diff s s') (fold f (inter s s') i)) (fold f s i).
Proof.
intros.
- trans_st (fold f (union (diff s s') (inter s s'))
- (fold f (inter (diff s s') (inter s s')) i)).
- sym_st; apply fold_union_inter; auto.
- trans_st (fold f s (fold f (inter (diff s s') (inter s s')) i)).
+ transitivity (fold f (union (diff s s') (inter s s'))
+ (fold f (inter (diff s s') (inter s s')) i)).
+ symmetry; apply fold_union_inter; auto.
+ transitivity (fold f s (fold f (inter (diff s s') (inter s s')) i)).
apply fold_equal; auto with set.
apply fold_init; auto.
apply fold_1; auto with set.
Qed.
- Lemma fold_union: forall s s',
+ Lemma fold_union: forall i s s',
(forall x, ~(In x s/\In x s')) ->
eqA (fold f (union s s') i) (fold f s (fold f s' i)).
Proof.
intros.
- trans_st (fold f (union s s') (fold f (inter s s') i)).
+ transitivity (fold f (union s s') (fold f (inter s s') i)).
apply fold_init; auto.
- sym_st; apply fold_1; auto with set.
+ symmetry; apply fold_1; auto with set.
unfold Empty; intro a; generalize (H a); set_iff; tauto.
apply fold_union_inter; auto.
Qed.
- End Fold_3.
- End Fold.
+ End Fold_More.
Lemma fold_plus :
forall s p, fold (fun _ => S) s p = fold (fun _ => S) s 0 + p.
Proof.
- assert (st := gen_st nat).
- assert (fe : compat_op E.eq (@Logic.eq _) (fun _ => S)) by (unfold compat_op; auto).
- assert (fp : transpose (@Logic.eq _) (fun _:elt => S)) by (unfold transpose; auto).
- intros s p; pattern s; apply set_induction; clear s; intros.
- rewrite (fold_1 st p (fun _ => S) H).
- rewrite (fold_1 st 0 (fun _ => S) H); trivial.
- assert (forall p s', Add x s s' -> fold (fun _ => S) s' p = S (fold (fun _ => S) s p)).
- change S with ((fun _ => S) x).
- intros; apply fold_2; auto.
- rewrite H2; auto.
- rewrite (H2 0); auto.
- rewrite H.
- simpl; auto.
- Qed.
-
- (** more properties of [cardinal] *)
+ intros. apply fold_rel with (R:=fun u v => u = v + p); simpl; auto.
+ Qed.
+
+ End Fold.
+
+ (** * Cardinal *)
+
+ (** ** Characterization of cardinal in terms of fold *)
+
+ Lemma cardinal_fold : forall s, cardinal s = fold (fun _ => S) s 0.
+ Proof.
+ intros; rewrite cardinal_1; rewrite M.fold_1.
+ symmetry; apply fold_left_length; auto.
+ Qed.
+
+ (** ** Old specifications for [cardinal]. *)
+
+ Lemma cardinal_0 :
+ forall s, exists l : list elt,
+ NoDupA E.eq l /\
+ (forall x : elt, In x s <-> InA E.eq x l) /\
+ cardinal s = length l.
+ Proof.
+ intros; exists (elements s); intuition; apply cardinal_1.
+ Qed.
+
+ Lemma cardinal_1 : forall s, Empty s -> cardinal s = 0.
+ Proof.
+ intros; rewrite cardinal_fold; apply fold_1; auto.
+ Qed.
+
+ Lemma cardinal_2 :
+ forall s s' x, ~ In x s -> Add x s s' -> cardinal s' = S (cardinal s).
+ Proof.
+ intros; do 2 rewrite cardinal_fold.
+ change S with ((fun _ => S) x).
+ apply fold_2; auto.
+ Qed.
+
+ (** ** Cardinal and (non-)emptiness *)
+
+ Lemma cardinal_Empty : forall s, Empty s <-> cardinal s = 0.
+ Proof.
+ intros.
+ rewrite elements_Empty, M.cardinal_1.
+ destruct (elements s); intuition; discriminate.
+ Qed.
+
+ Lemma cardinal_inv_1 : forall s, cardinal s = 0 -> Empty s.
+ Proof.
+ intros; rewrite cardinal_Empty; auto.
+ Qed.
+ Hint Resolve cardinal_inv_1.
+
+ Lemma cardinal_inv_2 :
+ forall s n, cardinal s = S n -> { x : elt | In x s }.
+ Proof.
+ intros; rewrite M.cardinal_1 in H.
+ generalize (elements_2 (s:=s)).
+ destruct (elements s); try discriminate.
+ exists e; auto.
+ Qed.
+
+ Lemma cardinal_inv_2b :
+ forall s, cardinal s <> 0 -> { x : elt | In x s }.
+ Proof.
+ intro; generalize (@cardinal_inv_2 s); destruct cardinal;
+ [intuition|eauto].
+ Qed.
+
+ (** ** Cardinal is a morphism *)
+
+ Lemma Equal_cardinal : forall s s', s[=]s' -> cardinal s = cardinal s'.
+ Proof.
+ symmetry.
+ remember (cardinal s) as n; symmetry in Heqn; revert s s' Heqn H.
+ induction n; intros.
+ 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.
+ Qed.
+
+ Add Morphism cardinal : cardinal_m.
+ Proof.
+ exact Equal_cardinal.
+ Qed.
+
+ Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal.
+
+ (** ** Cardinal and set operators *)
Lemma empty_cardinal : cardinal empty = 0.
Proof.
@@ -773,18 +885,18 @@ Module WProperties (Import E : DecidableType)(M : WSfun E).
Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2.
-End WProperties.
+End WProperties_fun.
+(** Now comes variants for self-contained weak sets and for full sets.
+ For these variants, only one argument is necessary. Thanks to
+ the subtyping [WS<=S], the [Properties] functor which is meant to be
+ used on modules [(M:S)] can simply be an alias of [WProperties]. *)
-(** A clone of [WProperties] working on full sets. *)
+Module WProperties (M:WS) := WProperties_fun M.E M.
+Module Properties := WProperties.
-Module Properties (M:S).
- Module D := OT_as_DT M.E.
- Include WProperties D M.
-End Properties.
-
-(** Now comes some properties specific to the element ordering,
+(** Now comes some properties specific to the element ordering,
invalid for Weak Sets. *)
Module OrdProperties (M:S).
@@ -973,7 +1085,7 @@ Module OrdProperties (M:S).
Lemma fold_3 :
forall s s' x (A : Type) (eqA : A -> A -> Prop)
- (st : Setoid_Theory A eqA) (i : A) (f : elt -> A -> A),
+ (st : Equivalence eqA) (i : A) (f : elt -> A -> A),
compat_op E.eq eqA f ->
Above x s -> Add x s s' -> eqA (fold f s' i) (f x (fold f s i)).
Proof.
@@ -990,7 +1102,7 @@ Module OrdProperties (M:S).
Lemma fold_4 :
forall s s' x (A : Type) (eqA : A -> A -> Prop)
- (st : Setoid_Theory A eqA) (i : A) (f : elt -> A -> A),
+ (st : Equivalence eqA) (i : A) (f : elt -> A -> A),
compat_op E.eq eqA f ->
Below x s -> Add x s s' -> eqA (fold f s' i) (fold f s (f x i)).
Proof.
@@ -1010,7 +1122,7 @@ Module OrdProperties (M:S).
no need for [(transpose eqA f)]. *)
Section FoldOpt.
- Variables (A:Type)(eqA:A->A->Prop)(st:Setoid_Theory _ eqA).
+ Variables (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA).
Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f).
Lemma fold_equal :
@@ -1024,14 +1136,6 @@ Module OrdProperties (M:S).
red; intro a; do 2 rewrite <- elements_iff; auto.
Qed.
- Lemma fold_init : forall i i' s, eqA i i' ->
- eqA (fold f s i) (fold f s i').
- Proof.
- intros; do 2 rewrite M.fold_1.
- do 2 rewrite <- fold_left_rev_right.
- induction (rev (elements s)); simpl; auto.
- Qed.
-
Lemma add_fold : forall i s x, In x s ->
eqA (fold f (add x s) i) (fold f s i).
Proof.
diff --git a/theories/FSets/FSetToFiniteSet.v b/theories/FSets/FSetToFiniteSet.v
index ae51d905..56a66261 100644
--- a/theories/FSets/FSetToFiniteSet.v
+++ b/theories/FSets/FSetToFiniteSet.v
@@ -11,7 +11,7 @@
* Institution: LRI, CNRS UMR 8623 - Université Paris Sud
* 91405 Orsay, France *)
-(* $Id: FSetToFiniteSet.v 10739 2008-04-01 14:45:20Z herbelin $ *)
+(* $Id: FSetToFiniteSet.v 11735 2009-01-02 17:22:31Z herbelin $ *)
Require Import Ensembles Finite_sets.
Require Import FSetInterface FSetProperties OrderedTypeEx DecidableTypeEx.
@@ -20,7 +20,7 @@ Require Import FSetInterface FSetProperties OrderedTypeEx DecidableTypeEx.
to the good old [Ensembles] and [Finite_sets] theory. *)
Module WS_to_Finite_set (U:UsualDecidableType)(M: WSfun U).
- Module MP:= WProperties U M.
+ Module MP:= WProperties_fun U M.
Import M MP FM Ensembles Finite_sets.
Definition mkEns : M.t -> Ensemble M.elt :=
@@ -30,7 +30,7 @@ Module WS_to_Finite_set (U:UsualDecidableType)(M: WSfun U).
Lemma In_In : forall s x, M.In x s <-> In _ (!!s) x.
Proof.
- unfold In; compute; auto.
+ unfold In; compute; auto with extcore.
Qed.
Lemma Subset_Included : forall s s', s[<=]s' <-> Included _ (!!s) (!!s').
@@ -155,9 +155,7 @@ Module WS_to_Finite_set (U:UsualDecidableType)(M: WSfun U).
End WS_to_Finite_set.
-Module S_to_Finite_set (U:UsualOrderedType)(M: Sfun U).
- Module D := OT_as_DT U.
- Include WS_to_Finite_set D M.
-End S_to_Finite_set.
+Module S_to_Finite_set (U:UsualOrderedType)(M: Sfun U) :=
+ WS_to_Finite_set U M.
diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v
index 71a0d584..309016ce 100644
--- a/theories/FSets/FSetWeakList.v
+++ b/theories/FSets/FSetWeakList.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FSetWeakList.v 10631 2008-03-06 18:17:24Z msozeau $ *)
+(* $Id: FSetWeakList.v 11866 2009-01-28 19:10:15Z letouzey $ *)
(** * Finite sets library *)
@@ -746,53 +746,12 @@ Module Raw (X: DecidableType).
Definition eq_dec : forall (s s':t)(Hs:NoDup s)(Hs':NoDup s'),
{ eq s s' }+{ ~eq s s' }.
Proof.
- unfold eq.
- induction s; intros s'.
- (* nil *)
- destruct s'; [left|right].
- firstorder.
- unfold not, Equal.
- intros H; generalize (H e); clear H.
- rewrite InA_nil, InA_cons; intuition.
- (* cons *)
- intros.
- case_eq (mem a s'); intros H;
- [ destruct (IHs (remove a s')) as [H'|H'];
- [ | | left|right]|right];
- clear IHs.
- inversion_clear Hs; auto.
- apply remove_unique; auto.
- (* In a s' /\ s [=] remove a s' *)
- generalize (mem_2 H); clear H; intro H.
- unfold Equal in *; intros b.
- rewrite InA_cons; split.
- destruct 1.
- apply In_eq with a; auto.
- rewrite H' in H0.
- apply remove_3 with a; auto.
- destruct (X.eq_dec b a); [left|right]; auto.
- rewrite H'.
- apply remove_2; auto.
- (* In a s' /\ ~ s [=] remove a s' *)
- generalize (mem_2 H); clear H; intro H.
- contradict H'.
- unfold Equal in *; intros b.
- split; intros.
- apply remove_2; auto.
- inversion_clear Hs.
- contradict H1; apply In_eq with b; auto.
- rewrite <- H'; rewrite InA_cons; auto.
- assert (In b s') by (apply remove_3 with a; auto).
- rewrite <- H', InA_cons in H1; destruct H1; auto.
- elim (remove_1 Hs' (X.eq_sym H1) H0).
- (* ~ In a s' *)
- assert (~In a s').
- red; intro H'; rewrite (mem_1 H') in H; discriminate.
- contradict H0.
- unfold Equal in *.
- rewrite <- H0.
- rewrite InA_cons; auto.
- Qed.
+ intros.
+ change eq with Equal.
+ case_eq (equal s s'); intro H; [left | right].
+ apply equal_2; auto.
+ intro H'; rewrite equal_1 in H; auto; discriminate.
+ Defined.
End ForNotations.
End Raw.
@@ -993,6 +952,6 @@ Module Make (X: DecidableType) <: WS with Module E := X.
{ eq s s' }+{ ~eq s s' }.
Proof.
intros s s'; exact (Raw.eq_dec s.(unique) s'.(unique)).
- Qed.
+ Defined.
End Make.
diff --git a/theories/FSets/OrderedType.v b/theories/FSets/OrderedType.v
index c56a24cf..fadd27dd 100644
--- a/theories/FSets/OrderedType.v
+++ b/theories/FSets/OrderedType.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: OrderedType.v 10616 2008-03-04 17:33:35Z letouzey $ *)
+(* $Id: OrderedType.v 11700 2008-12-18 11:49:10Z letouzey $ *)
Require Export SetoidList.
Set Implicit Arguments.
@@ -19,7 +19,7 @@ Inductive Compare (X : Type) (lt eq : X -> X -> Prop) (x y : X) : Type :=
| EQ : eq x y -> Compare lt eq x y
| GT : lt y x -> Compare lt eq x y.
-Module Type OrderedType.
+Module Type MiniOrderedType.
Parameter Inline t : Type.
@@ -29,7 +29,7 @@ Module Type OrderedType.
Axiom eq_refl : forall x : t, eq x x.
Axiom eq_sym : forall x y : t, eq x y -> eq y x.
Axiom eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
-
+
Axiom lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
Axiom lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
@@ -38,15 +38,34 @@ Module Type OrderedType.
Hint Immediate eq_sym.
Hint Resolve eq_refl eq_trans lt_not_eq lt_trans.
+End MiniOrderedType.
+
+Module Type OrderedType.
+ Include Type MiniOrderedType.
+
+ (** A [eq_dec] can be deduced from [compare] below. But adding this
+ redundant field allows to see an OrderedType as a DecidableType. *)
+ Parameter eq_dec : forall x y, { eq x y } + { ~ eq x y }.
+
End OrderedType.
+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.
+ Defined.
+
+End MOT_to_OT.
+
(** * Ordered types properties *)
(** Additional properties that can be derived from signature
[OrderedType]. *)
-Module OrderedTypeFacts (O: OrderedType).
- Import O.
+Module OrderedTypeFacts (Import O: OrderedType).
Lemma lt_antirefl : forall x, ~ lt x x.
Proof.
@@ -293,10 +312,8 @@ Ltac false_order := elimtype False; order.
elim (elim_compare_gt (x:=x) (y:=y));
[ intros _1 _2; rewrite _2; clear _1 _2 | auto ].
- Lemma eq_dec : forall x y : t, {eq x y} + {~ eq x y}.
- Proof.
- intros; elim (compare x y); [ right | left | right ]; auto.
- Defined.
+ (** For compatibility reasons *)
+ Definition eq_dec := eq_dec.
Lemma lt_dec : forall x y : t, {lt x y} + {~ lt x y}.
Proof.
diff --git a/theories/FSets/OrderedTypeAlt.v b/theories/FSets/OrderedTypeAlt.v
index 516df0f0..9d179995 100644
--- a/theories/FSets/OrderedTypeAlt.v
+++ b/theories/FSets/OrderedTypeAlt.v
@@ -11,11 +11,12 @@
* Institution: LRI, CNRS UMR 8623 - Université Paris Sud
* 91405 Orsay, France *)
-(* $Id: OrderedTypeAlt.v 10739 2008-04-01 14:45:20Z herbelin $ *)
+(* $Id: OrderedTypeAlt.v 11699 2008-12-18 11:49:08Z letouzey $ *)
Require Import OrderedType.
-(** * An alternative (but equivalent) presentation for an Ordered Type inferface. *)
+(** * An alternative (but equivalent) presentation for an Ordered Type
+ inferface. *)
(** NB: [comparison], defined in [Datatypes.v] is [Eq|Lt|Gt]
whereas [compare], defined in [OrderedType.v] is [EQ _ | LT _ | GT _ ]
@@ -81,6 +82,12 @@ Module OrderedType_from_Alt (O:OrderedTypeAlt) <: OrderedType.
rewrite compare_sym; rewrite H; auto.
Defined.
+ Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }.
+ Proof.
+ intros; unfold eq.
+ case (x ?= y); [ left | right | right ]; auto; discriminate.
+ Defined.
+
End OrderedType_from_Alt.
(** From the original presentation to this alternative one. *)
diff --git a/theories/FSets/OrderedTypeEx.v b/theories/FSets/OrderedTypeEx.v
index 03171396..03e3ab83 100644
--- a/theories/FSets/OrderedTypeEx.v
+++ b/theories/FSets/OrderedTypeEx.v
@@ -11,7 +11,7 @@
* Institution: LRI, CNRS UMR 8623 - Université Paris Sud
* 91405 Orsay, France *)
-(* $Id: OrderedTypeEx.v 10739 2008-04-01 14:45:20Z herbelin $ *)
+(* $Id: OrderedTypeEx.v 11699 2008-12-18 11:49:08Z letouzey $ *)
Require Import OrderedType.
Require Import ZArith.
@@ -34,6 +34,7 @@ Module Type UsualOrderedType.
Axiom lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
Axiom lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
Parameter compare : forall x y : t, Compare lt eq x y.
+ Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }.
End UsualOrderedType.
(** a [UsualOrderedType] is in particular an [OrderedType]. *)
@@ -68,6 +69,8 @@ Module Nat_as_OT <: UsualOrderedType.
intro; constructor 3; auto.
Defined.
+ Definition eq_dec := eq_nat_dec.
+
End Nat_as_OT.
@@ -99,6 +102,8 @@ Module Z_as_OT <: UsualOrderedType.
apply GT; unfold lt, Zlt; rewrite <- Zcompare_Gt_Lt_antisym; auto.
Defined.
+ Definition eq_dec := Z_eq_dec.
+
End Z_as_OT.
(** [positive] is an ordered type with respect to the usual order on natural numbers. *)
@@ -140,6 +145,11 @@ Module Positive_as_OT <: UsualOrderedType.
rewrite <- Pcompare_antisym; rewrite H; auto.
Defined.
+ Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }.
+ Proof.
+ intros; unfold eq; decide equality.
+ Defined.
+
End Positive_as_OT.
@@ -183,6 +193,11 @@ Module N_as_OT <: UsualOrderedType.
destruct (Nleb x y); intuition.
Defined.
+ Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }.
+ Proof.
+ intros. unfold eq. decide equality. apply Positive_as_OT.eq_dec.
+ Defined.
+
End N_as_OT.
@@ -243,5 +258,12 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType.
apply GT; unfold lt; auto.
Defined.
+ 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.
+ auto using lt_not_eq.
+ assert (~ eq y x); auto using lt_not_eq, eq_sym.
+ Defined.
+
End PairOrderedType.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 08:15:34 +0000