diff options
Diffstat (limited to 'theories/FSets/FMapIntMap.v')
-rw-r--r-- | theories/FSets/FMapIntMap.v | 622 |
1 files changed, 622 insertions, 0 deletions
diff --git a/theories/FSets/FMapIntMap.v b/theories/FSets/FMapIntMap.v new file mode 100644 index 00000000..c7681bd4 --- /dev/null +++ b/theories/FSets/FMapIntMap.v @@ -0,0 +1,622 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) + +(* Finite sets library. + * Authors: Pierre Letouzey and Jean-Christophe Filliâtre + * Institution: LRI, CNRS UMR 8623 - Université Paris Sud + * 91405 Orsay, France *) + +(* $Id: FMapIntMap.v 8876 2006-05-30 13:43:15Z letouzey $ *) + +Require Import Bool. +Require Import NArith Ndigits Ndec Nnat. +Require Import Allmaps. +Require Import OrderedType. +Require Import OrderedTypeEx. +Require Import FMapInterface FMapList. + + +Set Implicit Arguments. + +(** * An implementation of [FMapInterface.S] based on [IntMap] *) + +(** Keys are of type [N]. The main functions are directly taken from + [IntMap]. Since they have no exact counterpart in [IntMap], functions + [fold], [map2] and [equal] are for now obtained by translation + to sorted lists. *) + +(** [N] is an ordered type, using not the usual order on numbers, + but lexicographic ordering on bits (lower bit considered first). *) + +Module NUsualOrderedType <: UsualOrderedType. + Definition t:=N. + Definition eq:=@eq N. + Definition eq_refl := @refl_equal t. + Definition eq_sym := @sym_eq t. + Definition eq_trans := @trans_eq t. + + Definition lt p q:= Nless p q = true. + + Definition lt_trans := Nless_trans. + + Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. + Proof. + intros; intro. + rewrite H0 in H. + red in H. + rewrite Nless_not_refl in H; discriminate. + Qed. + + Definition compare : forall x y : t, Compare lt eq x y. + Proof. + intros x y. + destruct (Nless_total x y) as [[H|H]|H]. + apply LT; unfold lt; auto. + apply GT; unfold lt; auto. + apply EQ; auto. + Qed. + +End NUsualOrderedType. + + +(** The module of maps over [N] keys based on [IntMap] *) + +Module MapIntMap <: S with Module E:=NUsualOrderedType. + + Module E:=NUsualOrderedType. + Module ME:=OrderedTypeFacts(E). + Module PE:=KeyOrderedType(E). + + Definition key := N. + + Definition t := Map. + + Section A. + Variable A:Set. + + Definition empty : t A := M0 A. + + Definition is_empty (m : t A) : bool := + MapEmptyp _ (MapCanonicalize _ m). + + Definition find (x:key)(m: t A) : option A := MapGet _ m x. + + Definition mem (x:key)(m: t A) : bool := + match find x m with + | Some _ => true + | None => false + end. + + Definition add (x:key)(v:A)(m:t A) : t A := MapPut _ m x v. + + Definition remove (x:key)(m:t A) : t A := MapRemove _ m x. + + Definition elements (m : t A) : list (N*A) := alist_of_Map _ m. + + Definition MapsTo (x:key)(v:A)(m:t A) := find x m = Some v. + + Definition In (x:key)(m:t A) := exists e:A, MapsTo x e m. + + Definition Empty m := forall (a : key)(e:A) , ~ MapsTo a e m. + + Definition eq_key (p p':key*A) := E.eq (fst p) (fst p'). + + Definition eq_key_elt (p p':key*A) := + E.eq (fst p) (fst p') /\ (snd p) = (snd p'). + + Definition lt_key (p p':key*A) := E.lt (fst p) (fst p'). + + Lemma Empty_alt : forall m, Empty m <-> forall a, find a m = None. + Proof. + unfold Empty, MapsTo. + intuition. + generalize (H a). + destruct (find a m); intuition. + elim (H0 a0); auto. + rewrite H in H0; discriminate. + Qed. + + Section Spec. + Variable m m' m'' : t A. + Variable x y z : key. + Variable e e' : A. + + Lemma MapsTo_1 : E.eq x y -> MapsTo x e m -> MapsTo y e m. + Proof. intros; rewrite <- H; auto. Qed. + + Lemma find_1 : MapsTo x e m -> find x m = Some e. + Proof. unfold MapsTo; auto. Qed. + + Lemma find_2 : find x m = Some e -> MapsTo x e m. + Proof. red; auto. Qed. + + Lemma empty_1 : Empty empty. + Proof. + rewrite Empty_alt; intros; unfold empty, find; simpl; auto. + Qed. + + Lemma is_empty_1 : Empty m -> is_empty m = true. + Proof. + unfold Empty, is_empty, find; intros. + cut (MapCanonicalize _ m = M0 _). + intros; rewrite H0; simpl; auto. + apply mapcanon_unique. + apply mapcanon_exists_2. + constructor. + red; red; simpl; intros. + rewrite <- (mapcanon_exists_1 _ m). + unfold MapsTo, find in *. + generalize (H a). + destruct (MapGet _ m a); auto. + intros; generalize (H0 a0); destruct 1; auto. + Qed. + + Lemma is_empty_2 : is_empty m = true -> Empty m. + Proof. + unfold Empty, is_empty, MapsTo, find; intros. + generalize (MapEmptyp_complete _ _ H); clear H; intros. + rewrite (mapcanon_exists_1 _ m). + rewrite H; simpl; auto. + discriminate. + Qed. + + Lemma mem_1 : In x m -> mem x m = true. + Proof. + unfold In, MapsTo, mem. + destruct (find x m); auto. + destruct 1; discriminate. + Qed. + + Lemma mem_2 : forall m x, mem x m = true -> In x m. + Proof. + unfold In, MapsTo, mem. + intros. + destruct (find x0 m0); auto; try discriminate. + exists a; auto. + Qed. + + Lemma add_1 : E.eq x y -> MapsTo y e (add x e m). + Proof. + unfold MapsTo, find, add. + intro H; rewrite H; clear H. + rewrite MapPut_semantics. + rewrite Neqb_correct; auto. + Qed. + + Lemma add_2 : ~ E.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m). + Proof. + unfold MapsTo, find, add. + intros. + rewrite MapPut_semantics. + rewrite H0. + generalize (Neqb_complete x y). + destruct (Neqb x y); auto. + intros. + elim H; auto. + apply H1; auto. + Qed. + + Lemma add_3 : ~ E.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m. + Proof. + unfold MapsTo, find, add. + rewrite MapPut_semantics. + intro H. + generalize (Neqb_complete x y). + destruct (Neqb x y); auto. + intros; elim H; auto. + apply H0; auto. + Qed. + + Lemma remove_1 : E.eq x y -> ~ In y (remove x m). + Proof. + unfold In, MapsTo, find, remove. + rewrite MapRemove_semantics. + intro H. + rewrite H; rewrite Neqb_correct. + red; destruct 1; discriminate. + Qed. + + Lemma remove_2 : ~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m). + Proof. + unfold MapsTo, find, remove. + rewrite MapRemove_semantics. + intros. + rewrite H0. + generalize (Neqb_complete x y). + destruct (Neqb x y); auto. + intros; elim H; apply H1; auto. + Qed. + + Lemma remove_3 : MapsTo y e (remove x m) -> MapsTo y e m. + Proof. + unfold MapsTo, find, remove. + rewrite MapRemove_semantics. + destruct (Neqb x y); intros; auto. + discriminate. + Qed. + + Lemma alist_sorted_sort : forall l, alist_sorted A l=true -> sort lt_key l. + Proof. + induction l. + auto. + simpl. + destruct a. + destruct l. + auto. + destruct p. + intros; destruct (andb_prop _ _ H); auto. + Qed. + + Lemma elements_3 : sort lt_key (elements m). + Proof. + unfold elements. + apply alist_sorted_sort. + apply alist_of_Map_sorts. + Qed. + + Lemma elements_1 : + MapsTo x e m -> InA eq_key_elt (x,e) (elements m). + Proof. + unfold MapsTo, find, elements. + rewrite InA_alt. + intro H. + exists (x,e). + split. + red; simpl; unfold E.eq; auto. + rewrite alist_of_Map_semantics in H. + generalize H. + set (l:=alist_of_Map A m); clearbody l; clear. + induction l; simpl; auto. + intro; discriminate. + destruct a; simpl; auto. + generalize (Neqb_complete a x). + destruct (Neqb a x); auto. + left. + injection H0; auto. + intros; f_equal; auto. + Qed. + + Lemma elements_2 : + InA eq_key_elt (x,e) (elements m) -> MapsTo x e m. + Proof. + generalize elements_3. + unfold MapsTo, find, elements. + rewrite InA_alt. + intros H ((e0,a),(H0,H1)). + red in H0; simpl in H0; unfold E.eq in H0; destruct H0; subst. + rewrite alist_of_Map_semantics. + generalize H H1; clear H H1. + set (l:=alist_of_Map A m); clearbody l; clear. + induction l; simpl; auto. + intro; contradiction. + intros. + destruct a0; simpl. + inversion H1. + injection H0; intros; subst. + rewrite Neqb_correct; auto. + assert (InA eq_key (e0,a) l). + rewrite InA_alt. + exists (e0,a); split; auto. + red; simpl; auto; red; auto. + generalize (PE.Sort_In_cons_1 H H2). + unfold PE.ltk; simpl. + intros H3; generalize (E.lt_not_eq H3). + generalize (Neqb_complete a0 e0). + destruct (Neqb a0 e0); auto. + destruct 2. + apply H4; auto. + inversion H; auto. + Qed. + + 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). + + (** unfortunately, the [MapFold] of [IntMap] isn't compatible with + the FMap interface. We use a naive version for now : *) + + Definition fold (B:Set)(f:key -> A -> B -> B)(m:t A)(i:B) : B := + fold_left (fun a p => f (fst p) (snd p) a) (elements m) i. + + Lemma fold_1 : + forall (B:Set) (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. auto. Qed. + + End Spec. + + Variable B : Set. + + Fixpoint mapi_aux (pf:N->N)(f : N -> A -> B)(m:t A) { struct m }: t B := + match m with + | M0 => M0 _ + | M1 x y => M1 _ x (f (pf x) y) + | M2 m0 m1 => M2 _ (mapi_aux (fun n => pf (Ndouble n)) f m0) + (mapi_aux (fun n => pf (Ndouble_plus_one n)) f m1) + end. + + Definition mapi := mapi_aux (fun n => n). + + Definition map (f:A->B) := mapi (fun _ => f). + + End A. + + Lemma mapi_aux_1 : forall (elt elt':Set)(m: t elt)(pf:N->N)(x:key)(e:elt) + (f:key->elt->elt'), MapsTo x e m -> + exists y, E.eq y x /\ MapsTo x (f (pf y) e) (mapi_aux pf f m). + Proof. + unfold MapsTo; induction m; simpl; auto. + inversion 1. + + intros. + exists x; split; [red; auto|]. + generalize (Neqb_complete a x). + destruct (Neqb a x); try discriminate. + injection H; intros; subst; auto. + rewrite H1; auto. + + intros. + exists x; split; [red;auto|]. + destruct x; simpl in *. + destruct (IHm1 (fun n : N => pf (Ndouble n)) _ _ f H) as (y,(Hy,Hy')). + rewrite Hy in Hy'; simpl in Hy'; auto. + destruct p; simpl in *. + destruct (IHm2 (fun n : N => pf (Ndouble_plus_one n)) _ _ f H) as (y,(Hy,Hy')). + rewrite Hy in Hy'; simpl in Hy'; auto. + destruct (IHm1 (fun n : N => pf (Ndouble n)) _ _ f H) as (y,(Hy,Hy')). + rewrite Hy in Hy'; simpl in Hy'; auto. + destruct (IHm2 (fun n : N => pf (Ndouble_plus_one n)) _ _ f H) as (y,(Hy,Hy')). + rewrite Hy in Hy'; simpl in Hy'; 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; exact (mapi_aux_1 (fun n => n)). + Qed. + + Lemma mapi_aux_2 : forall (elt elt':Set)(m: t elt)(pf:N->N)(x:key) + (f:key->elt->elt'), In x (mapi_aux pf f m) -> In x m. + Proof. + unfold In, MapsTo. + induction m; simpl in *. + intros pf x f (e,He); inversion He. + intros pf x f (e,He). + exists a0. + destruct (Neqb a x); try discriminate; auto. + intros pf x f (e,He). + destruct x; [|destruct p]; eauto. + 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 (mapi_aux_2 m (fun n => n)). + Qed. + + 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. + unfold map; intros. + destruct (@mapi_1 _ _ m x e (fun _ => f)) as (e',(_,H0)); auto. + 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. + unfold map; intros. + eapply mapi_2; eauto. + Qed. + + Module L := FMapList.Raw E. + + (** Not exactly pretty nor perfect, but should suffice as a first naive implem. + Anyway, map2 isn't in Ocaml... + *) + + Definition anti_elements (A:Set)(l:list (key*A)) := L.fold (@add _) l (empty _). + + Definition map2 (A B C:Set)(f:option A->option B -> option C)(m:t A)(m':t B) : t C := + anti_elements (L.map2 f (elements m) (elements m')). + + Lemma add_spec : forall (A:Set)(m:t A) x y e, + find x (add y e m) = if ME.eq_dec x y then Some e else find x m. + Proof. + intros. + destruct (ME.eq_dec x y). + apply find_1. + eapply MapsTo_1 with y; eauto. + red; auto. + apply add_1; auto. + red; auto. + case_eq (find x m); intros. + apply find_1. + 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); unfold E.eq in *; auto. + Qed. + + Lemma anti_elements_mapsto_aux : forall (A:Set)(l:list (key*A)) m k e, + NoDupA (eq_key (A:=A)) l -> + (forall x, L.PX.In x l -> In x m -> False) -> + (MapsTo k e (L.fold (@add _) l m) <-> L.PX.MapsTo k e l \/ MapsTo k e m). + Proof. + induction l. + simpl; auto. + intuition. + inversion H2. + simpl; destruct a; intros. + rewrite IHl; clear IHl. + inversion H; auto. + intros. + inversion_clear H. + assert (~E.eq x k). + swap H3. + destruct H1. + apply InA_eqA with (x,x0); eauto. + unfold eq_key, E.eq; eauto. + unfold eq_key, E.eq; congruence. + apply (H0 x). + destruct H1; exists x0; auto. + revert H2. + unfold In. + intros (e',He'). + exists e'; apply (@add_3 _ m k x e' a); unfold E.eq; auto. + intuition. + red in H2. + rewrite add_spec in H2; auto. + destruct (ME.eq_dec k0 k). + inversion_clear H2; subst; auto. + right; apply find_2; auto. + inversion_clear H2; auto. + compute in H1; destruct H1. + subst; right; apply add_1; auto. + red; auto. + inversion_clear H. + destruct (ME.eq_dec k0 k). + unfold E.eq in *; subst. + destruct (H0 k); eauto. + red; eauto. + 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 -> + (MapsTo k e (anti_elements l) <-> L.PX.MapsTo k e l). + Proof. + intros. + unfold anti_elements. + rewrite anti_elements_mapsto_aux; auto; unfold empty; auto. + inversion 2. + inversion H2. + intuition. + inversion H1. + Qed. + + Lemma find_anti_elements : forall (A:Set)(l: list (key*A)) x, sort (@lt_key _) l -> + find x (anti_elements l) = L.find x l. + Proof. + intros. + case_eq (L.find x l); intros. + apply find_1. + rewrite anti_elements_mapsto. + apply L.PX.Sort_NoDupA; auto. + apply L.find_2; auto. + case_eq (find x (anti_elements l)); auto; intros. + rewrite <- H0; symmetry. + apply L.find_1; auto. + rewrite <- anti_elements_mapsto. + apply L.PX.Sort_NoDupA; auto. + apply find_2; auto. + Qed. + + Lemma find_elements : forall (A:Set)(m: t A) x, + L.find x (elements m) = find x m. + Proof. + intros. + case_eq (find x m); intros. + apply L.find_1. + apply elements_3; auto. + red; apply elements_1. + apply find_2; auto. + case_eq (L.find x (elements m)); auto; intros. + rewrite <- H; symmetry. + apply find_1; auto. + apply elements_2. + apply L.find_2; auto. + Qed. + + Lemma elements_in : forall (A:Set)(s:t A) x, L.PX.In x (elements s) <-> In x s. + Proof. + intros. + unfold L.PX.In, In. + firstorder. + exists x0. + red; rewrite <- find_elements; auto. + apply L.find_1; auto. + apply elements_3. + exists x0. + apply L.find_2. + rewrite find_elements; auto. + Qed. + + Lemma map2_1 : forall (A B C:Set)(m: t A)(m': t B)(x:key) + (f:option A->option B ->option C), + In x m \/ In x m' -> find x (map2 f m m') = f (find x m) (find x m'). + Proof. + unfold map2; intros. + rewrite find_anti_elements; auto. + rewrite <- find_elements; auto. + rewrite <- find_elements; auto. + apply L.map2_1; auto. + apply elements_3; auto. + apply elements_3; auto. + do 2 rewrite elements_in; auto. + apply L.map2_sorted; auto. + apply elements_3; auto. + apply elements_3; auto. + Qed. + + Lemma map2_2 : forall (A B C: Set)(m: t A)(m': t B)(x:key) + (f:option A->option B ->option C), + In x (map2 f m m') -> In x m \/ In x m'. + Proof. + unfold map2; intros. + do 2 rewrite <- elements_in. + apply L.map2_2 with (f:=f); auto. + apply elements_3; auto. + apply elements_3; auto. + destruct H. + exists x0. + rewrite <- anti_elements_mapsto; auto. + apply L.PX.Sort_NoDupA; auto. + apply L.map2_sorted; auto. + apply elements_3; auto. + apply elements_3; auto. + Qed. + + (** same trick for [equal] *) + + Definition equal (A:Set)(cmp:A -> A -> bool)(m m' : t A) : bool := + L.equal cmp (elements m) (elements m'). + + Lemma equal_1 : + forall (A:Set)(m: t A)(m': t A)(cmp: A -> A -> bool), + Equal cmp m m' -> equal cmp m m' = true. + Proof. + unfold equal, Equal. + intros. + apply L.equal_1. + apply elements_3. + apply elements_3. + unfold L.Equal. + destruct H. + split; intros. + do 2 rewrite elements_in; auto. + apply (H0 k); + red; rewrite <- find_elements; apply L.find_1; auto; + apply elements_3. + Qed. + + Lemma equal_2 : + forall (A:Set)(m: t A)(m': t A)(cmp: A -> A -> bool), + equal cmp m m' = true -> Equal cmp m m'. + Proof. + unfold equal, Equal. + intros. + destruct (L.equal_2 (elements_3 m) (elements_3 m') H); clear H. + split. + intros; do 2 rewrite <- elements_in; auto. + intros; apply (H1 k); + apply L.find_2; rewrite find_elements;auto. + Qed. + +End MapIntMap. + |