Library Mapsubset

Require Import Bool.
Require Import Sumbool.
Require Import Arith.
Require Import NArith.
Require Import Ndigits.
Require Import Ndec.
Require Import Map.
Require Import Fset.
Require Import Mapaxioms.
Require Import Mapiter.

Section MapSubsetDef.

  Variables A B : Type.

  Definition MapSubset (m:Map A) (m':Map B) :=
    forall a:ad, in_dom A a m = true -> in_dom B a m' = true.

  Definition MapSubset_1 (m:Map A) (m':Map B) :=
    match MapSweep A (fun (a:ad) (_:A) => negb (in_dom B a m')) m with
    | None => true
    | _ => false
    end.

  Definition MapSubset_2 (m:Map A) (m':Map B) :=
    eqmap A (MapDomRestrBy A B m m') (M0 A).

  Lemma MapSubset_imp_1 :
   forall (m:Map A) (m':Map B), MapSubset m m' -> MapSubset_1 m m' = true.

  Lemma MapSubset_1_imp :
   forall (m:Map A) (m':Map B), MapSubset_1 m m' = true -> MapSubset m m'.

  Lemma map_dom_empty_1 :
   forall m:Map A, eqmap A m (M0 A) -> forall a:ad, in_dom _ a m = false.

  Lemma map_dom_empty_2 :
   forall m:Map A, (forall a:ad, in_dom _ a m = false) -> eqmap A m (M0 A).

  Lemma MapSubset_imp_2 :
   forall (m:Map A) (m':Map B), MapSubset m m' -> MapSubset_2 m m'.

  Lemma MapSubset_2_imp :
   forall (m:Map A) (m':Map B), MapSubset_2 m m' -> MapSubset m m'.

End MapSubsetDef.

Section MapSubsetOrder.

  Variables A B C : Type.

  Lemma MapSubset_refl : forall m:Map A, MapSubset A A m m.

  Lemma MapSubset_antisym :
   forall (m:Map A) (m':Map B),
     MapSubset A B m m' ->
     MapSubset B A m' m -> eqmap unit (MapDom A m) (MapDom B m').

  Lemma MapSubset_trans :
   forall (m:Map A) (m':Map B) (m'':Map C),
     MapSubset A B m m' -> MapSubset B C m' m'' -> MapSubset A C m m''.

End MapSubsetOrder.

Section FSubsetOrder.

  Lemma FSubset_refl : forall s:FSet, MapSubset _ _ s s.

  Lemma FSubset_antisym :
   forall s s':FSet,
     MapSubset _ _ s s' -> MapSubset _ _ s' s -> eqmap unit s s'.

  Lemma FSubset_trans :
   forall s s' s'':FSet,
     MapSubset _ _ s s' -> MapSubset _ _ s' s'' -> MapSubset _ _ s s''.

End FSubsetOrder.

Section MapSubsetExtra.

  Variables A B : Type.

  Lemma MapSubset_Dom_1 :
   forall (m:Map A) (m':Map B),
     MapSubset A B m m' -> MapSubset unit unit (MapDom A m) (MapDom B m').

  Lemma MapSubset_Dom_2 :
   forall (m:Map A) (m':Map B),
     MapSubset unit unit (MapDom A m) (MapDom B m') -> MapSubset A B m m'.

  Lemma MapSubset_1_Dom :
   forall (m:Map A) (m':Map B),
     MapSubset_1 A B m m' = MapSubset_1 unit unit (MapDom A m) (MapDom B m').

  Lemma MapSubset_Put :
   forall (m:Map A) (a:ad) (y:A), MapSubset A A m (MapPut A m a y).

  Lemma MapSubset_Put_mono :
   forall (m:Map A) (m':Map B) (a:ad) (y:A) (y':B),
     MapSubset A B m m' -> MapSubset A B (MapPut A m a y) (MapPut B m' a y').

  Lemma MapSubset_Put_behind :
   forall (m:Map A) (a:ad) (y:A), MapSubset A A m (MapPut_behind A m a y).

  Lemma MapSubset_Put_behind_mono :
   forall (m:Map A) (m':Map B) (a:ad) (y:A) (y':B),
     MapSubset A B m m' ->
     MapSubset A B (MapPut_behind A m a y) (MapPut_behind B m' a y').

  Lemma MapSubset_Remove :
   forall (m:Map A) (a:ad), MapSubset A A (MapRemove A m a) m.

  Lemma MapSubset_Remove_mono :
   forall (m:Map A) (m':Map B) (a:ad),
     MapSubset A B m m' -> MapSubset A B (MapRemove A m a) (MapRemove B m' a).

  Lemma MapSubset_Merge_l :
   forall m m':Map A, MapSubset A A m (MapMerge A m m').

  Lemma MapSubset_Merge_r :
   forall m m':Map A, MapSubset A A m' (MapMerge A m m').

  Lemma MapSubset_Merge_mono :
   forall (m m':Map A) (m'' m''':Map B),
     MapSubset A B m m'' ->
     MapSubset A B m' m''' ->
     MapSubset A B (MapMerge A m m') (MapMerge B m'' m''').

  Lemma MapSubset_DomRestrTo_l :
   forall (m:Map A) (m':Map B), MapSubset A A (MapDomRestrTo A B m m') m.

  Lemma MapSubset_DomRestrTo_r :
   forall (m:Map A) (m':Map B), MapSubset A B (MapDomRestrTo A B m m') m'.

  Lemma MapSubset_ext :
   forall (m0 m1:Map A) (m2 m3:Map B),
     eqmap A m0 m1 ->
     eqmap B m2 m3 -> MapSubset A B m0 m2 -> MapSubset A B m1 m3.

  Variables C D : Type.

  Lemma MapSubset_DomRestrTo_mono :
   forall (m:Map A) (m':Map B) (m'':Map C) (m''':Map D),
     MapSubset _ _ m m'' ->
     MapSubset _ _ m' m''' ->
     MapSubset _ _ (MapDomRestrTo _ _ m m') (MapDomRestrTo _ _ m'' m''').

  Lemma MapSubset_DomRestrBy_l :
   forall (m:Map A) (m':Map B), MapSubset A A (MapDomRestrBy A B m m') m.

  Lemma MapSubset_DomRestrBy_mono :
   forall (m:Map A) (m':Map B) (m'':Map C) (m''':Map D),
     MapSubset _ _ m m'' ->
     MapSubset _ _ m''' m' ->
     MapSubset _ _ (MapDomRestrBy _ _ m m') (MapDomRestrBy _ _ m'' m''').

End MapSubsetExtra.

Section MapDisjointDef.

  Variables A B : Type.

  Definition MapDisjoint (m:Map A) (m':Map B) :=
    forall a:ad, in_dom A a m = true -> in_dom B a m' = true -> False.

  Definition MapDisjoint_1 (m:Map A) (m':Map B) :=
    match MapSweep A (fun (a:ad) (_:A) => in_dom B a m') m with
    | None => true
    | _ => false
    end.

  Definition MapDisjoint_2 (m:Map A) (m':Map B) :=
    eqmap A (MapDomRestrTo A B m m') (M0 A).

  Lemma MapDisjoint_imp_1 :
   forall (m:Map A) (m':Map B), MapDisjoint m m' -> MapDisjoint_1 m m' = true.

  Lemma MapDisjoint_1_imp :
   forall (m:Map A) (m':Map B), MapDisjoint_1 m m' = true -> MapDisjoint m m'.

  Lemma MapDisjoint_imp_2 :
   forall (m:Map A) (m':Map B), MapDisjoint m m' -> MapDisjoint_2 m m'.

  Lemma MapDisjoint_2_imp :
   forall (m:Map A) (m':Map B), MapDisjoint_2 m m' -> MapDisjoint m m'.

  Lemma Map_M0_disjoint : forall m:Map B, MapDisjoint (M0 A) m.

  Lemma Map_disjoint_M0 : forall m:Map A, MapDisjoint m (M0 B).

End MapDisjointDef.

Section MapDisjointExtra.

  Variables A B : Type.

  Lemma MapDisjoint_ext :
   forall (m0 m1:Map A) (m2 m3:Map B),
     eqmap A m0 m1 ->
     eqmap B m2 m3 -> MapDisjoint A B m0 m2 -> MapDisjoint A B m1 m3.

  Lemma MapMerge_disjoint :
   forall m m':Map A,
     MapDisjoint A A m m' ->
     forall a:ad,
       in_dom A a (MapMerge A m m') =
       orb (andb (in_dom A a m) (negb (in_dom A a m')))
         (andb (in_dom A a m') (negb (in_dom A a m))).

  Lemma MapDisjoint_M2_l :
   forall (m0 m1:Map A) (m2 m3:Map B),
     MapDisjoint A B (M2 A m0 m1) (M2 B m2 m3) -> MapDisjoint A B m0 m2.

  Lemma MapDisjoint_M2_r :
   forall (m0 m1:Map A) (m2 m3:Map B),
     MapDisjoint A B (M2 A m0 m1) (M2 B m2 m3) -> MapDisjoint A B m1 m3.

  Lemma MapDisjoint_M2 :
   forall (m0 m1:Map A) (m2 m3:Map B),
     MapDisjoint A B m0 m2 ->
     MapDisjoint A B m1 m3 -> MapDisjoint A B (M2 A m0 m1) (M2 B m2 m3).

  Lemma MapDisjoint_M1_l :
   forall (m:Map A) (a:ad) (y:B),
     MapDisjoint B A (M1 B a y) m -> in_dom A a m = false.

  Lemma MapDisjoint_M1_r :
   forall (m:Map A) (a:ad) (y:B),
     MapDisjoint A B m (M1 B a y) -> in_dom A a m = false.

  Lemma MapDisjoint_M1_conv_l :
   forall (m:Map A) (a:ad) (y:B),
     in_dom A a m = false -> MapDisjoint B A (M1 B a y) m.

  Lemma MapDisjoint_M1_conv_r :
   forall (m:Map A) (a:ad) (y:B),
     in_dom A a m = false -> MapDisjoint A B m (M1 B a y).

  Lemma MapDisjoint_sym :
   forall (m:Map A) (m':Map B), MapDisjoint A B m m' -> MapDisjoint B A m' m.

  Lemma MapDisjoint_empty :
   forall m:Map A, MapDisjoint A A m m -> eqmap A m (M0 A).

  Lemma MapDelta_disjoint :
   forall m m':Map A,
     MapDisjoint A A m m' -> eqmap A (MapDelta A m m') (MapMerge A m m').

  Variable C : Type.

  Lemma MapDomRestr_disjoint :
   forall (m:Map A) (m':Map B) (m'':Map C),
     MapDisjoint A B (MapDomRestrTo A C m m'') (MapDomRestrBy B C m' m'').

  Lemma MapDelta_RestrTo_disjoint :
   forall m m':Map A,
     MapDisjoint A A (MapDelta A m m') (MapDomRestrTo A A m m').

  Lemma MapDelta_RestrTo_disjoint_2 :
   forall m m':Map A,
     MapDisjoint A A (MapDelta A m m') (MapDomRestrTo A A m' m).

  Variable D : Type.

  Lemma MapSubset_Disjoint :
   forall (m:Map A) (m':Map B) (m'':Map C) (m''':Map D),
     MapSubset _ _ m m' ->
     MapSubset _ _ m'' m''' ->
     MapDisjoint _ _ m' m''' -> MapDisjoint _ _ m m''.

  Lemma MapSubset_Disjoint_l :
   forall (m:Map A) (m':Map B) (m'':Map C),
     MapSubset _ _ m m' -> MapDisjoint _ _ m' m'' -> MapDisjoint _ _ m m''.

  Lemma MapSubset_Disjoint_r :
   forall (m:Map A) (m'':Map C) (m''':Map D),
     MapSubset _ _ m'' m''' ->
     MapDisjoint _ _ m m''' -> MapDisjoint _ _ m m''.

End MapDisjointExtra.