Library Mapcanon

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

Section MapCanon.

  Variable A : Type.

  Inductive mapcanon : Map A -> Prop :=
    | M0_canon : mapcanon (M0 A)
    | M1_canon : forall (a:ad) (y:A), mapcanon (M1 A a y)
    | M2_canon :
        forall m1 m2:Map A,
          mapcanon m1 ->
          mapcanon m2 -> 2 <= MapCard A (M2 A m1 m2) -> mapcanon (M2 A m1 m2).

  Lemma mapcanon_M2 :
   forall m1 m2:Map A, mapcanon (M2 A m1 m2) -> 2 <= MapCard A (M2 A m1 m2).

  Lemma mapcanon_M2_1 :
   forall m1 m2:Map A, mapcanon (M2 A m1 m2) -> mapcanon m1.

  Lemma mapcanon_M2_2 :
   forall m1 m2:Map A, mapcanon (M2 A m1 m2) -> mapcanon m2.

  Lemma M2_eqmap_1 :
   forall m0 m1 m2 m3:Map A,
     eqmap A (M2 A m0 m1) (M2 A m2 m3) -> eqmap A m0 m2.

  Lemma M2_eqmap_2 :
   forall m0 m1 m2 m3:Map A,
     eqmap A (M2 A m0 m1) (M2 A m2 m3) -> eqmap A m1 m3.

  Lemma mapcanon_unique :
   forall m m':Map A, mapcanon m -> mapcanon m' -> eqmap A m m' -> m = m'.

  Lemma MapPut1_canon :
   forall (p:positive) (a a':ad) (y y':A), mapcanon (MapPut1 A a y a' y' p).

  Lemma MapPut_canon :
   forall m:Map A,
     mapcanon m -> forall (a:ad) (y:A), mapcanon (MapPut A m a y).

  Lemma MapPut_behind_canon :
   forall m:Map A,
     mapcanon m -> forall (a:ad) (y:A), mapcanon (MapPut_behind A m a y).

  Lemma makeM2_canon :
   forall m m':Map A, mapcanon m -> mapcanon m' -> mapcanon (makeM2 A m m').

  Fixpoint MapCanonicalize (m:Map A) : Map A :=
    match m with
    | M2 _ m0 m1 => makeM2 A (MapCanonicalize m0) (MapCanonicalize m1)
    | _ => m
    end.

  Lemma mapcanon_exists_1 : forall m:Map A, eqmap A m (MapCanonicalize m).

  Lemma mapcanon_exists_2 : forall m:Map A, mapcanon (MapCanonicalize m).

  Lemma mapcanon_exists :
   forall m:Map A, {m' : Map A | eqmap A m m' /\ mapcanon m'}.

  Lemma MapRemove_canon :
   forall m:Map A, mapcanon m -> forall a:ad, mapcanon (MapRemove A m a).

  Lemma MapMerge_canon :
   forall m m':Map A, mapcanon m -> mapcanon m' -> mapcanon (MapMerge A m m').

  Lemma MapDelta_canon :
   forall m m':Map A, mapcanon m -> mapcanon m' -> mapcanon (MapDelta A m m').

  Variable B : Type.

  Lemma MapDomRestrTo_canon :
   forall m:Map A,
     mapcanon m -> forall m':Map B, mapcanon (MapDomRestrTo A B m m').

  Lemma MapDomRestrBy_canon :
   forall m:Map A,
     mapcanon m -> forall m':Map B, mapcanon (MapDomRestrBy A B m m').

  Lemma Map_of_alist_canon : forall l:alist A, mapcanon (Map_of_alist A l).

  Lemma MapSubset_c_1 :
   forall (m:Map A) (m':Map B),
     mapcanon m -> MapSubset A B m m' -> MapDomRestrBy A B m m' = M0 A.

  Lemma MapSubset_c_2 :
   forall (m:Map A) (m':Map B),
     MapDomRestrBy A B m m' = M0 A -> MapSubset A B m m'.

End MapCanon.

Section FSetCanon.

  Variable A : Type.

  Lemma MapDom_canon :
   forall m:Map A, mapcanon A m -> mapcanon unit (MapDom A m).

End FSetCanon.

Section MapFoldCanon.

  Variables A B : Type.

  Lemma MapFold_canon_1 :
   forall m0:Map B,
     mapcanon B m0 ->
     forall op:Map B -> Map B -> Map B,
       (forall m1:Map B,
          mapcanon B m1 ->
          forall m2:Map B, mapcanon B m2 -> mapcanon B (op m1 m2)) ->
       forall f:ad -> A -> Map B,
         (forall (a:ad) (y:A), mapcanon B (f a y)) ->
         forall (m:Map A) (pf:ad -> ad),
           mapcanon B (MapFold1 A (Map B) m0 op f pf m).

  Lemma MapFold_canon :
   forall m0:Map B,
     mapcanon B m0 ->
     forall op:Map B -> Map B -> Map B,
       (forall m1:Map B,
          mapcanon B m1 ->
          forall m2:Map B, mapcanon B m2 -> mapcanon B (op m1 m2)) ->
       forall f:ad -> A -> Map B,
         (forall (a:ad) (y:A), mapcanon B (f a y)) ->
         forall m:Map A, mapcanon B (MapFold A (Map B) m0 op f m).

  Lemma MapCollect_canon :
   forall f:ad -> A -> Map B,
     (forall (a:ad) (y:A), mapcanon B (f a y)) ->
     forall m:Map A, mapcanon B (MapCollect A B f m).

End MapFoldCanon.