diff options
Diffstat (limited to 'theories/IntMap/Map.v')
| -rw-r--r-- | theories/IntMap/Map.v | 556 |
1 files changed, 280 insertions, 276 deletions
diff --git a/theories/IntMap/Map.v b/theories/IntMap/Map.v index 5345f81b..2be6de04 100644 --- a/theories/IntMap/Map.v +++ b/theories/IntMap/Map.v @@ -5,21 +5,26 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Map.v 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: Map.v 8733 2006-04-25 22:52:18Z letouzey $ i*) (** Definition of finite sets as trees indexed by adresses *) Require Import Bool. Require Import Sumbool. -Require Import ZArith. -Require Import Addr. -Require Import Adist. -Require Import Addec. +Require Import NArith. +Require Import Ndigits. +Require Import Ndec. +(* The type [ad] of addresses is now [N] in [BinNat]. *) + +Definition ad := N. + +(* a Notation or complete replacement would be nice, + but that would changes hyps names *) Section MapDefs. -(** We define maps from ad to A. *) +(** We now define maps from ad to A. *) Variable A : Set. Inductive Map : Set := @@ -27,31 +32,28 @@ Section MapDefs. | M1 : ad -> A -> Map | M2 : Map -> Map -> Map. - Inductive option : Set := - | NONE : option - | SOME : A -> option. - - Lemma option_sum : forall o:option, {y : A | o = SOME y} + {o = NONE}. + Lemma option_sum : forall o:option A, {y : A | o = Some y} + {o = None}. Proof. - simple induction o. right. reflexivity. + simple induction o. left. split with a. reflexivity. + right. 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 := + Fixpoint MapGet (m:Map) : ad -> option A := match m with - | M0 => fun a:ad => NONE - | M1 x y => fun a:ad => if ad_eq x a then SOME y else NONE + | M0 => fun a:ad => None + | M1 x y => fun a:ad => if Neqb 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) + | N0 => MapGet m1 N0 + | Npos xH => MapGet m2 N0 + | Npos (xO p) => MapGet m1 (Npos p) + | Npos (xI p) => MapGet m2 (Npos p) end end. @@ -59,9 +61,9 @@ Section MapDefs. Definition MapSingleton := M1. - Definition eqm (g g':ad -> option) := forall a:ad, g a = g' a. + Definition eqm (g g':ad -> option A) := forall a:ad, g a = g' a. - Lemma newMap_semantics : eqm (MapGet newMap) (fun a:ad => NONE). + Lemma newMap_semantics : eqm (MapGet newMap) (fun a:ad => None). Proof. simpl in |- *. unfold eqm in |- *. trivial. Qed. @@ -69,61 +71,61 @@ Section MapDefs. 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). + (fun a':ad => if Neqb a a' then Some y else None). Proof. simpl in |- *. unfold eqm in |- *. trivial. Qed. - Lemma M1_semantics_1 : forall (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 in |- *. intros. rewrite (ad_eq_correct a). reflexivity. + unfold MapGet in |- *. intros. rewrite (Neqb_correct a). reflexivity. Qed. Lemma M1_semantics_2 : - forall (a a':ad) (y:A), ad_eq a a' = false -> MapGet (M1 a y) a' = NONE. + forall (a a':ad) (y:A), Neqb a a' = false -> MapGet (M1 a y) a' = None. Proof. intros. simpl in |- *. rewrite H. reflexivity. Qed. Lemma Map2_semantics_1 : forall m m':Map, - eqm (MapGet m) (fun a:ad => MapGet (M2 m m') (ad_double a)). + eqm (MapGet m) (fun a:ad => MapGet (M2 m m') (Ndouble a)). Proof. unfold eqm in |- *. simple induction a; trivial. Qed. 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)). + forall (m m':Map) (f:ad -> option A), + eqm (MapGet (M2 m m')) f -> eqm (MapGet m) (fun a:ad => f (Ndouble a)). Proof. unfold eqm in |- *. intros. - rewrite <- (H (ad_double a)). + rewrite <- (H (Ndouble a)). exact (Map2_semantics_1 m m' a). Qed. Lemma Map2_semantics_2 : forall m m':Map, - eqm (MapGet m') (fun a:ad => MapGet (M2 m m') (ad_double_plus_un a)). + eqm (MapGet m') (fun a:ad => MapGet (M2 m m') (Ndouble_plus_one a)). Proof. unfold eqm in |- *. simple induction a; trivial. Qed. Lemma Map2_semantics_2_eq : - forall (m m':Map) (f:ad -> option), + forall (m m':Map) (f:ad -> option A), eqm (MapGet (M2 m m')) f -> - eqm (MapGet m') (fun a:ad => f (ad_double_plus_un a)). + eqm (MapGet m') (fun a:ad => f (Ndouble_plus_one a)). Proof. unfold eqm in |- *. intros. - rewrite <- (H (ad_double_plus_un a)). + rewrite <- (H (Ndouble_plus_one 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). + Nbit0 a = false -> + forall m m':Map, MapGet (M2 m m') a = MapGet m (Ndiv2 a). Proof. simple induction a; trivial. simple induction p. intros. discriminate H0. trivial. @@ -132,8 +134,8 @@ Section MapDefs. 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). + Nbit0 a = true -> + forall m m':Map, MapGet (M2 m m') a = MapGet m' (Ndiv2 a). Proof. simple induction a. intros. discriminate H. simple induction p. trivial. @@ -144,19 +146,19 @@ Section MapDefs. 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)). + (if Nbit0 a then MapGet m' (Ndiv2 a) else MapGet m (Ndiv2 a)). Proof. - intros. elim (sumbool_of_bool (ad_bit_0 a)). intro H. rewrite H. + intros. elim (sumbool_of_bool (Nbit0 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). + (if Nbit0 a then MapGet (M2 m' m) a else MapGet (M2 m m'') a) = + MapGet m (Ndiv2 a). Proof. - intros. elim (sumbool_of_bool (ad_bit_0 a)). intro H. rewrite H. + intros. elim (sumbool_of_bool (Nbit0 a)). intro H. rewrite H. apply MapGet_M2_bit_0_1; assumption. intro H. rewrite H. apply MapGet_M2_bit_0_0; assumption. Qed. @@ -165,9 +167,9 @@ Section MapDefs. 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) + match Nbit0 a with + | false => MapGet m (Ndiv2 a) + | true => MapGet m' (Ndiv2 a) end). Proof. unfold eqm in |- *. @@ -176,20 +178,20 @@ Section MapDefs. Qed. Lemma Map2_semantics_3_eq : - forall (m m':Map) (f f':ad -> option), + forall (m m':Map) (f f':ad -> option A), 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) + match Nbit0 a with + | false => f (Ndiv2 a) + | true => f' (Ndiv2 a) end). Proof. unfold eqm in |- *. intros. - rewrite <- (H (ad_div_2 a)). - rewrite <- (H0 (ad_div_2 a)). + rewrite <- (H (Ndiv2 a)). + rewrite <- (H0 (Ndiv2 a)). exact (Map2_semantics_3 m m' a). Qed. @@ -197,15 +199,15 @@ Section MapDefs. 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 + let m := MapPut1 (Ndiv2 a) y (Ndiv2 a') y' p' in + match Nbit0 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) + match Nbit0 a with + | false => M2 (M1 (Ndiv2 a) y) (M1 (Ndiv2 a') y') + | true => M2 (M1 (Ndiv2 a') y') (M1 (Ndiv2 a) y) end end. @@ -218,14 +220,14 @@ Section MapDefs. (*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)). + (a:ad) (MapGet (if (Nbit0 a) then (M2 m m') else (M2 m'' m''')) a)= + (MapGet (if (Nbit0 a) then m' else m'') (Ndiv2 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. + Intros. Rewrite (MapGet_if_commute (Nbit0 a)). Rewrite (MapGet_if_commute (Nbit0 a)). + Cut (Nbit0 a)=false\/(Nbit0 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. + Case (Nbit0 a); Auto. Qed. i*) @@ -237,107 +239,107 @@ Section MapDefs. 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). + MapGet (if Nbit0 a then M2 m m' else M2 m' m'') a = + MapGet m' (Ndiv2 a). Proof. intros. rewrite MapGet_if_commute. apply MapGet_M2_bit_0. Qed. 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. + Nxor a a' = Npos p -> MapGet (MapPut1 a y a' y' p) a = Some y. Proof. 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. + intros. simpl in |- *. rewrite MapGet_M2_bit_0_2. apply H. rewrite <- Nxor_div2. rewrite H0. reflexivity. intros. unfold MapPut1 in |- *. rewrite MapGet_M2_bit_0_2. apply M1_semantics_1. Qed. 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'. + Nxor a a' = Npos p -> MapGet (MapPut1 a y a' y' p) a' = Some y'. Proof. - simple induction p. intros. unfold MapPut1 in |- *. rewrite (ad_neg_bit_0_2 a a' p0 H0). + simple induction p. intros. unfold MapPut1 in |- *. rewrite (Nneg_bit0_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. + intros. simpl in |- *. rewrite (Nsame_bit0 a a' p0 H0). rewrite MapGet_M2_bit_0_2. + apply H. rewrite <- Nxor_div2. rewrite H0. reflexivity. + intros. unfold MapPut1 in |- *. rewrite (Nneg_bit0_1 a a' H). rewrite if_negb. rewrite MapGet_M2_bit_0_2. apply M1_semantics_1. Qed. - Lemma MapGet_M2_both_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. + MapGet m (Ndiv2 a) = None -> + MapGet m' (Ndiv2 a) = None -> MapGet (M2 m m') a = None. Proof. intros. rewrite (Map2_semantics_3 m m' a). - case (ad_bit_0 a); assumption. + case (Nbit0 a); assumption. Qed. 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. + Nxor a a' = Npos p -> + Neqb a a0 = false -> + Neqb a' a0 = false -> MapGet (MapPut1 a y a' y' p) a0 = None. + Proof. + simple induction p. intros. unfold MapPut1 in |- *. elim (Nneq_elim a a0 H1). intro. rewrite H3. rewrite if_negb. + rewrite MapGet_M2_bit_0_2. apply M1_semantics_2. apply Ndiv2_bit_neq. assumption. + rewrite (Nneg_bit0_2 a a' p0 H0) in H3. rewrite (negb_intro (Nbit0 a')). + rewrite (negb_intro (Nbit0 a0)). rewrite H3. reflexivity. + intro. elim (Nneq_elim a' a0 H2). intro. rewrite (Nneg_bit0_2 a a' p0 H0). rewrite H4. + rewrite (negb_elim (Nbit0 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; + intro; case (Nbit0 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. + intros. simpl in |- *. elim (Nneq_elim 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. + intro. elim (Nneq_elim a' a0 H2). intro. rewrite (Nsame_bit0 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; + intro. cut (Nxor (Ndiv2 a) (Ndiv2 a') = Npos p0). intro. + case (Nbit0 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. + rewrite <- Nxor_div2. rewrite H0. reflexivity. + intros. simpl in |- *. elim (Nneq_elim a a0 H0). intro. rewrite H2. rewrite if_negb. + rewrite MapGet_M2_bit_0_2. apply M1_semantics_2. apply Ndiv2_bit_neq. assumption. + rewrite (Nneg_bit0_1 a a' H) in H2. rewrite (negb_intro (Nbit0 a')). + rewrite (negb_intro (Nbit0 a0)). rewrite H2. reflexivity. + intro. elim (Nneq_elim a' a0 H1). intro. rewrite (Nneg_bit0_1 a a' H). rewrite H3. + rewrite (negb_elim (Nbit0 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; + intro. case (Nbit0 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 -> + Nxor a a' = Npos 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'). + if Neqb a a0 + then Some y + else if Neqb a' a0 then Some y' else None). + Proof. + unfold eqm in |- *. intros. elim (sumbool_of_bool (Neqb a a0)). intro H0. rewrite H0. + rewrite <- (Neqb_complete _ _ H0). exact (MapPut1_semantics_1 p a a' y y' H). + intro H0. rewrite H0. elim (sumbool_of_bool (Neqb a' a0)). intro H1. + rewrite <- (Neqb_complete _ _ H1). rewrite (Neqb_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 -> + Nxor a a' = Npos 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). + if Neqb a' a0 + then Some y' + else if Neqb 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. + elim (sumbool_of_bool (Neqb a a0)). intro H0. rewrite H0. + rewrite <- (Neqb_complete a a0 H0). rewrite (Neqb_comm a' a). + rewrite (Nxor_eq_false a a' p H). reflexivity. intro H0. rewrite H0. reflexivity. Qed. @@ -346,17 +348,17 @@ Section MapDefs. | 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 + match Nxor a a' with + | N0 => M1 a' y' + | Npos 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) + | N0 => M2 (MapPut m1 N0 y) m2 + | Npos xH => M2 m1 (MapPut m2 N0 y) + | Npos (xO p) => M2 (MapPut m1 (Npos p) y) m2 + | Npos (xI p) => M2 m1 (MapPut m2 (Npos p) y) end end. @@ -370,39 +372,39 @@ Section MapDefs. 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). + (if Neqb a a0 then Some y' else None). Proof. - simpl in |- *. intros. rewrite (ad_xor_nilpotent a). trivial. + simpl in |- *. intros. rewrite (Nxor_nilpotent a). trivial. Qed. Lemma MapPut_semantics_2_2 : forall (a a':ad) (y y':A) (a0 a'':ad), - ad_xor a a' = a'' -> + Nxor 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). + (if Neqb a' a0 then Some y' else if Neqb 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. + simple induction a''. intro. rewrite (Nxor_eq _ _ H). rewrite MapPut_semantics_2_1. + case (Neqb 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. + elim (sumbool_of_bool (Neqb a a0)). intro H0. rewrite H0. rewrite <- (Neqb_complete _ _ H0). + rewrite (Neqb_comm a' a). rewrite (Nxor_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). + (if Neqb a' a0 then Some y' else if Neqb a a0 then Some y else None). Proof. - intros. apply MapPut_semantics_2_2 with (a'' := ad_xor a a'); trivial. + intros. apply MapPut_semantics_2_2 with (a'' := Nxor 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'). + (if Nbit0 a + then M2 m (MapPut m' (Ndiv2 a) y) + else M2 (MapPut m (Ndiv2 a) y) m'). Proof. simple induction a. trivial. simple induction p; trivial. @@ -411,24 +413,24 @@ Section MapDefs. 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'). + (fun a':ad => if Neqb 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). + elim (sumbool_of_bool (Nbit0 a)). intro H1. rewrite H1. rewrite MapGet_M2_bit_0_if. + elim (sumbool_of_bool (Nbit0 a0)). intro H2. rewrite H2. + rewrite (H0 (Ndiv2 a) y (Ndiv2 a0)). elim (sumbool_of_bool (Neqb a a0)). + intro H3. rewrite H3. rewrite (Ndiv2_eq _ _ H3). reflexivity. + intro H3. rewrite H3. rewrite <- H2 in H1. rewrite (Ndiv2_bit_neq _ _ H3 H1). reflexivity. + intro H2. rewrite H2. rewrite (Neqb_comm a a0). rewrite (Nbit0_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. + intro H1. rewrite H1. rewrite MapGet_M2_bit_0_if. elim (sumbool_of_bool (Nbit0 a0)). + intro H2. rewrite H2. rewrite (Nbit0_neq a a0 H1 H2). reflexivity. + intro H2. rewrite H2. rewrite (H (Ndiv2 a) y (Ndiv2 a0)). + elim (sumbool_of_bool (Neqb a a0)). intro H3. rewrite H3. + rewrite (Ndiv2_eq a a0 H3). reflexivity. + intro H3. rewrite H3. rewrite <- H2 in H1. rewrite (Ndiv2_bit_neq a a0 H3 H1). reflexivity. Qed. Fixpoint MapPut_behind (m:Map) : ad -> A -> Map := @@ -436,26 +438,26 @@ Section MapDefs. | 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 + match Nxor a a' with + | N0 => m + | Npos 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) + | N0 => M2 (MapPut_behind m1 N0 y) m2 + | Npos xH => M2 m1 (MapPut_behind m2 N0 y) + | Npos (xO p) => M2 (MapPut_behind m1 (Npos p) y) m2 + | Npos (xI p) => M2 m1 (MapPut_behind m2 (Npos p) y) end end. 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'). + (if Nbit0 a + then M2 m (MapPut_behind m' (Ndiv2 a) y) + else M2 (MapPut_behind m (Ndiv2 a) y) m'). Proof. simple induction a. trivial. simple induction p; trivial. @@ -463,52 +465,52 @@ Section MapDefs. Lemma MapPut_behind_as_before_1 : forall a a' a0:ad, - ad_eq a' a0 = false -> + Neqb 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 a a' a0. simpl in |- *. intros H y y'. elim (Ndiscr (Nxor 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). + intro H0. rewrite H0. rewrite (Nxor_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 -> + Neqb 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). + elim (sumbool_of_bool (Nbit0 a)). intro H2. rewrite H2. rewrite MapGet_M2_bit_0_if. + rewrite MapGet_M2_bit_0_if. elim (sumbool_of_bool (Nbit0 a0)). intro H3. + rewrite H3. apply H0. rewrite <- H3 in H2. exact (Ndiv2_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). + elim (sumbool_of_bool (Nbit0 a0)). intro H3. rewrite H3. reflexivity. + intro H3. rewrite H3. apply H. rewrite <- H3 in H2. exact (Ndiv2_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 + | 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). + simple induction m. simpl in |- *. intros. rewrite (Neqb_correct a). reflexivity. + intros. elim (Ndiscr (Nxor a a1)). intro H. elim H. intros p H0. simpl in |- *. + rewrite H0. rewrite (Nxor_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). + intro H. simpl in |- *. rewrite H. rewrite <- (Nxor_eq _ _ H). rewrite (Neqb_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). + elim (sumbool_of_bool (Nbit0 a)). intro H1. rewrite H1. rewrite (MapGet_M2_bit_0_1 a H1). + exact (H0 (Ndiv2 a) y). + intro H1. rewrite H1. rewrite (MapGet_M2_bit_0_0 a H1). exact (H (Ndiv2 a) y). Qed. Lemma MapPut_behind_semantics : @@ -516,12 +518,12 @@ Section MapDefs. 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 + | Some y' => Some y' + | _ => if Neqb 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. + unfold eqm in |- *. intros. elim (sumbool_of_bool (Neqb a a0)). intro H. rewrite H. + rewrite (Neqb_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. @@ -529,41 +531,41 @@ Section MapDefs. 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 + | M0, M1 a y => M1 (Ndouble_plus_one a) y + | M1 a y, M0 => M1 (Ndouble a) y | _, _ => M2 m m' end. 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. + unfold eqm in |- *. intros. elim (sumbool_of_bool (Nbit0 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 a0 y. simpl in |- *. rewrite (Nodd_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. + case m. intros a0 y. simpl in |- *. elim (sumbool_of_bool (Neqb a0 (Ndiv2 a))). + intro H0. rewrite H0. rewrite (Neqb_complete _ _ H0). rewrite (Ndiv2_double_plus_one a H). + rewrite (Neqb_correct a). reflexivity. + intro H0. rewrite H0. rewrite (Neqb_comm a0 (Ndiv2 a)) in H0. + rewrite (Nnot_div2_not_double_plus_one 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)). + cut (MapGet (M2 m (M2 m1 m2)) a = MapGet (M2 m1 m2) (Ndiv2 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 a0 y. simpl in |- *. rewrite (Neven_not_double_plus_one 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). + case m'. intros a0 y. simpl in |- *. elim (sumbool_of_bool (Neqb a0 (Ndiv2 a))). intro H0. + rewrite H0. rewrite (Neqb_complete _ _ H0). rewrite (Ndiv2_double a H). + rewrite (Neqb_correct a). reflexivity. + intro H0. rewrite H0. rewrite (Neqb_comm (Ndouble a0) a). + rewrite (Neqb_comm a0 (Ndiv2 a)) in H0. rewrite (Nnot_div2_not_double a a0 H0). reflexivity. intros a0 y0 a1 y1. unfold makeM2 in |- *. rewrite MapGet_M2_bit_0_0. reflexivity. assumption. @@ -576,55 +578,55 @@ Section MapDefs. match m with | M0 => fun _:ad => M0 | M1 a y => - fun a':ad => match ad_eq a a' with + fun a':ad => match Neqb 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 + if Nbit0 a + then makeM2 m1 (MapRemove m2 (Ndiv2 a)) + else makeM2 (MapRemove m1 (Ndiv2 a)) m2 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. + (fun a':ad => if Neqb a a' then None else MapGet m a'). + Proof. + unfold eqm in |- *. simple induction m. simpl in |- *. intros. case (Neqb a a0); trivial. + intros. simpl in |- *. elim (sumbool_of_bool (Neqb a1 a2)). intro H. rewrite H. + elim (sumbool_of_bool (Neqb a a1)). intro H0. rewrite H0. reflexivity. + intro H0. rewrite H0. rewrite (Neqb_complete _ _ H) in H0. exact (M1_semantics_2 a a2 a0 H0). + intro H. elim (sumbool_of_bool (Neqb a a1)). intro H0. rewrite H0. rewrite H. + rewrite <- (Neqb_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)) + (if Nbit0 a + then makeM2 m0 (MapRemove m1 (Ndiv2 a)) + else makeM2 (MapRemove m0 (Ndiv2 a)) m1) a0 = + (if Neqb 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). + elim (sumbool_of_bool (Nbit0 a)). intro H1. rewrite H1. + rewrite (makeM2_M2 m0 (MapRemove m1 (Ndiv2 a)) a0). elim (sumbool_of_bool (Nbit0 a0)). + intro H2. rewrite MapGet_M2_bit_0_1. rewrite (H0 (Ndiv2 a) (Ndiv2 a0)). + elim (sumbool_of_bool (Neqb a a0)). intro H3. rewrite H3. rewrite (Ndiv2_eq _ _ H3). reflexivity. - intro H3. rewrite H3. rewrite <- H2 in H1. rewrite (ad_div_bit_neq _ _ H3 H1). + intro H3. rewrite H3. rewrite <- H2 in H1. rewrite (Ndiv2_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). + intro H2. rewrite (MapGet_M2_bit_0_0 a0 H2 m0 (MapRemove m1 (Ndiv2 a))). + rewrite (Neqb_comm a a0). rewrite (Nbit0_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. + intro H1. rewrite H1. rewrite (makeM2_M2 (MapRemove m0 (Ndiv2 a)) m1 a0). + elim (sumbool_of_bool (Nbit0 a0)). intro H2. rewrite MapGet_M2_bit_0_1. + rewrite (MapGet_M2_bit_0_1 a0 H2 m0 m1). rewrite (Nbit0_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. + intro H2. rewrite MapGet_M2_bit_0_0. rewrite (H (Ndiv2 a) (Ndiv2 a0)). + rewrite (MapGet_M2_bit_0_0 a0 H2 m0 m1). elim (sumbool_of_bool (Neqb a a0)). intro H3. + rewrite H3. rewrite (Ndiv2_eq _ _ H3). reflexivity. + intro H3. rewrite H3. rewrite <- H2 in H1. rewrite (Ndiv2_bit_neq _ _ H3 H1). reflexivity. assumption. Qed. @@ -653,21 +655,21 @@ Section MapDefs. eqm (MapGet (MapMerge m m')) (fun a0:ad => match MapGet m' a0 with - | SOME y' => SOME y' - | NONE => MapGet m a0 + | 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). + elim (sumbool_of_bool (Neqb a a1)). intro H1. rewrite H1. rewrite (Neqb_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. + intro. rewrite H3. rewrite MapGet_M2_bit_0_if. rewrite (H0 m3 (Ndiv2 a)). + rewrite (H m2 (Ndiv2 a)). rewrite (MapGet_M2_bit_0_if m2 m3 a). + rewrite (MapGet_M2_bit_0_if m0 m1 a). case (Nbit0 a); trivial. reflexivity. Qed. @@ -680,7 +682,7 @@ Section MapDefs. | M1 a y => fun m':Map => match MapGet m' a with - | NONE => MapPut m' a y + | None => MapPut m' a y | _ => MapRemove m' a end | M2 m1 m2 => @@ -689,7 +691,7 @@ Section MapDefs. | M0 => m | M1 a' y' => match MapGet m a' with - | NONE => MapPut m a' y' + | None => MapPut m a' y' | _ => MapRemove m a' end | M2 m'1 m'2 => makeM2 (MapDelta m1 m'1) (MapDelta m2 m'2) @@ -701,17 +703,17 @@ Section MapDefs. 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. + unfold MapDelta in |- *. intros. elim (sumbool_of_bool (Neqb a a1)). intro H. + rewrite <- (Neqb_complete _ _ H). rewrite (M1_semantics_1 a a2). + rewrite (M1_semantics_1 a a0). simpl in |- *. rewrite (Neqb_correct a). reflexivity. + intro H. rewrite (M1_semantics_2 a a1 a0 H). rewrite (Neqb_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. + rewrite (MapPut_semantics (M1 a1 a2) a a0 a3). elim (sumbool_of_bool (Neqb a a3)). + intro H0. rewrite H0. rewrite (Neqb_complete _ _ H0) in H. rewrite H. + rewrite (Neqb_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). + elim (sumbool_of_bool (Neqb a1 a3)). intro H1. rewrite H1. + rewrite (Neqb_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. @@ -720,24 +722,25 @@ Section MapDefs. 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. + rewrite (H0 m3 (Ndiv2 a)). rewrite (H m2 (Ndiv2 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. + 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. + intros. unfold MapDelta in |- *. elim (sumbool_of_bool (Neqb a a0)). intro H1. + rewrite (Neqb_complete _ _ H1) in H. rewrite (M1_semantics_1 a0 y) in H. discriminate H. + intro H1. case (MapGet m' a). rewrite (MapRemove_semantics m' a a0). rewrite H1. trivial. + rewrite (MapPut_semantics m' a y a0). rewrite H1. assumption. 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. + MapGet m a = None -> + MapGet m' a = None -> MapGet (MapDelta m m') a = None. Proof. simple induction m. trivial. exact MapDelta_semantics_1_1. @@ -745,7 +748,7 @@ Section MapDefs. 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. + rewrite MapGet_M2_bit_0_if. elim (sumbool_of_bool (Nbit0 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. @@ -754,31 +757,32 @@ Section MapDefs. 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. + 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. + intros. unfold MapDelta in |- *. elim (sumbool_of_bool (Neqb a a0)). intro H1. + rewrite (Neqb_complete _ _ H1) in H. rewrite (M1_semantics_1 a0 y) in H. discriminate H. + intro H1. case (MapGet m' a). rewrite (MapRemove_semantics m' a a0). rewrite H1. trivial. + rewrite (MapPut_semantics m' a y a0). rewrite H1. assumption. 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. + 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). + intros. unfold MapDelta in |- *. elim (sumbool_of_bool (Neqb a a0)). intro H1. + rewrite (Neqb_complete _ _ H1) in H. rewrite (Neqb_complete _ _ H1). + rewrite H0. rewrite (MapPut_semantics m' a0 y a0). rewrite (Neqb_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. + 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. @@ -786,7 +790,7 @@ Section MapDefs. 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. + rewrite MapGet_M2_bit_0_if. elim (sumbool_of_bool (Nbit0 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. @@ -795,19 +799,19 @@ Section MapDefs. 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. + 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. + intros. unfold MapDelta in |- *. elim (sumbool_of_bool (Neqb a0 a)). intro H1. + rewrite (Neqb_complete a0 a H1). rewrite H0. rewrite (MapRemove_semantics m' a a). + rewrite (Neqb_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. + 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. @@ -815,10 +819,10 @@ Section MapDefs. 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_if. elim (sumbool_of_bool (Nbit0 a)). intro H5. rewrite H5. + apply (H0 m3 (Ndiv2 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'). + intro H5. rewrite H5. apply (H m2 (Ndiv2 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. @@ -828,9 +832,9 @@ Section MapDefs. 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 + | 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. |