Library Mapiter

Require Import Bool.
Require Import Sumbool.
Require Import NArith.
Require Import Ndigits.
Require Import Ndec.
Require Import Map.
Require Import Mapaxioms.
Require Import Fset.
Require Import List.

Section MapIter.

  Variable A : Type.

  Section MapSweepDef.

  Variable f : ad -> A -> bool.

  Definition MapSweep2 (a0:ad) (y:A) :=
    if f a0 y then Some (a0, y) else None.

  Fixpoint MapSweep1 (pf:ad -> ad) (m:Map A) {struct m} :
   option (ad * A) :=
    match m with
    | M0 _ => None
    | M1 _ a y => MapSweep2 (pf a) y
    | M2 _ m m' =>
        match MapSweep1 (fun a:ad => pf (Ndouble a)) m with
        | Some r => Some r
        | None => MapSweep1 (fun a:ad => pf (Ndouble_plus_one a)) m'
        end
    end.

  Definition MapSweep (m:Map A) := MapSweep1 (fun a:ad => a) m.

  Lemma MapSweep_semantics_1_1 :
   forall (m:Map A) (pf:ad -> ad) (a:ad) (y:A),
     MapSweep1 pf m = Some (a, y) -> f a y = true.

  Lemma MapSweep_semantics_1 :
   forall (m:Map A) (a:ad) (y:A), MapSweep m = Some (a, y) -> f a y = true.

  Lemma MapSweep_semantics_2_1 :
   forall (m:Map A) (pf:ad -> ad) (a:ad) (y:A),
     MapSweep1 pf m = Some (a, y) -> {a' : ad | a = pf a'}.

  Lemma MapSweep_semantics_2_2 :
   forall (m:Map A) (pf fp:ad -> ad),
     (forall a0:ad, fp (pf a0) = a0) ->
     forall (a:ad) (y:A),
       MapSweep1 pf m = Some (a, y) -> MapGet A m (fp a) = Some y.

  Lemma MapSweep_semantics_2 :
   forall (m:Map A) (a:ad) (y:A),
     MapSweep m = Some (a, y) -> MapGet A m a = Some y.

  Lemma MapSweep_semantics_3_1 :
   forall (m:Map A) (pf:ad -> ad),
     MapSweep1 pf m = None ->
     forall (a:ad) (y:A), MapGet A m a = Some y -> f (pf a) y = false.

  Lemma MapSweep_semantics_3 :
   forall m:Map A,
     MapSweep m = None ->
     forall (a:ad) (y:A), MapGet A m a = Some y -> f a y = false.

  Lemma MapSweep_semantics_4_1 :
   forall (m:Map A) (pf:ad -> ad) (a:ad) (y:A),
     MapGet A m a = Some y ->
     f (pf a) y = true ->
     {a' : ad & {y' : A | MapSweep1 pf m = Some (a', y')}}.

  Lemma MapSweep_semantics_4 :
   forall (m:Map A) (a:ad) (y:A),
     MapGet A m a = Some y ->
     f a y = true -> {a' : ad & {y' : A | MapSweep m = Some (a', y')}}.

  End MapSweepDef.

  Variable B : Type.

  Fixpoint MapCollect1 (f:ad -> A -> Map B) (pf:ad -> ad)
   (m:Map A) {struct m} : Map B :=
    match m with
    | M0 _ => M0 B
    | M1 _ a y => f (pf a) y
    | M2 _ m1 m2 =>
        MapMerge B (MapCollect1 f (fun a0:ad => pf (Ndouble a0)) m1)
          (MapCollect1 f (fun a0:ad => pf (Ndouble_plus_one a0)) m2)
    end.

  Definition MapCollect (f:ad -> A -> Map B) (m:Map A) :=
    MapCollect1 f (fun a:ad => a) m.

  Section MapFoldDef.

    Variable M : Type.
    Variable neutral : M.
    Variable op : M -> M -> M.

    Fixpoint MapFold1 (f:ad -> A -> M) (pf:ad -> ad)
     (m:Map A) {struct m} : M :=
      match m with
      | M0 _ => neutral
      | M1 _ a y => f (pf a) y
      | M2 _ m1 m2 =>
          op (MapFold1 f (fun a0:ad => pf (Ndouble a0)) m1)
            (MapFold1 f (fun a0:ad => pf (Ndouble_plus_one a0)) m2)
      end.

    Definition MapFold (f:ad -> A -> M) (m:Map A) :=
      MapFold1 f (fun a:ad => a) m.

    Lemma MapFold_empty : forall f:ad -> A -> M, MapFold f (M0 A) = neutral.

    Lemma MapFold_M1 :
     forall (f:ad -> A -> M) (a:ad) (y:A), MapFold f (M1 A a y) = f a y.

    Variable State : Type.
    Variable f : State -> ad -> A -> State * M.

    Fixpoint MapFold1_state (state:State) (pf:ad -> ad)
     (m:Map A) {struct m} : State * M :=
      match m with
      | M0 _ => (state, neutral)
      | M1 _ a y => f state (pf a) y
      | M2 _ m1 m2 =>
          match MapFold1_state state (fun a0:ad => pf (Ndouble a0)) m1 with
          | (state1, x1) =>
              match
                MapFold1_state state1
                  (fun a0:ad => pf (Ndouble_plus_one a0)) m2
              with
              | (state2, x2) => (state2, op x1 x2)
              end
          end
      end.

    Definition MapFold_state (state:State) :=
      MapFold1_state state (fun a:ad => a).

    Lemma pair_sp : forall (B C:Type) (x:B * C), x = (fst x, snd x).

    Lemma MapFold_state_stateless_1 :
     forall (m:Map A) (g:ad -> A -> M) (pf:ad -> ad),
       (forall (state:State) (a:ad) (y:A), snd (f state a y) = g a y) ->
       forall state:State, snd (MapFold1_state state pf m) = MapFold1 g pf m.

    Lemma MapFold_state_stateless :
     forall g:ad -> A -> M,
       (forall (state:State) (a:ad) (y:A), snd (f state a y) = g a y) ->
       forall (state:State) (m:Map A),
         snd (MapFold_state state m) = MapFold g m.

  End MapFoldDef.

  Lemma MapCollect_as_Fold :
   forall (f:ad -> A -> Map B) (m:Map A),
     MapCollect f m = MapFold (Map B) (M0 B) (MapMerge B) f m.

  Definition alist := list (ad * A).
  Definition anil := nil (A:=(ad * A)).
  Definition acons := cons (A:=(ad * A)).
  Definition aapp := app (A:=(ad * A)).

  Definition alist_of_Map :=
    MapFold alist anil aapp (fun (a:ad) (y:A) => acons (a, y) anil).

  Fixpoint alist_semantics (l:alist) : ad -> option A :=
    match l with
    | nil => fun _:ad => None
    | (a, y) :: l' =>
        fun a0:ad => if Neqb a a0 then Some y else alist_semantics l' a0
    end.

  Lemma alist_semantics_app :
   forall (l l':alist) (a:ad),
     alist_semantics (aapp l l') a =
     match alist_semantics l a with
     | None => alist_semantics l' a
     | Some y => Some y
     end.

  Lemma alist_of_Map_semantics_1_1 :
   forall (m:Map A) (pf:ad -> ad) (a:ad) (y:A),
     alist_semantics
       (MapFold1 alist anil aapp (fun (a0:ad) (y:A) => acons (a0, y) anil) pf
          m) a = Some y -> {a' : ad | a = pf a'}.

  Definition ad_inj (pf:ad -> ad) :=
    forall a0 a1:ad, pf a0 = pf a1 -> a0 = a1.

  Lemma ad_comp_double_inj :
   forall pf:ad -> ad, ad_inj pf -> ad_inj (fun a0:ad => pf (Ndouble a0)).

  Lemma ad_comp_double_plus_un_inj :
   forall pf:ad -> ad,
     ad_inj pf -> ad_inj (fun a0:ad => pf (Ndouble_plus_one a0)).

  Lemma alist_of_Map_semantics_1 :
   forall (m:Map A) (pf:ad -> ad),
     ad_inj pf ->
     forall a:ad,
       MapGet A m a =
       alist_semantics
         (MapFold1 alist anil aapp (fun (a0:ad) (y:A) => acons (a0, y) anil)
            pf m) (pf a).

  Lemma alist_of_Map_semantics :
   forall m:Map A, eqm A (MapGet A m) (alist_semantics (alist_of_Map m)).

  Fixpoint Map_of_alist (l:alist) : Map A :=
    match l with
    | nil => M0 A
    | (a, y) :: l' => MapPut A (Map_of_alist l') a y
    end.

  Lemma Map_of_alist_semantics :
   forall l:alist, eqm A (alist_semantics l) (MapGet A (Map_of_alist l)).

  Lemma Map_of_alist_of_Map :
   forall m:Map A, eqmap A (Map_of_alist (alist_of_Map m)) m.

  Lemma alist_of_Map_of_alist :
   forall l:alist,
     eqm A (alist_semantics (alist_of_Map (Map_of_alist l)))
       (alist_semantics l).

  Lemma fold_right_aapp :
   forall (M:Type) (neutral:M) (op:M -> M -> M),
     (forall a b c:M, op (op a b) c = op a (op b c)) ->
     (forall a:M, op neutral a = a) ->
     forall (f:ad -> A -> M) (l l':alist),
       fold_right (fun (r:ad * A) (m:M) => let (a, y) := r in op (f a y) m)
         neutral (aapp l l') =
       op
         (fold_right
            (fun (r:ad * A) (m:M) => let (a, y) := r in op (f a y) m) neutral
            l)
         (fold_right
            (fun (r:ad * A) (m:M) => let (a, y) := r in op (f a y) m) neutral
            l').

  Lemma MapFold_as_fold_1 :
   forall (M:Type) (neutral:M) (op:M -> M -> M),
     (forall a b c:M, op (op a b) c = op a (op b c)) ->
     (forall a:M, op neutral a = a) ->
     (forall a:M, op a neutral = a) ->
     forall (f:ad -> A -> M) (m:Map A) (pf:ad -> ad),
       MapFold1 M neutral op f pf m =
       fold_right (fun (r:ad * A) (m:M) => let (a, y) := r in op (f a y) m)
         neutral
         (MapFold1 alist anil aapp (fun (a:ad) (y:A) => acons (a, y) anil) pf
            m).

  Lemma MapFold_as_fold :
   forall (M:Type) (neutral:M) (op:M -> M -> M),
     (forall a b c:M, op (op a b) c = op a (op b c)) ->
     (forall a:M, op neutral a = a) ->
     (forall a:M, op a neutral = a) ->
     forall (f:ad -> A -> M) (m:Map A),
       MapFold M neutral op f m =
       fold_right (fun (r:ad * A) (m:M) => let (a, y) := r in op (f a y) m)
         neutral (alist_of_Map m).

  Lemma alist_MapMerge_semantics :
   forall m m':Map A,
     eqm A (alist_semantics (aapp (alist_of_Map m') (alist_of_Map m)))
       (alist_semantics (alist_of_Map (MapMerge A m m'))).

  Lemma alist_MapMerge_semantics_disjoint :
   forall m m':Map A,
     eqmap A (MapDomRestrTo A A m m') (M0 A) ->
     eqm A (alist_semantics (aapp (alist_of_Map m) (alist_of_Map m')))
       (alist_semantics (alist_of_Map (MapMerge A m m'))).

  Lemma alist_semantics_disjoint_comm :
   forall l l':alist,
     eqmap A (MapDomRestrTo A A (Map_of_alist l) (Map_of_alist l')) (M0 A) ->
     eqm A (alist_semantics (aapp l l')) (alist_semantics (aapp l' l)).

End MapIter.