diff options
Diffstat (limited to 'theories/FSets/FMapWeakList.v')
| -rw-r--r-- | theories/FSets/FMapWeakList.v | 960 |
1 files changed, 960 insertions, 0 deletions
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v new file mode 100644 index 00000000..ce3893e0 --- /dev/null +++ b/theories/FSets/FMapWeakList.v @@ -0,0 +1,960 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id: FMapWeakList.v 8639 2006-03-16 19:21:55Z letouzey $ *) + +(** * Finite map library *) + +(** This file proposes an implementation of the non-dependant interface + [FMapInterface.S] using lists of pairs, unordered but without redundancy. *) + +Require Import FSetInterface. +Require Import FSetWeakInterface. +Require Import FMapWeakInterface. + +Set Implicit Arguments. +Unset Strict Implicit. + +Arguments Scope list [type_scope]. + +Module Raw (X:DecidableType). + +Module PX := PairDecidableType X. +Import PX. + +Definition key := X.t. +Definition t (elt:Set) := list (X.t * elt). + +Section Elt. + +Variable elt : Set. + +(* now in PairDecidableType: +Definition eqk (p p':key*elt) := X.eq (fst p) (fst p'). +Definition eqke (p p':key*elt) := + X.eq (fst p) (fst p') /\ (snd p) = (snd p'). +*) + +Notation eqk := (eqk (elt:=elt)). +Notation eqke := (eqke (elt:=elt)). +Notation MapsTo := (MapsTo (elt:=elt)). +Notation In := (In (elt:=elt)). +Notation NoDupA := (NoDupA eqk). + +(** * [empty] *) + +Definition empty : t elt := nil. + +Definition Empty m := forall (a : key)(e:elt), ~ MapsTo a e m. + +Lemma empty_1 : Empty empty. +Proof. + unfold Empty,empty. + intros a e. + intro abs. + inversion abs. +Qed. + +Hint Resolve empty_1. + +Lemma empty_NoDup : NoDupA empty. +Proof. + unfold empty; auto. +Qed. + +(** * [is_empty] *) + +Definition is_empty (l : t elt) : bool := if l then true else false. + +Lemma is_empty_1 :forall m, Empty m -> is_empty m = true. +Proof. + unfold Empty, PX.MapsTo. + intros m. + case m;auto. + intros p l inlist. + destruct p. + absurd (InA eqke (t0, e) ((t0, e) :: l));auto. +Qed. + +Lemma is_empty_2 : forall m, is_empty m = true -> Empty m. +Proof. + intros m. + case m;auto. + intros p l abs. + inversion abs. +Qed. + +(** * [mem] *) + +Fixpoint mem (k : key) (s : t elt) {struct s} : bool := + match s with + | nil => false + | (k',_) :: l => if X.eq_dec k k' then true else mem k l + end. + +Lemma mem_1 : forall m (Hm:NoDupA m) x, In x m -> mem x m = true. +Proof. + intros m Hm x; generalize Hm; clear Hm. + functional induction mem x m;intros NoDup belong1;trivial. + inversion belong1. inversion H. + inversion_clear NoDup. + inversion_clear belong1. + inversion_clear H3. + compute in H4; destruct H4. + elim H; auto. + apply H0; auto. + exists x; auto. +Qed. + +Lemma mem_2 : forall m (Hm:NoDupA m) x, mem x m = true -> In x m. +Proof. + intros m Hm x; generalize Hm; clear Hm; unfold PX.In,PX.MapsTo. + functional induction mem x m; intros NoDup hyp; try discriminate. + exists e; auto. + inversion_clear NoDup. + destruct H0; auto. + exists x; auto. +Qed. + +(** * [find] *) + +Fixpoint find (k:key) (s: t elt) {struct s} : option elt := + match s with + | nil => None + | (k',x)::s' => if X.eq_dec k k' then Some x else find k s' + end. + +Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m. +Proof. + intros m x. unfold PX.MapsTo. + functional induction find x m;simpl;intros e' eqfind; inversion eqfind; auto. +Qed. + +Lemma find_1 : forall m (Hm:NoDupA m) x e, + MapsTo x e m -> find x m = Some e. +Proof. + intros m Hm x e; generalize Hm; clear Hm; unfold PX.MapsTo. + functional induction find x m;simpl; subst; try clear H_eq_1. + + inversion 2. + + do 2 inversion_clear 1. + compute in H3; destruct H3; subst; trivial. + elim H0; apply InA_eqk with (k,e); auto. + + do 2 inversion_clear 1; auto. + compute in H4; destruct H4; elim H; auto. +Qed. + +(* Not part of the exported specifications, used later for [combine]. *) + +Lemma find_eq : forall m (Hm:NoDupA m) x x', + X.eq x x' -> find x m = find x' m. +Proof. + induction m; simpl; auto; destruct a; intros. + inversion_clear Hm. + rewrite (IHm H1 x x'); auto. + destruct (X.eq_dec x t0); destruct (X.eq_dec x' t0); trivial. + elim n; apply X.eq_trans with x; auto. + elim n; apply X.eq_trans with x'; auto. +Qed. + +(** * [add] *) + +Fixpoint add (k : key) (x : elt) (s : t elt) {struct s} : t elt := + match s with + | nil => (k,x) :: nil + | (k',y) :: l => if X.eq_dec k k' then (k,x)::l else (k',y)::add k x l + end. + +Lemma add_1 : forall m x y e, X.eq x y -> MapsTo y e (add x e m). +Proof. + intros m x y e; generalize y; clear y; unfold PX.MapsTo. + functional induction add x e m;simpl;auto. +Qed. + +Lemma add_2 : forall m x y e e', + ~ X.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m). +Proof. + intros m x y e e'; generalize y e; clear y e; unfold PX.MapsTo. + functional induction add x e' m;simpl;auto. + intros y' e' eqky'; inversion_clear 1. + destruct H1; simpl in *. + elim eqky'; apply X.eq_trans with k'; auto. + auto. + intros y' e' eqky'; inversion_clear 1; intuition. +Qed. + +Lemma add_3 : forall m x y e e', + ~ X.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m. +Proof. + intros m x y e e'. generalize y e; clear y e; unfold PX.MapsTo. + functional induction add x e' m;simpl;auto. + intros; apply (In_inv_3 H0); auto. + constructor 2; apply (In_inv_3 H1); auto. + inversion_clear 2; auto. +Qed. + +Lemma add_3' : forall m x y e e', + ~ X.eq x y -> InA eqk (y,e) (add x e' m) -> InA eqk (y,e) m. +Proof. + intros m x y e e'. generalize y e; clear y e. + functional induction add x e' m;simpl;auto. + inversion_clear 2. + compute in H1; elim H; auto. + inversion H1. + constructor 2; inversion_clear H1; auto. + compute in H2; elim H0; auto. + inversion_clear 2; auto. +Qed. + +Lemma add_NoDup : forall m (Hm:NoDupA m) x e, NoDupA (add x e m). +Proof. + induction m. + simpl; constructor; auto; red; inversion 1. + intros. + destruct a as (x',e'). + simpl; case (X.eq_dec x x'); inversion_clear Hm; auto. + constructor; auto. + swap H. + apply InA_eqk with (x,e); auto. + constructor; auto. + swap H; apply add_3' with x e; auto. +Qed. + +(* Not part of the exported specifications, used later for [combine]. *) + +Lemma add_eq : forall m (Hm:NoDupA m) x a e, + X.eq x a -> find x (add a e m) = Some e. +Proof. + intros. + apply find_1; auto. + apply add_NoDup; auto. + apply add_1; auto. +Qed. + +Lemma add_not_eq : forall m (Hm:NoDupA m) x a e, + ~X.eq x a -> find x (add a e m) = find x m. +Proof. + intros. + case_eq (find x m); intros. + apply find_1; auto. + apply add_NoDup; auto. + apply add_2; auto. + apply find_2; auto. + case_eq (find x (add a e m)); intros; auto. + rewrite <- H0; symmetry. + apply find_1; auto. + apply add_3 with a e; auto. + apply find_2; auto. +Qed. + + +(** * [remove] *) + +Fixpoint remove (k : key) (s : t elt) {struct s} : t elt := + match s with + | nil => nil + | (k',x) :: l => if X.eq_dec k k' then l else (k',x) :: remove k l + end. + +Lemma remove_1 : forall m (Hm:NoDupA m) x y, X.eq x y -> ~ In y (remove x m). +Proof. + intros m Hm x y; generalize Hm; clear Hm. + functional induction remove x m;simpl;intros;auto. + + red; inversion 1; inversion H1. + + inversion_clear Hm. + subst. + swap H1. + destruct H3 as (e,H3); unfold PX.MapsTo in H3. + apply InA_eqk with (y,e); auto. + compute; apply X.eq_trans with k; auto. + + intro H2. + destruct H2 as (e,H2); inversion_clear H2. + compute in H3; destruct H3. + elim H; apply X.eq_trans with y; auto. + inversion_clear Hm. + elim (H0 H4 H1). + exists e; auto. +Qed. + +Lemma remove_2 : forall m (Hm:NoDupA m) x y e, + ~ X.eq x y -> MapsTo y e m -> MapsTo y e (remove x m). +Proof. + intros m Hm x y e; generalize Hm; clear Hm; unfold PX.MapsTo. + functional induction remove x m;auto. + inversion_clear 3; auto. + compute in H2; destruct H2. + elim H0; apply X.eq_trans with k'; auto. + + inversion_clear 1; inversion_clear 2; auto. +Qed. + +Lemma remove_3 : forall m (Hm:NoDupA m) x y e, + MapsTo y e (remove x m) -> MapsTo y e m. +Proof. + intros m Hm x y e; generalize Hm; clear Hm; unfold PX.MapsTo. + functional induction remove x m;auto. + do 2 inversion_clear 1; auto. +Qed. + +Lemma remove_3' : forall m (Hm:NoDupA m) x y e, + InA eqk (y,e) (remove x m) -> InA eqk (y,e) m. +Proof. + intros m Hm x y e; generalize Hm; clear Hm; unfold PX.MapsTo. + functional induction remove x m;auto. + do 2 inversion_clear 1; auto. +Qed. + +Lemma remove_NoDup : forall m (Hm:NoDupA m) x, NoDupA (remove x m). +Proof. + induction m. + simpl; intuition. + intros. + inversion_clear Hm. + destruct a as (x',e'). + simpl; case (X.eq_dec x x'); auto. + constructor; auto. + swap H; apply remove_3' with x; auto. +Qed. + +(** * [elements] *) + +Definition elements (m: t elt) := m. + +Lemma elements_1 : forall m x e, MapsTo x e m -> InA eqke (x,e) (elements m). +Proof. + auto. +Qed. + +Lemma elements_2 : forall m x e, InA eqke (x,e) (elements m) -> MapsTo x e m. +Proof. +auto. +Qed. + +Lemma elements_3 : forall m (Hm:NoDupA m), NoDupA (elements m). +Proof. + auto. +Qed. + +(** * [fold] *) + +Fixpoint fold (A:Set)(f:key->elt->A->A)(m:t elt) {struct m} : A -> A := + fun acc => + match m with + | nil => acc + | (k,e)::m' => fold f m' (f k e acc) + end. + +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; functional induction fold A f m i; auto. +Qed. + +(** * [equal] *) + +Definition check (cmp : elt -> elt -> bool)(k:key)(e:elt)(m': t elt) := + match find k m' with + | None => false + | Some e' => cmp e e' + end. + +Definition submap (cmp : elt -> elt -> bool)(m m' : t elt) : bool := + fold (fun k e b => andb (check cmp k e m') b) m true. + +Definition equal (cmp : elt -> elt -> bool)(m m' : t elt) : bool := + andb (submap cmp m m') (submap (fun e' e => cmp e e') m' m). + +Definition Submap cmp m m' := + (forall k, In k m -> In k m') /\ + (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true). + +Definition Equal cmp m m' := + (forall k, In k m <-> In k m') /\ + (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true). + +Lemma submap_1 : forall m (Hm:NoDupA m) m' (Hm': NoDupA m') cmp, + Submap cmp m m' -> submap cmp m m' = true. +Proof. + unfold Submap, submap. + induction m. + simpl; auto. + destruct a; simpl; intros. + destruct H. + inversion_clear Hm. + assert (H3 : In t0 m'). + apply H; exists e; auto. + destruct H3 as (e', H3). + unfold check at 2; rewrite (find_1 Hm' H3). + rewrite (H0 t0); simpl; auto. + eapply IHm; auto. + split; intuition. + apply H. + destruct H5 as (e'',H5); exists e''; auto. + apply H0 with k; auto. +Qed. + +Lemma submap_2 : forall m (Hm:NoDupA m) m' (Hm': NoDupA m') cmp, + submap cmp m m' = true -> Submap cmp m m'. +Proof. + unfold Submap, submap. + induction m. + simpl; auto. + intuition. + destruct H0; inversion H0. + inversion H0. + + destruct a; simpl; intros. + inversion_clear Hm. + rewrite andb_b_true in H. + assert (check cmp t0 e m' = true). + clear H1 H0 Hm' IHm. + set (b:=check cmp t0 e m') in *. + generalize H; clear H; generalize b; clear b. + induction m; simpl; auto; intros. + destruct a; simpl in *. + destruct (andb_prop _ _ (IHm _ H)); auto. + rewrite H2 in H. + destruct (IHm H1 m' Hm' cmp H); auto. + unfold check in H2. + case_eq (find t0 m'); [intros e' H5 | intros H5]; + rewrite H5 in H2; try discriminate. + split; intros. + destruct H6 as (e0,H6); inversion_clear H6. + compute in H7; destruct H7; subst. + exists e'. + apply PX.MapsTo_eq with t0; auto. + apply find_2; auto. + apply H3. + exists e0; auto. + inversion_clear H6. + compute in H8; destruct H8; subst. + rewrite (find_1 Hm' (PX.MapsTo_eq H6 H7)) in H5; congruence. + apply H4 with k; auto. +Qed. + +(** Specification of [equal] *) + +Lemma equal_1 : forall m (Hm:NoDupA m) m' (Hm': NoDupA m') cmp, + Equal cmp m m' -> equal cmp m m' = true. +Proof. + unfold Equal, equal. + intuition. + apply andb_true_intro; split; apply submap_1; unfold Submap; firstorder. +Qed. + +Lemma equal_2 : forall m (Hm:NoDupA m) m' (Hm':NoDupA m') cmp, + equal cmp m m' = true -> Equal cmp m m'. +Proof. + unfold Equal, equal. + intros. + destruct (andb_prop _ _ H); clear H. + generalize (submap_2 Hm Hm' H0). + generalize (submap_2 Hm' Hm H1). + firstorder. +Qed. + +Variable elt':Set. + +(** * [map] and [mapi] *) + +Fixpoint map (f:elt -> elt') (m:t elt) {struct m} : t elt' := + match m with + | nil => nil + | (k,e)::m' => (k,f e) :: map f m' + end. + +Fixpoint mapi (f: key -> elt -> elt') (m:t elt) {struct m} : t elt' := + match m with + | nil => nil + | (k,e)::m' => (k,f k e) :: mapi f m' + end. + +End Elt. +Section Elt2. +(* A new section is necessary for previous definitions to work + with different [elt], especially [MapsTo]... *) + +Variable elt elt' : Set. + +(** Specification of [map] *) + +Lemma map_1 : forall (m:t elt)(x:key)(e:elt)(f:elt->elt'), + MapsTo x e m -> MapsTo x (f e) (map f m). +Proof. + intros m x e f. + (* functional induction map elt elt' f m. *) (* Marche pas ??? *) + induction m. + inversion 1. + + destruct a as (x',e'). + simpl. + inversion_clear 1. + constructor 1. + unfold eqke in *; simpl in *; intuition congruence. + constructor 2. + unfold MapsTo in *; auto. +Qed. + +Lemma map_2 : forall (m:t elt)(x:key)(f:elt->elt'), + In x (map f m) -> In x m. +Proof. + intros m x f. + (* functional induction map elt elt' f m. *) (* Marche pas ??? *) + induction m; simpl. + intros (e,abs). + inversion abs. + + destruct a as (x',e). + intros hyp. + inversion hyp. clear hyp. + inversion H; subst; rename x0 into e'. + exists e; constructor. + unfold eqke in *; simpl in *; intuition. + destruct IHm as (e'',hyp). + exists e'; auto. + exists e''. + constructor 2; auto. +Qed. + +Lemma map_NoDup : forall m (Hm : NoDupA (@eqk elt) m)(f:elt->elt'), + NoDupA (@eqk elt') (map f m). +Proof. + induction m; simpl; auto. + intros. + destruct a as (x',e'). + inversion_clear Hm. + constructor; auto. + swap H. + (* il faut un map_1 avec eqk au lieu de eqke *) + clear IHm H0. + induction m; simpl in *; auto. + inversion H1. + destruct a; inversion H1; auto. +Qed. + +(** Specification of [mapi] *) + +Lemma mapi_1 : forall (m:t elt)(x:key)(e:elt)(f:key->elt->elt'), + MapsTo x e m -> + exists y, X.eq y x /\ MapsTo x (f y e) (mapi f m). +Proof. + intros m x e f. + (* functional induction mapi elt elt' f m. *) (* Marche pas ??? *) + induction m. + inversion 1. + + destruct a as (x',e'). + simpl. + inversion_clear 1. + exists x'. + destruct H0; simpl in *. + split; auto. + constructor 1. + unfold eqke in *; simpl in *; intuition congruence. + destruct IHm as (y, hyp); auto. + exists y; intuition. +Qed. + +Lemma mapi_2 : forall (m:t elt)(x:key)(f:key->elt->elt'), + In x (mapi f m) -> In x m. +Proof. + intros m x f. + (* functional induction mapi elt elt' f m. *) (* Marche pas ??? *) + induction m; simpl. + intros (e,abs). + inversion abs. + + destruct a as (x',e). + intros hyp. + inversion hyp. clear hyp. + inversion H; subst; rename x0 into e'. + exists e; constructor. + unfold eqke in *; simpl in *; intuition. + destruct IHm as (e'',hyp). + exists e'; auto. + exists e''. + constructor 2; auto. +Qed. + +Lemma mapi_NoDup : forall m (Hm : NoDupA (@eqk elt) m)(f: key->elt->elt'), + NoDupA (@eqk elt') (mapi f m). +Proof. + induction m; simpl; auto. + intros. + destruct a as (x',e'). + inversion_clear Hm; auto. + constructor; auto. + swap H. + clear IHm H0. + induction m; simpl in *; auto. + inversion_clear H1. + destruct a; inversion_clear H1; auto. +Qed. + +End Elt2. +Section Elt3. + +Variable elt elt' elt'' : Set. + +Notation oee' := (option elt * option elt')%type. + +Definition combine_l (m:t elt)(m':t elt') : t oee' := + mapi (fun k e => (Some e, find k m')) m. + +Definition combine_r (m:t elt)(m':t elt') : t oee' := + mapi (fun k e' => (find k m, Some e')) m'. + +Definition fold_right_pair (A B C:Set)(f:A->B->C->C)(l:list (A*B))(i:C) := + List.fold_right (fun p => f (fst p) (snd p)) i l. + +Definition combine (m:t elt)(m':t elt') : t oee' := + let l := combine_l m m' in + let r := combine_r m m' in + fold_right_pair (add (elt:=oee')) l r. + +Lemma fold_right_pair_NoDup : + forall l r (Hl: NoDupA (eqk (elt:=oee')) l) + (Hl: NoDupA (eqk (elt:=oee')) r), + NoDupA (eqk (elt:=oee')) (fold_right_pair (add (elt:=oee')) l r). +Proof. + induction l; simpl; auto. + destruct a; simpl; auto. + inversion_clear 1. + intros; apply add_NoDup; auto. +Qed. +Hint Resolve fold_right_pair_NoDup. + +Lemma combine_NoDup : + forall m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m'), + NoDupA (@eqk oee') (combine m m'). +Proof. + unfold combine, combine_r, combine_l. + intros. + set (f1 := fun (k : key) (e : elt) => (Some e, find k m')). + set (f2 := fun (k : key) (e' : elt') => (find k m, Some e')). + generalize (mapi_NoDup Hm f1). + generalize (mapi_NoDup Hm' f2). + set (l := mapi f1 m); clearbody l. + set (r := mapi f2 m'); clearbody r. + auto. +Qed. + +Definition at_least_left (o:option elt)(o':option elt') := + match o with + | None => None + | _ => Some (o,o') + end. + +Definition at_least_right (o:option elt)(o':option elt') := + match o' with + | None => None + | _ => Some (o,o') + end. + +Lemma combine_l_1 : + forall m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m')(x:key), + find x (combine_l m m') = at_least_left (find x m) (find x m'). +Proof. + unfold combine_l. + intros. + case_eq (find x m); intros. + simpl. + apply find_1. + apply mapi_NoDup; auto. + destruct (mapi_1 (fun k e => (Some e, find k m')) (find_2 H)) as (y,(H0,H1)). + rewrite (find_eq Hm' (X.eq_sym H0)); auto. + simpl. + case_eq (find x (mapi (fun k e => (Some e, find k m')) m)); intros; auto. + destruct (@mapi_2 _ _ m x (fun k e => (Some e, find k m'))). + exists p; apply find_2; auto. + rewrite (find_1 Hm H1) in H; discriminate. +Qed. + +Lemma combine_r_1 : + forall m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m')(x:key), + find x (combine_r m m') = at_least_right (find x m) (find x m'). +Proof. + unfold combine_r. + intros. + case_eq (find x m'); intros. + simpl. + apply find_1. + apply mapi_NoDup; auto. + destruct (mapi_1 (fun k e => (find k m, Some e)) (find_2 H)) as (y,(H0,H1)). + rewrite (find_eq Hm (X.eq_sym H0)); auto. + simpl. + case_eq (find x (mapi (fun k e' => (find k m, Some e')) m')); intros; auto. + destruct (@mapi_2 _ _ m' x (fun k e' => (find k m, Some e'))). + exists p; apply find_2; auto. + rewrite (find_1 Hm' H1) in H; discriminate. +Qed. + +Definition at_least_one (o:option elt)(o':option elt') := + match o, o' with + | None, None => None + | _, _ => Some (o,o') + end. + +Lemma combine_1 : + forall m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m')(x:key), + find x (combine m m') = at_least_one (find x m) (find x m'). +Proof. + unfold combine. + intros. + generalize (combine_r_1 Hm Hm' x). + generalize (combine_l_1 Hm Hm' x). + assert (NoDupA (eqk (elt:=oee')) (combine_l m m')). + unfold combine_l; apply mapi_NoDup; auto. + assert (NoDupA (eqk (elt:=oee')) (combine_r m m')). + unfold combine_r; apply mapi_NoDup; auto. + set (l := combine_l m m') in *; clearbody l. + set (r := combine_r m m') in *; clearbody r. + set (o := find x m); clearbody o. + set (o' := find x m'); clearbody o'. + clear Hm' Hm m m'. + induction l. + destruct o; destruct o'; simpl; intros; discriminate || auto. + destruct a; simpl in *; intros. + destruct (X.eq_dec x t0); simpl in *. + unfold at_least_left in H1. + destruct o; simpl in *; try discriminate. + inversion H1; subst. + apply add_eq; auto. + inversion_clear H; auto. + inversion_clear H. + rewrite <- IHl; auto. + apply add_not_eq; auto. +Qed. + +Variable f : option elt -> option elt' -> option elt''. + +Definition option_cons (A:Set)(k:key)(o:option A)(l:list (key*A)) := + match o with + | Some e => (k,e)::l + | None => l + end. + +Definition map2 m m' := + let m0 : t oee' := combine m m' in + let m1 : t (option elt'') := map (fun p => f (fst p) (snd p)) m0 in + fold_right_pair (option_cons (A:=elt'')) m1 nil. + +Lemma map2_NoDup : + forall m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m'), + NoDupA (@eqk elt'') (map2 m m'). +Proof. + intros. + unfold map2. + assert (H0:=combine_NoDup Hm Hm'). + set (l0:=combine m m') in *; clearbody l0. + set (f':= fun p : oee' => f (fst p) (snd p)). + assert (H1:=map_NoDup (elt' := option elt'') H0 f'). + set (l1:=map f' l0) in *; clearbody l1. + clear f' f H0 l0 Hm Hm' m m'. + induction l1. + simpl; auto. + inversion_clear H1. + destruct a; destruct o; simpl; auto. + constructor; auto. + swap H. + clear IHl1. + induction l1. + inversion H1. + inversion_clear H0. + destruct a; destruct o; simpl in *; auto. + inversion_clear H1; auto. +Qed. + +Definition at_least_one_then_f (o:option elt)(o':option elt') := + match o, o' with + | None, None => None + | _, _ => f o o' + end. + +Lemma map2_0 : + forall m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m')(x:key), + find x (map2 m m') = at_least_one_then_f (find x m) (find x m'). +Proof. + intros. + unfold map2. + assert (H:=combine_1 Hm Hm' x). + assert (H2:=combine_NoDup Hm Hm'). + set (f':= fun p : oee' => f (fst p) (snd p)). + set (m0 := combine m m') in *; clearbody m0. + set (o:=find x m) in *; clearbody o. + set (o':=find x m') in *; clearbody o'. + clear Hm Hm' m m'. + generalize H; clear H. + match goal with |- ?m=?n -> ?p=?q => + assert ((m=n->p=q)/\(m=None -> p=None)); [|intuition] end. + induction m0; simpl in *; intuition. + destruct o; destruct o'; simpl in *; try discriminate; auto. + destruct a as (k,(oo,oo')); simpl in *. + inversion_clear H2. + destruct (X.eq_dec x k); simpl in *. + (* x = k *) + assert (at_least_one_then_f o o' = f oo oo'). + destruct o; destruct o'; simpl in *; inversion_clear H; auto. + rewrite H2. + unfold f'; simpl. + destruct (f oo oo'); simpl. + destruct (X.eq_dec x k); try absurd_hyp n; auto. + destruct (IHm0 H1) as (_,H4); apply H4; auto. + case_eq (find x m0); intros; auto. + elim H0. + apply InA_eqk with (x,p); auto. + apply InA_eqke_eqk. + exact (find_2 H3). + (* k < x *) + unfold f'; simpl. + destruct (f oo oo'); simpl. + destruct (X.eq_dec x k); [ absurd_hyp n; auto | auto]. + destruct (IHm0 H1) as (H3,_); apply H3; auto. + destruct (IHm0 H1) as (H3,_); apply H3; auto. + + (* None -> None *) + destruct a as (k,(oo,oo')). + simpl. + inversion_clear H2. + destruct (X.eq_dec x k). + (* x = k *) + discriminate. + (* k < x *) + unfold f'; simpl. + destruct (f oo oo'); simpl. + destruct (X.eq_dec x k); [ absurd_hyp n; auto | auto]. + destruct (IHm0 H1) as (_,H4); apply H4; auto. + destruct (IHm0 H1) as (_,H4); apply H4; auto. +Qed. + +(** Specification of [map2] *) +Lemma map2_1 : + forall m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m')(x:key), + In x m \/ In x m' -> + find x (map2 m m') = f (find x m) (find x m'). +Proof. + intros. + rewrite map2_0; auto. + destruct H as [(e,H)|(e,H)]. + rewrite (find_1 Hm H). + destruct (find x m'); simpl; auto. + rewrite (find_1 Hm' H). + destruct (find x m); simpl; auto. +Qed. + +Lemma map2_2 : + forall m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m')(x:key), + In x (map2 m m') -> In x m \/ In x m'. +Proof. + intros. + destruct H as (e,H). + generalize (map2_0 Hm Hm' x). + rewrite (find_1 (map2_NoDup Hm Hm') H). + generalize (@find_2 _ m x). + generalize (@find_2 _ m' x). + destruct (find x m); + destruct (find x m'); simpl; intros. + left; exists e0; auto. + left; exists e0; auto. + right; exists e0; auto. + discriminate. +Qed. + +End Elt3. +End Raw. + + +Module Make (X: DecidableType) <: S with Module E:=X. + Module Raw := Raw X. + + Module E := X. + Definition key := X.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. + 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). + 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 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). + + Definition eq_key (p p':key*elt) := X.eq (fst p) (fst p'). + + 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). + + 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. + + |