Library CoLoR.Util.Bool.BoolUtil

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2005-06-17
general results on booleans
equality

Lemma false_not_true : forall b, b = false <-> ~(b = true).

Lemma beq_true : forall b c, b = c <-> (b = true <-> c = true).

implication

Lemma implb1 : forall b, implb b b = true.

Lemma implb2 : forall b, implb b true = true.

conjunction

Lemma andb_elim : forall b c, b && c = true -> b = true /\ c = true.


Lemma andb_eliml : forall b c, b && c = true -> b = true.


Lemma andb_elimr : forall b c, b && c = true -> c = true.


Lemma andb_intro : forall b c, b = true -> c = true -> b && c = true.

Lemma andb_eq : forall b c, b && c = true <-> b = true /\ c = true.

Lemma andb_eq_false : forall b c, b && c = false <-> b = false \/ c = false.

negation

Definition neg (A : Type) (f : A->A->bool) x y := negb (f x y).

Lemma negb_lr : forall b c, negb b = c <-> b = negb c.

disjonction

Lemma orb_intror : forall b c, c = true -> b || c = true.

Lemma orb_introl : forall b c, c = true -> b || c = true.

Lemma orb_eq : forall b c, b || c = true <-> b = true \/ c = true.

equality

Lemma eqb_equiv : forall b b', b = b' <-> (b = true <-> b' = true).

decidability

Section dec.

  Variables (A : Type) (P : A -> Prop)
    (f : A -> bool) (f_ok : forall x, f x = true <-> P x).

  Lemma ko : forall x, f x = false <-> ~P x.

  Lemma dec : forall x, {P x}+{~P x}.

End dec.


correspondance between boolean functions and logical connectors

Section bool_ok.

  Variables (A : Type) (P Q : A->Prop) (bP bQ : A-> bool)
    (bP_ok : forall x, bP x = true <-> P x)
    (bQ_ok : forall x, bQ x = true <-> Q x).

  Lemma negb_ok : forall x, negb (bP x) = true <-> ~P x.

  Lemma andb_ok : forall x, bP x && bQ x = true <-> P x /\ Q x.

  Lemma orb_ok : forall x, bP x || bQ x = true <-> P x \/ Q x.

  Lemma implb_ok : forall x, implb (bP x) (bQ x) = true <-> (P x -> Q x).

End bool_ok.

checking a property (P i) for all i<n

Section bforall_lt.

  Variables (P : nat->Prop) (bP : nat->bool)
    (bP_ok : forall x, bP x = true <-> P x).

  Definition forall_lt n := forall i, i < n -> P i.

  Fixpoint bforall_lt_aux b n := b &&
    match n with
      | 0 => true
      | S n' => bforall_lt_aux (bP n') n'
    end.

  Lemma bforall_lt_aux_ok : forall n b,
    bforall_lt_aux b n = true <-> b = true /\ forall_lt n.

  Definition bforall_lt := bforall_lt_aux true.

  Lemma bforall_lt_ok : forall n, bforall_lt n = true <-> forall_lt n.

End bforall_lt.