From 540fbd2e6d63c1be0dd520499132c134f5b0f8b3 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 16 Apr 2020 23:18:26 +0200 Subject: moved to extra --- lib/extra/HashedMap.v | 448 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 448 insertions(+) create mode 100644 lib/extra/HashedMap.v (limited to 'lib/extra') diff --git a/lib/extra/HashedMap.v b/lib/extra/HashedMap.v new file mode 100644 index 00000000..df724867 --- /dev/null +++ b/lib/extra/HashedMap.v @@ -0,0 +1,448 @@ +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. + +Section MAP2. + + Variable f : option T -> option T -> option T. + + Section NONE_NONE. + Hypothesis f_none_none : f None None = None. + + Fixpoint map2_Empty (b : pmap) := + match b with + | Empty => Empty + | Node b0 bf b1 => + node (map2_Empty b0) (f None bf) (map2_Empty b1) + end. + + Lemma gmap2_Empty: forall i b, + get i (map2_Empty b) = f None (get i b). + Proof. + induction i; destruct b as [ | b0 bf b1]; intros; simpl in *. + all: try congruence. + - replace + (match node (map2_Empty b0) (f None bf) (map2_Empty b1) with + | Empty => None + | Node _ _ c1 => get i c1 + end) + with (get (xI i) (node (map2_Empty b0) (f None bf) (map2_Empty b1))). + + rewrite gnode. + simpl. apply IHi. + + destruct node; auto with pmap. + - replace + (match node (map2_Empty b0) (f None bf) (map2_Empty b1) with + | Empty => None + | Node c0 _ _ => get i c0 + end) + with (get (xO i) (node (map2_Empty b0) (f None bf) (map2_Empty b1))). + + rewrite gnode. + simpl. apply IHi. + + destruct node; auto with pmap. + - change (match node (map2_Empty b0) (f None bf) (map2_Empty b1) with + | Empty => None + | Node _ cf _ => cf + end) with (get xH (node (map2_Empty b0) (f None bf) (map2_Empty b1))). + rewrite gnode. reflexivity. + Qed. + + Fixpoint map2 (a b : pmap) := + match a with + | Empty => map2_Empty b + | (Node a0 af a1) => + match b with + | (Node b0 bf b1) => + node (map2 a0 b0) (f af bf) (map2 a1 b1) + | Empty => + node (map2 a0 Empty) (f af None) (map2 a1 Empty) + end + end. + + Lemma gmap2: forall a b i, + get i (map2 a b) = f (get i a) (get i b). + Proof. + induction a as [ | a0 IHa0 af a1 IHa1]; intros; simpl. + { rewrite gmap2_Empty. + rewrite gempty. + reflexivity. } + destruct b as [ | b0 bf b1 ]; simpl; rewrite gnode. + - destruct i; simpl. + + rewrite IHa1. rewrite gempty. + reflexivity. + + rewrite IHa0. rewrite gempty. + reflexivity. + + reflexivity. + - destruct i; simpl; congruence. + Qed. + End NONE_NONE. + + Section IDEM. + Hypothesis f_idem : forall x, f x x = x. + + Fixpoint map2_idem (a b : pmap) := + if pmap_eq a b then a else + match a with + | Empty => map2_Empty b + | (Node a0 af a1) => + match b with + | (Node b0 bf b1) => + node (map2_idem a0 b0) (f af bf) (map2_idem a1 b1) + | Empty => + node (map2_idem a0 Empty) (f af None) (map2_idem a1 Empty) + end + end. + + Lemma gmap2_idem: forall a b i, + get i (map2_idem a b) = f (get i a) (get i b). + Proof. + induction a as [ | a0 IHa0 af a1 IHa1]; intros; simpl. + { destruct pmap_eq. + - subst b. rewrite gempty. congruence. + - rewrite gempty. + rewrite gmap2_Empty by congruence. + reflexivity. + } + destruct pmap_eq. + { subst b. + congruence. + } + destruct b as [ | b0 bf b1 ]; simpl; rewrite gnode. + - destruct i; simpl. + + rewrite IHa1. rewrite gempty. + reflexivity. + + rewrite IHa0. rewrite gempty. + reflexivity. + + reflexivity. + - destruct i; simpl; congruence. + Qed. + End IDEM. +End MAP2. -- cgit