From 931b424732474cef10858af4959af6f53a082581 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 16 Apr 2020 20:34:23 +0200 Subject: begin HashedMaps --- lib/HashedMap.v | 332 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 332 insertions(+) create mode 100644 lib/HashedMap.v (limited to 'lib') diff --git a/lib/HashedMap.v b/lib/HashedMap.v new file mode 100644 index 00000000..baeb524c --- /dev/null +++ b/lib/HashedMap.v @@ -0,0 +1,332 @@ +Require Import ZArith. +Require Import Bool. +Require Import List. +Require Coq.Logic.Eqdep_dec. + +(* begin from Maps *) +Fixpoint prev_append (i j: positive) {struct i} : positive := + match i with + | xH => j + | xI i' => prev_append i' (xI j) + | xO i' => prev_append i' (xO j) + end. + +Definition prev (i: positive) : positive := + prev_append i xH. + +Lemma prev_append_prev i j: + prev (prev_append i j) = prev_append j i. +Proof. + revert j. unfold prev. + induction i as [i IH|i IH|]. 3: reflexivity. + intros j. simpl. rewrite IH. reflexivity. + intros j. simpl. rewrite IH. reflexivity. +Qed. + +Lemma prev_involutive i : + prev (prev i) = i. +Proof (prev_append_prev i xH). + +Lemma prev_append_inj i j j' : + prev_append i j = prev_append i j' -> j = j'. +Proof. + revert j j'. + induction i as [i Hi|i Hi|]; intros j j' H; auto; + specialize (Hi _ _ H); congruence. +Qed. + +(* end from Maps *) + +Lemma orb_idem: forall b, orb b b = b. +Proof. + destruct b; reflexivity. +Qed. + +Lemma andb_idem: forall b, andb b b = b. +Proof. + destruct b; reflexivity. +Qed. + +Lemma andb_negb_false: forall b, andb b (negb b) = false. +Proof. + destruct b; reflexivity. +Qed. + +Hint Rewrite orb_false_r andb_false_r andb_true_r orb_true_r orb_idem andb_idem andb_negb_false : pmap. + +Parameter T : Type. +Parameter T_eq_dec : forall (x y : T), {x = y} + {x <> y}. + +Inductive pmap : Type := +| Empty : pmap +| Node : pmap -> option T -> pmap -> pmap. +Definition empty := Empty. + +Definition is_empty x := + match x with + | Empty => true + | Node _ _ _ => false + end. + +Definition is_some (x : option T) := + match x with + | Some _ => true + | None => false + end. + +Fixpoint wf x := + match x with + | Empty => true + | Node b0 f b1 => + (wf b0) && (wf b1) && + ((negb (is_empty b0)) || (is_some f) || (negb (is_empty b1))) + end. + +Definition iswf x := (wf x)=true. + +Lemma empty_wf : iswf empty. +Proof. + reflexivity. +Qed. + +Definition pmap_eq : + forall s s': pmap, { s=s' } + { s <> s' }. +Proof. + generalize T_eq_dec. + induction s; destruct s'; repeat decide equality. +Qed. + +Fixpoint get (i : positive) (s : pmap) {struct i} : option T := + match s with + | Empty => None + | Node b0 f b1 => + match i with + | xH => f + | xO ii => get ii b0 + | xI ii => get ii b1 + end + end. + +Lemma gempty : + forall i : positive, + get i Empty = None. +Proof. + destruct i; simpl; reflexivity. +Qed. + +Hint Resolve gempty : pmap. +Hint Rewrite gempty : pmap. + +Definition node (b0 : pmap) (f : option T) (b1 : pmap) : pmap := + match b0, f, b1 with + | Empty, None, Empty => Empty + | _, _, _ => Node b0 f b1 + end. + +Lemma wf_node : + forall b0 f b1, + iswf b0 -> iswf b1 -> iswf (node b0 f b1). +Proof. + destruct b0; destruct f; destruct b1; simpl. + all: unfold iswf; simpl; intros; trivial. + all: autorewrite with pmap; trivial. + all: rewrite H. + all: rewrite H0. + all: reflexivity. +Qed. + +Hint Resolve wf_node: pmap. + +Lemma gnode : + forall b0 f b1 i, + get i (node b0 f b1) = + get i (Node b0 f b1). +Proof. + destruct b0; simpl; trivial. + destruct f; simpl; trivial. + destruct b1; simpl; trivial. + intro. + rewrite gempty. + destruct i; simpl; trivial. + all: symmetry; apply gempty. +Qed. + +Hint Rewrite gnode : pmap. + +Fixpoint set (i : positive) (j : T) (s : pmap) {struct i} : pmap := + match s with + | Empty => + match i with + | xH => Node Empty (Some j) Empty + | xO ii => Node (set ii j Empty) None Empty + | xI ii => Node Empty None (set ii j Empty) + end + | Node b0 f b1 => + match i with + | xH => Node b0 (Some j) b1 + | xO ii => Node (set ii j b0) f b1 + | xI ii => Node b0 f (set ii j b1) + end + end. + +Lemma set_nonempty: + forall i j s, is_empty (set i j s) = false. +Proof. + induction i; destruct s; simpl; trivial. +Qed. + +Hint Rewrite set_nonempty : pmap. +Hint Resolve set_nonempty : pmap. + +Lemma wf_set: + forall i j s, (iswf s) -> (iswf (set i j s)). +Proof. + induction i; destruct s; simpl; trivial. + all: unfold iswf in *; simpl. + all: autorewrite with pmap; simpl; trivial. + 1,3: auto with pmap. + all: intro Z. + all: repeat rewrite andb_true_iff in Z. + all: intuition. +Qed. + +Hint Resolve wf_set : pset. + +Theorem gss : + forall (i : positive) (j : T) (s : pmap), + get i (set i j s) = Some j. +Proof. + induction i; destruct s; simpl; auto. +Qed. + +Hint Resolve gss : pmap. +Hint Rewrite gss : pmap. + +Theorem gso : + forall (i j : positive) (k : T) (s : pmap), + i <> j -> + get j (set i k s) = get j s. +Proof. + induction i; destruct j; destruct s; simpl; intro; auto with pmap. + 5, 6: congruence. + all: rewrite IHi by congruence. + all: trivial. + all: apply gempty. +Qed. + +Hint Resolve gso : pmap. + +Fixpoint remove (i : positive) (s : pmap) { struct i } : pmap := + match i with + | xH => + match s with + | Empty => Empty + | Node b0 f b1 => node b0 None b1 + end + | xO ii => + match s with + | Empty => Empty + | Node b0 f b1 => node (remove ii b0) f b1 + end + | xI ii => + match s with + | Empty => Empty + | Node b0 f b1 => node b0 f (remove ii b1) + end + end. + +Lemma wf_remove : + forall i s, (iswf s) -> (iswf (remove i s)). +Proof. + induction i; destruct s; simpl; trivial. + all: unfold iswf in *; simpl. + all: intro Z. + all: repeat rewrite andb_true_iff in Z. + all: apply wf_node. + all: intuition. + all: apply IHi. + all: assumption. +Qed. + +Fixpoint remove_noncanon (i : positive) (s : pmap) { struct i } : pmap := + match i with + | xH => + match s with + | Empty => Empty + | Node b0 f b1 => Node b0 None b1 + end + | xO ii => + match s with + | Empty => Empty + | Node b0 f b1 => Node (remove_noncanon ii b0) f b1 + end + | xI ii => + match s with + | Empty => Empty + | Node b0 f b1 => Node b0 f (remove_noncanon ii b1) + end + end. + +Lemma remove_noncanon_same: + forall i j s, (get j (remove i s)) = (get j (remove_noncanon i s)). +Proof. + induction i; destruct s; simpl; trivial. + all: rewrite gnode. + 3: reflexivity. + all: destruct j; simpl; trivial. +Qed. + +Lemma remove_empty : + forall i, remove i Empty = Empty. +Proof. + induction i; simpl; trivial. +Qed. + +Hint Rewrite remove_empty : pmap. +Hint Resolve remove_empty : pmap. + +Lemma gremove_noncanon_s : + forall i : positive, + forall s : pmap, + get i (remove_noncanon i s) = None. +Proof. + induction i; destruct s; simpl; trivial. +Qed. + +Theorem grs : + forall i : positive, + forall s : pmap, + get i (remove i s) = None. +Proof. + intros. + rewrite remove_noncanon_same. + apply gremove_noncanon_s. +Qed. + +Hint Resolve grs : pmap. +Hint Rewrite grs : pmap. + +Lemma gremove_noncanon_o : + forall i j : positive, + forall s : pmap, + i<>j -> + get j (remove_noncanon i s) = get j s. +Proof. + induction i; destruct j; destruct s; simpl; intro; trivial. + 1, 2: rewrite IHi by congruence. + 1, 2: reflexivity. + congruence. +Qed. + +Theorem gro : + forall (i j : positive) (s : pmap), + i<>j -> + get j (remove i s) = get j s. +Proof. + intros. + rewrite remove_noncanon_same. + apply gremove_noncanon_o. + assumption. +Qed. + +Hint Resolve gro : pmap. -- cgit