Library 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 : 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}.
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}.
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).
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).
Lemma M1_semantics_1 : forall (a:ad) (y:A), MapGet (M1 a y) a = Some y.
Lemma M1_semantics_2 :
forall (a a':ad) (y:A), Neqb a a' = false -> MapGet (M1 a y) a' = None.
Lemma Map2_semantics_1 :
forall m m':Map,
eqm (MapGet m) (fun a:ad => MapGet (M2 m m') (Ndouble a)).
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)).
Lemma Map2_semantics_2 :
forall m m':Map,
eqm (MapGet m') (fun a:ad => MapGet (M2 m m') (Ndouble_plus_one a)).
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)).
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).
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).
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)).
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).
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).
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).
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).
Lemma MapGet_if_same :
forall (m:Map) (b:bool) (a:ad), MapGet (if b then m else m) a = MapGet m a.
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).
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.
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'.
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.
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.
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).
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).
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.
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).
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).
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).
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').
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').
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').
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.
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.
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.
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).
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')).
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').
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).
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)).
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.
Lemma MapDelta_semantics_1 :
forall (m m':Map) (a:ad),
MapGet m a = None ->
MapGet m' a = None -> MapGet (MapDelta m m') a = None.
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.
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.
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.
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.
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.
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).
Definition MapEmptyp (m:Map) := match m with
| M0 => true
| _ => false
end.
Lemma MapEmptyp_correct : MapEmptyp M0 = true.
Lemma MapEmptyp_complete : forall m:Map, MapEmptyp m = true -> m = M0.
MapSplit not implemented: not the preferred way of recursing over Maps
(use MapSweep, MapCollect, or MapFold in Mapiter.v.