diff options
Diffstat (limited to 'theories/MMaps/MMapPositive.v')
| -rw-r--r-- | theories/MMaps/MMapPositive.v | 698 |
1 files changed, 0 insertions, 698 deletions
diff --git a/theories/MMaps/MMapPositive.v b/theories/MMaps/MMapPositive.v deleted file mode 100644 index d3aab238..00000000 --- a/theories/MMaps/MMapPositive.v +++ /dev/null @@ -1,698 +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 *) -(***********************************************************************) - -(** * MMapPositive : an implementation of MMapInterface for [positive] keys. *) - -Require Import Bool PeanoNat BinPos Orders OrdersEx OrdersLists MMapInterface. - -Set Implicit Arguments. -Local Open Scope lazy_bool_scope. -Local Open Scope positive_scope. -Local Unset Elimination Schemes. - -(** This file is an adaptation to the [MMap] framework of a work by - Xavier Leroy and Sandrine Blazy (used for building certified compilers). - Keys are of type [positive], and maps are binary trees: the sequence - of binary digits of a positive number corresponds to a path in such a tree. - This is quite similar to the [IntMap] library, except that no path - compression is implemented, and that the current file is simple enough to be - self-contained. *) - -(** Reverses the positive [y] and concatenate it with [x] *) - -Fixpoint rev_append (y x : positive) : positive := - match y with - | 1 => x - | y~1 => rev_append y x~1 - | y~0 => rev_append y x~0 - end. -Local Infix "@" := rev_append (at level 60). -Definition rev x := x@1. - -(** The module of maps over positive keys *) - -Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. - - Module E:=PositiveOrderedTypeBits. - Module ME:=KeyOrderedType E. - - Definition key := positive : Type. - - Definition eq_key {A} (p p':key*A) := E.eq (fst p) (fst p'). - - Definition eq_key_elt {A} (p p':key*A) := - E.eq (fst p) (fst p') /\ (snd p) = (snd p'). - - Definition lt_key {A} (p p':key*A) := E.lt (fst p) (fst p'). - - Instance eqk_equiv {A} : Equivalence (@eq_key A) := _. - Instance eqke_equiv {A} : Equivalence (@eq_key_elt A) := _. - Instance ltk_strorder {A} : StrictOrder (@lt_key A) := _. - - Inductive tree (A : Type) := - | Leaf : tree A - | Node : tree A -> option A -> tree A -> tree A. - - Arguments Leaf {A}. - - Scheme tree_ind := Induction for tree Sort Prop. - - Definition t := tree. - - Definition empty {A} : t A := Leaf. - - Section A. - Variable A:Type. - - Fixpoint is_empty (m : t A) : bool := - match m with - | Leaf => true - | Node l None r => (is_empty l) &&& (is_empty r) - | _ => false - end. - - Fixpoint find (i : key) (m : t A) : option A := - match m with - | Leaf => None - | Node l o r => - match i with - | xH => o - | xO ii => find ii l - | xI ii => find ii r - end - end. - - Fixpoint mem (i : key) (m : t A) : bool := - match m with - | Leaf => false - | Node l o r => - match i with - | xH => match o with None => false | _ => true end - | xO ii => mem ii l - | xI ii => mem ii r - end - end. - - Fixpoint add (i : key) (v : A) (m : t A) : t A := - match m with - | Leaf => - match i with - | xH => Node Leaf (Some v) Leaf - | xO ii => Node (add ii v Leaf) None Leaf - | xI ii => Node Leaf None (add ii v Leaf) - end - | Node l o r => - match i with - | xH => Node l (Some v) r - | xO ii => Node (add ii v l) o r - | xI ii => Node l o (add ii v r) - end - end. - - (** helper function to avoid creating empty trees that are not leaves *) - - Definition node (l : t A) (o: option A) (r : t A) : t A := - match o,l,r with - | None,Leaf,Leaf => Leaf - | _,_,_ => Node l o r - end. - - Fixpoint remove (i : key) (m : t A) : t A := - match m with - | Leaf => Leaf - | Node l o r => - match i with - | xH => node l None r - | xO ii => node (remove ii l) o r - | xI ii => node l o (remove ii r) - end - end. - - (** [bindings] *) - - Fixpoint xbindings (m : t A) (i : positive) (a: list (key*A)) := - match m with - | Leaf => a - | Node l None r => xbindings l i~0 (xbindings r i~1 a) - | Node l (Some e) r => xbindings l i~0 ((rev i,e) :: xbindings r i~1 a) - end. - - Definition bindings (m : t A) := xbindings m 1 nil. - - (** [cardinal] *) - - Fixpoint cardinal (m : t A) : nat := - match m with - | Leaf => 0%nat - | Node l None r => (cardinal l + cardinal r)%nat - | Node l (Some _) r => S (cardinal l + cardinal r) - end. - - (** Specification proofs *) - - Definition MapsTo (i:key)(v:A)(m:t A) := find i m = Some v. - Definition In (i:key)(m:t A) := exists e:A, MapsTo i e m. - - Lemma MapsTo_compat : Proper (E.eq==>eq==>eq==>iff) MapsTo. - Proof. - intros k k' Hk e e' He m m' Hm. red in Hk. now subst. - Qed. - - Lemma find_spec m x e : find x m = Some e <-> MapsTo x e m. - Proof. reflexivity. Qed. - - Lemma mem_find : - forall m x, mem x m = match find x m with None => false | _ => true end. - Proof. - induction m; destruct x; simpl; auto. - Qed. - - Lemma mem_spec : forall m x, mem x m = true <-> In x m. - Proof. - unfold In, MapsTo; intros m x; rewrite mem_find. - split. - - destruct (find x m). - exists a; auto. - intros; discriminate. - - destruct 1 as (e0,H0); rewrite H0; auto. - Qed. - - Lemma gleaf : forall (i : key), find i Leaf = None. - Proof. destruct i; simpl; auto. Qed. - - Theorem empty_spec: - forall (i: key), find i empty = None. - Proof. exact gleaf. Qed. - - Lemma is_empty_spec m : - is_empty m = true <-> forall k, find k m = None. - Proof. - induction m; simpl. - - intuition. apply empty_spec. - - destruct o. split; try discriminate. - intros H. now specialize (H xH). - rewrite <- andb_lazy_alt, andb_true_iff, IHm1, IHm2. - clear IHm1 IHm2. - split. - + intros (H1,H2) k. destruct k; simpl; auto. - + intros H; split; intros k. apply (H (xO k)). apply (H (xI k)). - Qed. - - Theorem add_spec1: - forall (m: t A) (i: key) (x: A), find i (add i x m) = Some x. - Proof. - intros m i; revert m. - induction i; destruct m; simpl; auto. - Qed. - - Theorem add_spec2: - forall (m: t A) (i j: key) (x: A), - i <> j -> find j (add i x m) = find j m. - Proof. - intros m i j; revert m i. - induction j; destruct i, m; simpl; intros; - rewrite ?IHj, ?gleaf; auto; try congruence. - Qed. - - Lemma rleaf : forall (i : key), remove i Leaf = Leaf. - Proof. destruct i; simpl; auto. Qed. - - Lemma gnode l o r i : find i (node l o r) = find i (Node l o r). - Proof. - destruct o,l,r; simpl; trivial. - destruct i; simpl; now rewrite ?gleaf. - Qed. - - Opaque node. - - Theorem remove_spec1: - forall (m: t A)(i: key), find i (remove i m) = None. - Proof. - induction m; simpl. - - intros; rewrite rleaf. apply gleaf. - - destruct i; simpl remove; rewrite gnode; simpl; auto. - Qed. - - Theorem remove_spec2: - forall (m: t A)(i j: key), - i <> j -> find j (remove i m) = find j m. - Proof. - induction m; simpl; intros. - - now rewrite rleaf. - - destruct i; simpl; rewrite gnode; destruct j; simpl; trivial; - try apply IHm1; try apply IHm2; congruence. - Qed. - - Local Notation InL := (InA eq_key_elt). - - Lemma xbindings_spec: forall m j acc k e, - InL (k,e) (xbindings m j acc) <-> - InL (k,e) acc \/ exists x, k=(j@x) /\ find x m = Some e. - Proof. - induction m as [|l IHl o r IHr]; simpl. - - intros. split; intro H. - + now left. - + destruct H as [H|[x [_ H]]]. assumption. - now rewrite gleaf in H. - - intros j acc k e. case o as [e'|]; - rewrite IHl, ?InA_cons, IHr; clear IHl IHr; split. - + intros [[H|[H|H]]|H]; auto. - * unfold eq_key_elt, E.eq, fst, snd in H. destruct H as (->,<-). - right. now exists 1. - * destruct H as (x,(->,H)). right. now exists x~1. - * destruct H as (x,(->,H)). right. now exists x~0. - + intros [H|H]; auto. - destruct H as (x,(->,H)). - destruct x; simpl in *. - * left. right. right. now exists x. - * right. now exists x. - * left. left. injection H as ->. reflexivity. - + intros [[H|H]|H]; auto. - * destruct H as (x,(->,H)). right. now exists x~1. - * destruct H as (x,(->,H)). right. now exists x~0. - + intros [H|H]; auto. - destruct H as (x,(->,H)). - destruct x; simpl in *. - * left. right. now exists x. - * right. now exists x. - * discriminate. - Qed. - - Lemma lt_rev_append: forall j x y, E.lt x y -> E.lt (j@x) (j@y). - Proof. induction j; intros; simpl; auto. Qed. - - Lemma xbindings_sort m j acc : - sort lt_key acc -> - (forall x p, In x m -> InL p acc -> E.lt (j@x) (fst p)) -> - sort lt_key (xbindings m j acc). - Proof. - revert j acc. - induction m as [|l IHl o r IHr]; simpl; trivial. - intros j acc Hacc Hsacc. destruct o as [e|]. - - apply IHl;[constructor;[apply IHr; [apply Hacc|]|]|]. - + intros. now apply Hsacc. - + case_eq (xbindings r j~1 acc); [constructor|]. - intros (z,e') q H. constructor. - assert (H': InL (z,e') (xbindings r j~1 acc)). - { rewrite H. now constructor. } - clear H q. rewrite xbindings_spec in H'. - destruct H' as [H'|H']. - * apply (Hsacc 1 (z,e')); trivial. now exists e. - * destruct H' as (x,(->,H)). - red. simpl. now apply lt_rev_append. - + intros x (y,e') Hx Hy. inversion_clear Hy. - rewrite H. simpl. now apply lt_rev_append. - rewrite xbindings_spec in H. - destruct H as [H|H]. - * now apply Hsacc. - * destruct H as (z,(->,H)). simpl. - now apply lt_rev_append. - - apply IHl; [apply IHr; [apply Hacc|]|]. - + intros. now apply Hsacc. - + intros x (y,e') Hx H. rewrite xbindings_spec in H. - destruct H as [H|H]. - * now apply Hsacc. - * destruct H as (z,(->,H)). simpl. - now apply lt_rev_append. - Qed. - - Lemma bindings_spec1 m k e : - InA eq_key_elt (k,e) (bindings m) <-> MapsTo k e m. - Proof. - unfold bindings, MapsTo. rewrite xbindings_spec. - split; [ intros [H|(y & H & H')] | intros IN ]. - - inversion H. - - simpl in *. now subst. - - right. now exists k. - Qed. - - Lemma bindings_spec2 m : sort lt_key (bindings m). - Proof. - unfold bindings. - apply xbindings_sort. constructor. inversion 2. - Qed. - - Lemma bindings_spec2w m : NoDupA eq_key (bindings m). - Proof. - apply ME.Sort_NoDupA. - apply bindings_spec2. - Qed. - - Lemma xbindings_length m j acc : - length (xbindings m j acc) = (cardinal m + length acc)%nat. - Proof. - revert j acc. - induction m; simpl; trivial; intros. - destruct o; simpl; rewrite IHm1; simpl; rewrite IHm2; - now rewrite ?Nat.add_succ_r, Nat.add_assoc. - Qed. - - Lemma cardinal_spec m : cardinal m = length (bindings m). - Proof. - unfold bindings. rewrite xbindings_length. simpl. - symmetry. apply Nat.add_0_r. - Qed. - - (** [map] and [mapi] *) - - Variable B : Type. - - Section Mapi. - - Variable f : key -> option A -> option B. - - Fixpoint xmapi (m : t A) (i : key) : t B := - match m with - | Leaf => Leaf - | Node l o r => Node (xmapi l (i~0)) - (f (rev i) o) - (xmapi r (i~1)) - end. - - End Mapi. - - Definition mapi (f : key -> A -> B) m := - xmapi (fun k => option_map (f k)) m 1. - - Definition map (f : A -> B) m := mapi (fun _ => f) m. - - End A. - - Lemma xgmapi: - forall (A B: Type) (f: key -> option A -> option B) (i j : key) (m: t A), - (forall k, f k None = None) -> - find i (xmapi f m j) = f (j@i) (find i m). - Proof. - induction i; intros; destruct m; simpl; rewrite ?IHi; auto. - Qed. - - Theorem mapi_spec0 : - forall (A B: Type) (f: key -> A -> B) (i: key) (m: t A), - find i (mapi f m) = option_map (f i) (find i m). - Proof. - intros. unfold mapi. rewrite xgmapi; simpl; auto. - Qed. - - Lemma mapi_spec : - forall (A B: Type) (f: key -> A -> B) (m: t A) (i:key), - exists j, E.eq j i /\ - find i (mapi f m) = option_map (f j) (find i m). - Proof. - intros. - exists i. split. reflexivity. apply mapi_spec0. - Qed. - - Lemma map_spec : - forall (elt elt':Type)(f:elt->elt')(m: t elt)(x:key), - find x (map f m) = option_map f (find x m). - Proof. - intros; unfold map. apply mapi_spec0. - Qed. - - Section merge. - Variable A B C : Type. - Variable f : key -> option A -> option B -> option C. - - Fixpoint xmerge (m1 : t A)(m2 : t B)(i:positive) : t C := - match m1 with - | Leaf => xmapi (fun k => f k None) m2 i - | Node l1 o1 r1 => - match m2 with - | Leaf => xmapi (fun k o => f k o None) m1 i - | Node l2 o2 r2 => - Node (xmerge l1 l2 (i~0)) - (f (rev i) o1 o2) - (xmerge r1 r2 (i~1)) - end - end. - - Lemma xgmerge: forall (i j: key)(m1:t A)(m2: t B), - (forall i, f i None None = None) -> - find i (xmerge m1 m2 j) = f (j@i) (find i m1) (find i m2). - Proof. - induction i; intros; destruct m1; destruct m2; simpl; auto; - rewrite ?xgmapi, ?IHi; simpl; auto. - Qed. - - End merge. - - Definition merge {A B C}(f:key->option A->option B->option C) m1 m2 := - xmerge - (fun k o1 o2 => match o1,o2 with - | None,None => None - | _, _ => f k o1 o2 - end) - m1 m2 xH. - - Lemma merge_spec1 {A B C}(f:key->option A->option B->option C) : - forall m m' x, - In x m \/ In x m' -> - exists y, E.eq y x /\ - find x (merge f m m') = f y (find x m) (find x m'). - Proof. - intros. exists x. split. reflexivity. - unfold merge. - rewrite xgmerge; simpl; auto. - rewrite <- 2 mem_spec, 2 mem_find in H. - destruct (find x m); simpl; auto. - destruct (find x m'); simpl; auto. intuition discriminate. - Qed. - - Lemma merge_spec2 {A B C}(f:key->option A->option B->option C) : - forall m m' x, In x (merge f m m') -> In x m \/ In x m'. - Proof. - intros. - rewrite <-mem_spec, mem_find in H. - unfold merge in H. - rewrite xgmerge in H; simpl; auto. - rewrite <- 2 mem_spec, 2 mem_find. - destruct (find x m); simpl in *; auto. - destruct (find x m'); simpl in *; auto. - Qed. - - Section Fold. - - Variables A B : Type. - Variable f : key -> A -> B -> B. - - (** the additional argument, [i], records the current path, in - reverse order (this should be more efficient: we reverse this argument - only at present nodes only, rather than at each node of the tree). - we also use this convention in all functions below - *) - - Fixpoint xfold (m : t A) (v : B) (i : key) := - match m with - | Leaf => v - | Node l (Some x) r => - xfold r (f (rev i) x (xfold l v i~0)) i~1 - | Node l None r => - xfold r (xfold l v i~0) i~1 - end. - Definition fold m i := xfold m i 1. - - End Fold. - - Lemma fold_spec : - forall {A}(m:t A){B}(i : B) (f : key -> A -> B -> B), - fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (bindings m) i. - Proof. - unfold fold, bindings. intros A m B i f. revert m i. - set (f' := fun a p => f (fst p) (snd p) a). - assert (H: forall m i j acc, - fold_left f' acc (xfold f m i j) = - fold_left f' (xbindings m j acc) i). - { induction m as [|l IHl o r IHr]; intros; trivial. - destruct o; simpl; now rewrite IHr, <- IHl. } - intros. exact (H m i 1 nil). - Qed. - - Fixpoint equal (A:Type)(cmp : A -> A -> bool)(m1 m2 : t A) : bool := - match m1, m2 with - | Leaf, _ => is_empty m2 - | _, Leaf => is_empty m1 - | Node l1 o1 r1, Node l2 o2 r2 => - (match o1, o2 with - | None, None => true - | Some v1, Some v2 => cmp v1 v2 - | _, _ => false - end) - &&& equal cmp l1 l2 &&& equal cmp r1 r2 - end. - - Definition Equal (A:Type)(m m':t A) := - forall y, find y m = find y m'. - Definition Equiv (A:Type)(eq_elt:A->A->Prop) m m' := - (forall k, In k m <-> In k m') /\ - (forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e'). - Definition Equivb (A:Type)(cmp: A->A->bool) := Equiv (Cmp cmp). - - Lemma equal_1 : forall (A:Type)(m m':t A)(cmp:A->A->bool), - Equivb cmp m m' -> equal cmp m m' = true. - Proof. - induction m. - - (* m = Leaf *) - destruct 1 as (E,_); simpl. - apply is_empty_spec; intros k. - destruct (find k m') eqn:F; trivial. - assert (H : In k m') by now exists a. - rewrite <- E in H. - destruct H as (x,H). red in H. now rewrite gleaf in H. - - (* m = Node *) - destruct m'. - + (* m' = Leaf *) - destruct 1 as (E,_); simpl. - destruct o. - * assert (H : In xH (@Leaf A)). - { rewrite <- E. now exists a. } - destruct H as (e,H). now red in H. - * apply andb_true_intro; split; apply is_empty_spec; intros k. - destruct (find k m1) eqn:F; trivial. - assert (H : In (xO k) (@Leaf A)). - { rewrite <- E. exists a; auto. } - destruct H as (x,H). red in H. now rewrite gleaf in H. - destruct (find k m2) eqn:F; trivial. - assert (H : In (xI k) (@Leaf A)). - { rewrite <- E. exists a; auto. } - destruct H as (x,H). red in H. now rewrite gleaf in H. - + (* m' = Node *) - destruct 1. - assert (Equivb cmp m1 m'1). - { split. - intros k; generalize (H (xO k)); unfold In, MapsTo; simpl; auto. - intros k e e'; generalize (H0 (xO k) e e'); unfold In, MapsTo; simpl; auto. } - assert (Equivb cmp m2 m'2). - { split. - intros k; generalize (H (xI k)); unfold In, MapsTo; simpl; auto. - intros k e e'; generalize (H0 (xI k) e e'); unfold In, MapsTo; simpl; auto. } - simpl. - destruct o; destruct o0; simpl. - repeat (apply andb_true_intro; split); auto. - apply (H0 xH); red; auto. - generalize (H xH); unfold In, MapsTo; simpl; intuition. - destruct H4; try discriminate; eauto. - generalize (H xH); unfold In, MapsTo; simpl; intuition. - destruct H5; try discriminate; eauto. - apply andb_true_intro; split; auto. - Qed. - - Lemma equal_2 : forall (A:Type)(m m':t A)(cmp:A->A->bool), - equal cmp m m' = true -> Equivb cmp m m'. - Proof. - induction m. - (* m = Leaf *) - simpl. - split; intros. - split. - destruct 1; red in H0; destruct k; discriminate. - rewrite is_empty_spec in H. - intros (e,H'). red in H'. now rewrite H in H'. - red in H0; destruct k; discriminate. - (* m = Node *) - destruct m'. - (* m' = Leaf *) - simpl. - destruct o; intros; try discriminate. - destruct (andb_prop _ _ H); clear H. - split; intros. - split; unfold In, MapsTo; destruct 1. - destruct k; simpl in *; try discriminate. - rewrite is_empty_spec in H1. - now rewrite H1 in H. - rewrite is_empty_spec in H0. - now rewrite H0 in H. - destruct k; simpl in *; discriminate. - unfold In, MapsTo; destruct k; simpl in *; discriminate. - (* m' = Node *) - destruct o; destruct o0; simpl; intros; try discriminate. - destruct (andb_prop _ _ H); clear H. - destruct (andb_prop _ _ H0); clear H0. - destruct (IHm1 _ _ H2); clear H2 IHm1. - destruct (IHm2 _ _ H1); clear H1 IHm2. - split; intros. - destruct k; unfold In, MapsTo in *; simpl; auto. - split; eauto. - destruct k; unfold In, MapsTo in *; simpl in *. - eapply H4; eauto. - eapply H3; eauto. - congruence. - destruct (andb_prop _ _ H); clear H. - destruct (IHm1 _ _ H0); clear H0 IHm1. - destruct (IHm2 _ _ H1); clear H1 IHm2. - split; intros. - destruct k; unfold In, MapsTo in *; simpl; auto. - split; eauto. - destruct k; unfold In, MapsTo in *; simpl in *. - eapply H3; eauto. - eapply H2; eauto. - try discriminate. - Qed. - - Lemma equal_spec : forall (A:Type)(m m':t A)(cmp:A->A->bool), - equal cmp m m' = true <-> Equivb cmp m m'. - Proof. - split. apply equal_2. apply equal_1. - Qed. - -End PositiveMap. - -(** Here come some additionnal facts about this implementation. - Most are facts that cannot be derivable from the general interface. *) - -Module PositiveMapAdditionalFacts. - Import PositiveMap. - - (* Derivable from the Map interface *) - Theorem gsspec {A} i j x (m: t A) : - find i (add j x m) = if E.eq_dec i j then Some x else find i m. - Proof. - destruct (E.eq_dec i j) as [->|]; - [ apply add_spec1 | apply add_spec2; auto ]. - Qed. - - (* Not derivable from the Map interface *) - Theorem gsident {A} i (m:t A) v : - find i m = Some v -> add i v m = m. - Proof. - revert m. - induction i; destruct m; simpl in *; try congruence. - - intro H; now rewrite (IHi m2 H). - - intro H; now rewrite (IHi m1 H). - Qed. - - Lemma xmapi_ext {A B}(f g: key -> option A -> option B) : - (forall k (o : option A), f k o = g k o) -> - forall m i, xmapi f m i = xmapi g m i. - Proof. - induction m; intros; simpl; auto. now f_equal. - Qed. - - Theorem xmerge_commut{A B C} - (f: key -> option A -> option B -> option C) - (g: key -> option B -> option A -> option C) : - (forall k o1 o2, f k o1 o2 = g k o2 o1) -> - forall m1 m2 i, xmerge f m1 m2 i = xmerge g m2 m1 i. - Proof. - intros E. - induction m1; destruct m2; intros i; simpl; trivial; f_equal; - try apply IHm1_1; try apply IHm1_2; try apply xmapi_ext; - intros; apply E. - Qed. - - Theorem merge_commut{A B C} - (f: key -> option A -> option B -> option C) - (g: key -> option B -> option A -> option C) : - (forall k o1 o2, f k o1 o2 = g k o2 o1) -> - forall m1 m2, merge f m1 m2 = merge g m2 m1. - Proof. - intros E m1 m2. - unfold merge. apply xmerge_commut. - intros k [x1|] [x2|]; trivial. - Qed. - -End PositiveMapAdditionalFacts. |