Library Coq.Bool.Bool
The type
bool is defined in the prelude as
Inductive bool : Set := true : bool | false : bool
Most of the lemmas in this file are trivial by case analysis
Ltac destr_bool :=
intros; destruct_all bool; simpl in *; trivial; try discriminate.
Interpretation of booleans as propositions
Definition eqb (
b1 b2:
bool) :
bool :=
match b1,
b2 with
|
true,
true =>
true
|
true,
false =>
false
|
false,
true =>
false
|
false,
false =>
true
end.
Lemma eqb_subst :
forall (
P:
bool -> Prop) (
b1 b2:
bool),
eqb b1 b2 = true -> P b1 -> P b2.
Lemma eqb_reflx :
forall b:
bool,
eqb b b = true.
Lemma eqb_prop :
forall a b:
bool,
eqb a b = true -> a = b.
Lemma eqb_true_iff :
forall a b:
bool,
eqb a b = true <-> a = b.
Lemma eqb_false_iff :
forall a b:
bool,
eqb a b = false <-> a <> b.
true is a zero for orb
false is neutral for orb
Complementation
Commutativity
Associativity
false is a zero for andb
true is neutral for andb
Complementation
Commutativity
Associativity
Properties mixing andb and orb
Distributivity
Absorption
Lemma implb_true_iff :
forall b1 b2:
bool,
implb b1 b2 = true <-> (b1 = true -> b2 = true).
Lemma implb_false_iff :
forall b1 b2:
bool,
implb b1 b2 = false <-> (b1 = true /\ b2 = false).
Lemma implb_orb :
forall b1 b2:
bool,
implb b1 b2 = negb b1 || b2.
Lemma implb_negb_orb :
forall b1 b2:
bool,
implb (
negb b1)
b2 = b1 || b2.
Lemma implb_true_r :
forall b:
bool,
implb b true = true.
Lemma implb_false_r :
forall b:
bool,
implb b false = negb b.
Lemma implb_true_l :
forall b:
bool,
implb true b = b.
Lemma implb_false_l :
forall b:
bool,
implb false b = true.
Lemma implb_same :
forall b:
bool,
implb b b = true.
Lemma implb_contrapositive :
forall b1 b2:
bool,
implb (
negb b1) (
negb b2)
= implb b2 b1.
Lemma implb_negb :
forall b1 b2:
bool,
implb (
negb b1)
b2 = implb (
negb b2)
b1.
Lemma implb_curry :
forall b1 b2 b3:
bool,
implb (
b1 && b2)
b3 = implb b1 (
implb b2 b3).
Lemma implb_andb_distrib_r :
forall b1 b2 b3:
bool,
implb b1 (
b2 && b3)
= implb b1 b2 && implb b1 b3.
Lemma implb_orb_distrib_r :
forall b1 b2 b3:
bool,
implb b1 (
b2 || b3)
= implb b1 b2 || implb b1 b3.
Lemma implb_orb_distrib_l :
forall b1 b2 b3:
bool,
implb (
b1 || b2)
b3 = implb b1 b3 && implb b2 b3.
Properties of xorb
false is neutral for
xorb
true is "complementing" for xorb
Nilpotency (alternatively: identity is a inverse for xorb)
Commutativity
Associativity
Lemmas about the b = true embedding of bool to Prop
Reflection of bool into Prop
Is_true and equality
Is_true and connectives
Lemma orb_prop_elim :
forall a b:
bool,
Is_true (
a || b)
-> Is_true a \/ Is_true b.
Notation orb_prop2 :=
orb_prop_elim (
only parsing).
Lemma orb_prop_intro :
forall a b:
bool,
Is_true a \/ Is_true b -> Is_true (
a || b).
Lemma andb_prop_intro :
forall b1 b2:
bool,
Is_true b1 /\ Is_true b2 -> Is_true (
b1 && b2).
Hint Resolve andb_prop_intro:
bool.
Notation andb_true_intro2 :=
(
fun b1 b2 H1 H2 =>
andb_prop_intro b1 b2 (
conj H1 H2))
(
only parsing).
Lemma andb_prop_elim :
forall a b:
bool,
Is_true (
a && b)
-> Is_true a /\ Is_true b.
Hint Resolve andb_prop_elim:
bool.
Notation andb_prop2 :=
andb_prop_elim (
only parsing).
Lemma eq_bool_prop_intro :
forall b1 b2,
(Is_true b1 <-> Is_true b2) -> b1 = b2.
Lemma eq_bool_prop_elim :
forall b1 b2,
b1 = b2 -> (Is_true b1 <-> Is_true b2).
Lemma negb_prop_elim :
forall b,
Is_true (
negb b)
-> ~ Is_true b.
Lemma negb_prop_intro :
forall b,
~ Is_true b -> Is_true (
negb b).
Lemma negb_prop_classical :
forall b,
~ Is_true (
negb b)
-> Is_true b.
Lemma negb_prop_involutive :
forall b,
Is_true b -> ~ Is_true (
negb b).
Rewrite rules about andb, orb and if (used in romega)
Alternative versions of andb and orb
with lazy behavior (for vm_compute)
Notation "a &&& b" := (
if a then b else false)
(
at level 40,
left associativity) :
lazy_bool_scope.
Notation "a ||| b" := (
if a then true else b)
(
at level 50,
left associativity) :
lazy_bool_scope.
Local Open Scope lazy_bool_scope.
Lemma andb_lazy_alt :
forall a b :
bool,
a && b = a &&& b.
Lemma orb_lazy_alt :
forall a b :
bool,
a || b = a ||| b.
Reflect: a specialized inductive type for
relating propositions and booleans,
as popularized by the Ssreflect library.
Interest: a case on a reflect lemma or hyp performs clever
unification, and leave the goal in a convenient shape
(a bit like case_eq).
Relation with iff :
It would be nice to join
reflect_iff and
iff_reflect
in a unique
iff statement, but this isn't allowed since
iff is in Prop.
Reflect implies decidability of the proposition
Reciprocally, from a decidability, we could state a
reflect as soon as we have a
bool_of_sumbool.
For instance, we could state the correctness of
Bool.eqb via
reflect:
Notations