Library Mapaxioms

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

Section MapAxioms.

  Variables A B C : Type.

  Lemma eqm_sym : forall f f':ad -> option A, eqm A f f' -> eqm A f' f.

  Lemma eqm_refl : forall f:ad -> option A, eqm A f f.

  Lemma eqm_trans :
   forall f f' f'':ad -> option A, eqm A f f' -> eqm A f' f'' -> eqm A f f''.

  Definition eqmap (m m':Map A) := eqm A (MapGet A m) (MapGet A m').

  Lemma eqmap_sym : forall m m':Map A, eqmap m m' -> eqmap m' m.

  Lemma eqmap_refl : forall m:Map A, eqmap m m.

  Lemma eqmap_trans :
   forall m m' m'':Map A, eqmap m m' -> eqmap m' m'' -> eqmap m m''.

  Lemma MapPut_as_Merge :
   forall (m:Map A) (a:ad) (y:A),
     eqmap (MapPut A m a y) (MapMerge A m (M1 A a y)).

  Lemma MapPut_ext :
   forall m m':Map A,
     eqmap m m' ->
     forall (a:ad) (y:A), eqmap (MapPut A m a y) (MapPut A m' a y).

  Lemma MapPut_behind_as_Merge :
   forall (m:Map A) (a:ad) (y:A),
     eqmap (MapPut_behind A m a y) (MapMerge A (M1 A a y) m).

  Lemma MapPut_behind_ext :
   forall m m':Map A,
     eqmap m m' ->
     forall (a:ad) (y:A),
       eqmap (MapPut_behind A m a y) (MapPut_behind A m' a y).

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

  Lemma MapMerge_empty_m : forall m:Map A, eqmap (MapMerge A (M0 A) m) m.

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

  Lemma MapMerge_m_empty : forall m:Map A, eqmap (MapMerge A m (M0 A)) m.

  Lemma MapMerge_empty_l :
   forall m m':Map A, eqmap (MapMerge A m m') (M0 A) -> eqmap m (M0 A).

  Lemma MapMerge_empty_r :
   forall m m':Map A, eqmap (MapMerge A m m') (M0 A) -> eqmap m' (M0 A).

  Lemma MapMerge_assoc :
   forall m m' m'':Map A,
     eqmap (MapMerge A (MapMerge A m m') m'')
       (MapMerge A m (MapMerge A m' m'')).

  Lemma MapMerge_idempotent : forall m:Map A, eqmap (MapMerge A m m) m.

  Lemma MapMerge_ext :
   forall m1 m2 m'1 m'2:Map A,
     eqmap m1 m'1 ->
     eqmap m2 m'2 -> eqmap (MapMerge A m1 m2) (MapMerge A m'1 m'2).

  Lemma MapMerge_ext_l :
   forall m1 m'1 m2:Map A,
     eqmap m1 m'1 -> eqmap (MapMerge A m1 m2) (MapMerge A m'1 m2).

  Lemma MapMerge_ext_r :
   forall m1 m2 m'2:Map A,
     eqmap m2 m'2 -> eqmap (MapMerge A m1 m2) (MapMerge A m1 m'2).

  Lemma MapMerge_RestrTo_l :
   forall m m' m'':Map A,
     eqmap (MapMerge A (MapDomRestrTo A A m m') m'')
       (MapDomRestrTo A A (MapMerge A m m'') (MapMerge A m' m'')).

  Lemma MapRemove_as_RestrBy :
   forall (m:Map A) (a:ad) (y:B),
     eqmap (MapRemove A m a) (MapDomRestrBy A B m (M1 B a y)).

  Lemma MapRemove_ext :
   forall m m':Map A,
     eqmap m m' -> forall a:ad, eqmap (MapRemove A m a) (MapRemove A m' a).

  Lemma MapDomRestrTo_empty_m_1 :
   forall m:Map B, MapDomRestrTo A B (M0 A) m = M0 A.

  Lemma MapDomRestrTo_empty_m :
   forall m:Map B, eqmap (MapDomRestrTo A B (M0 A) m) (M0 A).

  Lemma MapDomRestrTo_m_empty_1 :
   forall m:Map A, MapDomRestrTo A B m (M0 B) = M0 A.

  Lemma MapDomRestrTo_m_empty :
   forall m:Map A, eqmap (MapDomRestrTo A B m (M0 B)) (M0 A).

  Lemma MapDomRestrTo_assoc :
   forall (m:Map A) (m':Map B) (m'':Map C),
     eqmap (MapDomRestrTo A C (MapDomRestrTo A B m m') m'')
       (MapDomRestrTo A B m (MapDomRestrTo B C m' m'')).

  Lemma MapDomRestrTo_idempotent :
   forall m:Map A, eqmap (MapDomRestrTo A A m m) m.

  Lemma MapDomRestrTo_Dom :
   forall (m:Map A) (m':Map B),
     eqmap (MapDomRestrTo A B m m') (MapDomRestrTo A unit m (MapDom B m')).

  Lemma MapDomRestrBy_empty_m_1 :
   forall m:Map B, MapDomRestrBy A B (M0 A) m = M0 A.

  Lemma MapDomRestrBy_empty_m :
   forall m:Map B, eqmap (MapDomRestrBy A B (M0 A) m) (M0 A).

  Lemma MapDomRestrBy_m_empty_1 :
   forall m:Map A, MapDomRestrBy A B m (M0 B) = m.

  Lemma MapDomRestrBy_m_empty :
   forall m:Map A, eqmap (MapDomRestrBy A B m (M0 B)) m.

  Lemma MapDomRestrBy_Dom :
   forall (m:Map A) (m':Map B),
     eqmap (MapDomRestrBy A B m m') (MapDomRestrBy A unit m (MapDom B m')).

  Lemma MapDomRestrBy_m_m_1 :
   forall m:Map A, eqmap (MapDomRestrBy A A m m) (M0 A).

  Lemma MapDomRestrBy_By :
   forall (m:Map A) (m' m'':Map B),
     eqmap (MapDomRestrBy A B (MapDomRestrBy A B m m') m'')
       (MapDomRestrBy A B m (MapMerge B m' m'')).

  Lemma MapDomRestrBy_By_comm :
   forall (m:Map A) (m':Map B) (m'':Map C),
     eqmap (MapDomRestrBy A C (MapDomRestrBy A B m m') m'')
       (MapDomRestrBy A B (MapDomRestrBy A C m m'') m').

  Lemma MapDomRestrBy_To :
   forall (m:Map A) (m':Map B) (m'':Map C),
     eqmap (MapDomRestrBy A C (MapDomRestrTo A B m m') m'')
       (MapDomRestrTo A B m (MapDomRestrBy B C m' m'')).

  Lemma MapDomRestrBy_To_comm :
   forall (m:Map A) (m':Map B) (m'':Map C),
     eqmap (MapDomRestrBy A C (MapDomRestrTo A B m m') m'')
       (MapDomRestrTo A B (MapDomRestrBy A C m m'') m').

  Lemma MapDomRestrTo_By :
   forall (m:Map A) (m':Map B) (m'':Map C),
     eqmap (MapDomRestrTo A C (MapDomRestrBy A B m m') m'')
       (MapDomRestrTo A C m (MapDomRestrBy C B m'' m')).

  Lemma MapDomRestrTo_By_comm :
   forall (m:Map A) (m':Map B) (m'':Map C),
     eqmap (MapDomRestrTo A C (MapDomRestrBy A B m m') m'')
       (MapDomRestrBy A B (MapDomRestrTo A C m m'') m').

  Lemma MapDomRestrTo_To_comm :
   forall (m:Map A) (m':Map B) (m'':Map C),
     eqmap (MapDomRestrTo A C (MapDomRestrTo A B m m') m'')
       (MapDomRestrTo A B (MapDomRestrTo A C m m'') m').

  Lemma MapMerge_DomRestrTo :
   forall (m m':Map A) (m'':Map B),
     eqmap (MapDomRestrTo A B (MapMerge A m m') m'')
       (MapMerge A (MapDomRestrTo A B m m'') (MapDomRestrTo A B m' m'')).

  Lemma MapMerge_DomRestrBy :
   forall (m m':Map A) (m'':Map B),
     eqmap (MapDomRestrBy A B (MapMerge A m m') m'')
       (MapMerge A (MapDomRestrBy A B m m'') (MapDomRestrBy A B m' m'')).

  Lemma MapDelta_empty_m_1 : forall m:Map A, MapDelta A (M0 A) m = m.

  Lemma MapDelta_empty_m : forall m:Map A, eqmap (MapDelta A (M0 A) m) m.

  Lemma MapDelta_m_empty_1 : forall m:Map A, MapDelta A m (M0 A) = m.

  Lemma MapDelta_m_empty : forall m:Map A, eqmap (MapDelta A m (M0 A)) m.

  Lemma MapDelta_nilpotent : forall m:Map A, eqmap (MapDelta A m m) (M0 A).

  Lemma MapDelta_as_Merge :
   forall m m':Map A,
     eqmap (MapDelta A m m')
       (MapMerge A (MapDomRestrBy A A m m') (MapDomRestrBy A A m' m)).

  Lemma MapDelta_as_DomRestrBy :
   forall m m':Map A,
     eqmap (MapDelta A m m')
       (MapDomRestrBy A A (MapMerge A m m') (MapDomRestrTo A A m m')).

  Lemma MapDelta_as_DomRestrBy_2 :
   forall m m':Map A,
     eqmap (MapDelta A m m')
       (MapDomRestrBy A A (MapMerge A m m') (MapDomRestrTo A A m' m)).

  Lemma MapDelta_sym :
   forall m m':Map A, eqmap (MapDelta A m m') (MapDelta A m' m).

  Lemma MapDelta_ext :
   forall m1 m2 m'1 m'2:Map A,
     eqmap m1 m'1 ->
     eqmap m2 m'2 -> eqmap (MapDelta A m1 m2) (MapDelta A m'1 m'2).

  Lemma MapDelta_ext_l :
   forall m1 m'1 m2:Map A,
     eqmap m1 m'1 -> eqmap (MapDelta A m1 m2) (MapDelta A m'1 m2).

  Lemma MapDelta_ext_r :
   forall m1 m2 m'2:Map A,
     eqmap m2 m'2 -> eqmap (MapDelta A m1 m2) (MapDelta A m1 m'2).

  Lemma MapDom_Split_1 :
   forall (m:Map A) (m':Map B),
     eqmap m (MapMerge A (MapDomRestrTo A B m m') (MapDomRestrBy A B m m')).

  Lemma MapDom_Split_2 :
   forall (m:Map A) (m':Map B),
     eqmap m (MapMerge A (MapDomRestrBy A B m m') (MapDomRestrTo A B m m')).

  Lemma MapDom_Split_3 :
   forall (m:Map A) (m':Map B),
     eqmap
       (MapDomRestrTo A A (MapDomRestrTo A B m m') (MapDomRestrBy A B m m'))
       (M0 A).

End MapAxioms.

Lemma MapDomRestrTo_ext :
 forall (A B:Type) (m1:Map A) (m2:Map B) (m'1:Map A)
   (m'2:Map B),
   eqmap A m1 m'1 ->
   eqmap B m2 m'2 ->
   eqmap A (MapDomRestrTo A B m1 m2) (MapDomRestrTo A B m'1 m'2).

Lemma MapDomRestrTo_ext_l :
 forall (A B:Type) (m1:Map A) (m2:Map B) (m'1:Map A),
   eqmap A m1 m'1 ->
   eqmap A (MapDomRestrTo A B m1 m2) (MapDomRestrTo A B m'1 m2).

Lemma MapDomRestrTo_ext_r :
 forall (A B:Type) (m1:Map A) (m2 m'2:Map B),
   eqmap B m2 m'2 ->
   eqmap A (MapDomRestrTo A B m1 m2) (MapDomRestrTo A B m1 m'2).

Lemma MapDomRestrBy_ext :
 forall (A B:Type) (m1:Map A) (m2:Map B) (m'1:Map A)
   (m'2:Map B),
   eqmap A m1 m'1 ->
   eqmap B m2 m'2 ->
   eqmap A (MapDomRestrBy A B m1 m2) (MapDomRestrBy A B m'1 m'2).

Lemma MapDomRestrBy_ext_l :
 forall (A B:Type) (m1:Map A) (m2:Map B) (m'1:Map A),
   eqmap A m1 m'1 ->
   eqmap A (MapDomRestrBy A B m1 m2) (MapDomRestrBy A B m'1 m2).

Lemma MapDomRestrBy_ext_r :
 forall (A B:Type) (m1:Map A) (m2 m'2:Map B),
   eqmap B m2 m'2 ->
   eqmap A (MapDomRestrBy A B m1 m2) (MapDomRestrBy A B m1 m'2).

Lemma MapDomRestrBy_m_m :
 forall (A:Type) (m:Map A),
   eqmap A (MapDomRestrBy A unit m (MapDom A m)) (M0 A).

Lemma FSetDelta_assoc :
 forall s s' s'':FSet,
   eqmap unit (MapDelta _ (MapDelta _ s s') s'')
     (MapDelta _ s (MapDelta _ s' s'')).

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

Lemma FSetUnion_comm :
 forall s s':FSet, eqmap unit (FSetUnion s s') (FSetUnion s' s).

Lemma FSetUnion_assoc :
 forall s s' s'':FSet,
   eqmap unit (FSetUnion (FSetUnion s s') s'')
     (FSetUnion s (FSetUnion s' s'')).

Lemma FSetUnion_M0_s : forall s:FSet, eqmap unit (FSetUnion (M0 unit) s) s.

Lemma FSetUnion_s_M0 : forall s:FSet, eqmap unit (FSetUnion s (M0 unit)) s.

Lemma FSetUnion_idempotent : forall s:FSet, eqmap unit (FSetUnion s s) s.

Lemma FSetInter_comm :
 forall s s':FSet, eqmap unit (FSetInter s s') (FSetInter s' s).

Lemma FSetInter_assoc :
 forall s s' s'':FSet,
   eqmap unit (FSetInter (FSetInter s s') s'')
     (FSetInter s (FSetInter s' s'')).

Lemma FSetInter_M0_s :
 forall s:FSet, eqmap unit (FSetInter (M0 unit) s) (M0 unit).

Lemma FSetInter_s_M0 :
 forall s:FSet, eqmap unit (FSetInter s (M0 unit)) (M0 unit).

Lemma FSetInter_idempotent : forall s:FSet, eqmap unit (FSetInter s s) s.

Lemma FSetUnion_Inter_l :
 forall s s' s'':FSet,
   eqmap unit (FSetUnion (FSetInter s s') s'')
     (FSetInter (FSetUnion s s'') (FSetUnion s' s'')).

Lemma FSetUnion_Inter_r :
 forall s s' s'':FSet,
   eqmap unit (FSetUnion s (FSetInter s' s''))
     (FSetInter (FSetUnion s s') (FSetUnion s s'')).

Lemma FSetInter_Union_l :
 forall s s' s'':FSet,
   eqmap unit (FSetInter (FSetUnion s s') s'')
     (FSetUnion (FSetInter s s'') (FSetInter s' s'')).

Lemma FSetInter_Union_r :
 forall s s' s'':FSet,
   eqmap unit (FSetInter s (FSetUnion s' s''))
     (FSetUnion (FSetInter s s') (FSetInter s s'')).