From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import Bool.

From Padec Require Import SetoidUtil.

Open Scope signature_scope.
Set Implicit Arguments.

Section BoolSet.

  Context {A: Type}.

  Definition BoolSet: Type := A -> bool.

  Definition empty_BoolSet: BoolSet := (fun _ => false).
  Definition full_BoolSet: BoolSet := (fun _ => true).

  Definition andBoolSet: BoolSet -> BoolSet -> BoolSet :=
    (fun s s' => (fun a => andb (s a) (s' a))).

  Definition orBoolSet: BoolSet -> BoolSet -> BoolSet :=
    (fun s s' => (fun a => orb (s a) (s' a))).

  Definition negBoolSet: BoolSet -> BoolSet :=
    (fun s => (fun a => negb (s a))).

  Definition diffBoolSet: BoolSet -> BoolSet -> BoolSet :=
    (fun s s' => andBoolSet s (negBoolSet s')).

  Section with_eqA.

    Context {eqA: relation A}.

    Definition eqBoolSet := (eqA ==> @eq bool).
    Definition leBoolSet := (eqA ==> Bool.le).

    Global Instance eqBoolSet_per `{PER _ eqA}: PER eqBoolSet.

    Global Instance eqBoolSet_compat `{PER _ eqA}: Proper (eqBoolSet ==> eqBoolSet ==> equiv) eqBoolSet.

    Global Instance leb_trans: Transitive Bool.le.

    Global Instance leb_refl: Reflexive Bool.le.

    Global Instance leBoolSet_trans `{PER _ eqA}: Transitive leBoolSet.

    Lemma eq_leb: forall b1 b2, b1 = b2 -> Bool.le b1 b2.

    Lemma eqBoolSet_leBoolSet: forall U1 U2, eqBoolSet U1 U2 -> leBoolSet U1 U2.

    Global Instance full_BoolSet_compat: Proper (eqBoolSet) full_BoolSet.

    Global Instance full_BoolSet_le_compat: Proper (leBoolSet) full_BoolSet.

    Global Instance empty_BoolSet_compat: Proper (eqBoolSet) empty_BoolSet.

    Global Instance empty_BoolSet_le_compat: Proper (leBoolSet) empty_BoolSet.

    Global Instance andBoolSet_compat:
      Proper (eqBoolSet ==> eqBoolSet ==> eqBoolSet) andBoolSet.

    Global Instance andBoolSet_le_compat:
      Proper (leBoolSet ==> leBoolSet ==> leBoolSet) andBoolSet.

    Global Instance orBoolSet_compat:
      Proper (eqBoolSet ==> eqBoolSet ==> eqBoolSet) orBoolSet.

    Global Instance orBoolSet_le_compat:
      Proper (leBoolSet ==> leBoolSet ==> leBoolSet) orBoolSet.

    Global Instance negBoolSet_compat:
      Proper (eqBoolSet ==> eqBoolSet) negBoolSet.

    Global Instance negBoolSet_le_compat `{Symmetric _ eqA}:
      Proper (flip leBoolSet ==> leBoolSet) negBoolSet.

    Global Instance diffBoolSet_compat:
      Proper (eqBoolSet ==> eqBoolSet ==> eqBoolSet) diffBoolSet.

    Global Instance diffBoolSet_le_compat `{Symmetric _ eqA}:
      Proper (leBoolSet ==> flip leBoolSet ==> leBoolSet) diffBoolSet.

    Section Tools.

      Lemma le_BoolSet_impl:
        forall s s', leBoolSet s s' ->
                     forall a a', eqA a a' ->
                                  s a = true -> s' a' = true.

      Lemma eq_le_iff:
        Symmetric eqA ->
        forall s s', eqBoolSet s s' <-> leBoolSet s s' /\ leBoolSet s' s.

      Lemma neg_neg:
        forall s, Proper eqBoolSet s -> eqBoolSet (negBoolSet (negBoolSet s)) s.

      Lemma and_le: forall s s',
          Proper eqBoolSet s -> leBoolSet (andBoolSet s s') s.

      Lemma le_or:
        forall s s', Proper eqBoolSet s -> leBoolSet s (orBoolSet s s').

      Lemma diff_le:
        forall s s', Proper eqBoolSet s -> leBoolSet (diffBoolSet s s') s.

      Lemma diff_empty_le:
        forall s s', Proper eqBoolSet s' -> eqBoolSet (diffBoolSet s s') empty_BoolSet -> leBoolSet s s'.

      Lemma negb_empty:
        eqBoolSet full_BoolSet (negBoolSet empty_BoolSet).

      Lemma negb_full:
        eqBoolSet empty_BoolSet (negBoolSet full_BoolSet).

      Lemma empty_and:
        forall s, eqBoolSet (andBoolSet s empty_BoolSet) empty_BoolSet.

      Lemma empty_or:
        forall s, Proper eqBoolSet s -> eqBoolSet (orBoolSet s empty_BoolSet) s.

      Lemma empty_diff:
        forall s, eqBoolSet (diffBoolSet empty_BoolSet s) empty_BoolSet.

      Lemma diff_empty:
        forall s, Proper eqBoolSet s ->
                  eqBoolSet (diffBoolSet s empty_BoolSet) s.

      Lemma full_and:
        forall s, Proper eqBoolSet s -> eqBoolSet (andBoolSet s full_BoolSet) s.

      Lemma full_or:
        forall s, eqBoolSet (orBoolSet s full_BoolSet) full_BoolSet.

      Lemma diff_full:
        forall s, eqBoolSet (diffBoolSet s full_BoolSet) empty_BoolSet.

      Lemma idem_and:
        Symmetric eqA -> Reflexive eqA ->
        forall s s', eqBoolSet s s' -> eqBoolSet (andBoolSet s s') s.

      Lemma idem_or:
        Symmetric eqA -> Reflexive eqA ->
        forall s s', eqBoolSet s s' -> eqBoolSet (orBoolSet s s') s.

      Lemma idem_diff:
        Reflexive eqA ->
        forall s s', eqBoolSet s s' ->
                     eqBoolSet (diffBoolSet s s') empty_BoolSet.

    End Tools.

    Section with_Finite_Set.

      Lemma epsilon_BoolSet:
        forall (lA: list A),
          (forall a, InA eqA a lA) ->
          forall BS: BoolSet, Proper (eqBoolSet) BS ->
                              ~ eqBoolSet BS (fun _ => false) ->
                              { a: A | BS a = true }.

      Lemma eqBoolSet_dec:
        Reflexive eqA ->
        forall (lA: list A), (forall a, InA eqA a lA) ->
                             forall BS1 BS2,
                               Proper eqBoolSet BS1 -> Proper eqBoolSet BS2 ->
                               { eqBoolSet BS1 BS2 } + { ~eqBoolSet BS1 BS2 }.

      Definition EMPTY (lA: list A) (BS: BoolSet): bool :=
        (forallb (fun a => negb (BS a)) lA).

      Lemma EMPTY_empty:
        Reflexive eqA ->
        forall (lA: list A),
          (forall a, InA eqA a lA) ->
          forall BS, Proper eqBoolSet BS ->
                     EMPTY lA BS = true <-> eqBoolSet BS empty_BoolSet.

      Lemma epsilon_BoolSet_:
        Reflexive eqA ->
        forall (lA: list A),
          (forall a, InA eqA a lA) ->
          forall BS: BoolSet, Proper (eqBoolSet) BS ->
                              EMPTY lA BS = false ->
                              { a: A | BS a = true }.

    End with_Finite_Set.

  End with_eqA.

  Global Instance BoolSet_PartialSetoid `{PartialSetoid A}:
    PartialSetoid BoolSet :=
    @Build_PartialSetoid _ (pequiv ==> @eq bool) _.

End BoolSet.

Close Scope signature_scope.
Unset Implicit Arguments.