Library Mapfold

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

Section MapFoldResults.

  Variable A : Type.

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

  Variable nleft : forall a:M, op neutral a = a.
  Variable nright : forall a:M, op a neutral = a.
  Variable assoc : forall a b c:M, op (op a b) c = op a (op b c).

  Lemma MapFold_ext :
   forall (f:ad -> A -> M) (m m':Map A),
     eqmap A m m' -> MapFold _ _ neutral op f m = MapFold _ _ neutral op f m'.

  Lemma MapFold_ext_f_1 :
   forall (m:Map A) (f g:ad -> A -> M) (pf:ad -> ad),
     (forall (a:ad) (y:A), MapGet _ m a = Some y -> f (pf a) y = g (pf a) y) ->
     MapFold1 _ _ neutral op f pf m = MapFold1 _ _ neutral op g pf m.

  Lemma MapFold_ext_f :
   forall (f g:ad -> A -> M) (m:Map A),
     (forall (a:ad) (y:A), MapGet _ m a = Some y -> f a y = g a y) ->
     MapFold _ _ neutral op f m = MapFold _ _ neutral op g m.

  Lemma MapFold1_as_Fold_1 :
   forall (m:Map A) (f f':ad -> A -> M) (pf pf':ad -> ad),
     (forall (a:ad) (y:A), f (pf a) y = f' (pf' a) y) ->
     MapFold1 _ _ neutral op f pf m = MapFold1 _ _ neutral op f' pf' m.

  Lemma MapFold1_as_Fold :
   forall (f:ad -> A -> M) (pf:ad -> ad) (m:Map A),
     MapFold1 _ _ neutral op f pf m =
     MapFold _ _ neutral op (fun (a:ad) (y:A) => f (pf a) y) m.

  Lemma MapFold1_ext :
   forall (f:ad -> A -> M) (m m':Map A),
     eqmap A m m' ->
     forall pf:ad -> ad,
       MapFold1 _ _ neutral op f pf m = MapFold1 _ _ neutral op f pf m'.

  Variable comm : forall a b:M, op a b = op b a.

  Lemma MapFold_Put_disjoint_1 :
   forall (p:positive) (f:ad -> A -> M) (pf:ad -> ad)
     (a1 a2:ad) (y1 y2:A),
     Nxor a1 a2 = Npos p ->
     MapFold1 A M neutral op f pf (MapPut1 A a1 y1 a2 y2 p) =
     op (f (pf a1) y1) (f (pf a2) y2).

  Lemma MapFold_Put_disjoint_2 :
   forall (f:ad -> A -> M) (m:Map A) (a:ad) (y:A) (pf:ad -> ad),
     MapGet A m a = None ->
     MapFold1 A M neutral op f pf (MapPut A m a y) =
     op (f (pf a) y) (MapFold1 A M neutral op f pf m).

  Lemma MapFold_Put_disjoint :
   forall (f:ad -> A -> M) (m:Map A) (a:ad) (y:A),
     MapGet A m a = None ->
     MapFold A M neutral op f (MapPut A m a y) =
     op (f a y) (MapFold A M neutral op f m).

  Lemma MapFold_Put_behind_disjoint_2 :
   forall (f:ad -> A -> M) (m:Map A) (a:ad) (y:A) (pf:ad -> ad),
     MapGet A m a = None ->
     MapFold1 A M neutral op f pf (MapPut_behind A m a y) =
     op (f (pf a) y) (MapFold1 A M neutral op f pf m).

  Lemma MapFold_Put_behind_disjoint :
   forall (f:ad -> A -> M) (m:Map A) (a:ad) (y:A),
     MapGet A m a = None ->
     MapFold A M neutral op f (MapPut_behind A m a y) =
     op (f a y) (MapFold A M neutral op f m).

  Lemma MapFold_Merge_disjoint_1 :
   forall (f:ad -> A -> M) (m1 m2:Map A) (pf:ad -> ad),
     MapDisjoint A A m1 m2 ->
     MapFold1 A M neutral op f pf (MapMerge A m1 m2) =
     op (MapFold1 A M neutral op f pf m1) (MapFold1 A M neutral op f pf m2).

  Lemma MapFold_Merge_disjoint :
   forall (f:ad -> A -> M) (m1 m2:Map A),
     MapDisjoint A A m1 m2 ->
     MapFold A M neutral op f (MapMerge A m1 m2) =
     op (MapFold A M neutral op f m1) (MapFold A M neutral op f m2).

End MapFoldResults.

Section MapFoldDistr.

  Variable A : Type.

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

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

  Variable N : Type.

  Variable times : M -> N -> M'.

  Variable absorb : forall c:N, times neutral c = neutral'.
  Variable
    distr :
      forall (a b:M) (c:N), times (op a b) c = op' (times a c) (times b c).

  Lemma MapFold_distr_r_1 :
   forall (f:ad -> A -> M) (m:Map A) (c:N) (pf:ad -> ad),
     times (MapFold1 A M neutral op f pf m) c =
     MapFold1 A M' neutral' op' (fun (a:ad) (y:A) => times (f a y) c) pf m.

  Lemma MapFold_distr_r :
   forall (f:ad -> A -> M) (m:Map A) (c:N),
     times (MapFold A M neutral op f m) c =
     MapFold A M' neutral' op' (fun (a:ad) (y:A) => times (f a y) c) m.

End MapFoldDistr.

Section MapFoldDistrL.

  Variable A : Type.

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

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

  Variable N : Type.

  Variable times : N -> M -> M'.

  Variable absorb : forall c:N, times c neutral = neutral'.
  Variable
    distr :
      forall (a b:M) (c:N), times c (op a b) = op' (times c a) (times c b).

  Lemma MapFold_distr_l :
   forall (f:ad -> A -> M) (m:Map A) (c:N),
     times c (MapFold A M neutral op f m) =
     MapFold A M' neutral' op' (fun (a:ad) (y:A) => times c (f a y)) m.

End MapFoldDistrL.

Section MapFoldExists.

  Variable A : Type.

  Lemma MapFold_orb_1 :
   forall (f:ad -> A -> bool) (m:Map A) (pf:ad -> ad),
     MapFold1 A bool false orb f pf m =
     match MapSweep1 A f pf m with
     | Some _ => true
     | _ => false
     end.

  Lemma MapFold_orb :
   forall (f:ad -> A -> bool) (m:Map A),
     MapFold A bool false orb f m =
     match MapSweep A f m with
     | Some _ => true
     | _ => false
     end.

End MapFoldExists.

Section DMergeDef.

  Variable A : Type.

  Definition DMerge :=
    MapFold (Map A) (Map A) (M0 A) (MapMerge A) (fun (_:ad) (m:Map A) => m).

  Lemma in_dom_DMerge_1 :
   forall (m:Map (Map A)) (a:ad),
     in_dom A a (DMerge m) =
     match MapSweep _ (fun (_:ad) (m0:Map A) => in_dom A a m0) m with
     | Some _ => true
     | _ => false
     end.

  Lemma in_dom_DMerge_2 :
   forall (m:Map (Map A)) (a:ad),
     in_dom A a (DMerge m) = true ->
     {b : ad &
     {m0 : Map A | MapGet _ m b = Some m0 /\ in_dom A a m0 = true}}.

  Lemma in_dom_DMerge_3 :
   forall (m:Map (Map A)) (a b:ad) (m0:Map A),
     MapGet _ m a = Some m0 ->
     in_dom A b m0 = true -> in_dom A b (DMerge m) = true.

End DMergeDef.