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 after breaking all booleans
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.
Definition ifb (
b1 b2 b3:
bool) :
bool :=
match b1 with
|
true =>
b2
|
false =>
b3
end.
Open Scope bool_scope.
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
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 v62.
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 v62.
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)
Lemma andb_if :
forall (
A:
Type)(
a a':
A)(
b b' :
bool),
(if b && b' then a else a') =
(if b then if b' then a else a' else a').
Lemma negb_if :
forall (
A:
Type)(
a a':
A)(
b:
bool),
(if negb b then a else a') =
(if b then a' else a).
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.
Open Local 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.