Library Mapcard

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 Mapsubset.
Require Import List.
Require Import Lsort.
Require Import Peano_dec.

Section MapCard.

  Variables A B : Type.

  Lemma MapCard_M0 : MapCard A (M0 A) = 0.

  Lemma MapCard_M1 : forall (a:ad) (y:A), MapCard A (M1 A a y) = 1.

  Lemma MapCard_is_O :
   forall m:Map A, MapCard A m = 0 -> forall a:ad, MapGet A m a = None.

  Lemma MapCard_is_not_O :
   forall (m:Map A) (a:ad) (y:A),
     MapGet A m a = Some y -> {n : nat | MapCard A m = S n}.

  Lemma MapCard_is_one :
   forall m:Map A,
     MapCard A m = 1 -> {a : ad & {y : A | MapGet A m a = Some y}}.

  Lemma MapCard_is_one_unique :
   forall m:Map A,
     MapCard A m = 1 ->
     forall (a a':ad) (y y':A),
       MapGet A m a = Some y ->
       MapGet A m a' = Some y' -> a = a' /\ y = y'.

  Lemma length_as_fold :
   forall (C:Type) (l:list C),
     length l = fold_right (fun (_:C) (n:nat) => S n) 0 l.

  Lemma length_as_fold_2 :
   forall l:alist A,
     length l =
     fold_right (fun (r:ad * A) (n:nat) => let (a, y) := r in 1 + n) 0 l.

  Lemma MapCard_as_Fold_1 :
   forall (m:Map A) (pf:ad -> ad),
     MapCard A m = MapFold1 A nat 0 plus (fun (_:ad) (_:A) => 1) pf m.

  Lemma MapCard_as_Fold :
   forall m:Map A,
     MapCard A m = MapFold A nat 0 plus (fun (_:ad) (_:A) => 1) m.

  Lemma MapCard_as_length :
   forall m:Map A, MapCard A m = length (alist_of_Map A m).

  Lemma MapCard_Put1_equals_2 :
   forall (p:positive) (a a':ad) (y y':A),
     MapCard A (MapPut1 A a y a' y' p) = 2.

  Lemma MapCard_Put_sum :
   forall (m m':Map A) (a:ad) (y:A) (n n':nat),
     m' = MapPut A m a y ->
     n = MapCard A m -> n' = MapCard A m' -> {n' = n} + {n' = S n}.

  Lemma MapCard_Put_lb :
   forall (m:Map A) (a:ad) (y:A), MapCard A (MapPut A m a y) >= MapCard A m.

  Lemma MapCard_Put_ub :
   forall (m:Map A) (a:ad) (y:A),
     MapCard A (MapPut A m a y) <= S (MapCard A m).

  Lemma MapCard_Put_1 :
   forall (m:Map A) (a:ad) (y:A),
     MapCard A (MapPut A m a y) = MapCard A m ->
     {y : A | MapGet A m a = Some y}.

  Lemma MapCard_Put_2 :
   forall (m:Map A) (a:ad) (y:A),
     MapCard A (MapPut A m a y) = S (MapCard A m) -> MapGet A m a = None.

  Lemma MapCard_Put_1_conv :
   forall (m:Map A) (a:ad) (y y':A),
     MapGet A m a = Some y -> MapCard A (MapPut A m a y') = MapCard A m.

  Lemma MapCard_Put_2_conv :
   forall (m:Map A) (a:ad) (y:A),
     MapGet A m a = None -> MapCard A (MapPut A m a y) = S (MapCard A m).

  Lemma MapCard_ext :
   forall m m':Map A,
     eqm A (MapGet A m) (MapGet A m') -> MapCard A m = MapCard A m'.

  Lemma MapCard_Dom : forall m:Map A, MapCard A m = MapCard unit (MapDom A m).

  Lemma MapCard_Dom_Put_behind :
   forall (m:Map A) (a:ad) (y:A),
     MapDom A (MapPut_behind A m a y) = MapDom A (MapPut A m a y).

  Lemma MapCard_Put_behind_Put :
   forall (m:Map A) (a:ad) (y:A),
     MapCard A (MapPut_behind A m a y) = MapCard A (MapPut A m a y).

  Lemma MapCard_Put_behind_sum :
   forall (m m':Map A) (a:ad) (y:A) (n n':nat),
     m' = MapPut_behind A m a y ->
     n = MapCard A m -> n' = MapCard A m' -> {n' = n} + {n' = S n}.

  Lemma MapCard_makeM2 :
   forall m m':Map A, MapCard A (makeM2 A m m') = MapCard A m + MapCard A m'.

  Lemma MapCard_Remove_sum :
   forall (m m':Map A) (a:ad) (n n':nat),
     m' = MapRemove A m a ->
     n = MapCard A m -> n' = MapCard A m' -> {n = n'} + {n = S n'}.

  Lemma MapCard_Remove_ub :
   forall (m:Map A) (a:ad), MapCard A (MapRemove A m a) <= MapCard A m.

  Lemma MapCard_Remove_lb :
   forall (m:Map A) (a:ad), S (MapCard A (MapRemove A m a)) >= MapCard A m.

  Lemma MapCard_Remove_1 :
   forall (m:Map A) (a:ad),
     MapCard A (MapRemove A m a) = MapCard A m -> MapGet A m a = None.

  Lemma MapCard_Remove_2 :
   forall (m:Map A) (a:ad),
     S (MapCard A (MapRemove A m a)) = MapCard A m ->
     {y : A | MapGet A m a = Some y}.

  Lemma MapCard_Remove_1_conv :
   forall (m:Map A) (a:ad),
     MapGet A m a = None -> MapCard A (MapRemove A m a) = MapCard A m.

  Lemma MapCard_Remove_2_conv :
   forall (m:Map A) (a:ad) (y:A),
     MapGet A m a = Some y -> S (MapCard A (MapRemove A m a)) = MapCard A m.

  Lemma MapMerge_Restr_Card :
   forall m m':Map A,
     MapCard A m + MapCard A m' =
     MapCard A (MapMerge A m m') + MapCard A (MapDomRestrTo A A m m').

  Lemma MapMerge_disjoint_Card :
   forall m m':Map A,
     MapDisjoint A A m m' ->
     MapCard A (MapMerge A m m') = MapCard A m + MapCard A m'.

  Lemma MapSplit_Card :
   forall (m:Map A) (m':Map B),
     MapCard A m =
     MapCard A (MapDomRestrTo A B m m') + MapCard A (MapDomRestrBy A B m m').

  Lemma MapMerge_Card_ub :
   forall m m':Map A,
     MapCard A (MapMerge A m m') <= MapCard A m + MapCard A m'.

  Lemma MapDomRestrTo_Card_ub_l :
   forall (m:Map A) (m':Map B),
     MapCard A (MapDomRestrTo A B m m') <= MapCard A m.

  Lemma MapDomRestrBy_Card_ub_l :
   forall (m:Map A) (m':Map B),
     MapCard A (MapDomRestrBy A B m m') <= MapCard A m.

  Lemma MapMerge_Card_disjoint :
   forall m m':Map A,
     MapCard A (MapMerge A m m') = MapCard A m + MapCard A m' ->
     MapDisjoint A A m m'.

  Lemma MapCard_is_Sn :
   forall (m:Map A) (n:nat),
     MapCard _ m = S n -> {a : ad | in_dom _ a m = true}.

End MapCard.

Section MapCard2.

  Variables A B : Type.

  Lemma MapSubset_card_eq_1 :
   forall (n:nat) (m:Map A) (m':Map B),
     MapSubset _ _ m m' ->
     MapCard _ m = n -> MapCard _ m' = n -> MapSubset _ _ m' m.

  Lemma MapDomRestrTo_Card_ub_r :
   forall (m:Map A) (m':Map B),
     MapCard A (MapDomRestrTo A B m m') <= MapCard B m'.

End MapCard2.

Section MapCard3.

  Variables A B : Type.

  Lemma MapMerge_Card_lb_l :
   forall m m':Map A, MapCard A (MapMerge A m m') >= MapCard A m.

  Lemma MapMerge_Card_lb_r :
   forall m m':Map A, MapCard A (MapMerge A m m') >= MapCard A m'.

  Lemma MapDomRestrBy_Card_lb :
   forall (m:Map A) (m':Map B),
     MapCard B m' + MapCard A (MapDomRestrBy A B m m') >= MapCard A m.

  Lemma MapSubset_Card_le :
   forall (m:Map A) (m':Map B),
     MapSubset A B m m' -> MapCard A m <= MapCard B m'.

  Lemma MapSubset_card_eq :
   forall (m:Map A) (m':Map B),
     MapSubset _ _ m m' ->
     MapCard _ m' <= MapCard _ m -> eqmap _ (MapDom _ m) (MapDom _ m').

End MapCard3.