diff options
Diffstat (limited to 'theories/FSets/FMapIntMap.v')
-rw-r--r-- | theories/FSets/FMapIntMap.v | 622 |
1 files changed, 0 insertions, 622 deletions
diff --git a/theories/FSets/FMapIntMap.v b/theories/FSets/FMapIntMap.v deleted file mode 100644 index c7681bd4..00000000 --- a/theories/FSets/FMapIntMap.v +++ /dev/null @@ -1,622 +0,0 @@ -(***********************************************************************) -(* 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. - |