Library Coq.Bool.Bool
The type bool is defined in the prelude as
Inductive bool : Set := true : bool | false : bool
Interpretation of booleans as propositions
Lemma bool_dec :
forall b1 b2 :
bool, {
b1 =
b2} + {
b1 <>
b2}.
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
Lemma orb_comm :
forall b1 b2:bool,
b1 ||
b2 =
b2 ||
b1.
Associativity
false is a zero for andb
true is neutral for andb
Complementation
Commutativity
Lemma andb_comm :
forall b1 b2:bool,
b1 &&
b2 =
b2 &&
b1.
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.