PADEC
Coq Library
Tools
PADEC - Coq Library

Library Padec.Tools.BoolSet

A Framework for Certified Self-Stabilization
PADEC Coq Library

Global Imports

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

Local Imports

From Padec Require Import SetoidUtil.

Open Scope signature_scope.
Set Implicit Arguments.

Bool Set

set represented by a Boolean function
+ tools on BoolSet

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 ==> leb).

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

    Global Instance leb_trans: Transitive leb.
    Global Instance leb_refl: Reflexive leb.

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

    Lemma eq_leb: forall b1 b2, b1 = b2 -> leb 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.