diff options
Diffstat (limited to 'theories7/IntMap/Map.v')
| -rw-r--r-- | theories7/IntMap/Map.v | 786 |
1 files changed, 786 insertions, 0 deletions
diff --git a/theories7/IntMap/Map.v b/theories7/IntMap/Map.v new file mode 100644 index 00000000..00ba3f8a --- /dev/null +++ b/theories7/IntMap/Map.v @@ -0,0 +1,786 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(*i $Id: Map.v,v 1.1.2.1 2004/07/16 19:31:27 herbelin Exp $ i*) + +(** Definition of finite sets as trees indexed by adresses *) + +Require Bool. +Require Sumbool. +Require ZArith. +Require Addr. +Require Adist. +Require Addec. + + +Section MapDefs. + +(** We define maps from ad to A. *) + Variable A : Set. + + Inductive Map : Set := + M0 : Map + | M1 : ad -> A -> Map + | M2 : Map -> Map -> Map. + + Inductive option : Set := + NONE : option + | SOME : A -> option. + + Lemma option_sum : (o:option) {y:A | o=(SOME y)}+{o=NONE}. + Proof. + Induction o. Right . Reflexivity. + Left . Split with a. Reflexivity. + Qed. + + (** The semantics of maps is given by the function [MapGet]. + The semantics of a map [m] is a partial, finite function from + [ad] to [A]: *) + + Fixpoint MapGet [m:Map] : ad -> option := + Cases m of + M0 => [a:ad] NONE + | (M1 x y) => [a:ad] + if (ad_eq x a) + then (SOME y) + else NONE + | (M2 m1 m2) => [a:ad] + Cases a of + ad_z => (MapGet m1 ad_z) + | (ad_x xH) => (MapGet m2 ad_z) + | (ad_x (xO p)) => (MapGet m1 (ad_x p)) + | (ad_x (xI p)) => (MapGet m2 (ad_x p)) + end + end. + + Definition newMap := M0. + + Definition MapSingleton := M1. + + Definition eqm := [g,g':ad->option] (a:ad) (g a)=(g' a). + + Lemma newMap_semantics : (eqm (MapGet newMap) [a:ad] NONE). + Proof. + Simpl. Unfold eqm. Trivial. + Qed. + + Lemma MapSingleton_semantics : (a:ad) (y:A) + (eqm (MapGet (MapSingleton a y)) [a':ad] if (ad_eq a a') then (SOME y) else NONE). + Proof. + Simpl. Unfold eqm. Trivial. + Qed. + + Lemma M1_semantics_1 : (a:ad) (y:A) (MapGet (M1 a y) a)=(SOME y). + Proof. + Unfold MapGet. Intros. Rewrite (ad_eq_correct a). Reflexivity. + Qed. + + Lemma M1_semantics_2 : + (a,a':ad) (y:A) (ad_eq a a')=false -> (MapGet (M1 a y) a')=NONE. + Proof. + Intros. Simpl. Rewrite H. Reflexivity. + Qed. + + Lemma Map2_semantics_1 : + (m,m':Map) (eqm (MapGet m) [a:ad] (MapGet (M2 m m') (ad_double a))). + Proof. + Unfold eqm. Induction a; Trivial. + Qed. + + Lemma Map2_semantics_1_eq : (m,m':Map) (f:ad->option) (eqm (MapGet (M2 m m')) f) + -> (eqm (MapGet m) [a:ad] (f (ad_double a))). + Proof. + Unfold eqm. + Intros. + Rewrite <- (H (ad_double a)). + Exact (Map2_semantics_1 m m' a). + Qed. + + Lemma Map2_semantics_2 : + (m,m':Map) (eqm (MapGet m') [a:ad] (MapGet (M2 m m') (ad_double_plus_un a))). + Proof. + Unfold eqm. Induction a; Trivial. + Qed. + + Lemma Map2_semantics_2_eq : (m,m':Map) (f:ad->option) (eqm (MapGet (M2 m m')) f) + -> (eqm (MapGet m') [a:ad] (f (ad_double_plus_un a))). + Proof. + Unfold eqm. + Intros. + Rewrite <- (H (ad_double_plus_un a)). + Exact (Map2_semantics_2 m m' a). + Qed. + + Lemma MapGet_M2_bit_0_0 : (a:ad) (ad_bit_0 a)=false + -> (m,m':Map) (MapGet (M2 m m') a)=(MapGet m (ad_div_2 a)). + Proof. + Induction a; Trivial. Induction p. Intros. Discriminate H0. + Trivial. + Intros. Discriminate H. + Qed. + + Lemma MapGet_M2_bit_0_1 : (a:ad) (ad_bit_0 a)=true + -> (m,m':Map) (MapGet (M2 m m') a)=(MapGet m' (ad_div_2 a)). + Proof. + Induction a. Intros. Discriminate H. + Induction p. Trivial. + Intros. Discriminate H0. + Trivial. + Qed. + + Lemma MapGet_M2_bit_0_if : (m,m':Map) (a:ad) (MapGet (M2 m m') a)= + (if (ad_bit_0 a) then (MapGet m' (ad_div_2 a)) else (MapGet m (ad_div_2 a))). + Proof. + Intros. Elim (sumbool_of_bool (ad_bit_0 a)). Intro H. Rewrite H. + Apply MapGet_M2_bit_0_1; Assumption. + Intro H. Rewrite H. Apply MapGet_M2_bit_0_0; Assumption. + Qed. + + Lemma MapGet_M2_bit_0 : (m,m',m'':Map) + (a:ad) (if (ad_bit_0 a) then (MapGet (M2 m' m) a) else (MapGet (M2 m m'') a))= + (MapGet m (ad_div_2 a)). + Proof. + Intros. Elim (sumbool_of_bool (ad_bit_0 a)). Intro H. Rewrite H. + Apply MapGet_M2_bit_0_1; Assumption. + Intro H. Rewrite H. Apply MapGet_M2_bit_0_0; Assumption. + Qed. + + Lemma Map2_semantics_3 : (m,m':Map) (eqm (MapGet (M2 m m')) + [a:ad] Cases (ad_bit_0 a) of + false => (MapGet m (ad_div_2 a)) + | true => (MapGet m' (ad_div_2 a)) + end). + Proof. + Unfold eqm. + Induction a; Trivial. + Induction p; Trivial. + Qed. + + Lemma Map2_semantics_3_eq : (m,m':Map) (f,f':ad->option) + (eqm (MapGet m) f) -> (eqm (MapGet m') f') -> (eqm (MapGet (M2 m m')) + [a:ad] Cases (ad_bit_0 a) of + false => (f (ad_div_2 a)) + | true => (f' (ad_div_2 a)) + end). + Proof. + Unfold eqm. + Intros. + Rewrite <- (H (ad_div_2 a)). + Rewrite <- (H0 (ad_div_2 a)). + Exact (Map2_semantics_3 m m' a). + Qed. + + Fixpoint MapPut1 [a:ad; y:A; a':ad; y':A; p:positive] : Map := + Cases p of + (xO p') => let m = (MapPut1 (ad_div_2 a) y (ad_div_2 a') y' p') in + Cases (ad_bit_0 a) of + false => (M2 m M0) + | true => (M2 M0 m) + end + | _ => Cases (ad_bit_0 a) of + false => (M2 (M1 (ad_div_2 a) y) (M1 (ad_div_2 a') y')) + | true => (M2 (M1 (ad_div_2 a') y') (M1 (ad_div_2 a) y)) + end + end. + + Lemma MapGet_if_commute : (b:bool) (m,m':Map) (a:ad) + (MapGet (if b then m else m') a)=(if b then (MapGet m a) else (MapGet m' a)). + Proof. + Intros. Case b; Trivial. + Qed. + + (*i + Lemma MapGet_M2_bit_0_1' : (m,m',m'',m''':Map) + (a:ad) (MapGet (if (ad_bit_0 a) then (M2 m m') else (M2 m'' m''')) a)= + (MapGet (if (ad_bit_0 a) then m' else m'') (ad_div_2 a)). + Proof. + Intros. Rewrite (MapGet_if_commute (ad_bit_0 a)). Rewrite (MapGet_if_commute (ad_bit_0 a)). + Cut (ad_bit_0 a)=false\/(ad_bit_0 a)=true. Intros. Elim H. Intros. Rewrite H0. + Apply MapGet_M2_bit_0_0. Assumption. + Intros. Rewrite H0. Apply MapGet_M2_bit_0_1. Assumption. + Case (ad_bit_0 a); Auto. + Qed. + i*) + + Lemma MapGet_if_same : (m:Map) (b:bool) (a:ad) + (MapGet (if b then m else m) a)=(MapGet m a). + Proof. + Induction b;Trivial. + Qed. + + Lemma MapGet_M2_bit_0_2 : (m,m',m'':Map) + (a:ad) (MapGet (if (ad_bit_0 a) then (M2 m m') else (M2 m' m'')) a)= + (MapGet m' (ad_div_2 a)). + Proof. + Intros. Rewrite MapGet_if_commute. Apply MapGet_M2_bit_0. + Qed. + + Lemma MapPut1_semantics_1 : (p:positive) (a,a':ad) (y,y':A) + (ad_xor a a')=(ad_x p) + -> (MapGet (MapPut1 a y a' y' p) a)=(SOME y). + Proof. + Induction p. Intros. Unfold MapPut1. Rewrite MapGet_M2_bit_0_2. Apply M1_semantics_1. + Intros. Simpl. Rewrite MapGet_M2_bit_0_2. Apply H. Rewrite <- ad_xor_div_2. Rewrite H0. + Reflexivity. + Intros. Unfold MapPut1. Rewrite MapGet_M2_bit_0_2. Apply M1_semantics_1. + Qed. + + Lemma MapPut1_semantics_2 : (p:positive) (a,a':ad) (y,y':A) + (ad_xor a a')=(ad_x p) + -> (MapGet (MapPut1 a y a' y' p) a')=(SOME y'). + Proof. + Induction p. Intros. Unfold MapPut1. Rewrite (ad_neg_bit_0_2 a a' p0 H0). + Rewrite if_negb. Rewrite MapGet_M2_bit_0_2. Apply M1_semantics_1. + Intros. Simpl. Rewrite (ad_same_bit_0 a a' p0 H0). Rewrite MapGet_M2_bit_0_2. + Apply H. Rewrite <- ad_xor_div_2. Rewrite H0. Reflexivity. + Intros. Unfold MapPut1. Rewrite (ad_neg_bit_0_1 a a' H). Rewrite if_negb. + Rewrite MapGet_M2_bit_0_2. Apply M1_semantics_1. + Qed. + + Lemma MapGet_M2_both_NONE : (m,m':Map) (a:ad) + (MapGet m (ad_div_2 a))=NONE -> (MapGet m' (ad_div_2 a))=NONE -> + (MapGet (M2 m m') a)=NONE. + Proof. + Intros. Rewrite (Map2_semantics_3 m m' a). + Case (ad_bit_0 a); Assumption. + Qed. + + Lemma MapPut1_semantics_3 : (p:positive) (a,a',a0:ad) (y,y':A) + (ad_xor a a')=(ad_x p) -> (ad_eq a a0)=false -> (ad_eq a' a0)=false -> + (MapGet (MapPut1 a y a' y' p) a0)=NONE. + Proof. + Induction p. Intros. Unfold MapPut1. Elim (ad_neq a a0 H1). Intro. Rewrite H3. Rewrite if_negb. + Rewrite MapGet_M2_bit_0_2. Apply M1_semantics_2. Apply ad_div_bit_neq. Assumption. + Rewrite (ad_neg_bit_0_2 a a' p0 H0) in H3. Rewrite (negb_intro (ad_bit_0 a')). + Rewrite (negb_intro (ad_bit_0 a0)). Rewrite H3. Reflexivity. + Intro. Elim (ad_neq a' a0 H2). Intro. Rewrite (ad_neg_bit_0_2 a a' p0 H0). Rewrite H4. + Rewrite (negb_elim (ad_bit_0 a0)). Rewrite MapGet_M2_bit_0_2. + Apply M1_semantics_2; Assumption. + Intro; Case (ad_bit_0 a); Apply MapGet_M2_both_NONE; + Apply M1_semantics_2; Assumption. + Intros. Simpl. Elim (ad_neq a a0 H1). Intro. Rewrite H3. Rewrite if_negb. + Rewrite MapGet_M2_bit_0_2. Reflexivity. + Intro. Elim (ad_neq a' a0 H2). Intro. Rewrite (ad_same_bit_0 a a' p0 H0). Rewrite H4. + Rewrite if_negb. Rewrite MapGet_M2_bit_0_2. Reflexivity. + Intro. Cut (ad_xor (ad_div_2 a) (ad_div_2 a'))=(ad_x p0). Intro. + Case (ad_bit_0 a); Apply MapGet_M2_both_NONE; Trivial; + Apply H; Assumption. + Rewrite <- ad_xor_div_2. Rewrite H0. Reflexivity. + Intros. Simpl. Elim (ad_neq a a0 H0). Intro. Rewrite H2. Rewrite if_negb. + Rewrite MapGet_M2_bit_0_2. Apply M1_semantics_2. Apply ad_div_bit_neq. Assumption. + Rewrite (ad_neg_bit_0_1 a a' H) in H2. Rewrite (negb_intro (ad_bit_0 a')). + Rewrite (negb_intro (ad_bit_0 a0)). Rewrite H2. Reflexivity. + Intro. Elim (ad_neq a' a0 H1). Intro. Rewrite (ad_neg_bit_0_1 a a' H). Rewrite H3. + Rewrite (negb_elim (ad_bit_0 a0)). Rewrite MapGet_M2_bit_0_2. + Apply M1_semantics_2; Assumption. + Intro. Case (ad_bit_0 a); Apply MapGet_M2_both_NONE; Apply M1_semantics_2; Assumption. + Qed. + + Lemma MapPut1_semantics : (p:positive) (a,a':ad) (y,y':A) + (ad_xor a a')=(ad_x p) + -> (eqm (MapGet (MapPut1 a y a' y' p)) + [a0:ad] if (ad_eq a a0) then (SOME y) + else if (ad_eq a' a0) then (SOME y') else NONE). + Proof. + Unfold eqm. Intros. Elim (sumbool_of_bool (ad_eq a a0)). Intro H0. Rewrite H0. + Rewrite <- (ad_eq_complete ? ? H0). Exact (MapPut1_semantics_1 p a a' y y' H). + Intro H0. Rewrite H0. Elim (sumbool_of_bool (ad_eq a' a0)). Intro H1. + Rewrite <- (ad_eq_complete ? ? H1). Rewrite (ad_eq_correct a'). + Exact (MapPut1_semantics_2 p a a' y y' H). + Intro H1. Rewrite H1. Exact (MapPut1_semantics_3 p a a' a0 y y' H H0 H1). + Qed. + + Lemma MapPut1_semantics' : (p:positive) (a,a':ad) (y,y':A) + (ad_xor a a')=(ad_x p) + -> (eqm (MapGet (MapPut1 a y a' y' p)) + [a0:ad] if (ad_eq a' a0) then (SOME y') + else if (ad_eq a a0) then (SOME y) else NONE). + Proof. + Unfold eqm. Intros. Rewrite (MapPut1_semantics p a a' y y' H a0). + Elim (sumbool_of_bool (ad_eq a a0)). Intro H0. Rewrite H0. + Rewrite <- (ad_eq_complete a a0 H0). Rewrite (ad_eq_comm a' a). + Rewrite (ad_xor_eq_false a a' p H). Reflexivity. + Intro H0. Rewrite H0. Reflexivity. + Qed. + + Fixpoint MapPut [m:Map] : ad -> A -> Map := + Cases m of + M0 => M1 + | (M1 a y) => [a':ad; y':A] + Cases (ad_xor a a') of + ad_z => (M1 a' y') + | (ad_x p) => (MapPut1 a y a' y' p) + end + | (M2 m1 m2) => [a:ad; y:A] + Cases a of + ad_z => (M2 (MapPut m1 ad_z y) m2) + | (ad_x xH) => (M2 m1 (MapPut m2 ad_z y)) + | (ad_x (xO p)) => (M2 (MapPut m1 (ad_x p) y) m2) + | (ad_x (xI p)) => (M2 m1 (MapPut m2 (ad_x p) y)) + end + end. + + Lemma MapPut_semantics_1 : (a:ad) (y:A) (a0:ad) + (MapGet (MapPut M0 a y) a0)=(MapGet (M1 a y) a0). + Proof. + Trivial. + Qed. + + Lemma MapPut_semantics_2_1 : (a:ad) (y,y':A) (a0:ad) + (MapGet (MapPut (M1 a y) a y') a0)=(if (ad_eq a a0) then (SOME y') else NONE). + Proof. + Simpl. Intros. Rewrite (ad_xor_nilpotent a). Trivial. + Qed. + + Lemma MapPut_semantics_2_2 : (a,a':ad) (y,y':A) (a0:ad) (a'':ad) (ad_xor a a')=a'' -> + (MapGet (MapPut (M1 a y) a' y') a0)= + (if (ad_eq a' a0) then (SOME y') else + if (ad_eq a a0) then (SOME y) else NONE). + Proof. + Induction a''. Intro. Rewrite (ad_xor_eq ? ? H). Rewrite MapPut_semantics_2_1. + Case (ad_eq a' a0); Trivial. + Intros. Simpl. Rewrite H. Rewrite (MapPut1_semantics p a a' y y' H a0). + Elim (sumbool_of_bool (ad_eq a a0)). Intro H0. Rewrite H0. Rewrite <- (ad_eq_complete ? ? H0). + Rewrite (ad_eq_comm a' a). Rewrite (ad_xor_eq_false ? ? ? H). Reflexivity. + Intro H0. Rewrite H0. Reflexivity. + Qed. + + Lemma MapPut_semantics_2 : (a,a':ad) (y,y':A) (a0:ad) + (MapGet (MapPut (M1 a y) a' y') a0)= + (if (ad_eq a' a0) then (SOME y') else + if (ad_eq a a0) then (SOME y) else NONE). + Proof. + Intros. Apply MapPut_semantics_2_2 with a'':=(ad_xor a a'); Trivial. + Qed. + + Lemma MapPut_semantics_3_1 : (m,m':Map) (a:ad) (y:A) + (MapPut (M2 m m') a y)=(if (ad_bit_0 a) then (M2 m (MapPut m' (ad_div_2 a) y)) + else (M2 (MapPut m (ad_div_2 a) y) m')). + Proof. + Induction a. Trivial. + Induction p; Trivial. + Qed. + + Lemma MapPut_semantics : (m:Map) (a:ad) (y:A) + (eqm (MapGet (MapPut m a y)) [a':ad] if (ad_eq a a') then (SOME y) else (MapGet m a')). + Proof. + Unfold eqm. Induction m. Exact MapPut_semantics_1. + Intros. Unfold 2 MapGet. Apply MapPut_semantics_2; Assumption. + Intros. Rewrite MapPut_semantics_3_1. Rewrite (MapGet_M2_bit_0_if m0 m1 a0). + Elim (sumbool_of_bool (ad_bit_0 a)). Intro H1. Rewrite H1. Rewrite MapGet_M2_bit_0_if. + Elim (sumbool_of_bool (ad_bit_0 a0)). Intro H2. Rewrite H2. + Rewrite (H0 (ad_div_2 a) y (ad_div_2 a0)). Elim (sumbool_of_bool (ad_eq a a0)). + Intro H3. Rewrite H3. Rewrite (ad_div_eq ? ? H3). Reflexivity. + Intro H3. Rewrite H3. Rewrite <- H2 in H1. Rewrite (ad_div_bit_neq ? ? H3 H1). Reflexivity. + Intro H2. Rewrite H2. Rewrite (ad_eq_comm a a0). Rewrite (ad_bit_0_neq a0 a H2 H1). + Reflexivity. + Intro H1. Rewrite H1. Rewrite MapGet_M2_bit_0_if. Elim (sumbool_of_bool (ad_bit_0 a0)). + Intro H2. Rewrite H2. Rewrite (ad_bit_0_neq a a0 H1 H2). Reflexivity. + Intro H2. Rewrite H2. Rewrite (H (ad_div_2 a) y (ad_div_2 a0)). + Elim (sumbool_of_bool (ad_eq a a0)). Intro H3. Rewrite H3. + Rewrite (ad_div_eq a a0 H3). Reflexivity. + Intro H3. Rewrite H3. Rewrite <- H2 in H1. Rewrite (ad_div_bit_neq a a0 H3 H1). Reflexivity. + Qed. + + Fixpoint MapPut_behind [m:Map] : ad -> A -> Map := + Cases m of + M0 => M1 + | (M1 a y) => [a':ad; y':A] + Cases (ad_xor a a') of + ad_z => m + | (ad_x p) => (MapPut1 a y a' y' p) + end + | (M2 m1 m2) => [a:ad; y:A] + Cases a of + ad_z => (M2 (MapPut_behind m1 ad_z y) m2) + | (ad_x xH) => (M2 m1 (MapPut_behind m2 ad_z y)) + | (ad_x (xO p)) => (M2 (MapPut_behind m1 (ad_x p) y) m2) + | (ad_x (xI p)) => (M2 m1 (MapPut_behind m2 (ad_x p) y)) + end + end. + + Lemma MapPut_behind_semantics_3_1 : (m,m':Map) (a:ad) (y:A) + (MapPut_behind (M2 m m') a y)= + (if (ad_bit_0 a) then (M2 m (MapPut_behind m' (ad_div_2 a) y)) + else (M2 (MapPut_behind m (ad_div_2 a) y) m')). + Proof. + Induction a. Trivial. + Induction p; Trivial. + Qed. + + Lemma MapPut_behind_as_before_1 : (a,a',a0:ad) (ad_eq a' a0)=false -> + (y,y':A) (MapGet (MapPut (M1 a y) a' y') a0) + =(MapGet (MapPut_behind (M1 a y) a' y') a0). + Proof. + Intros a a' a0. Simpl. Intros H y y'. Elim (ad_sum (ad_xor a a')). Intro H0. Elim H0. + Intros p H1. Rewrite H1. Reflexivity. + Intro H0. Rewrite H0. Rewrite (ad_xor_eq ? ? H0). Rewrite (M1_semantics_2 a' a0 y H). + Exact (M1_semantics_2 a' a0 y' H). + Qed. + + Lemma MapPut_behind_as_before : (m:Map) (a:ad) (y:A) + (a0:ad) (ad_eq a a0)=false -> + (MapGet (MapPut m a y) a0)=(MapGet (MapPut_behind m a y) a0). + Proof. + Induction m. Trivial. + Intros a y a' y' a0 H. Exact (MapPut_behind_as_before_1 a a' a0 H y y'). + Intros. Rewrite MapPut_semantics_3_1. Rewrite MapPut_behind_semantics_3_1. + Elim (sumbool_of_bool (ad_bit_0 a)). Intro H2. Rewrite H2. Rewrite MapGet_M2_bit_0_if. + Rewrite MapGet_M2_bit_0_if. Elim (sumbool_of_bool (ad_bit_0 a0)). Intro H3. + Rewrite H3. Apply H0. Rewrite <- H3 in H2. Exact (ad_div_bit_neq a a0 H1 H2). + Intro H3. Rewrite H3. Reflexivity. + Intro H2. Rewrite H2. Rewrite MapGet_M2_bit_0_if. Rewrite MapGet_M2_bit_0_if. + Elim (sumbool_of_bool (ad_bit_0 a0)). Intro H3. Rewrite H3. Reflexivity. + Intro H3. Rewrite H3. Apply H. Rewrite <- H3 in H2. Exact (ad_div_bit_neq a a0 H1 H2). + Qed. + + Lemma MapPut_behind_new : (m:Map) (a:ad) (y:A) + (MapGet (MapPut_behind m a y) a)=(Cases (MapGet m a) of + (SOME y') => (SOME y') + | _ => (SOME y) + end). + Proof. + Induction m. Simpl. Intros. Rewrite (ad_eq_correct a). Reflexivity. + Intros. Elim (ad_sum (ad_xor a a1)). Intro H. Elim H. Intros p H0. Simpl. + Rewrite H0. Rewrite (ad_xor_eq_false a a1 p). Exact (MapPut1_semantics_2 p a a1 a0 y H0). + Assumption. + Intro H. Simpl. Rewrite H. Rewrite <- (ad_xor_eq ? ? H). Rewrite (ad_eq_correct a). + Exact (M1_semantics_1 a a0). + Intros. Rewrite MapPut_behind_semantics_3_1. Rewrite (MapGet_M2_bit_0_if m0 m1 a). + Elim (sumbool_of_bool (ad_bit_0 a)). Intro H1. Rewrite H1. Rewrite (MapGet_M2_bit_0_1 a H1). + Exact (H0 (ad_div_2 a) y). + Intro H1. Rewrite H1. Rewrite (MapGet_M2_bit_0_0 a H1). Exact (H (ad_div_2 a) y). + Qed. + + Lemma MapPut_behind_semantics : (m:Map) (a:ad) (y:A) + (eqm (MapGet (MapPut_behind m a y)) + [a':ad] Cases (MapGet m a') of + (SOME y') => (SOME y') + | _ => if (ad_eq a a') then (SOME y) else NONE + end). + Proof. + Unfold eqm. Intros. Elim (sumbool_of_bool (ad_eq a a0)). Intro H. Rewrite H. + Rewrite (ad_eq_complete ? ? H). Apply MapPut_behind_new. + Intro H. Rewrite H. Rewrite <- (MapPut_behind_as_before m a y a0 H). + Rewrite (MapPut_semantics m a y a0). Rewrite H. Case (MapGet m a0); Trivial. + Qed. + + Definition makeM2 := [m,m':Map] Cases m m' of + M0 M0 => M0 + | M0 (M1 a y) => (M1 (ad_double_plus_un a) y) + | (M1 a y) M0 => (M1 (ad_double a) y) + | _ _ => (M2 m m') + end. + + Lemma makeM2_M2 : (m,m':Map) (eqm (MapGet (makeM2 m m')) (MapGet (M2 m m'))). + Proof. + Unfold eqm. Intros. Elim (sumbool_of_bool (ad_bit_0 a)). Intro H. + Rewrite (MapGet_M2_bit_0_1 a H m m'). Case m'. Case m. Reflexivity. + Intros a0 y. Simpl. Rewrite (ad_bit_0_1_not_double a H a0). Reflexivity. + Intros m1 m2. Unfold makeM2. Rewrite MapGet_M2_bit_0_1. Reflexivity. + Assumption. + Case m. Intros a0 y. Simpl. Elim (sumbool_of_bool (ad_eq a0 (ad_div_2 a))). + Intro H0. Rewrite H0. Rewrite (ad_eq_complete ? ? H0). Rewrite (ad_div_2_double_plus_un a H). + Rewrite (ad_eq_correct a). Reflexivity. + Intro H0. Rewrite H0. Rewrite (ad_eq_comm a0 (ad_div_2 a)) in H0. + Rewrite (ad_not_div_2_not_double_plus_un a a0 H0). Reflexivity. + Intros a0 y0 a1 y1. Unfold makeM2. Rewrite MapGet_M2_bit_0_1. Reflexivity. + Assumption. + Intros m1 m2 a0 y. Unfold makeM2. Rewrite MapGet_M2_bit_0_1. Reflexivity. + Assumption. + Intros m1 m2. Unfold makeM2. + Cut (MapGet (M2 m (M2 m1 m2)) a)=(MapGet (M2 m1 m2) (ad_div_2 a)). + Case m; Trivial. + Exact (MapGet_M2_bit_0_1 a H m (M2 m1 m2)). + Intro H. Rewrite (MapGet_M2_bit_0_0 a H m m'). Case m. Case m'. Reflexivity. + Intros a0 y. Simpl. Rewrite (ad_bit_0_0_not_double_plus_un a H a0). Reflexivity. + Intros m1 m2. Unfold makeM2. Rewrite MapGet_M2_bit_0_0. Reflexivity. + Assumption. + Case m'. Intros a0 y. Simpl. Elim (sumbool_of_bool (ad_eq a0 (ad_div_2 a))). Intro H0. + Rewrite H0. Rewrite (ad_eq_complete ? ? H0). Rewrite (ad_div_2_double a H). + Rewrite (ad_eq_correct a). Reflexivity. + Intro H0. Rewrite H0. Rewrite (ad_eq_comm (ad_double a0) a). + Rewrite (ad_eq_comm a0 (ad_div_2 a)) in H0. Rewrite (ad_not_div_2_not_double a a0 H0). + Reflexivity. + Intros a0 y0 a1 y1. Unfold makeM2. Rewrite MapGet_M2_bit_0_0. Reflexivity. + Assumption. + Intros m1 m2 a0 y. Unfold makeM2. Rewrite MapGet_M2_bit_0_0. Reflexivity. + Assumption. + Intros m1 m2. Unfold makeM2. Exact (MapGet_M2_bit_0_0 a H (M2 m1 m2) m'). + Qed. + + Fixpoint MapRemove [m:Map] : ad -> Map := + Cases m of + M0 => [_:ad] M0 + | (M1 a y) => [a':ad] + Cases (ad_eq a a') of + true => M0 + | false => m + end + | (M2 m1 m2) => [a:ad] + if (ad_bit_0 a) + then (makeM2 m1 (MapRemove m2 (ad_div_2 a))) + else (makeM2 (MapRemove m1 (ad_div_2 a)) m2) + end. + + Lemma MapRemove_semantics : (m:Map) (a:ad) + (eqm (MapGet (MapRemove m a)) [a':ad] if (ad_eq a a') then NONE else (MapGet m a')). + Proof. + Unfold eqm. Induction m. Simpl. Intros. Case (ad_eq a a0); Trivial. + Intros. Simpl. Elim (sumbool_of_bool (ad_eq a1 a2)). Intro H. Rewrite H. + Elim (sumbool_of_bool (ad_eq a a1)). Intro H0. Rewrite H0. Reflexivity. + Intro H0. Rewrite H0. Rewrite (ad_eq_complete ? ? H) in H0. Exact (M1_semantics_2 a a2 a0 H0). + Intro H. Elim (sumbool_of_bool (ad_eq a a1)). Intro H0. Rewrite H0. Rewrite H. + Rewrite <- (ad_eq_complete ? ? H0) in H. Rewrite H. Reflexivity. + Intro H0. Rewrite H0. Rewrite H. Reflexivity. + Intros. Change (MapGet (if (ad_bit_0 a) + then (makeM2 m0 (MapRemove m1 (ad_div_2 a))) + else (makeM2 (MapRemove m0 (ad_div_2 a)) m1)) + a0) + =(if (ad_eq a a0) then NONE else (MapGet (M2 m0 m1) a0)). + Elim (sumbool_of_bool (ad_bit_0 a)). Intro H1. Rewrite H1. + Rewrite (makeM2_M2 m0 (MapRemove m1 (ad_div_2 a)) a0). Elim (sumbool_of_bool (ad_bit_0 a0)). + Intro H2. Rewrite MapGet_M2_bit_0_1. Rewrite (H0 (ad_div_2 a) (ad_div_2 a0)). + Elim (sumbool_of_bool (ad_eq a a0)). Intro H3. Rewrite H3. Rewrite (ad_div_eq ? ? H3). + Reflexivity. + Intro H3. Rewrite H3. Rewrite <- H2 in H1. Rewrite (ad_div_bit_neq ? ? H3 H1). + Rewrite (MapGet_M2_bit_0_1 a0 H2 m0 m1). Reflexivity. + Assumption. + Intro H2. Rewrite (MapGet_M2_bit_0_0 a0 H2 m0 (MapRemove m1 (ad_div_2 a))). + Rewrite (ad_eq_comm a a0). Rewrite (ad_bit_0_neq ? ? H2 H1). + Rewrite (MapGet_M2_bit_0_0 a0 H2 m0 m1). Reflexivity. + Intro H1. Rewrite H1. Rewrite (makeM2_M2 (MapRemove m0 (ad_div_2 a)) m1 a0). + Elim (sumbool_of_bool (ad_bit_0 a0)). Intro H2. Rewrite MapGet_M2_bit_0_1. + Rewrite (MapGet_M2_bit_0_1 a0 H2 m0 m1). Rewrite (ad_bit_0_neq a a0 H1 H2). Reflexivity. + Assumption. + Intro H2. Rewrite MapGet_M2_bit_0_0. Rewrite (H (ad_div_2 a) (ad_div_2 a0)). + Rewrite (MapGet_M2_bit_0_0 a0 H2 m0 m1). Elim (sumbool_of_bool (ad_eq a a0)). Intro H3. + Rewrite H3. Rewrite (ad_div_eq ? ? H3). Reflexivity. + Intro H3. Rewrite H3. Rewrite <- H2 in H1. Rewrite (ad_div_bit_neq ? ? H3 H1). Reflexivity. + Assumption. + Qed. + + Fixpoint MapCard [m:Map] : nat := + Cases m of + M0 => O + | (M1 _ _) => (S O) + | (M2 m m') => (plus (MapCard m) (MapCard m')) + end. + + Fixpoint MapMerge [m:Map] : Map -> Map := + Cases m of + M0 => [m':Map] m' + | (M1 a y) => [m':Map] (MapPut_behind m' a y) + | (M2 m1 m2) => [m':Map] Cases m' of + M0 => m + | (M1 a' y') => (MapPut m a' y') + | (M2 m'1 m'2) => (M2 (MapMerge m1 m'1) + (MapMerge m2 m'2)) + end + end. + + Lemma MapMerge_semantics : (m,m':Map) + (eqm (MapGet (MapMerge m m')) + [a0:ad] Cases (MapGet m' a0) of + (SOME y') => (SOME y') + | NONE => (MapGet m a0) + end). + Proof. + Unfold eqm. Induction m. Intros. Simpl. Case (MapGet m' a); Trivial. + Intros. Simpl. Rewrite (MapPut_behind_semantics m' a a0 a1). Reflexivity. + Induction m'. Trivial. + Intros. Unfold MapMerge. Rewrite (MapPut_semantics (M2 m0 m1) a a0 a1). + Elim (sumbool_of_bool (ad_eq a a1)). Intro H1. Rewrite H1. Rewrite (ad_eq_complete ? ? H1). + Rewrite (M1_semantics_1 a1 a0). Reflexivity. + Intro H1. Rewrite H1. Rewrite (M1_semantics_2 a a1 a0 H1). Reflexivity. + Intros. Cut (MapMerge (M2 m0 m1) (M2 m2 m3))=(M2 (MapMerge m0 m2) (MapMerge m1 m3)). + Intro. Rewrite H3. Rewrite MapGet_M2_bit_0_if. Rewrite (H0 m3 (ad_div_2 a)). + Rewrite (H m2 (ad_div_2 a)). Rewrite (MapGet_M2_bit_0_if m2 m3 a). + Rewrite (MapGet_M2_bit_0_if m0 m1 a). Case (ad_bit_0 a); Trivial. + Reflexivity. + Qed. + + (** [MapInter], [MapRngRestrTo], [MapRngRestrBy], [MapInverse] + not implemented: need a decidable equality on [A]. *) + + Fixpoint MapDelta [m:Map] : Map -> Map := + Cases m of + M0 => [m':Map] m' + | (M1 a y) => [m':Map] Cases (MapGet m' a) of + NONE => (MapPut m' a y) + | _ => (MapRemove m' a) + end + | (M2 m1 m2) => [m':Map] Cases m' of + M0 => m + | (M1 a' y') => Cases (MapGet m a') of + NONE => (MapPut m a' y') + | _ => (MapRemove m a') + end + | (M2 m'1 m'2) => (makeM2 (MapDelta m1 m'1) + (MapDelta m2 m'2)) + end + end. + + Lemma MapDelta_semantics_comm : (m,m':Map) + (eqm (MapGet (MapDelta m m')) (MapGet (MapDelta m' m))). + Proof. + Unfold eqm. Induction m. Induction m'; Reflexivity. + Induction m'. Reflexivity. + Unfold MapDelta. Intros. Elim (sumbool_of_bool (ad_eq a a1)). Intro H. + Rewrite <- (ad_eq_complete ? ? H). Rewrite (M1_semantics_1 a a2). + Rewrite (M1_semantics_1 a a0). Simpl. Rewrite (ad_eq_correct a). Reflexivity. + Intro H. Rewrite (M1_semantics_2 a a1 a0 H). Rewrite (ad_eq_comm a a1) in H. + Rewrite (M1_semantics_2 a1 a a2 H). Rewrite (MapPut_semantics (M1 a a0) a1 a2 a3). + Rewrite (MapPut_semantics (M1 a1 a2) a a0 a3). Elim (sumbool_of_bool (ad_eq a a3)). + Intro H0. Rewrite H0. Rewrite (ad_eq_complete ? ? H0) in H. Rewrite H. + Rewrite (ad_eq_complete ? ? H0). Rewrite (M1_semantics_1 a3 a0). Reflexivity. + Intro H0. Rewrite H0. Rewrite (M1_semantics_2 a a3 a0 H0). + Elim (sumbool_of_bool (ad_eq a1 a3)). Intro H1. Rewrite H1. + Rewrite (ad_eq_complete ? ? H1). Exact (M1_semantics_1 a3 a2). + Intro H1. Rewrite H1. Exact (M1_semantics_2 a1 a3 a2 H1). + Intros. Reflexivity. + Induction m'. Reflexivity. + Reflexivity. + Intros. Simpl. Rewrite (makeM2_M2 (MapDelta m0 m2) (MapDelta m1 m3) a). + Rewrite (makeM2_M2 (MapDelta m2 m0) (MapDelta m3 m1) a). + Rewrite (MapGet_M2_bit_0_if (MapDelta m0 m2) (MapDelta m1 m3) a). + Rewrite (MapGet_M2_bit_0_if (MapDelta m2 m0) (MapDelta m3 m1) a). + Rewrite (H0 m3 (ad_div_2 a)). Rewrite (H m2 (ad_div_2 a)). Reflexivity. + Qed. + + Lemma MapDelta_semantics_1_1 : (a:ad) (y:A) (m':Map) (a0:ad) + (MapGet (M1 a y) a0)=NONE -> (MapGet m' a0)=NONE -> + (MapGet (MapDelta (M1 a y) m') a0)=NONE. + Proof. + Intros. Unfold MapDelta. Elim (sumbool_of_bool (ad_eq a a0)). Intro H1. + Rewrite (ad_eq_complete ? ? H1) in H. Rewrite (M1_semantics_1 a0 y) in H. Discriminate H. + Intro H1. Case (MapGet m' a). Rewrite (MapPut_semantics m' a y a0). Rewrite H1. Assumption. + Rewrite (MapRemove_semantics m' a a0). Rewrite H1. Trivial. + Qed. + + Lemma MapDelta_semantics_1 : (m,m':Map) (a:ad) + (MapGet m a)=NONE -> (MapGet m' a)=NONE -> + (MapGet (MapDelta m m') a)=NONE. + Proof. + Induction m. Trivial. + Exact MapDelta_semantics_1_1. + Induction m'. Trivial. + Intros. Rewrite (MapDelta_semantics_comm (M2 m0 m1) (M1 a a0) a1). + Apply MapDelta_semantics_1_1; Trivial. + Intros. Simpl. Rewrite (makeM2_M2 (MapDelta m0 m2) (MapDelta m1 m3) a). + Rewrite MapGet_M2_bit_0_if. Elim (sumbool_of_bool (ad_bit_0 a)). Intro H5. Rewrite H5. + Apply H0. Rewrite (MapGet_M2_bit_0_1 a H5 m0 m1) in H3. Exact H3. + Rewrite (MapGet_M2_bit_0_1 a H5 m2 m3) in H4. Exact H4. + Intro H5. Rewrite H5. Apply H. Rewrite (MapGet_M2_bit_0_0 a H5 m0 m1) in H3. Exact H3. + Rewrite (MapGet_M2_bit_0_0 a H5 m2 m3) in H4. Exact H4. + Qed. + + Lemma MapDelta_semantics_2_1 : (a:ad) (y:A) (m':Map) (a0:ad) (y0:A) + (MapGet (M1 a y) a0)=NONE -> (MapGet m' a0)=(SOME y0) -> + (MapGet (MapDelta (M1 a y) m') a0)=(SOME y0). + Proof. + Intros. Unfold MapDelta. Elim (sumbool_of_bool (ad_eq a a0)). Intro H1. + Rewrite (ad_eq_complete ? ? H1) in H. Rewrite (M1_semantics_1 a0 y) in H. Discriminate H. + Intro H1. Case (MapGet m' a). Rewrite (MapPut_semantics m' a y a0). Rewrite H1. Assumption. + Rewrite (MapRemove_semantics m' a a0). Rewrite H1. Trivial. + Qed. + + Lemma MapDelta_semantics_2_2 : (a:ad) (y:A) (m':Map) (a0:ad) (y0:A) + (MapGet (M1 a y) a0)=(SOME y0) -> (MapGet m' a0)=NONE -> + (MapGet (MapDelta (M1 a y) m') a0)=(SOME y0). + Proof. + Intros. Unfold MapDelta. Elim (sumbool_of_bool (ad_eq a a0)). Intro H1. + Rewrite (ad_eq_complete ? ? H1) in H. Rewrite (ad_eq_complete ? ? H1). + Rewrite H0. Rewrite (MapPut_semantics m' a0 y a0). Rewrite (ad_eq_correct a0). + Rewrite (M1_semantics_1 a0 y) in H. Simple Inversion H. Assumption. + Intro H1. Rewrite (M1_semantics_2 a a0 y H1) in H. Discriminate H. + Qed. + + Lemma MapDelta_semantics_2 : (m,m':Map) (a:ad) (y:A) + (MapGet m a)=NONE -> (MapGet m' a)=(SOME y) -> + (MapGet (MapDelta m m') a)=(SOME y). + Proof. + Induction m. Trivial. + Exact MapDelta_semantics_2_1. + Induction m'. Intros. Discriminate H2. + Intros. Rewrite (MapDelta_semantics_comm (M2 m0 m1) (M1 a a0) a1). + Apply MapDelta_semantics_2_2; Assumption. + Intros. Simpl. Rewrite (makeM2_M2 (MapDelta m0 m2) (MapDelta m1 m3) a). + Rewrite MapGet_M2_bit_0_if. Elim (sumbool_of_bool (ad_bit_0 a)). Intro H5. Rewrite H5. + Apply H0. Rewrite <- (MapGet_M2_bit_0_1 a H5 m0 m1). Assumption. + Rewrite <- (MapGet_M2_bit_0_1 a H5 m2 m3). Assumption. + Intro H5. Rewrite H5. Apply H. Rewrite <- (MapGet_M2_bit_0_0 a H5 m0 m1). Assumption. + Rewrite <- (MapGet_M2_bit_0_0 a H5 m2 m3). Assumption. + Qed. + + Lemma MapDelta_semantics_3_1 : (a0:ad) (y0:A) (m':Map) (a:ad) (y,y':A) + (MapGet (M1 a0 y0) a)=(SOME y) -> (MapGet m' a)=(SOME y') -> + (MapGet (MapDelta (M1 a0 y0) m') a)=NONE. + Proof. + Intros. Unfold MapDelta. Elim (sumbool_of_bool (ad_eq a0 a)). Intro H1. + Rewrite (ad_eq_complete a0 a H1). Rewrite H0. Rewrite (MapRemove_semantics m' a a). + Rewrite (ad_eq_correct a). Reflexivity. + Intro H1. Rewrite (M1_semantics_2 a0 a y0 H1) in H. Discriminate H. + Qed. + + Lemma MapDelta_semantics_3 : (m,m':Map) (a:ad) (y,y':A) + (MapGet m a)=(SOME y) -> (MapGet m' a)=(SOME y') -> + (MapGet (MapDelta m m') a)=NONE. + Proof. + Induction m. Intros. Discriminate H. + Exact MapDelta_semantics_3_1. + Induction m'. Intros. Discriminate H2. + Intros. Rewrite (MapDelta_semantics_comm (M2 m0 m1) (M1 a a0) a1). + Exact (MapDelta_semantics_3_1 a a0 (M2 m0 m1) a1 y' y H2 H1). + Intros. Simpl. Rewrite (makeM2_M2 (MapDelta m0 m2) (MapDelta m1 m3) a). + Rewrite MapGet_M2_bit_0_if. Elim (sumbool_of_bool (ad_bit_0 a)). Intro H5. Rewrite H5. + Apply (H0 m3 (ad_div_2 a) y y'). Rewrite <- (MapGet_M2_bit_0_1 a H5 m0 m1). Assumption. + Rewrite <- (MapGet_M2_bit_0_1 a H5 m2 m3). Assumption. + Intro H5. Rewrite H5. Apply (H m2 (ad_div_2 a) y y'). + Rewrite <- (MapGet_M2_bit_0_0 a H5 m0 m1). Assumption. + Rewrite <- (MapGet_M2_bit_0_0 a H5 m2 m3). Assumption. + Qed. + + Lemma MapDelta_semantics : (m,m':Map) + (eqm (MapGet (MapDelta m m')) + [a0:ad] Cases (MapGet m a0) (MapGet m' a0) of + NONE (SOME y') => (SOME y') + | (SOME y) NONE => (SOME y) + | _ _ => NONE + end). + Proof. + Unfold eqm. Intros. Elim (option_sum (MapGet m' a)). Intro H. Elim H. Intros a0 H0. + Rewrite H0. Elim (option_sum (MapGet m a)). Intro H1. Elim H1. Intros a1 H2. Rewrite H2. + Exact (MapDelta_semantics_3 m m' a a1 a0 H2 H0). + Intro H1. Rewrite H1. Exact (MapDelta_semantics_2 m m' a a0 H1 H0). + Intro H. Rewrite H. Elim (option_sum (MapGet m a)). Intro H0. Elim H0. Intros a0 H1. + Rewrite H1. Rewrite (MapDelta_semantics_comm m m' a). + Exact (MapDelta_semantics_2 m' m a a0 H H1). + Intro H0. Rewrite H0. Exact (MapDelta_semantics_1 m m' a H0 H). + Qed. + + Definition MapEmptyp := [m:Map] + Cases m of + M0 => true + | _ => false + end. + + Lemma MapEmptyp_correct : (MapEmptyp M0)=true. + Proof. + Reflexivity. + Qed. + + Lemma MapEmptyp_complete : (m:Map) (MapEmptyp m)=true -> m=M0. + Proof. + Induction m; Trivial. Intros. Discriminate H. + Intros. Discriminate H1. + Qed. + + (** [MapSplit] not implemented: not the preferred way of recursing over Maps + (use [MapSweep], [MapCollect], or [MapFold] in Mapiter.v. *) + +End MapDefs. |