diff options
Diffstat (limited to 'theories/IntMap/Map.v')
| -rw-r--r-- | theories/IntMap/Map.v | 1415 |
1 files changed, 747 insertions, 668 deletions
diff --git a/theories/IntMap/Map.v b/theories/IntMap/Map.v index b89f610421..68091d6f0b 100644 --- a/theories/IntMap/Map.v +++ b/theories/IntMap/Map.v @@ -9,12 +9,12 @@ (** Definition of finite sets as trees indexed by adresses *) -Require Bool. -Require Sumbool. -Require ZArith. -Require Addr. -Require Adist. -Require Addec. +Require Import Bool. +Require Import Sumbool. +Require Import ZArith. +Require Import Addr. +Require Import Adist. +Require Import Addec. Section MapDefs. @@ -23,174 +23,197 @@ Section MapDefs. Variable A : Set. Inductive Map : Set := - M0 : Map + | M0 : Map | M1 : ad -> A -> Map | M2 : Map -> Map -> Map. Inductive option : Set := - NONE : option + | NONE : option | SOME : A -> option. - Lemma option_sum : (o:option) {y:A | o=(SOME y)}+{o=NONE}. + Lemma option_sum : forall o:option, {y : A | o = SOME y} + {o = NONE}. Proof. - Induction o. Right . Reflexivity. - Left . Split with a. Reflexivity. + simple 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 + Fixpoint MapGet (m:Map) : ad -> option := + match m with + | M0 => fun a:ad => NONE + | M1 x y => fun a:ad => if ad_eq x a then SOME y else NONE + | M2 m1 m2 => + fun a:ad => + match a with + | 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). + Definition eqm (g g':ad -> option) := forall a:ad, g a = g' a. - Lemma newMap_semantics : (eqm (MapGet newMap) [a:ad] NONE). + Lemma newMap_semantics : eqm (MapGet newMap) (fun a:ad => NONE). Proof. - Simpl. Unfold eqm. Trivial. + simpl in |- *. unfold eqm in |- *. 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). + Lemma MapSingleton_semantics : + forall (a:ad) (y:A), + eqm (MapGet (MapSingleton a y)) + (fun a':ad => if ad_eq a a' then SOME y else NONE). Proof. - Simpl. Unfold eqm. Trivial. + simpl in |- *. unfold eqm in |- *. trivial. Qed. - Lemma M1_semantics_1 : (a:ad) (y:A) (MapGet (M1 a y) a)=(SOME y). + Lemma M1_semantics_1 : forall (a:ad) (y:A), MapGet (M1 a y) a = SOME y. Proof. - Unfold MapGet. Intros. Rewrite (ad_eq_correct a). Reflexivity. + unfold MapGet in |- *. 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. + forall (a a':ad) (y:A), ad_eq a a' = false -> MapGet (M1 a y) a' = NONE. Proof. - Intros. Simpl. Rewrite H. Reflexivity. + intros. simpl in |- *. rewrite H. reflexivity. Qed. Lemma Map2_semantics_1 : - (m,m':Map) (eqm (MapGet m) [a:ad] (MapGet (M2 m m') (ad_double a))). + forall m m':Map, + eqm (MapGet m) (fun a:ad => MapGet (M2 m m') (ad_double a)). Proof. - Unfold eqm. Induction a; Trivial. + unfold eqm in |- *. simple 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))). + Lemma Map2_semantics_1_eq : + forall (m m':Map) (f:ad -> option), + eqm (MapGet (M2 m m')) f -> eqm (MapGet m) (fun a:ad => f (ad_double a)). Proof. - Unfold eqm. - Intros. - Rewrite <- (H (ad_double a)). - Exact (Map2_semantics_1 m m' a). + unfold eqm in |- *. + 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 + forall m m':Map, + eqm (MapGet m') (fun a:ad => MapGet (M2 m m') (ad_double_plus_un a)). + Proof. + unfold eqm in |- *. simple induction a; trivial. + Qed. + + Lemma Map2_semantics_2_eq : + forall (m m':Map) (f:ad -> option), + eqm (MapGet (M2 m m')) f -> + eqm (MapGet m') (fun a:ad => f (ad_double_plus_un a)). + Proof. + unfold eqm in |- *. + intros. + rewrite <- (H (ad_double_plus_un a)). + exact (Map2_semantics_2 m m' a). + Qed. + + Lemma MapGet_M2_bit_0_0 : + forall a:ad, + ad_bit_0 a = false -> + forall m m':Map, MapGet (M2 m m') a = MapGet m (ad_div_2 a). + Proof. + simple induction a; trivial. simple induction p. intros. discriminate H0. + trivial. + intros. discriminate H. + Qed. + + Lemma MapGet_M2_bit_0_1 : + forall a:ad, + ad_bit_0 a = true -> + forall m m':Map, MapGet (M2 m m') a = MapGet m' (ad_div_2 a). + Proof. + simple induction a. intros. discriminate H. + simple induction p. trivial. + intros. discriminate H0. + trivial. + Qed. + + Lemma MapGet_M2_bit_0_if : + forall (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 : + forall (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 : + forall m m':Map, + eqm (MapGet (M2 m m')) + (fun a:ad => + match ad_bit_0 a with + | false => MapGet m (ad_div_2 a) + | true => MapGet m' (ad_div_2 a) + end). + Proof. + unfold eqm in |- *. + simple induction a; trivial. + simple induction p; trivial. + Qed. + + Lemma Map2_semantics_3_eq : + forall (m m':Map) (f f':ad -> option), + eqm (MapGet m) f -> + eqm (MapGet m') f' -> + eqm (MapGet (M2 m m')) + (fun a:ad => + match ad_bit_0 a with + | false => f (ad_div_2 a) + | true => f' (ad_div_2 a) + end). + Proof. + unfold eqm in |- *. + 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) {struct p} : + Map := + match p with + | xO p' => + let m := MapPut1 (ad_div_2 a) y (ad_div_2 a') y' p' in + match ad_bit_0 a with + | false => M2 m M0 + | true => M2 M0 m + end + | _ => + match ad_bit_0 a with + | 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)). + Lemma MapGet_if_commute : + forall (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. + intros. case b; trivial. Qed. (*i @@ -206,581 +229,637 @@ Section MapDefs. Qed. i*) - Lemma MapGet_if_same : (m:Map) (b:bool) (a:ad) - (MapGet (if b then m else m) a)=(MapGet m a). + Lemma MapGet_if_same : + forall (m:Map) (b:bool) (a:ad), MapGet (if b then m else m) a = MapGet m a. Proof. - Induction b;Trivial. + simple 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)). + Lemma MapGet_M2_bit_0_2 : + forall (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. + 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). + Lemma MapPut1_semantics_1 : + forall (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. + simple induction p. intros. unfold MapPut1 in |- *. rewrite MapGet_M2_bit_0_2. apply M1_semantics_1. + intros. simpl in |- *. rewrite MapGet_M2_bit_0_2. apply H. rewrite <- ad_xor_div_2. rewrite H0. + reflexivity. + intros. unfold MapPut1 in |- *. 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'). + Lemma MapPut1_semantics_2 : + forall (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. + simple induction p. intros. unfold MapPut1 in |- *. 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 in |- *. 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 in |- *. 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. + Lemma MapGet_M2_both_NONE : + forall (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. + 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) + Lemma MapPut1_semantics_3 : + forall (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. + simple induction p. intros. unfold MapPut1 in |- *. 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 in |- *. 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 in |- *. 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 : + forall (p:positive) (a a':ad) (y y':A), + ad_xor a a' = ad_x p -> + eqm (MapGet (MapPut1 a y a' y' p)) + (fun a0:ad => + if ad_eq a a0 + then SOME y + else if ad_eq a' a0 then SOME y' else NONE). + Proof. + unfold eqm in |- *. 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' : + forall (p:positive) (a a':ad) (y y':A), + ad_xor a a' = ad_x p -> + eqm (MapGet (MapPut1 a y a' y' p)) + (fun a0:ad => + if ad_eq a' a0 + then SOME y' + else if ad_eq a a0 then SOME y else NONE). + Proof. + unfold eqm in |- *. 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 := + match m with + | M0 => M1 + | M1 a y => + fun (a':ad) (y':A) => + match ad_xor a a' with + | ad_z => M1 a' y' + | ad_x p => MapPut1 a y a' y' p + end + | M2 m1 m2 => + fun (a:ad) (y:A) => + match a with + | 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 - | (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) + Lemma MapPut_semantics_1 : + forall (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 : + forall (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 in |- *. intros. rewrite (ad_xor_nilpotent a). trivial. + Qed. + + Lemma MapPut_semantics_2_2 : + forall (a a':ad) (y y':A) (a0 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. + simple induction a''. intro. rewrite (ad_xor_eq _ _ H). rewrite MapPut_semantics_2_1. + case (ad_eq a' a0); trivial. + intros. simpl in |- *. 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 : + forall (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 : + forall (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. + simple induction a. trivial. + simple induction p; trivial. + Qed. + + Lemma MapPut_semantics : + forall (m:Map) (a:ad) (y:A), + eqm (MapGet (MapPut m a y)) + (fun a':ad => if ad_eq a a' then SOME y else MapGet m a'). + Proof. + unfold eqm in |- *. simple induction m. exact MapPut_semantics_1. + intros. unfold MapGet at 2 in |- *. 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 := + match m with + | M0 => M1 + | M1 a y => + fun (a':ad) (y':A) => + match ad_xor a a' with + | ad_z => m + | ad_x p => MapPut1 a y a' y' p + end + | M2 m1 m2 => + fun (a:ad) (y:A) => + match a with + | 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 - | (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) + Lemma MapPut_behind_semantics_3_1 : + forall (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. + simple induction a. trivial. + simple induction p; trivial. + Qed. + + Lemma MapPut_behind_as_before_1 : + forall a a' a0:ad, + ad_eq a' a0 = false -> + forall 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 in |- *. 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 : + forall (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. + simple 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 : + forall (m:Map) (a:ad) (y:A), + MapGet (MapPut_behind m a y) a = + match MapGet m a with + | SOME y' => SOME y' + | _ => SOME y + end. + Proof. + simple induction m. simpl in |- *. intros. rewrite (ad_eq_correct a). reflexivity. + intros. elim (ad_sum (ad_xor a a1)). intro H. elim H. intros p H0. simpl in |- *. + rewrite H0. rewrite (ad_xor_eq_false a a1 p). exact (MapPut1_semantics_2 p a a1 a0 y H0). + assumption. + intro H. simpl in |- *. 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 : + forall (m:Map) (a:ad) (y:A), + eqm (MapGet (MapPut_behind m a y)) + (fun a':ad => + match MapGet m a' with + | SOME y' => SOME y' + | _ => if ad_eq a a' then SOME y else NONE + end). + Proof. + unfold eqm in |- *. 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) := + match m, m' with + | 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 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')) + Lemma makeM2_M2 : + forall m m':Map, eqm (MapGet (makeM2 m m')) (MapGet (M2 m m')). + Proof. + unfold eqm in |- *. 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 in |- *. rewrite (ad_bit_0_1_not_double a H a0). reflexivity. + intros m1 m2. unfold makeM2 in |- *. rewrite MapGet_M2_bit_0_1. reflexivity. + assumption. + case m. intros a0 y. simpl in |- *. 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 in |- *. rewrite MapGet_M2_bit_0_1. reflexivity. + assumption. + intros m1 m2 a0 y. unfold makeM2 in |- *. rewrite MapGet_M2_bit_0_1. reflexivity. + assumption. + intros m1 m2. unfold makeM2 in |- *. + 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 in |- *. rewrite (ad_bit_0_0_not_double_plus_un a H a0). reflexivity. + intros m1 m2. unfold makeM2 in |- *. rewrite MapGet_M2_bit_0_0. reflexivity. + assumption. + case m'. intros a0 y. simpl in |- *. 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 in |- *. rewrite MapGet_M2_bit_0_0. reflexivity. + assumption. + intros m1 m2 a0 y. unfold makeM2 in |- *. rewrite MapGet_M2_bit_0_0. reflexivity. + assumption. + intros m1 m2. unfold makeM2 in |- *. exact (MapGet_M2_bit_0_0 a H (M2 m1 m2) m'). + Qed. + + Fixpoint MapRemove (m:Map) : ad -> Map := + match m with + | M0 => fun _:ad => M0 + | M1 a y => + fun a':ad => match ad_eq a a' with + | true => M0 + | false => m + end + | M2 m1 m2 => + fun 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. - 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 + Lemma MapRemove_semantics : + forall (m:Map) (a:ad), + eqm (MapGet (MapRemove m a)) + (fun a':ad => if ad_eq a a' then NONE else MapGet m a'). + Proof. + unfold eqm in |- *. simple induction m. simpl in |- *. intros. case (ad_eq a a0); trivial. + intros. simpl in |- *. 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)) + in |- *. + 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 := + match m with + | M0 => 0 + | M1 _ _ => 1 + | M2 m m' => MapCard m + MapCard m' + end. + + Fixpoint MapMerge (m:Map) : Map -> Map := + match m with + | M0 => fun m':Map => m' + | M1 a y => fun m':Map => MapPut_behind m' a y + | M2 m1 m2 => + fun m':Map => + match m' with + | 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. + Lemma MapMerge_semantics : + forall m m':Map, + eqm (MapGet (MapMerge m m')) + (fun a0:ad => + match MapGet m' a0 with + | SOME y' => SOME y' + | NONE => MapGet m a0 + end). + Proof. + unfold eqm in |- *. simple induction m. intros. simpl in |- *. case (MapGet m' a); trivial. + intros. simpl in |- *. rewrite (MapPut_behind_semantics m' a a0 a1). reflexivity. + simple induction m'. trivial. + intros. unfold MapMerge in |- *. 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 + Fixpoint MapDelta (m:Map) : Map -> Map := + match m with + | M0 => fun m':Map => m' + | M1 a y => + fun m':Map => + match MapGet m' a with + | NONE => MapPut m' a y + | _ => MapRemove m' a + end + | M2 m1 m2 => + fun m':Map => + match m' with + | M0 => m + | M1 a' y' => + match MapGet m a' with + | 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 MapEmptyp_correct : (MapEmptyp M0)=true. - Proof. - Reflexivity. - Qed. - - Lemma MapEmptyp_complete : (m:Map) (MapEmptyp m)=true -> m=M0. + Lemma MapDelta_semantics_comm : + forall m m':Map, eqm (MapGet (MapDelta m m')) (MapGet (MapDelta m' m)). + Proof. + unfold eqm in |- *. simple induction m. simple induction m'; reflexivity. + simple induction m'. reflexivity. + unfold MapDelta in |- *. 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 in |- *. 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. + simple induction m'. reflexivity. + reflexivity. + intros. simpl in |- *. 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 : + forall (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 in |- *. 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 : + forall (m m':Map) (a:ad), + MapGet m a = NONE -> + MapGet m' a = NONE -> MapGet (MapDelta m m') a = NONE. + Proof. + simple induction m. trivial. + exact MapDelta_semantics_1_1. + simple induction m'. trivial. + intros. rewrite (MapDelta_semantics_comm (M2 m0 m1) (M1 a a0) a1). + apply MapDelta_semantics_1_1; trivial. + intros. simpl in |- *. 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 : + forall (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 in |- *. 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 : + forall (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 in |- *. 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 : + forall (m m':Map) (a:ad) (y:A), + MapGet m a = NONE -> + MapGet m' a = SOME y -> MapGet (MapDelta m m') a = SOME y. + Proof. + simple induction m. trivial. + exact MapDelta_semantics_2_1. + simple 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 in |- *. 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 : + forall (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 in |- *. 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 : + forall (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. + simple induction m. intros. discriminate H. + exact MapDelta_semantics_3_1. + simple 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 in |- *. 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 : + forall m m':Map, + eqm (MapGet (MapDelta m m')) + (fun a0:ad => + match MapGet m a0, MapGet m' a0 with + | NONE, SOME y' => SOME y' + | SOME y, NONE => SOME y + | _, _ => NONE + end). + Proof. + unfold eqm in |- *. 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) := match m with + | M0 => true + | _ => false + end. + + Lemma MapEmptyp_correct : MapEmptyp M0 = true. Proof. - Induction m; Trivial. Intros. Discriminate H. - Intros. Discriminate H1. + reflexivity. + Qed. + + Lemma MapEmptyp_complete : forall m:Map, MapEmptyp m = true -> m = M0. + Proof. + simple 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. +End MapDefs.
\ No newline at end of file |