Library Mapc

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

Section MapC.

  Variables A B C : Type.

  Lemma MapPut_as_Merge_c :
   forall m:Map A,
     mapcanon A m ->
     forall (a:ad) (y:A), MapPut A m a y = MapMerge A m (M1 A a y).

  Lemma MapPut_behind_as_Merge_c :
   forall m:Map A,
     mapcanon A m ->
     forall (a:ad) (y:A), MapPut_behind A m a y = MapMerge A (M1 A a y) m.

  Lemma MapMerge_empty_m_c : forall m:Map A, MapMerge A (M0 A) m = m.

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

  Lemma MapMerge_idempotent_c :
   forall m:Map A, mapcanon A m -> MapMerge A m m = m.

  Lemma MapMerge_RestrTo_l_c :
   forall m m' m'':Map A,
     mapcanon A m ->
     mapcanon A m'' ->
     MapMerge A (MapDomRestrTo A A m m') m'' =
     MapDomRestrTo A A (MapMerge A m m'') (MapMerge A m' m'').

  Lemma MapRemove_as_RestrBy_c :
   forall m:Map A,
     mapcanon A m ->
     forall (a:ad) (y:B), MapRemove A m a = MapDomRestrBy A B m (M1 B a y).

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

  Lemma MapDomRestrTo_idempotent_c :
   forall m:Map A, mapcanon A m -> MapDomRestrTo A A m m = m.

  Lemma MapDomRestrTo_Dom_c :
   forall (m:Map A) (m':Map B),
     mapcanon A m ->
     MapDomRestrTo A B m m' = MapDomRestrTo A unit m (MapDom B m').

  Lemma MapDomRestrBy_Dom_c :
   forall (m:Map A) (m':Map B),
     mapcanon A m ->
     MapDomRestrBy A B m m' = MapDomRestrBy A unit m (MapDom B m').

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

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

  Lemma MapDomRestrBy_To_c :
   forall (m:Map A) (m':Map B) (m'':Map C),
     mapcanon A m ->
     MapDomRestrBy A C (MapDomRestrTo A B m m') m'' =
     MapDomRestrTo A B m (MapDomRestrBy B C m' m'').

  Lemma MapDomRestrBy_To_comm_c :
   forall (m:Map A) (m':Map B) (m'':Map C),
     mapcanon A m ->
     MapDomRestrBy A C (MapDomRestrTo A B m m') m'' =
     MapDomRestrTo A B (MapDomRestrBy A C m m'') m'.

  Lemma MapDomRestrTo_By_c :
   forall (m:Map A) (m':Map B) (m'':Map C),
     mapcanon A m ->
     MapDomRestrTo A C (MapDomRestrBy A B m m') m'' =
     MapDomRestrTo A C m (MapDomRestrBy C B m'' m').

  Lemma MapDomRestrTo_By_comm_c :
   forall (m:Map A) (m':Map B) (m'':Map C),
     mapcanon A m ->
     MapDomRestrTo A C (MapDomRestrBy A B m m') m'' =
     MapDomRestrBy A B (MapDomRestrTo A C m m'') m'.

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

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

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

  Lemma MapDelta_nilpotent_c :
   forall m:Map A, mapcanon A m -> MapDelta A m m = M0 A.

  Lemma MapDelta_as_Merge_c :
   forall m m':Map A,
     mapcanon A m ->
     mapcanon A m' ->
     MapDelta A m m' =
     MapMerge A (MapDomRestrBy A A m m') (MapDomRestrBy A A m' m).

  Lemma MapDelta_as_DomRestrBy_c :
   forall m m':Map A,
     mapcanon A m ->
     mapcanon A m' ->
     MapDelta A m m' =
     MapDomRestrBy A A (MapMerge A m m') (MapDomRestrTo A A m m').

  Lemma MapDelta_as_DomRestrBy_2_c :
   forall m m':Map A,
     mapcanon A m ->
     mapcanon A m' ->
     MapDelta A m m' =
     MapDomRestrBy A A (MapMerge A m m') (MapDomRestrTo A A m' m).

  Lemma MapDelta_sym_c :
   forall m m':Map A,
     mapcanon A m -> mapcanon A m' -> MapDelta A m m' = MapDelta A m' m.

  Lemma MapDom_Split_1_c :
   forall (m:Map A) (m':Map B),
     mapcanon A m ->
     m = MapMerge A (MapDomRestrTo A B m m') (MapDomRestrBy A B m m').

  Lemma MapDom_Split_2_c :
   forall (m:Map A) (m':Map B),
     mapcanon A m ->
     m = MapMerge A (MapDomRestrBy A B m m') (MapDomRestrTo A B m m').

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

  Lemma Map_of_alist_of_Map_c :
   forall m:Map A, mapcanon A m -> Map_of_alist A (alist_of_Map A m) = m.

  Lemma alist_of_Map_of_alist_c :
   forall l:alist A,
     alist_sorted_2 A l -> alist_of_Map A (Map_of_alist A l) = l.

  Lemma MapSubset_antisym_c :
   forall (m:Map A) (m':Map B),
     mapcanon A m ->
     mapcanon B m' ->
     MapSubset A B m m' -> MapSubset B A m' m -> MapDom A m = MapDom B m'.

  Lemma FSubset_antisym_c :
   forall s s':FSet,
     mapcanon unit s ->
     mapcanon unit s' -> MapSubset _ _ s s' -> MapSubset _ _ s' s -> s = s'.

  Lemma MapDisjoint_empty_c :
   forall m:Map A, mapcanon A m -> MapDisjoint A A m m -> m = M0 A.

  Lemma MapDelta_disjoint_c :
   forall m m':Map A,
     mapcanon A m ->
     mapcanon A m' ->
     MapDisjoint A A m m' -> MapDelta A m m' = MapMerge A m m'.

End MapC.

Lemma FSetDelta_assoc_c :
 forall s s' s'':FSet,
   mapcanon unit s ->
   mapcanon unit s' ->
   mapcanon unit s'' ->
   MapDelta _ (MapDelta _ s s') s'' = MapDelta _ s (MapDelta _ s' s'').

Lemma FSet_ext_c :
 forall s s':FSet,
   mapcanon unit s ->
   mapcanon unit s' -> (forall a:ad, in_FSet a s = in_FSet a s') -> s = s'.

Lemma FSetUnion_comm_c :
 forall s s':FSet,
   mapcanon unit s -> mapcanon unit s' -> FSetUnion s s' = FSetUnion s' s.

Lemma FSetUnion_assoc_c :
 forall s s' s'':FSet,
   mapcanon unit s ->
   mapcanon unit s' ->
   mapcanon unit s'' ->
   FSetUnion (FSetUnion s s') s'' = FSetUnion s (FSetUnion s' s'').

Lemma FSetUnion_M0_s_c : forall s:FSet, FSetUnion (M0 unit) s = s.

Lemma FSetUnion_s_M0_c : forall s:FSet, FSetUnion s (M0 unit) = s.

Lemma FSetUnion_idempotent :
 forall s:FSet, mapcanon unit s -> FSetUnion s s = s.

Lemma FSetInter_comm_c :
 forall s s':FSet,
   mapcanon unit s -> mapcanon unit s' -> FSetInter s s' = FSetInter s' s.

Lemma FSetInter_assoc_c :
 forall s s' s'':FSet,
   mapcanon unit s ->
   FSetInter (FSetInter s s') s'' = FSetInter s (FSetInter s' s'').

Lemma FSetInter_M0_s_c : forall s:FSet, FSetInter (M0 unit) s = M0 unit.

Lemma FSetInter_s_M0_c : forall s:FSet, FSetInter s (M0 unit) = M0 unit.

Lemma FSetInter_idempotent :
 forall s:FSet, mapcanon unit s -> FSetInter s s = s.

Lemma FSetUnion_Inter_l_c :
 forall s s' s'':FSet,
   mapcanon unit s ->
   mapcanon unit s'' ->
   FSetUnion (FSetInter s s') s'' =
   FSetInter (FSetUnion s s'') (FSetUnion s' s'').

Lemma FSetUnion_Inter_r :
 forall s s' s'':FSet,
   mapcanon unit s ->
   mapcanon unit s' ->
   FSetUnion s (FSetInter s' s'') =
   FSetInter (FSetUnion s s') (FSetUnion s s'').

Lemma FSetInter_Union_l_c :
 forall s s' s'':FSet,
   mapcanon unit s ->
   mapcanon unit s' ->
   FSetInter (FSetUnion s s') s'' =
   FSetUnion (FSetInter s s'') (FSetInter s' s'').

Lemma FSetInter_Union_r :
 forall s s' s'':FSet,
   mapcanon unit s ->
   mapcanon unit s' ->
   FSetInter s (FSetUnion s' s'') =
   FSetUnion (FSetInter s s') (FSetInter s s'').