diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-30 13:43:15 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-30 13:43:15 +0000 |
commit | 493367ccdfe146d4f898bb49f1ff43ead382dbf9 (patch) | |
tree | 666293128093cd5b39a64851caf1cd6852319ac6 | |
parent | af354d63a814b0855eefda81852029d72b3544db (diff) |
* suite de la revision des wrappers Make
* quelques unfold E.eq en cas de changement de la semantique des foncteurs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8876 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | theories/FSets/FMapAVL.v | 156 | ||||
-rw-r--r-- | theories/FSets/FMapIntMap.v | 8 | ||||
-rw-r--r-- | theories/FSets/FMapList.v | 174 | ||||
-rw-r--r-- | theories/FSets/FMapWeakList.v | 171 | ||||
-rw-r--r-- | theories/FSets/FSetToFiniteSet.v | 6 |
5 files changed, 311 insertions, 204 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index a24b1adbf..17be9405c 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -1702,107 +1702,111 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Module E := X. Module Raw := Raw I X. - Import Raw. - Record bbst (elt:Set) : Set := Bbst {this :> tree elt; is_bst : bst this; is_avl: avl this}. + Record bbst (elt:Set) : Set := + Bbst {this :> Raw.tree elt; is_bst : Raw.bst this; is_avl: Raw.avl this}. Definition t := bbst. - Definition key := X.t. + Definition key := E.t. Section Elt. Variable elt elt' elt'': Set. Implicit Types m : t elt. - - Definition empty := Bbst (empty_bst elt) (empty_avl elt). - Definition is_empty m := is_empty m.(this). - Definition add x e m := - Bbst (add_bst x e m.(is_bst) m.(is_avl)) (add_avl x e m.(is_avl)). - Definition remove x m := - Bbst (remove_bst x m.(is_bst) m.(is_avl)) (remove_avl x m.(is_avl)). - Definition mem x m := mem x m.(this). - Definition find x m := find x m.(this). + Implicit Types x y : key. + Implicit Types e : elt. + + Definition empty : t elt := Bbst (Raw.empty_bst elt) (Raw.empty_avl elt). + Definition is_empty m : bool := Raw.is_empty m.(this). + Definition add x e m : t elt := + Bbst (Raw.add_bst x e m.(is_bst) m.(is_avl)) (Raw.add_avl x e m.(is_avl)). + Definition remove x m : t elt := + Bbst (Raw.remove_bst x m.(is_bst) m.(is_avl)) (Raw.remove_avl x m.(is_avl)). + Definition mem x m : bool := Raw.mem x m.(this). + Definition find x m : option elt := Raw.find x m.(this). Definition map f m : t elt' := - Bbst (map_bst f m.(is_bst)) (map_avl f m.(is_avl)). - Definition mapi f m : t elt' := - Bbst (mapi_bst f m.(is_bst)) (mapi_avl f m.(is_avl)). + Bbst (Raw.map_bst f m.(is_bst)) (Raw.map_avl f m.(is_avl)). + Definition mapi (f:key->elt->elt') m : t elt' := + Bbst (Raw.mapi_bst f m.(is_bst)) (Raw.mapi_avl f m.(is_avl)). Definition map2 f m (m':t elt') : t elt'' := - Bbst (map2_bst f m m') (map2_avl f m m'). - Definition elements m := elements m.(this). - Definition fold (A:Set) f m i := fold (A:=A) f m.(this) i. - Definition equal cmp m m' := - if (equal cmp m.(is_bst) m'.(is_bst)) then true else false. - - Definition MapsTo x e m := MapsTo x e m.(this). - Definition In x m := In0 x m.(this). - Definition Empty m := Empty m.(this). - - Definition eq_key := @Raw.PX.eqk elt. - Definition eq_key_elt := @Raw.PX.eqke elt. - Definition lt_key := @Raw.PX.ltk elt. - - Definition MapsTo_1 m := @MapsTo_1 _ m.(this). + Bbst (Raw.map2_bst f m m') (Raw.map2_avl f m m'). + Definition elements m : list (key*elt) := Raw.elements m.(this). + Definition fold (A:Set) (f:key->elt->A->A) m i := Raw.fold (A:=A) f m.(this) i. + Definition equal cmp m m' : bool := + if (Raw.equal cmp m.(is_bst) m'.(is_bst)) then true else false. + + Definition MapsTo x e m : Prop := Raw.MapsTo x e m.(this). + Definition In x m : Prop := Raw.In0 x m.(this). + Definition Empty m : Prop := Raw.Empty m.(this). + + Definition eq_key : (key*elt) -> (key*elt) -> Prop := @Raw.PX.eqk elt. + Definition eq_key_elt : (key*elt) -> (key*elt) -> Prop := @Raw.PX.eqke elt. + Definition lt_key : (key*elt) -> (key*elt) -> Prop := @Raw.PX.ltk elt. + + Lemma MapsTo_1 : forall m x y e, E.eq x y -> MapsTo x e m -> MapsTo y e m. + Proof. intros m; exact (@Raw.MapsTo_1 _ m.(this)). Qed. Lemma mem_1 : forall m x, In x m -> mem x m = true. Proof. - unfold In, mem; intros m x; rewrite In_alt; simpl; apply mem_1; auto. + unfold In, mem; intros m x; rewrite Raw.In_alt; simpl; apply Raw.mem_1; auto. apply m.(is_bst). Qed. Lemma mem_2 : forall m x, mem x m = true -> In x m. Proof. - unfold In, mem; intros m x; rewrite In_alt; simpl; apply mem_2; auto. + unfold In, mem; intros m x; rewrite Raw.In_alt; simpl; apply Raw.mem_2; auto. Qed. - Definition empty_1 := empty_1. + Lemma empty_1 : Empty empty. + Proof. exact (@Raw.empty_1 elt). Qed. - Definition is_empty_1 m := @is_empty_1 _ m.(this). - Definition is_empty_2 m := @is_empty_2 _ m.(this). + Lemma is_empty_1 : forall m, Empty m -> is_empty m = true. + Proof. intros m; exact (@Raw.is_empty_1 _ m.(this)). Qed. + Lemma is_empty_2 : forall m, is_empty m = true -> Empty m. + Proof. intros m; exact (@Raw.is_empty_2 _ m.(this)). Qed. - Definition add_1 m x y e := @add_1 elt m.(this) x y e m.(is_avl). - Definition add_2 m x y e e':= @add_2 elt m.(this) x y e e' m.(is_avl). - Definition add_3 m x y e e' := @add_3 elt m.(this) x y e e' m.(is_avl). + Lemma add_1 : forall m x y e, E.eq x y -> MapsTo y e (add x e m). + Proof. intros m x y e; exact (@Raw.add_1 elt _ x y e m.(is_avl)). Qed. + Lemma add_2 : forall m x y e e', ~ E.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m). + Proof. intros m x y e e'; exact (@Raw.add_2 elt _ x y e e' m.(is_avl)). Qed. + Lemma add_3 : forall m x y e e', ~ E.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m. + Proof. intros m x y e e'; exact (@Raw.add_3 elt _ x y e e' m.(is_avl)). Qed. Lemma remove_1 : forall m x y, E.eq x y -> ~ In y (remove x m). Proof. - unfold In, remove; intros m x y; rewrite In_alt; simpl; apply remove_1; auto. + unfold In, remove; intros m x y; rewrite Raw.In_alt; simpl; apply Raw.remove_1; auto. apply m.(is_bst). apply m.(is_avl). Qed. + Lemma remove_2 : forall m x y e, ~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m). + Proof. intros m x y e; exact (@Raw.remove_2 elt _ x y e m.(is_bst) m.(is_avl)). Qed. + Lemma remove_3 : forall m x y e, MapsTo y e (remove x m) -> MapsTo y e m. + Proof. intros m x y e; exact (@Raw.remove_3 elt _ x y e m.(is_bst) m.(is_avl)). Qed. - Definition remove_2 m x y e := @remove_2 elt m.(this) x y e m.(is_bst) m.(is_avl). - Definition remove_3 m x y e := @remove_3 elt m.(this) x y e m.(is_bst) m.(is_avl). - - Definition find_1 m x e := @find_1 elt m.(this) x e m.(is_bst). - Definition find_2 m x e := @find_2 elt m.(this) x e. - Definition fold_1 m := @fold_1 elt m.(this) m.(is_bst). + Lemma find_1 : forall m x e, MapsTo x e m -> find x m = Some e. + Proof. intros m x e; exact (@Raw.find_1 elt _ x e m.(is_bst)). Qed. + Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m. + Proof. intros m; exact (@Raw.find_2 elt m.(this)). Qed. - Definition map_1 m x e f := @map_1 elt elt' f m.(this) x e. - Lemma map_2 : forall m x f, In0 x (map f m) -> In0 x m. - Proof. - intros m x f; do 2 rewrite In_alt; simpl; apply map_2; auto. - Qed. - - Definition mapi_1 m x e f := @mapi_1 elt elt' f m.(this) x e. - Lemma mapi_2 : forall m x f, In0 x (mapi f m) -> In0 x m. - Proof. - intros m x f; do 2 rewrite In_alt; simpl; apply mapi_2; auto. - Qed. + Lemma fold_1 : forall m (A : Set) (i : A) (f : key -> elt -> A -> A), + fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i. + Proof. intros m; exact (@Raw.fold_1 elt m.(this) m.(is_bst)). Qed. Lemma elements_1 : forall m x e, MapsTo x e m -> InA eq_key_elt (x,e) (elements m). Proof. - intros; unfold elements, MapsTo, eq_key_elt; rewrite elements_mapsto; auto. + intros; unfold elements, MapsTo, eq_key_elt; rewrite Raw.elements_mapsto; auto. Qed. Lemma elements_2 : forall m x e, InA eq_key_elt (x,e) (elements m) -> MapsTo x e m. Proof. - intros; unfold elements, MapsTo, eq_key_elt; rewrite <- elements_mapsto; auto. + intros; unfold elements, MapsTo, eq_key_elt; rewrite <- Raw.elements_mapsto; auto. Qed. - - Definition elements_3 m := @elements_sort elt m.(this) m.(is_bst). + + Lemma elements_3 : forall m, sort lt_key (elements m). + Proof. intros m; exact (@Raw.elements_sort elt m.(this) m.(is_bst)). Qed. Definition Equal cmp m m' := (forall k, In k m <-> In k m') /\ @@ -1811,10 +1815,10 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Lemma Equal_Equal : forall cmp m m', Equal cmp m m' <-> Raw.Equal cmp m m'. Proof. intros; unfold Equal, Raw.Equal, In; intuition. - generalize (H0 k); do 2 rewrite In_alt; intuition. - generalize (H0 k); do 2 rewrite In_alt; intuition. - generalize (H0 k); do 2 rewrite <- In_alt; intuition. - generalize (H0 k); do 2 rewrite <- In_alt; intuition. + generalize (H0 k); do 2 rewrite Raw.In_alt; intuition. + generalize (H0 k); do 2 rewrite Raw.In_alt; intuition. + generalize (H0 k); do 2 rewrite <- Raw.In_alt; intuition. + generalize (H0 k); do 2 rewrite <- Raw.In_alt; intuition. Qed. Lemma equal_1 : forall m m' cmp, @@ -1833,13 +1837,33 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. End Elt. + Lemma map_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt)(f:elt->elt'), + MapsTo x e m -> MapsTo x (f e) (map f m). + Proof. intros elt elt' m x e f; exact (@Raw.map_1 elt elt' f m.(this) x e). Qed. + + Lemma map_2 : forall (elt elt':Set)(m:t elt)(x:key)(f:elt->elt'), In x (map f m) -> In x m. + Proof. + intros elt elt' m x f; do 2 unfold In in *; do 2 rewrite Raw.In_alt; simpl. + apply Raw.map_2; auto. + Qed. + + Lemma mapi_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt) + (f:key->elt->elt'), MapsTo x e m -> + exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m). + Proof. intros elt elt' m x e f; exact (@Raw.mapi_1 elt elt' f m.(this) x e). Qed. + Lemma mapi_2 : forall (elt elt':Set)(m: t elt)(x:key) + (f:key->elt->elt'), In x (mapi f m) -> In x m. + Proof. + intros elt elt' m x f; unfold In in *; do 2 rewrite Raw.In_alt; simpl; apply Raw.mapi_2; auto. + Qed. + Lemma map2_1 : forall (elt elt' elt'':Set)(m: t elt)(m': t elt') (x:key)(f:option elt->option elt'->option elt''), In x m \/ In x m' -> find x (map2 f m m') = f (find x m) (find x m'). Proof. unfold find, map2, In; intros elt elt' elt'' m m' x f. - do 2 rewrite In_alt; intros; simpl; apply map2_1; auto. + do 2 rewrite Raw.In_alt; intros; simpl; apply Raw.map2_1; auto. apply m.(is_bst). apply m'.(is_bst). Qed. @@ -1849,7 +1873,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. In x (map2 f m m') -> In x m \/ In x m'. Proof. unfold In, map2; intros elt elt' elt'' m m' x f. - do 3 rewrite In_alt; intros; simpl in *; eapply map2_2; eauto. + do 3 rewrite Raw.In_alt; intros; simpl in *; eapply Raw.map2_2; eauto. apply m.(is_bst). apply m'.(is_bst). Qed. diff --git a/theories/FSets/FMapIntMap.v b/theories/FSets/FMapIntMap.v index 5e4da1cd6..90df4019f 100644 --- a/theories/FSets/FMapIntMap.v +++ b/theories/FSets/FMapIntMap.v @@ -437,11 +437,11 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType. red; auto. case_eq (find x m); intros. apply find_1. - apply add_2; auto. + apply add_2; unfold E.eq in *; auto. case_eq (find x (add y e m)); auto; intros. rewrite <- H; symmetry. apply find_1; auto. - apply (@add_3 _ m y x a e); auto. + apply (@add_3 _ m y x a e); unfold E.eq in *; auto. Qed. Lemma anti_elements_mapsto_aux : forall (A:Set)(l:list (key*A)) m k e, @@ -482,10 +482,10 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType. red; auto. inversion_clear H. destruct (ME.eq_dec k0 k). - subst. + unfold E.eq in *; subst. destruct (H0 k); eauto. red; eauto. - right; apply add_2; auto. + right; apply add_2; unfold E.eq in *; auto. Qed. Lemma anti_elements_mapsto : forall (A:Set) l k e, NoDupA (eq_key (A:=A)) l -> diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v index 8a75228bb..4b2761f10 100644 --- a/theories/FSets/FMapList.v +++ b/theories/FSets/FMapList.v @@ -1006,84 +1006,126 @@ Module Make (X: OrderedType) <: S with Module E := X. Module Raw := Raw X. Module E := X. -Definition key := X.t. +Definition key := E.t. Record slist (elt:Set) : Set := {this :> Raw.t elt; sorted : sort (@Raw.PX.ltk elt) this}. -Definition t (elt:Set) := slist elt. +Definition t (elt:Set) : Set := slist elt. Section Elt. Variable elt elt' elt'':Set. Implicit Types m : t elt. - - Definition empty := Build_slist (Raw.empty_sorted elt). - Definition is_empty m := Raw.is_empty m.(this). - Definition add x e m := Build_slist (Raw.add_sorted m.(sorted) x e). - Definition find x m := Raw.find x m.(this). - Definition remove x m := Build_slist (Raw.remove_sorted m.(sorted) x). - Definition mem x m := Raw.mem x m.(this). + Implicit Types x y : key. + Implicit Types e : elt. + + Definition empty : t elt := Build_slist (Raw.empty_sorted elt). + Definition is_empty m : bool := Raw.is_empty m.(this). + Definition add x e m : t elt := Build_slist (Raw.add_sorted m.(sorted) x e). + Definition find x m : option elt := Raw.find x m.(this). + Definition remove x m : t elt := Build_slist (Raw.remove_sorted m.(sorted) x). + Definition mem x m : bool := Raw.mem x m.(this). Definition map f m : t elt' := Build_slist (Raw.map_sorted m.(sorted) f). - Definition mapi f m : t elt' := Build_slist (Raw.mapi_sorted m.(sorted) f). + Definition mapi (f:key->elt->elt') m : t elt' := Build_slist (Raw.mapi_sorted m.(sorted) f). Definition map2 f m (m':t elt') : t elt'' := - Build_slist (Raw.map2_sorted f m.(sorted) m'.(sorted)). - Definition elements m := @Raw.elements elt m.(this). - Definition fold A f m i := @Raw.fold elt A f m.(this) i. - Definition equal cmp m m' := @Raw.equal elt cmp m.(this) m'.(this). - - Definition MapsTo x e m := Raw.PX.MapsTo x e m.(this). - Definition In x m := Raw.PX.In x m.(this). - Definition Empty m := Raw.Empty m.(this). - Definition Equal cmp m m' := @Raw.Equal elt cmp m.(this) m'.(this). - - Definition eq_key := Raw.PX.eqk. - Definition eq_key_elt := Raw.PX.eqke. - Definition lt_key := Raw.PX.ltk. - - Definition MapsTo_1 m := @Raw.PX.MapsTo_eq elt m.(this). - - Definition mem_1 m := @Raw.mem_1 elt m.(this) m.(sorted). - Definition mem_2 m := @Raw.mem_2 elt m.(this) m.(sorted). - - Definition empty_1 := @Raw.empty_1. - - Definition is_empty_1 m := @Raw.is_empty_1 elt m.(this). - Definition is_empty_2 m := @Raw.is_empty_2 elt m.(this). - - Definition add_1 m := @Raw.add_1 elt m.(this). - Definition add_2 m := @Raw.add_2 elt m.(this). - Definition add_3 m := @Raw.add_3 elt m.(this). - - Definition remove_1 m := @Raw.remove_1 elt m.(this) m.(sorted). - Definition remove_2 m := @Raw.remove_2 elt m.(this) m.(sorted). - Definition remove_3 m := @Raw.remove_3 elt m.(this) m.(sorted). - - Definition find_1 m := @Raw.find_1 elt m.(this) m.(sorted). - Definition find_2 m := @Raw.find_2 elt m.(this). - - Definition elements_1 m := @Raw.elements_1 elt m.(this). - Definition elements_2 m := @Raw.elements_2 elt m.(this). - Definition elements_3 m := @Raw.elements_3 elt m.(this) m.(sorted). - - Definition fold_1 m := @Raw.fold_1 elt m.(this). - - Definition map_1 m := @Raw.map_1 elt elt' m.(this). - Definition map_2 m := @Raw.map_2 elt elt' m.(this). - - Definition mapi_1 m := @Raw.mapi_1 elt elt' m.(this). - Definition mapi_2 m := @Raw.mapi_2 elt elt' m.(this). - - Definition map2_1 m (m':t elt') x f := - @Raw.map2_1 elt elt' elt'' f m.(this) m.(sorted) m'.(this) m'.(sorted) x. - Definition map2_2 m (m':t elt') x f := - @Raw.map2_2 elt elt' elt'' f m.(this) m.(sorted) m'.(this) m'.(sorted) x. - - Definition equal_1 m m' := - @Raw.equal_1 elt m.(this) m.(sorted) m'.(this) m'.(sorted). - Definition equal_2 m m' := - @Raw.equal_2 elt m.(this) m.(sorted) m'.(this) m'.(sorted). + Build_slist (Raw.map2_sorted f m.(sorted) m'.(sorted)). + Definition elements m : list (key*elt) := @Raw.elements elt m.(this). + Definition fold (A:Set)(f:key->elt->A->A) m (i:A) : A := @Raw.fold elt A f m.(this) i. + Definition equal cmp m m' : bool := @Raw.equal elt cmp m.(this) m'.(this). + + Definition MapsTo x e m : Prop := Raw.PX.MapsTo x e m.(this). + Definition In x m : Prop := Raw.PX.In x m.(this). + Definition Empty m : Prop := Raw.Empty m.(this). + Definition Equal cmp m m' : Prop := @Raw.Equal elt cmp m.(this) m'.(this). + + Definition eq_key : (key*elt) -> (key*elt) -> Prop := @Raw.PX.eqk elt. + Definition eq_key_elt : (key*elt) -> (key*elt) -> Prop:= @Raw.PX.eqke elt. + Definition lt_key : (key*elt) -> (key*elt) -> Prop := @Raw.PX.ltk elt. + + Lemma MapsTo_1 : forall m x y e, E.eq x y -> MapsTo x e m -> MapsTo y e m. + Proof. intros m; exact (@Raw.PX.MapsTo_eq elt m.(this)). Qed. + + Lemma mem_1 : forall m x, In x m -> mem x m = true. + Proof. intros m; exact (@Raw.mem_1 elt m.(this) m.(sorted)). Qed. + Lemma mem_2 : forall m x, mem x m = true -> In x m. + Proof. intros m; exact (@Raw.mem_2 elt m.(this) m.(sorted)). Qed. + + Lemma empty_1 : Empty empty. + Proof. exact (@Raw.empty_1 elt). Qed. + + Lemma is_empty_1 : forall m, Empty m -> is_empty m = true. + Proof. intros m; exact (@Raw.is_empty_1 elt m.(this)). Qed. + Lemma is_empty_2 : forall m, is_empty m = true -> Empty m. + Proof. intros m; exact (@Raw.is_empty_2 elt m.(this)). Qed. + + Lemma add_1 : forall m x y e, E.eq x y -> MapsTo y e (add x e m). + Proof. intros m; exact (@Raw.add_1 elt m.(this)). Qed. + Lemma add_2 : forall m x y e e', ~ E.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m). + Proof. intros m; exact (@Raw.add_2 elt m.(this)). Qed. + Lemma add_3 : forall m x y e e', ~ E.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m. + Proof. intros m; exact (@Raw.add_3 elt m.(this)). Qed. + + Lemma remove_1 : forall m x y, E.eq x y -> ~ In y (remove x m). + Proof. intros m; exact (@Raw.remove_1 elt m.(this) m.(sorted)). Qed. + Lemma remove_2 : forall m x y e, ~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m). + Proof. intros m; exact (@Raw.remove_2 elt m.(this) m.(sorted)). Qed. + Lemma remove_3 : forall m x y e, MapsTo y e (remove x m) -> MapsTo y e m. + Proof. intros m; exact (@Raw.remove_3 elt m.(this) m.(sorted)). Qed. + + Lemma find_1 : forall m x e, MapsTo x e m -> find x m = Some e. + Proof. intros m; exact (@Raw.find_1 elt m.(this) m.(sorted)). Qed. + Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m. + Proof. intros m; exact (@Raw.find_2 elt m.(this)). Qed. + + Lemma elements_1 : forall m x e, MapsTo x e m -> InA eq_key_elt (x,e) (elements m). + Proof. intros m; exact (@Raw.elements_1 elt m.(this)). Qed. + Lemma elements_2 : forall m x e, InA eq_key_elt (x,e) (elements m) -> MapsTo x e m. + Proof. intros m; exact (@Raw.elements_2 elt m.(this)). Qed. + Lemma elements_3 : forall m, sort lt_key (elements m). + Proof. intros m; exact (@Raw.elements_3 elt m.(this) m.(sorted)). Qed. + + Lemma fold_1 : forall m (A : Set) (i : A) (f : key -> elt -> A -> A), + fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i. + Proof. intros m; exact (@Raw.fold_1 elt m.(this)). Qed. + + Lemma equal_1 : forall m m' cmp, Equal cmp m m' -> equal cmp m m' = true. + Proof. intros m m'; exact (@Raw.equal_1 elt m.(this) m.(sorted) m'.(this) m'.(sorted)). Qed. + Lemma equal_2 : forall m m' cmp, equal cmp m m' = true -> Equal cmp m m'. + Proof. intros m m'; exact (@Raw.equal_2 elt m.(this) m.(sorted) m'.(this) m'.(sorted)). Qed. End Elt. + + Lemma map_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt)(f:elt->elt'), + MapsTo x e m -> MapsTo x (f e) (map f m). + Proof. intros elt elt' m; exact (@Raw.map_1 elt elt' m.(this)). Qed. + Lemma map_2 : forall (elt elt':Set)(m: t elt)(x:key)(f:elt->elt'), + In x (map f m) -> In x m. + Proof. intros elt elt' m; exact (@Raw.map_2 elt elt' m.(this)). Qed. + + Lemma mapi_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt) + (f:key->elt->elt'), MapsTo x e m -> + exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m). + Proof. intros elt elt' m; exact (@Raw.mapi_1 elt elt' m.(this)). Qed. + Lemma mapi_2 : forall (elt elt':Set)(m: t elt)(x:key) + (f:key->elt->elt'), In x (mapi f m) -> In x m. + Proof. intros elt elt' m; exact (@Raw.mapi_2 elt elt' m.(this)). Qed. + + Lemma map2_1 : forall (elt elt' elt'':Set)(m: t elt)(m': t elt') + (x:key)(f:option elt->option elt'->option elt''), + In x m \/ In x m' -> + find x (map2 f m m') = f (find x m) (find x m'). + Proof. + intros elt elt' elt'' m m' x f; + exact (@Raw.map2_1 elt elt' elt'' f m.(this) m.(sorted) m'.(this) m'.(sorted) x). + Qed. + Lemma map2_2 : forall (elt elt' elt'':Set)(m: t elt)(m': t elt') + (x:key)(f:option elt->option elt'->option elt''), + In x (map2 f m m') -> In x m \/ In x m'. + Proof. + intros elt elt' elt'' m m' x f; + exact (@Raw.map2_2 elt elt' elt'' f m.(this) m.(sorted) m'.(this) m'.(sorted) x). + Qed. + End Make. Module Make_ord (X: OrderedType)(D : OrderedType) <: diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v index bfa97d0b2..dc034bf83 100644 --- a/theories/FSets/FMapWeakList.v +++ b/theories/FSets/FMapWeakList.v @@ -878,83 +878,124 @@ Module Make (X: DecidableType) <: S with Module E:=X. Module Raw := Raw X. Module E := X. - Definition key := X.t. + Definition key := E.t. Record slist (elt:Set) : Set := {this :> Raw.t elt; NoDup : NoDupA (@Raw.PX.eqk elt) this}. Definition t (elt:Set) := slist elt. - Section Elt. +Section Elt. Variable elt elt' elt'':Set. Implicit Types m : t elt. - - Definition empty := Build_slist (Raw.empty_NoDup elt). - Definition is_empty m := Raw.is_empty m.(this). - Definition add x e m := Build_slist (Raw.add_NoDup m.(NoDup) x e). - Definition find x m := Raw.find x m.(this). - Definition remove x m := Build_slist (Raw.remove_NoDup m.(NoDup) x). - Definition mem x m := Raw.mem x m.(this). + Implicit Types x y : key. + Implicit Types e : elt. + + Definition empty : t elt := Build_slist (Raw.empty_NoDup elt). + Definition is_empty m : bool := Raw.is_empty m.(this). + Definition add x e m : t elt := Build_slist (Raw.add_NoDup m.(NoDup) x e). + Definition find x m : option elt := Raw.find x m.(this). + Definition remove x m : t elt := Build_slist (Raw.remove_NoDup m.(NoDup) x). + Definition mem x m : bool := Raw.mem x m.(this). Definition map f m : t elt' := Build_slist (Raw.map_NoDup m.(NoDup) f). - Definition mapi f m : t elt' := Build_slist (Raw.mapi_NoDup m.(NoDup) f). + Definition mapi (f:key->elt->elt') m : t elt' := Build_slist (Raw.mapi_NoDup m.(NoDup) f). Definition map2 f m (m':t elt') : t elt'' := - Build_slist (Raw.map2_NoDup f m.(NoDup) m'.(NoDup)). - Definition elements m := @Raw.elements elt m.(this). - Definition fold A f m i := @Raw.fold elt A f m.(this) i. - Definition equal cmp m m' := @Raw.equal elt cmp m.(this) m'.(this). - - Definition MapsTo x e m := Raw.PX.MapsTo x e m.(this). - Definition In x m := Raw.PX.In x m.(this). - Definition Empty m := Raw.Empty m.(this). - Definition Equal cmp m m' := @Raw.Equal elt cmp m.(this) m'.(this). + Build_slist (Raw.map2_NoDup f m.(NoDup) m'.(NoDup)). + Definition elements m : list (key*elt) := @Raw.elements elt m.(this). + Definition fold (A:Set)(f:key->elt->A->A) m (i:A) : A := @Raw.fold elt A f m.(this) i. + Definition equal cmp m m' : bool := @Raw.equal elt cmp m.(this) m'.(this). + + Definition MapsTo x e m : Prop := Raw.PX.MapsTo x e m.(this). + Definition In x m : Prop := Raw.PX.In x m.(this). + Definition Empty m : Prop := Raw.Empty m.(this). + Definition Equal cmp m m' : Prop := @Raw.Equal elt cmp m.(this) m'.(this). + + Definition eq_key : (key*elt) -> (key*elt) -> Prop := @Raw.PX.eqk elt. + Definition eq_key_elt : (key*elt) -> (key*elt) -> Prop:= @Raw.PX.eqke elt. + + Lemma MapsTo_1 : forall m x y e, E.eq x y -> MapsTo x e m -> MapsTo y e m. + Proof. intros m; exact (@Raw.PX.MapsTo_eq elt m.(this)). Qed. + + Lemma mem_1 : forall m x, In x m -> mem x m = true. + Proof. intros m; exact (@Raw.mem_1 elt m.(this) m.(NoDup)). Qed. + Lemma mem_2 : forall m x, mem x m = true -> In x m. + Proof. intros m; exact (@Raw.mem_2 elt m.(this) m.(NoDup)). Qed. + + Lemma empty_1 : Empty empty. + Proof. exact (@Raw.empty_1 elt). Qed. + + Lemma is_empty_1 : forall m, Empty m -> is_empty m = true. + Proof. intros m; exact (@Raw.is_empty_1 elt m.(this)). Qed. + Lemma is_empty_2 : forall m, is_empty m = true -> Empty m. + Proof. intros m; exact (@Raw.is_empty_2 elt m.(this)). Qed. + + Lemma add_1 : forall m x y e, E.eq x y -> MapsTo y e (add x e m). + Proof. intros m; exact (@Raw.add_1 elt m.(this)). Qed. + Lemma add_2 : forall m x y e e', ~ E.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m). + Proof. intros m; exact (@Raw.add_2 elt m.(this)). Qed. + Lemma add_3 : forall m x y e e', ~ E.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m. + Proof. intros m; exact (@Raw.add_3 elt m.(this)). Qed. + + Lemma remove_1 : forall m x y, E.eq x y -> ~ In y (remove x m). + Proof. intros m; exact (@Raw.remove_1 elt m.(this) m.(NoDup)). Qed. + Lemma remove_2 : forall m x y e, ~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m). + Proof. intros m; exact (@Raw.remove_2 elt m.(this) m.(NoDup)). Qed. + Lemma remove_3 : forall m x y e, MapsTo y e (remove x m) -> MapsTo y e m. + Proof. intros m; exact (@Raw.remove_3 elt m.(this) m.(NoDup)). Qed. + + Lemma find_1 : forall m x e, MapsTo x e m -> find x m = Some e. + Proof. intros m; exact (@Raw.find_1 elt m.(this) m.(NoDup)). Qed. + Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m. + Proof. intros m; exact (@Raw.find_2 elt m.(this)). Qed. + + Lemma elements_1 : forall m x e, MapsTo x e m -> InA eq_key_elt (x,e) (elements m). + Proof. intros m; exact (@Raw.elements_1 elt m.(this)). Qed. + Lemma elements_2 : forall m x e, InA eq_key_elt (x,e) (elements m) -> MapsTo x e m. + Proof. intros m; exact (@Raw.elements_2 elt m.(this)). Qed. + Lemma elements_3 : forall m, NoDupA eq_key (elements m). + Proof. intros m; exact (@Raw.elements_3 elt m.(this) m.(NoDup)). Qed. + + Lemma fold_1 : forall m (A : Set) (i : A) (f : key -> elt -> A -> A), + fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i. + Proof. intros m; exact (@Raw.fold_1 elt m.(this)). Qed. + + Lemma equal_1 : forall m m' cmp, Equal cmp m m' -> equal cmp m m' = true. + Proof. intros m m'; exact (@Raw.equal_1 elt m.(this) m.(NoDup) m'.(this) m'.(NoDup)). Qed. + Lemma equal_2 : forall m m' cmp, equal cmp m m' = true -> Equal cmp m m'. + Proof. intros m m'; exact (@Raw.equal_2 elt m.(this) m.(NoDup) m'.(this) m'.(NoDup)). Qed. - Definition eq_key (p p':key*elt) := X.eq (fst p) (fst p'). + End Elt. - Definition eq_key_elt (p p':key*elt) := - X.eq (fst p) (fst p') /\ (snd p) = (snd p'). - - Definition MapsTo_1 m := @Raw.PX.MapsTo_eq elt m.(this). - - Definition mem_1 m := @Raw.mem_1 elt m.(this) m.(NoDup). - Definition mem_2 m := @Raw.mem_2 elt m.(this) m.(NoDup). - - Definition empty_1 := @Raw.empty_1. - - Definition is_empty_1 m := @Raw.is_empty_1 elt m.(this). - Definition is_empty_2 m := @Raw.is_empty_2 elt m.(this). - - Definition add_1 m := @Raw.add_1 elt m.(this). - Definition add_2 m := @Raw.add_2 elt m.(this). - Definition add_3 m := @Raw.add_3 elt m.(this). - - Definition remove_1 m := @Raw.remove_1 elt m.(this) m.(NoDup). - Definition remove_2 m := @Raw.remove_2 elt m.(this) m.(NoDup). - Definition remove_3 m := @Raw.remove_3 elt m.(this) m.(NoDup). + Lemma map_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt)(f:elt->elt'), + MapsTo x e m -> MapsTo x (f e) (map f m). + Proof. intros elt elt' m; exact (@Raw.map_1 elt elt' m.(this)). Qed. + Lemma map_2 : forall (elt elt':Set)(m: t elt)(x:key)(f:elt->elt'), + In x (map f m) -> In x m. + Proof. intros elt elt' m; exact (@Raw.map_2 elt elt' m.(this)). Qed. + + Lemma mapi_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt) + (f:key->elt->elt'), MapsTo x e m -> + exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m). + Proof. intros elt elt' m; exact (@Raw.mapi_1 elt elt' m.(this)). Qed. + Lemma mapi_2 : forall (elt elt':Set)(m: t elt)(x:key) + (f:key->elt->elt'), In x (mapi f m) -> In x m. + Proof. intros elt elt' m; exact (@Raw.mapi_2 elt elt' m.(this)). Qed. + + Lemma map2_1 : forall (elt elt' elt'':Set)(m: t elt)(m': t elt') + (x:key)(f:option elt->option elt'->option elt''), + In x m \/ In x m' -> + find x (map2 f m m') = f (find x m) (find x m'). + Proof. + intros elt elt' elt'' m m' x f; + exact (@Raw.map2_1 elt elt' elt'' f m.(this) m.(NoDup) m'.(this) m'.(NoDup) x). + Qed. + Lemma map2_2 : forall (elt elt' elt'':Set)(m: t elt)(m': t elt') + (x:key)(f:option elt->option elt'->option elt''), + In x (map2 f m m') -> In x m \/ In x m'. + Proof. + intros elt elt' elt'' m m' x f; + exact (@Raw.map2_2 elt elt' elt'' f m.(this) m.(NoDup) m'.(this) m'.(NoDup) x). + Qed. - Definition find_1 m := @Raw.find_1 elt m.(this) m.(NoDup). - Definition find_2 m := @Raw.find_2 elt m.(this). - - Definition elements_1 m := @Raw.elements_1 elt m.(this). - Definition elements_2 m := @Raw.elements_2 elt m.(this). - Definition elements_3 m := @Raw.elements_3 elt m.(this) m.(NoDup). - - Definition fold_1 m := @Raw.fold_1 elt m.(this). - - Definition map_1 m := @Raw.map_1 elt elt' m.(this). - Definition map_2 m := @Raw.map_2 elt elt' m.(this). - - Definition mapi_1 m := @Raw.mapi_1 elt elt' m.(this). - Definition mapi_2 m := @Raw.mapi_2 elt elt' m.(this). - - Definition map2_1 m (m':t elt') x f := - @Raw.map2_1 elt elt' elt'' f m.(this) m.(NoDup) m'.(this) m'.(NoDup) x. - Definition map2_2 m (m':t elt') x f := - @Raw.map2_2 elt elt' elt'' f m.(this) m.(NoDup) m'.(this) m'.(NoDup) x. - - Definition equal_1 m m' := @Raw.equal_1 elt m.(this) m.(NoDup) m'.(this) m'.(NoDup). - Definition equal_2 m m' := @Raw.equal_2 elt m.(this) m.(NoDup) m'.(this) m'.(NoDup). - - End Elt. End Make. - diff --git a/theories/FSets/FSetToFiniteSet.v b/theories/FSets/FSetToFiniteSet.v index 9dd5f2739..747fd3796 100644 --- a/theories/FSets/FSetToFiniteSet.v +++ b/theories/FSets/FSetToFiniteSet.v @@ -82,7 +82,7 @@ Module S_to_Finite_set (U:UsualOrderedType)(M:S with Module E := U). Lemma add_Add : forall x s, !!(add x s) === Add _ (!!s) x. Proof. unfold Same_set, Included, mkEns, In. - split; intro; set_iff; inversion 1; auto with sets. + split; intro; set_iff; inversion 1; unfold E.eq; auto with sets. inversion H0. constructor 2; constructor. constructor 1; auto. @@ -97,7 +97,7 @@ Module S_to_Finite_set (U:UsualOrderedType)(M:S with Module E := U). inversion H0. constructor 2; constructor. constructor 1; auto. - red in H; rewrite H. + red in H; rewrite H; unfold E.eq in *. inversion H0; auto. inversion H1; auto. Qed. @@ -105,7 +105,7 @@ Module S_to_Finite_set (U:UsualOrderedType)(M:S with Module E := U). Lemma remove_Subtract : forall x s, !!(remove x s) === Subtract _ (!!s) x. Proof. unfold Same_set, Included, mkEns, In. - split; intro; set_iff; inversion 1; auto with sets. + split; intro; set_iff; inversion 1; unfold E.eq in *; auto with sets. split; auto. swap H1. inversion H2; auto. |