Library 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.

Section MapDefs.

We now define maps from ad to A.
Variable A : Type.

Inductive Map :=
| 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 =>
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 :
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 :
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 :
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 :
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 :
(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'))
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'))
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.

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 :
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 :
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 :
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))
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))
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 =>
match Nxor a a' with
| N0 => M1 a' y'
| Npos p => MapPut1 a y a' y' p
end
| M2 m1 m2 =>
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 :
MapGet (MapPut M0 a y) a0 = MapGet (M1 a y) a0.
Proof.
trivial.
Qed.

Lemma MapPut_semantics_2_1 :
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 :
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 :
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 :
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 :
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 =>
match Nxor a a' with
| N0 => m
| Npos p => MapPut1 a y a' y' p
end
| M2 m1 m2 =>
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 :
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 :
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 :
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 :
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 :
eqm (MapGet (MapPut_behind m a y))
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 =>
if Nbit0 a
then makeM2 m1 (MapRemove m2 (Ndiv2 a))
else makeM2 (MapRemove m1 (Ndiv2 a)) m2
end.

Lemma MapRemove_semantics :
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'))
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 :
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 :
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 :
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 :
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 :
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 :
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'))
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.