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.