Library Fset

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

Section Dom.

  Variables A B : Type.

  Fixpoint MapDomRestrTo (m:Map A) : Map B -> Map A :=
    match m with
    | M0 _ => fun _:Map B => M0 A
    | M1 _ a y =>
        fun m':Map B => match MapGet B m' a with
                        | None => M0 A
                        | _ => m
                        end
    | M2 _ m1 m2 =>
        fun m':Map B =>
          match m' with
          | M0 _ => M0 A
          | M1 _ a' y' =>
              match MapGet A m a' with
              | None => M0 A
              | Some y => M1 A a' y
              end
          | M2 _ m'1 m'2 =>
              makeM2 A (MapDomRestrTo m1 m'1) (MapDomRestrTo m2 m'2)
          end
    end.

  Lemma MapDomRestrTo_semantics :
   forall (m:Map A) (m':Map B),
     eqm A (MapGet A (MapDomRestrTo m m'))
       (fun a0:ad =>
          match MapGet B m' a0 with
          | None => None
          | _ => MapGet A m a0
          end).

  Fixpoint MapDomRestrBy (m:Map A) : Map B -> Map A :=
    match m with
    | M0 _ => fun _:Map B => M0 A
    | M1 _ a y =>
        fun m':Map B => match MapGet B m' a with
                        | None => m
                        | _ => M0 A
                        end
    | M2 _ m1 m2 =>
        fun m':Map B =>
          match m' with
          | M0 _ => m
          | M1 _ a' y' => MapRemove A m a'
          | M2 _ m'1 m'2 =>
              makeM2 A (MapDomRestrBy m1 m'1) (MapDomRestrBy m2 m'2)
          end
    end.

  Lemma MapDomRestrBy_semantics :
   forall (m:Map A) (m':Map B),
     eqm A (MapGet A (MapDomRestrBy m m'))
       (fun a0:ad =>
          match MapGet B m' a0 with
          | None => MapGet A m a0
          | _ => None
          end).

  Definition in_dom (a:ad) (m:Map A) :=
    match MapGet A m a with
    | None => false
    | _ => true
    end.

  Lemma in_dom_M0 : forall a:ad, in_dom a (M0 A) = false.

  Lemma in_dom_M1 : forall (a a0:ad) (y:A), in_dom a0 (M1 A a y) = Neqb a a0.

  Lemma in_dom_M1_1 : forall (a:ad) (y:A), in_dom a (M1 A a y) = true.

  Lemma in_dom_M1_2 :
   forall (a a0:ad) (y:A), in_dom a0 (M1 A a y) = true -> a = a0.

  Lemma in_dom_some :
   forall (m:Map A) (a:ad),
     in_dom a m = true -> {y : A | MapGet A m a = Some y}.

  Lemma in_dom_none :
   forall (m:Map A) (a:ad), in_dom a m = false -> MapGet A m a = None.

  Lemma in_dom_put :
   forall (m:Map A) (a0:ad) (y0:A) (a:ad),
     in_dom a (MapPut A m a0 y0) = orb (Neqb a a0) (in_dom a m).

  Lemma in_dom_put_behind :
   forall (m:Map A) (a0:ad) (y0:A) (a:ad),
     in_dom a (MapPut_behind A m a0 y0) = orb (Neqb a a0) (in_dom a m).

  Lemma in_dom_remove :
   forall (m:Map A) (a0 a:ad),
     in_dom a (MapRemove A m a0) = andb (negb (Neqb a a0)) (in_dom a m).

  Lemma in_dom_merge :
   forall (m m':Map A) (a:ad),
     in_dom a (MapMerge A m m') = orb (in_dom a m) (in_dom a m').

  Lemma in_dom_delta :
   forall (m m':Map A) (a:ad),
     in_dom a (MapDelta A m m') = xorb (in_dom a m) (in_dom a m').

End Dom.

Section InDom.

  Variables A B : Type.

  Lemma in_dom_restrto :
   forall (m:Map A) (m':Map B) (a:ad),
     in_dom A a (MapDomRestrTo A B m m') =
     andb (in_dom A a m) (in_dom B a m').

  Lemma in_dom_restrby :
   forall (m:Map A) (m':Map B) (a:ad),
     in_dom A a (MapDomRestrBy A B m m') =
     andb (in_dom A a m) (negb (in_dom B a m')).

End InDom.

Definition FSet := Map unit.

Section FSetDefs.

  Variable A : Type.

  Definition in_FSet : ad -> FSet -> bool := in_dom unit.

  Fixpoint MapDom (m:Map A) : FSet :=
    match m with
    | M0 _ => M0 unit
    | M1 _ a _ => M1 unit a tt
    | M2 _ m m' => M2 unit (MapDom m) (MapDom m')
    end.

  Lemma MapDom_semantics_1 :
   forall (m:Map A) (a:ad) (y:A),
     MapGet A m a = Some y -> in_FSet a (MapDom m) = true.

  Lemma MapDom_semantics_2 :
   forall (m:Map A) (a:ad),
     in_FSet a (MapDom m) = true -> {y : A | MapGet A m a = Some y}.

  Lemma MapDom_semantics_3 :
   forall (m:Map A) (a:ad),
     MapGet A m a = None -> in_FSet a (MapDom m) = false.

  Lemma MapDom_semantics_4 :
   forall (m:Map A) (a:ad),
     in_FSet a (MapDom m) = false -> MapGet A m a = None.

  Lemma MapDom_Dom :
   forall (m:Map A) (a:ad), in_dom A a m = in_FSet a (MapDom m).

  Definition FSetUnion (s s':FSet) : FSet := MapMerge unit s s'.

  Lemma in_FSet_union :
   forall (s s':FSet) (a:ad),
     in_FSet a (FSetUnion s s') = orb (in_FSet a s) (in_FSet a s').

  Definition FSetInter (s s':FSet) : FSet := MapDomRestrTo unit unit s s'.

  Lemma in_FSet_inter :
   forall (s s':FSet) (a:ad),
     in_FSet a (FSetInter s s') = andb (in_FSet a s) (in_FSet a s').

  Definition FSetDiff (s s':FSet) : FSet := MapDomRestrBy unit unit s s'.

  Lemma in_FSet_diff :
   forall (s s':FSet) (a:ad),
     in_FSet a (FSetDiff s s') = andb (in_FSet a s) (negb (in_FSet a s')).

  Definition FSetDelta (s s':FSet) : FSet := MapDelta unit s s'.

  Lemma in_FSet_delta :
   forall (s s':FSet) (a:ad),
     in_FSet a (FSetDelta s s') = xorb (in_FSet a s) (in_FSet a s').

End FSetDefs.

Lemma FSet_Dom : forall s:FSet, MapDom unit s = s.