Library Coq.IntMap.Map
Definition of finite sets as trees indexed by adresses
Require Import Bool.
Require Import Sumbool.
Require Import NArith.
Require Import Ndigits.
Require Import Ndec.
Definition ad := N.
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.
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.