diff options
Diffstat (limited to 'theories/IntMap/Map.v')
| -rw-r--r-- | theories/IntMap/Map.v | 869 |
1 files changed, 0 insertions, 869 deletions
diff --git a/theories/IntMap/Map.v b/theories/IntMap/Map.v deleted file mode 100644 index 2be6de04..00000000 --- a/theories/IntMap/Map.v +++ /dev/null @@ -1,869 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(*i $Id: Map.v 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 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 now define maps from ad to A. *) - Variable A : Set. - - Inductive Map : Set := - | M0 : Map - | M1 : ad -> A -> Map - | M2 : Map -> Map -> Map. - - Lemma option_sum : forall o:option A, {y : A | o = Some y} + {o = None}. - Proof. - 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 A := - match m with - | 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 - | 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. - - Definition newMap := M0. - - Definition MapSingleton := M1. - - Definition eqm (g g':ad -> option A) := forall a:ad, g a = g' a. - - Lemma newMap_semantics : eqm (MapGet newMap) (fun a:ad => None). - Proof. - simpl in |- *. unfold eqm in |- *. trivial. - Qed. - - Lemma MapSingleton_semantics : - forall (a:ad) (y:A), - eqm (MapGet (MapSingleton a y)) - (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. - Proof. - unfold MapGet in |- *. intros. rewrite (Neqb_correct a). reflexivity. - Qed. - - Lemma M1_semantics_2 : - 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') (Ndouble a)). - Proof. - unfold eqm in |- *. simple induction a; trivial. - Qed. - - Lemma Map2_semantics_1_eq : - 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 (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') (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 A), - eqm (MapGet (M2 m m')) f -> - eqm (MapGet m') (fun a:ad => f (Ndouble_plus_one a)). - Proof. - unfold eqm in |- *. - intros. - rewrite <- (H (Ndouble_plus_one a)). - exact (Map2_semantics_2 m m' a). - Qed. - - Lemma MapGet_M2_bit_0_0 : - forall a:ad, - 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. - intros. discriminate H. - Qed. - - Lemma MapGet_M2_bit_0_1 : - forall a:ad, - 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. - intros. discriminate H0. - trivial. - Qed. - - Lemma MapGet_M2_bit_0_if : - forall (m m':Map) (a:ad), - MapGet (M2 m m') a = - (if Nbit0 a then MapGet m' (Ndiv2 a) else MapGet m (Ndiv2 a)). - Proof. - 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 Nbit0 a then MapGet (M2 m' m) a else MapGet (M2 m m'') a) = - MapGet m (Ndiv2 a). - Proof. - 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 Map2_semantics_3 : - forall m m':Map, - eqm (MapGet (M2 m m')) - (fun a:ad => - match Nbit0 a with - | false => MapGet m (Ndiv2 a) - | true => MapGet m' (Ndiv2 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 A), - eqm (MapGet m) f -> - eqm (MapGet m') f' -> - eqm (MapGet (M2 m m')) - (fun a:ad => - match Nbit0 a with - | false => f (Ndiv2 a) - | true => f' (Ndiv2 a) - end). - Proof. - unfold eqm in |- *. - intros. - rewrite <- (H (Ndiv2 a)). - rewrite <- (H0 (Ndiv2 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 (Ndiv2 a) y (Ndiv2 a') y' p' in - match Nbit0 a with - | false => M2 m M0 - | true => M2 M0 m - end - | _ => - 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. - - 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. - Qed. - - (*i - Lemma MapGet_M2_bit_0_1' : (m,m',m'',m''':Map) - (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 (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 (Nbit0 a); Auto. - Qed. - i*) - - Lemma MapGet_if_same : - forall (m:Map) (b:bool) (a:ad), MapGet (if b then m else m) a = MapGet m a. - Proof. - simple induction b; trivial. - Qed. - - Lemma MapGet_M2_bit_0_2 : - forall (m m' m'':Map) (a:ad), - 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), - 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 <- 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), - Nxor a a' = Npos p -> MapGet (MapPut1 a y a' y' p) a' = Some y'. - Proof. - 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 (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 : - forall (m m':Map) (a:ad), - 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 (Nbit0 a); assumption. - Qed. - - Lemma MapPut1_semantics_3 : - forall (p:positive) (a a' a0:ad) (y y':A), - 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 (Nbit0 a); apply MapGet_M2_both_None; apply M1_semantics_2; - assumption. - intros. simpl in |- *. elim (Nneq_elim a a0 H1). intro. rewrite H3. rewrite if_negb. - rewrite MapGet_M2_bit_0_2. reflexivity. - 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 (Nxor (Ndiv2 a) (Ndiv2 a') = Npos p0). intro. - case (Nbit0 a); apply MapGet_M2_both_None; trivial; apply H; - assumption. - 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 (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), - Nxor a a' = Npos p -> - eqm (MapGet (MapPut1 a y a' y' p)) - (fun a0:ad => - 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), - Nxor a a' = Npos p -> - eqm (MapGet (MapPut1 a y a' y' p)) - (fun a0:ad => - 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 (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. - - Fixpoint MapPut (m:Map) : ad -> A -> Map := - match m with - | M0 => M1 - | M1 a y => - fun (a':ad) (y':A) => - 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 - | 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. - - 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 Neqb a a0 then Some y' else None). - Proof. - simpl in |- *. intros. rewrite (Nxor_nilpotent a). trivial. - Qed. - - Lemma MapPut_semantics_2_2 : - forall (a a':ad) (y y':A) (a0 a'':ad), - Nxor a a' = a'' -> - MapGet (MapPut (M1 a y) a' y') a0 = - (if Neqb a' a0 then Some y' else if Neqb a a0 then Some y else None). - Proof. - 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 (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 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'' := 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 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. - Qed. - - Lemma MapPut_semantics : - forall (m:Map) (a:ad) (y:A), - eqm (MapGet (MapPut m a y)) - (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 (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 (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 := - match m with - | M0 => M1 - | M1 a y => - fun (a':ad) (y':A) => - 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 - | 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 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. - Qed. - - Lemma MapPut_behind_as_before_1 : - forall a a' a0:ad, - 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 (Ndiscr (Nxor a a')). intro H0. elim H0. - intros p H1. rewrite H1. reflexivity. - 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), - 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 (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 (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 - end. - Proof. - 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 <- (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 (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 : - 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 Neqb a a' then Some y else None - end). - Proof. - 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. - - Definition makeM2 (m m':Map) := - match m, m' with - | M0, M0 => M0 - | 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 (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 (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 (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) (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 (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 (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. - 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 Neqb a a' with - | true => M0 - | false => m - end - | M2 m1 m2 => - fun a:ad => - 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 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 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 (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 (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 (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 (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 (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. - - 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 : - 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 (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 (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. - - (** [MapInter], [MapRngRestrTo], [MapRngRestrBy], [MapInverse] - not implemented: need a decidable equality on [A]. *) - - 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 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 (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 (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 (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. - 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 (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. - Proof. - 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. - 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 (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. - 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 (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. - Proof. - 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. - 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 (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. - 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 (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. - 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 (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 (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. - - 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. - 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.
\ No newline at end of file |