diff options
Diffstat (limited to 'theories/FSets/FMapPositive.v')
-rw-r--r-- | theories/FSets/FMapPositive.v | 99 |
1 files changed, 49 insertions, 50 deletions
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index 792b88717..253800a45 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -8,7 +8,7 @@ (** * FMapPositive : an implementation of FMapInterface for [positive] keys. *) -Require Import Bool ZArith OrderedType OrderedTypeEx FMapInterface. +Require Import Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface. Set Implicit Arguments. Local Open Scope positive_scope. @@ -69,7 +69,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Module E:=PositiveOrderedTypeBits. Module ME:=KeyOrderedType E. - Definition key := positive. + Definition key := positive : Type. Inductive tree (A : Type) := | Leaf : tree A @@ -93,7 +93,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. | _ => false end. - Fixpoint find (i : positive) (m : t A) : option A := + Fixpoint find (i : key) (m : t A) : option A := match m with | Leaf => None | Node l o r => @@ -104,7 +104,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint mem (i : positive) (m : t A) : bool := + Fixpoint mem (i : key) (m : t A) : bool := match m with | Leaf => false | Node l o r => @@ -115,7 +115,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint add (i : positive) (v : A) (m : t A) : t A := + Fixpoint add (i : key) (v : A) (m : t A) : t A := match m with | Leaf => match i with @@ -131,7 +131,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint remove (i : positive) (m : t A) : t A := + Fixpoint remove (i : key) (m : t A) : t A := match i with | xH => match m with @@ -163,7 +163,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. (** [elements] *) - Fixpoint xelements (m : t A) (i : positive) : list (positive * A) := + Fixpoint xelements (m : t A) (i : key) : list (key * A) := match m with | Leaf => nil | Node l None r => @@ -190,33 +190,33 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Section CompcertSpec. Theorem gempty: - forall (i: positive), find i empty = None. + forall (i: key), find i empty = None. Proof. destruct i; simpl; auto. Qed. Theorem gss: - forall (i: positive) (x: A) (m: t A), find i (add i x m) = Some x. + forall (i: key) (x: A) (m: t A), find i (add i x m) = Some x. Proof. induction i; destruct m; simpl; auto. Qed. - Lemma gleaf : forall (i : positive), find i (Leaf : t A) = None. + Lemma gleaf : forall (i : key), find i (Leaf : t A) = None. Proof. exact gempty. Qed. Theorem gso: - forall (i j: positive) (x: A) (m: t A), + forall (i j: key) (x: A) (m: t A), i <> j -> find i (add j x m) = find i m. Proof. induction i; intros; destruct j; destruct m; simpl; try rewrite <- (gleaf i); auto; try apply IHi; congruence. Qed. - Lemma rleaf : forall (i : positive), remove i (Leaf : t A) = Leaf. + Lemma rleaf : forall (i : key), remove i (Leaf : t A) = Leaf. Proof. destruct i; simpl; auto. Qed. Theorem grs: - forall (i: positive) (m: t A), find i (remove i m) = None. + forall (i: key) (m: t A), find i (remove i m) = None. Proof. induction i; destruct m. simpl; auto. @@ -236,7 +236,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Theorem gro: - forall (i j: positive) (m: t A), + forall (i j: key) (m: t A), i <> j -> find i (remove j m) = find i m. Proof. induction i; intros; destruct j; destruct m; @@ -265,11 +265,11 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma xelements_correct: - forall (m: t A) (i j : positive) (v: A), + forall (m: t A) (i j : key) (v: A), find i m = Some v -> List.In (append j i, v) (xelements m j). Proof. induction m; intros. - rewrite (gleaf i) in H; congruence. + rewrite (gleaf i) in H; discriminate. destruct o; destruct i; simpl; simpl in H. rewrite append_assoc_1; apply in_or_app; right; apply in_cons; apply IHm2; auto. @@ -282,14 +282,14 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Theorem elements_correct: - forall (m: t A) (i: positive) (v: A), + forall (m: t A) (i: key) (v: A), find i m = Some v -> List.In (i, v) (elements m). Proof. intros m i v H. exact (xelements_correct m i xH H). Qed. - Fixpoint xfind (i j : positive) (m : t A) : option A := + Fixpoint xfind (i j : key) (m : t A) : option A := match i, j with | _, xH => find i m | xO ii, xO jj => xfind ii jj m @@ -298,7 +298,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. end. Lemma xfind_left : - forall (j i : positive) (m1 m2 : t A) (o : option A) (v : A), + forall (j i : key) (m1 m2 : t A) (o : option A) (v : A), xfind i (append j (xO xH)) m1 = Some v -> xfind i j (Node m1 o m2) = Some v. Proof. induction j; intros; destruct i; simpl; simpl in H; auto; try congruence. @@ -306,7 +306,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma xelements_ii : - forall (m: t A) (i j : positive) (v: A), + forall (m: t A) (i j : key) (v: A), List.In (xI i, v) (xelements m (xI j)) -> List.In (i, v) (xelements m j). Proof. induction m. @@ -322,7 +322,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma xelements_io : - forall (m: t A) (i j : positive) (v: A), + forall (m: t A) (i j : key) (v: A), ~List.In (xI i, v) (xelements m (xO j)). Proof. induction m. @@ -337,7 +337,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma xelements_oo : - forall (m: t A) (i j : positive) (v: A), + forall (m: t A) (i j : key) (v: A), List.In (xO i, v) (xelements m (xO j)) -> List.In (i, v) (xelements m j). Proof. induction m. @@ -353,7 +353,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma xelements_oi : - forall (m: t A) (i j : positive) (v: A), + forall (m: t A) (i j : key) (v: A), ~List.In (xO i, v) (xelements m (xI j)). Proof. induction m. @@ -368,7 +368,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma xelements_ih : - forall (m1 m2: t A) (o: option A) (i : positive) (v: A), + forall (m1 m2: t A) (o: option A) (i : key) (v: A), List.In (xI i, v) (xelements (Node m1 o m2) xH) -> List.In (i, v) (xelements m2 xH). Proof. destruct o; simpl; intros; destruct (in_app_or _ _ _ H). @@ -381,7 +381,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma xelements_oh : - forall (m1 m2: t A) (o: option A) (i : positive) (v: A), + forall (m1 m2: t A) (o: option A) (i : key) (v: A), List.In (xO i, v) (xelements (Node m1 o m2) xH) -> List.In (i, v) (xelements m1 xH). Proof. destruct o; simpl; intros; destruct (in_app_or _ _ _ H). @@ -394,7 +394,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma xelements_hi : - forall (m: t A) (i : positive) (v: A), + forall (m: t A) (i : key) (v: A), ~List.In (xH, v) (xelements m (xI i)). Proof. induction m; intros. @@ -409,7 +409,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma xelements_ho : - forall (m: t A) (i : positive) (v: A), + forall (m: t A) (i : key) (v: A), ~List.In (xH, v) (xelements m (xO i)). Proof. induction m; intros. @@ -424,13 +424,13 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma find_xfind_h : - forall (m: t A) (i: positive), find i m = xfind i xH m. + forall (m: t A) (i: key), find i m = xfind i xH m. Proof. destruct i; simpl; auto. Qed. Lemma xelements_complete: - forall (i j : positive) (m: t A) (v: A), + forall (i j : key) (m: t A) (v: A), List.In (i, v) (xelements m j) -> xfind i j m = Some v. Proof. induction i; simpl; intros; destruct j; simpl. @@ -458,7 +458,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Theorem elements_complete: - forall (m: t A) (i: positive) (v: A), + forall (m: t A) (i: key) (v: A), List.In (i, v) (elements m) -> find i m = Some v. Proof. intros m i v H. @@ -479,18 +479,18 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. End CompcertSpec. - Definition MapsTo (i:positive)(v:A)(m:t A) := find i m = Some v. + Definition MapsTo (i:key)(v:A)(m:t A) := find i m = Some v. - Definition In (i:positive)(m:t A) := exists e:A, MapsTo i e m. + Definition In (i:key)(m:t A) := exists e:A, MapsTo i e m. - Definition Empty m := forall (a : positive)(e:A) , ~ MapsTo a e m. + Definition Empty m := forall (a : key)(e:A) , ~ MapsTo a e m. - Definition eq_key (p p':positive*A) := E.eq (fst p) (fst p'). + Definition eq_key (p p':key*A) := E.eq (fst p) (fst p'). - Definition eq_key_elt (p p':positive*A) := + Definition eq_key_elt (p p':key*A) := E.eq (fst p) (fst p') /\ (snd p) = (snd p'). - Definition lt_key (p p':positive*A) := E.lt (fst p) (fst p'). + Definition lt_key (p p':key*A) := E.lt (fst p) (fst p'). Global Instance eqk_equiv : Equivalence eq_key := _. Global Instance eqke_equiv : Equivalence eq_key_elt := _. @@ -715,8 +715,8 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Lemma elements_3w : NoDupA eq_key (elements m). Proof. - change eq_key with (@ME.eqk A). - apply ME.Sort_NoDupA; apply elements_3; auto. + apply ME.Sort_NoDupA. + apply elements_3. Qed. End FMapSpec. @@ -727,9 +727,9 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Section Mapi. - Variable f : positive -> A -> B. + Variable f : key -> A -> B. - Fixpoint xmapi (m : t A) (i : positive) : t B := + Fixpoint xmapi (m : t A) (i : key) : t B := match m with | Leaf => @Leaf B | Node l o r => Node (xmapi l (append i (xO xH))) @@ -746,7 +746,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. End A. Lemma xgmapi: - forall (A B: Type) (f: positive -> A -> B) (i j : positive) (m: t A), + forall (A B: Type) (f: key -> A -> B) (i j : key) (m: t A), find i (xmapi f m j) = option_map (f (append j i)) (find i m). Proof. induction i; intros; destruct m; simpl; auto. @@ -756,7 +756,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Theorem gmapi: - forall (A B: Type) (f: positive -> A -> B) (i: positive) (m: t A), + 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. @@ -820,7 +820,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. | Node l o r => Node (xmap2_l l) (f o None) (xmap2_l r) end. - Lemma xgmap2_l : forall (i : positive) (m : t A), + Lemma xgmap2_l : forall (i : key) (m : t A), f None None = None -> find i (xmap2_l m) = f (find i m) None. Proof. induction i; intros; destruct m; simpl; auto. @@ -832,7 +832,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. | Node l o r => Node (xmap2_r l) (f None o) (xmap2_r r) end. - Lemma xgmap2_r : forall (i : positive) (m : t B), + Lemma xgmap2_r : forall (i : key) (m : t B), f None None = None -> find i (xmap2_r m) = f None (find i m). Proof. induction i; intros; destruct m; simpl; auto. @@ -848,7 +848,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. end end. - Lemma gmap2: forall (i: positive)(m1:t A)(m2: t B), + Lemma gmap2: forall (i: key)(m1:t A)(m2: t B), f None None = None -> find i (_map2 m1 m2) = f (find i m1) (find i m2). Proof. @@ -896,9 +896,9 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Section Fold. Variables A B : Type. - Variable f : positive -> A -> B -> B. + Variable f : key -> A -> B -> B. - Fixpoint xfoldi (m : t A) (v : B) (i : positive) := + Fixpoint xfoldi (m : t A) (v : B) (i : key) := match m with | Leaf _ => v | Node l (Some x) r => @@ -1070,7 +1070,7 @@ Module PositiveMapAdditionalFacts. (* Derivable from the Map interface *) Theorem gsspec: - forall (A:Type)(i j: positive) (x: A) (m: t A), + forall (A:Type)(i j: key) (x: A) (m: t A), find i (add j x m) = if E.eq_dec i j then Some x else find i m. Proof. intros. @@ -1079,7 +1079,7 @@ Module PositiveMapAdditionalFacts. (* Not derivable from the Map interface *) Theorem gsident: - forall (A:Type)(i: positive) (m: t A) (v: A), + forall (A:Type)(i: key) (m: t A) (v: A), find i m = Some v -> add i v m = m. Proof. induction i; intros; destruct m; simpl; simpl in H; try congruence. @@ -1118,4 +1118,3 @@ Module PositiveMapAdditionalFacts. Qed. End PositiveMapAdditionalFacts. - |