Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

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 Is_true (b:bool) :=
  match b with
    | true => True
    | false => False
  end.

(*******************)

Decidability

(*******************)

Lemma bool_dec : forall b1 b2 : bool, {b1 = b2} + {b1 <> b2}.forall b1 b2 : bool, {b1 = b2} + {b1 <> b2}
Proof.forall b1 b2 : bool, {b1 = b2} + {b1 <> b2}
  decide equality.
Defined.

(*********************)

Discrimination

(*********************)

Lemma diff_true_false : true <> false.true <> false
Proof.true <> false
  discriminate.
Qed.
Hint Resolve diff_true_false : bool.

Lemma diff_false_true : false <> true.false <> true
Proof.false <> true
  discriminate.
Qed.
Hint Resolve diff_false_true : bool.
Hint Extern 1 (false <> true) => exact diff_false_true : core.

Lemma eq_true_false_abs : forall b:bool, b = true -> b = false -> False.forall b : bool, b = true -> b = false -> False
Proof.forall b : bool, b = true -> b = false -> False
  destr_bool.
Qed.

Lemma not_true_is_false : forall b:bool, b <> true -> b = false.forall b : bool, b <> true -> b = false
Proof.forall b : bool, b <> true -> b = false
  destr_bool; intuition.
Qed.

Lemma not_false_is_true : forall b:bool, b <> false -> b = true.forall b : bool, b <> false -> b = true
Proof.forall b : bool, b <> false -> b = true
  destr_bool; intuition.
Qed.

Lemma not_true_iff_false : forall b, b <> true <-> b = false.forall b : bool, b <> true <-> b = false
Proof.forall b : bool, b <> true <-> b = false
  destr_bool; intuition.
Qed.

Lemma not_false_iff_true : forall b, b <> false <-> b = true.forall b : bool, b <> false <-> b = true
Proof.forall b : bool, b <> false <-> b = true
  destr_bool; intuition.
Qed.

(**********************)

Order on booleans

(**********************)

Definition leb (b1 b2:bool) :=
  match b1 with
    | true => b2 = true
    | false => True
  end.
Hint Unfold leb: bool.

Lemma leb_implb : forall b1 b2, leb b1 b2 <-> implb b1 b2 = true.forall b1 b2 : bool, leb b1 b2 <-> implb b1 b2 = true
Proof.forall b1 b2 : bool, leb b1 b2 <-> implb b1 b2 = true
  destr_bool; intuition.
Qed.

(* Infix "<=" := leb : bool_scope. *)

(*************)

Equality

(*************)

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.forall (P : bool -> Prop) (b1 b2 : bool),
eqb b1 b2 = true -> P b1 -> P b2
Proof.forall (P : bool -> Prop) (b1 b2 : bool),
eqb b1 b2 = true -> P b1 -> P b2
  destr_bool.
Qed.

Lemma eqb_reflx : forall b:bool, eqb b b = true.forall b : bool, eqb b b = true
Proof.forall b : bool, eqb b b = true
  destr_bool.
Qed.

Lemma eqb_prop : forall a b:bool, eqb a b = true -> a = b.forall a b : bool, eqb a b = true -> a = b
Proof.forall a b : bool, eqb a b = true -> a = b
  destr_bool.
Qed.

Lemma eqb_true_iff : forall a b:bool, eqb a b = true <-> a = b.forall a b : bool, eqb a b = true <-> a = b
Proof.forall a b : bool, eqb a b = true <-> a = b
  destr_bool; intuition.
Qed.

Lemma eqb_false_iff : forall a b:bool, eqb a b = false <-> a <> b.forall a b : bool, eqb a b = false <-> a <> b
Proof.forall a b : bool, eqb a b = false <-> a <> b
  destr_bool; intuition.
Qed.

(************************)

A synonym of if on bool

(************************)

Definition ifb (b1 b2 b3:bool) : bool :=
  match b1 with
    | true => b2
    | false => b3
  end.

Open Scope bool_scope.

(****************************)

De Morgan laws

(****************************)

Lemma negb_orb : forall b1 b2:bool, negb (b1 || b2) = negb b1 && negb b2.forall b1 b2 : bool,
negb (b1 || b2) = negb b1 && negb b2
Proof.forall b1 b2 : bool,
negb (b1 || b2) = negb b1 && negb b2
  destr_bool.
Qed.

Lemma negb_andb : forall b1 b2:bool, negb (b1 && b2) = negb b1 || negb b2.forall b1 b2 : bool,
negb (b1 && b2) = negb b1 || negb b2
Proof.forall b1 b2 : bool,
negb (b1 && b2) = negb b1 || negb b2
  destr_bool.
Qed.

(********************************)

Properties of negb

(********************************)

Lemma negb_involutive : forall b:bool, negb (negb b) = b.forall b : bool, negb (negb b) = b
Proof.forall b : bool, negb (negb b) = b
  destr_bool.
Qed.

Lemma negb_involutive_reverse : forall b:bool, b = negb (negb b).forall b : bool, b = negb (negb b)
Proof.forall b : bool, b = negb (negb b)
  destr_bool.
Qed.

Notation negb_elim := negb_involutive (only parsing).
Notation negb_intro := negb_involutive_reverse (only parsing).

Lemma negb_sym : forall b b':bool, b' = negb b -> b = negb b'.forall b b' : bool, b' = negb b -> b = negb b'
Proof.forall b b' : bool, b' = negb b -> b = negb b'
  destr_bool.
Qed.

Lemma no_fixpoint_negb : forall b:bool, negb b <> b.forall b : bool, negb b <> b
Proof.forall b : bool, negb b <> b
  destr_bool.
Qed.

Lemma eqb_negb1 : forall b:bool, eqb (negb b) b = false.forall b : bool, eqb (negb b) b = false
Proof.forall b : bool, eqb (negb b) b = false
  destr_bool.
Qed.

Lemma eqb_negb2 : forall b:bool, eqb b (negb b) = false.forall b : bool, eqb b (negb b) = false
Proof.forall b : bool, eqb b (negb b) = false
  destr_bool.
Qed.

Lemma if_negb :
  forall (A:Type) (b:bool) (x y:A),
    (if negb b then x else y) = (if b then y else x).forall (A : Type) (b : bool) (x y : A),
(if negb b then x else y) = (if b then y else x)
Proof.forall (A : Type) (b : bool) (x y : A),
(if negb b then x else y) = (if b then y else x)
  destr_bool.
Qed.

Lemma negb_true_iff : forall b, negb b = true <-> b = false.forall b : bool, negb b = true <-> b = false
Proof.forall b : bool, negb b = true <-> b = false
  destr_bool; intuition.
Qed.

Lemma negb_false_iff : forall b, negb b = false <-> b = true.forall b : bool, negb b = false <-> b = true
Proof.forall b : bool, negb b = false <-> b = true
  destr_bool; intuition.
Qed.


(********************************)

Properties of orb

(********************************)

Lemma orb_true_iff :
  forall b1 b2, b1 || b2 = true <-> b1 = true \/ b2 = true.forall b1 b2 : bool,
b1 || b2 = true <-> b1 = true \/ b2 = true
Proof.forall b1 b2 : bool,
b1 || b2 = true <-> b1 = true \/ b2 = true
  destr_bool; intuition.
Qed.

Lemma orb_false_iff :
  forall b1 b2, b1 || b2 = false <-> b1 = false /\ b2 = false.forall b1 b2 : bool,
b1 || b2 = false <-> b1 = false /\ b2 = false
Proof.forall b1 b2 : bool,
b1 || b2 = false <-> b1 = false /\ b2 = false
  destr_bool; intuition.
Qed.

Lemma orb_true_elim :
  forall b1 b2:bool, b1 || b2 = true -> {b1 = true} + {b2 = true}.forall b1 b2 : bool,
b1 || b2 = true -> {b1 = true} + {b2 = true}
Proof.forall b1 b2 : bool,
b1 || b2 = true -> {b1 = true} + {b2 = true}
  destruct b1; simpl; auto.
Defined.

Lemma orb_prop : forall a b:bool, a || b = true -> a = true \/ b = true.forall a b : bool,
a || b = true -> a = true \/ b = true
Proof.forall a b : bool,
a || b = true -> a = true \/ b = true
 intros; apply orb_true_iff; trivial.
Qed.

Lemma orb_true_intro :
  forall b1 b2:bool, b1 = true \/ b2 = true -> b1 || b2 = true.forall b1 b2 : bool,
b1 = true \/ b2 = true -> b1 || b2 = true
Proof.forall b1 b2 : bool,
b1 = true \/ b2 = true -> b1 || b2 = true
 intros; apply orb_true_iff; trivial.
Qed.
Hint Resolve orb_true_intro: bool.

Lemma orb_false_intro :
  forall b1 b2:bool, b1 = false -> b2 = false -> b1 || b2 = false.forall b1 b2 : bool,
b1 = false -> b2 = false -> b1 || b2 = false
Proof.forall b1 b2 : bool,
b1 = false -> b2 = false -> b1 || b2 = false
 intros.b1, b2:bool
H:b1 = false
H0:b2 = false
b1 || b2 = false subst.false || false = false reflexivity.
Qed.
Hint Resolve orb_false_intro: bool.

Lemma orb_false_elim :
  forall b1 b2:bool, b1 || b2 = false -> b1 = false /\ b2 = false.forall b1 b2 : bool,
b1 || b2 = false -> b1 = false /\ b2 = false
Proof.forall b1 b2 : bool,
b1 || b2 = false -> b1 = false /\ b2 = false
  intros.b1, b2:bool
H:b1 || b2 = false
b1 = false /\ b2 = false apply orb_false_iff; trivial.
Qed.

Lemma orb_diag : forall b, b || b = b.forall b : bool, b || b = b
Proof.forall b : bool, b || b = b
 destr_bool.
Qed.

true is a zero for orb

Lemma orb_true_r : forall b:bool, b || true = true.forall b : bool, b || true = true
Proof.forall b : bool, b || true = true
  destr_bool.
Qed.
Hint Resolve orb_true_r: bool.

Lemma orb_true_l : forall b:bool, true || b = true.forall b : bool, true || b = true
Proof.forall b : bool, true || b = true
  reflexivity.
Qed.

Notation orb_b_true := orb_true_r (only parsing).
Notation orb_true_b := orb_true_l (only parsing).

false is neutral for orb

Lemma orb_false_r : forall b:bool, b || false = b.forall b : bool, b || false = b
Proof.forall b : bool, b || false = b
  destr_bool.
Qed.
Hint Resolve orb_false_r: bool.

Lemma orb_false_l : forall b:bool, false || b = b.forall b : bool, false || b = b
Proof.forall b : bool, false || b = b
  destr_bool.
Qed.
Hint Resolve orb_false_l: bool.

Notation orb_b_false := orb_false_r (only parsing).
Notation orb_false_b := orb_false_l (only parsing).

Complementation

Lemma orb_negb_r : forall b:bool, b || negb b = true.forall b : bool, b || negb b = true
Proof.forall b : bool, b || negb b = true
  destr_bool.
Qed.
Hint Resolve orb_negb_r: bool.

Notation orb_neg_b := orb_negb_r (only parsing).

Commutativity

Lemma orb_comm : forall b1 b2:bool, b1 || b2 = b2 || b1.forall b1 b2 : bool, b1 || b2 = b2 || b1
Proof.forall b1 b2 : bool, b1 || b2 = b2 || b1
  destr_bool.
Qed.

Associativity

Lemma orb_assoc : forall b1 b2 b3:bool, b1 || (b2 || b3) = b1 || b2 || b3.forall b1 b2 b3 : bool,
b1 || (b2 || b3) = b1 || b2 || b3
Proof.forall b1 b2 b3 : bool,
b1 || (b2 || b3) = b1 || b2 || b3
  destr_bool.
Qed.
Hint Resolve orb_comm orb_assoc: bool.

(*******************************)

Properties of andb

(*******************************)

Lemma andb_true_iff :
  forall b1 b2:bool, b1 && b2 = true <-> b1 = true /\ b2 = true.forall b1 b2 : bool,
b1 && b2 = true <-> b1 = true /\ b2 = true
Proof.forall b1 b2 : bool,
b1 && b2 = true <-> b1 = true /\ b2 = true
  destr_bool; intuition.
Qed.

Lemma andb_false_iff :
  forall b1 b2:bool, b1 && b2 = false <-> b1 = false \/ b2 = false.forall b1 b2 : bool,
b1 && b2 = false <-> b1 = false \/ b2 = false
Proof.forall b1 b2 : bool,
b1 && b2 = false <-> b1 = false \/ b2 = false
  destr_bool; intuition.
Qed.

Lemma andb_true_eq :
  forall a b:bool, true = a && b -> true = a /\ true = b.forall a b : bool,
true = a && b -> true = a /\ true = b
Proof.forall a b : bool,
true = a && b -> true = a /\ true = b
  destr_bool.H:true = true
true = true /\ true = true auto.
Defined.

Lemma andb_false_intro1 : forall b1 b2:bool, b1 = false -> b1 && b2 = false.forall b1 b2 : bool, b1 = false -> b1 && b2 = false
Proof.forall b1 b2 : bool, b1 = false -> b1 && b2 = false
  intros.b1, b2:bool
H:b1 = false
b1 && b2 = false apply andb_false_iff.b1, b2:bool
H:b1 = false
b1 = false \/ b2 = false auto.
Qed.

Lemma andb_false_intro2 : forall b1 b2:bool, b2 = false -> b1 && b2 = false.forall b1 b2 : bool, b2 = false -> b1 && b2 = false
Proof.forall b1 b2 : bool, b2 = false -> b1 && b2 = false
  intros.b1, b2:bool
H:b2 = false
b1 && b2 = false apply andb_false_iff.b1, b2:bool
H:b2 = false
b1 = false \/ b2 = false auto.
Qed.

false is a zero for andb

Lemma andb_false_r : forall b:bool, b && false = false.forall b : bool, b && false = false
Proof.forall b : bool, b && false = false
  destr_bool.
Qed.

Lemma andb_false_l : forall b:bool, false && b = false.forall b : bool, false && b = false
Proof.forall b : bool, false && b = false
  reflexivity.
Qed.

Notation andb_b_false := andb_false_r (only parsing).
Notation andb_false_b := andb_false_l (only parsing).

Lemma andb_diag : forall b, b && b = b.forall b : bool, b && b = b
Proof.forall b : bool, b && b = b
 destr_bool.
Qed.

true is neutral for andb

Lemma andb_true_r : forall b:bool, b && true = b.forall b : bool, b && true = b
Proof.forall b : bool, b && true = b
  destr_bool.
Qed.

Lemma andb_true_l : forall b:bool, true && b = b.forall b : bool, true && b = b
Proof.forall b : bool, true && b = b
  reflexivity.
Qed.

Notation andb_b_true := andb_true_r (only parsing).
Notation andb_true_b := andb_true_l (only parsing).

Lemma andb_false_elim :
  forall b1 b2:bool, b1 && b2 = false -> {b1 = false} + {b2 = false}.forall b1 b2 : bool,
b1 && b2 = false -> {b1 = false} + {b2 = false}
Proof.forall b1 b2 : bool,
b1 && b2 = false -> {b1 = false} + {b2 = false}
  destruct b1; simpl; auto.
Defined.
Hint Resolve andb_false_elim: bool.

Complementation

Lemma andb_negb_r : forall b:bool, b && negb b = false.forall b : bool, b && negb b = false
Proof.forall b : bool, b && negb b = false
  destr_bool.
Qed.
Hint Resolve andb_negb_r: bool.

Notation andb_neg_b := andb_negb_r (only parsing).

Commutativity

Lemma andb_comm : forall b1 b2:bool, b1 && b2 = b2 && b1.forall b1 b2 : bool, b1 && b2 = b2 && b1
Proof.forall b1 b2 : bool, b1 && b2 = b2 && b1
  destr_bool.
Qed.

Associativity

Lemma andb_assoc : forall b1 b2 b3:bool, b1 && (b2 && b3) = b1 && b2 && b3.forall b1 b2 b3 : bool,
b1 && (b2 && b3) = b1 && b2 && b3
Proof.forall b1 b2 b3 : bool,
b1 && (b2 && b3) = b1 && b2 && b3
  destr_bool.
Qed.

Hint Resolve andb_comm andb_assoc: bool.

(*******************************************)

Properties mixing andb and orb

(*******************************************)

Distributivity

Lemma andb_orb_distrib_r :
  forall b1 b2 b3:bool, b1 && (b2 || b3) = b1 && b2 || b1 && b3.forall b1 b2 b3 : bool,
b1 && (b2 || b3) = b1 && b2 || b1 && b3
Proof.forall b1 b2 b3 : bool,
b1 && (b2 || b3) = b1 && b2 || b1 && b3
  destr_bool.
Qed.

Lemma andb_orb_distrib_l :
 forall b1 b2 b3:bool, (b1 || b2) && b3 = b1 && b3 || b2 && b3.forall b1 b2 b3 : bool,
(b1 || b2) && b3 = b1 && b3 || b2 && b3
Proof.forall b1 b2 b3 : bool,
(b1 || b2) && b3 = b1 && b3 || b2 && b3
  destr_bool.
Qed.

Lemma orb_andb_distrib_r :
  forall b1 b2 b3:bool, b1 || b2 && b3 = (b1 || b2) && (b1 || b3).forall b1 b2 b3 : bool,
b1 || b2 && b3 = (b1 || b2) && (b1 || b3)
Proof.forall b1 b2 b3 : bool,
b1 || b2 && b3 = (b1 || b2) && (b1 || b3)
  destr_bool.
Qed.

Lemma orb_andb_distrib_l :
  forall b1 b2 b3:bool, b1 && b2 || b3 = (b1 || b3) && (b2 || b3).forall b1 b2 b3 : bool,
b1 && b2 || b3 = (b1 || b3) && (b2 || b3)
Proof.forall b1 b2 b3 : bool,
b1 && b2 || b3 = (b1 || b3) && (b2 || b3)
  destr_bool.
Qed.

(* Compatibility *)
Notation demorgan1 := andb_orb_distrib_r (only parsing).
Notation demorgan2 := andb_orb_distrib_l (only parsing).
Notation demorgan3 := orb_andb_distrib_r (only parsing).
Notation demorgan4 := orb_andb_distrib_l (only parsing).

Absorption

Lemma absorption_andb : forall b1 b2:bool, b1 && (b1 || b2) = b1.forall b1 b2 : bool, b1 && (b1 || b2) = b1
Proof.forall b1 b2 : bool, b1 && (b1 || b2) = b1
  destr_bool.
Qed.

Lemma absorption_orb : forall b1 b2:bool, b1 || b1 && b2 = b1.forall b1 b2 : bool, b1 || b1 && b2 = b1
Proof.forall b1 b2 : bool, b1 || b1 && b2 = b1
  destr_bool.
Qed.

(* begin hide *)
(* Compatibility *)
Notation absoption_andb := absorption_andb (only parsing).
Notation absoption_orb := absorption_orb (only parsing).
(* end hide *)

(*********************************)

Properties of xorb

(*********************************)

false is neutral for xorb

Lemma xorb_false_r : forall b:bool, xorb b false = b.forall b : bool, xorb b false = b
Proof.forall b : bool, xorb b false = b
  destr_bool.
Qed.

Lemma xorb_false_l : forall b:bool, xorb false b = b.forall b : bool, xorb false b = b
Proof.forall b : bool, xorb false b = b
  destr_bool.
Qed.

Notation xorb_false := xorb_false_r (only parsing).
Notation false_xorb := xorb_false_l (only parsing).

true is "complementing" for xorb

Lemma xorb_true_r : forall b:bool, xorb b true = negb b.forall b : bool, xorb b true = negb b
Proof.forall b : bool, xorb b true = negb b
  reflexivity.
Qed.

Lemma xorb_true_l : forall b:bool, xorb true b = negb b.forall b : bool, xorb true b = negb b
Proof.forall b : bool, xorb true b = negb b
  reflexivity.
Qed.

Notation xorb_true := xorb_true_r (only parsing).
Notation true_xorb := xorb_true_l (only parsing).

Nilpotency (alternatively: identity is a inverse for xorb)

Lemma xorb_nilpotent : forall b:bool, xorb b b = false.forall b : bool, xorb b b = false
Proof.forall b : bool, xorb b b = false
  destr_bool.
Qed.

Commutativity

Lemma xorb_comm : forall b b':bool, xorb b b' = xorb b' b.forall b b' : bool, xorb b b' = xorb b' b
Proof.forall b b' : bool, xorb b b' = xorb b' b
  destr_bool.
Qed.

Associativity

Lemma xorb_assoc_reverse :
  forall b b' b'':bool, xorb (xorb b b') b'' = xorb b (xorb b' b'').forall b b' b'' : bool,
xorb (xorb b b') b'' = xorb b (xorb b' b'')
Proof.forall b b' b'' : bool,
xorb (xorb b b') b'' = xorb b (xorb b' b'')
  destr_bool.
Qed.

Notation xorb_assoc := xorb_assoc_reverse (only parsing). (* Compatibility *)

Lemma xorb_eq : forall b b':bool, xorb b b' = false -> b = b'.forall b b' : bool, xorb b b' = false -> b = b'
Proof.forall b b' : bool, xorb b b' = false -> b = b'
  destr_bool.
Qed.

Lemma xorb_move_l_r_1 :
  forall b b' b'':bool, xorb b b' = b'' -> b' = xorb b b''.forall b b' b'' : bool,
xorb b b' = b'' -> b' = xorb b b''
Proof.forall b b' b'' : bool,
xorb b b' = b'' -> b' = xorb b b''
  destr_bool.
Qed.

Lemma xorb_move_l_r_2 :
  forall b b' b'':bool, xorb b b' = b'' -> b = xorb b'' b'.forall b b' b'' : bool,
xorb b b' = b'' -> b = xorb b'' b'
Proof.forall b b' b'' : bool,
xorb b b' = b'' -> b = xorb b'' b'
  destr_bool.
Qed.

Lemma xorb_move_r_l_1 :
  forall b b' b'':bool, b = xorb b' b'' -> xorb b' b = b''.forall b b' b'' : bool,
b = xorb b' b'' -> xorb b' b = b''
Proof.forall b b' b'' : bool,
b = xorb b' b'' -> xorb b' b = b''
  destr_bool.
Qed.

Lemma xorb_move_r_l_2 :
  forall b b' b'':bool, b = xorb b' b'' -> xorb b b'' = b'.forall b b' b'' : bool,
b = xorb b' b'' -> xorb b b'' = b'
Proof.forall b b' b'' : bool,
b = xorb b' b'' -> xorb b b'' = b'
  destr_bool.
Qed.

Lemma negb_xorb_l : forall b b', negb (xorb b b') = xorb (negb b) b'.forall b b' : bool,
negb (xorb b b') = xorb (negb b) b'
Proof.forall b b' : bool,
negb (xorb b b') = xorb (negb b) b'
 destruct b,b'; trivial.
Qed.

Lemma negb_xorb_r : forall b b', negb (xorb b b') = xorb b (negb b').forall b b' : bool,
negb (xorb b b') = xorb b (negb b')
Proof.forall b b' : bool,
negb (xorb b b') = xorb b (negb b')
 destruct b,b'; trivial.
Qed.

Lemma xorb_negb_negb : forall b b', xorb (negb b) (negb b') = xorb b b'.forall b b' : bool,
xorb (negb b) (negb b') = xorb b b'
Proof.forall b b' : bool,
xorb (negb b) (negb b') = xorb b b'
 destruct b,b'; trivial.
Qed.

Lemmas about the b = true embedding of bool to Prop

Lemma eq_iff_eq_true : forall b1 b2, b1 = b2 <-> (b1 = true <-> b2 = true).forall b1 b2 : bool,
b1 = b2 <-> (b1 = true <-> b2 = true)
Proof.forall b1 b2 : bool,
b1 = b2 <-> (b1 = true <-> b2 = true)
  destr_bool; intuition.
Qed.

Lemma eq_true_iff_eq : forall b1 b2, (b1 = true <-> b2 = true) -> b1 = b2.forall b1 b2 : bool,
b1 = true <-> b2 = true -> b1 = b2
Proof.forall b1 b2 : bool,
b1 = true <-> b2 = true -> b1 = b2
  apply eq_iff_eq_true.
Qed.

Notation bool_1 := eq_true_iff_eq (only parsing). (* Compatibility *)

Lemma eq_true_negb_classical : forall b:bool, negb b <> true -> b = true.forall b : bool, negb b <> true -> b = true
Proof.forall b : bool, negb b <> true -> b = true
  destr_bool; intuition.
Qed.

Notation bool_3 := eq_true_negb_classical (only parsing). (* Compatibility *)

Lemma eq_true_not_negb : forall b:bool, b <> true -> negb b = true.forall b : bool, b <> true -> negb b = true
Proof.forall b : bool, b <> true -> negb b = true
  destr_bool; intuition.
Qed.

Notation bool_6 := eq_true_not_negb (only parsing). (* Compatibility *)

Hint Resolve eq_true_not_negb : bool.

(* An interesting lemma for auto but too strong to keep compatibility *)

Lemma absurd_eq_bool : forall b b':bool, False -> b = b'.forall b b' : bool, False -> b = b'
Proof.forall b b' : bool, False -> b = b'
  contradiction.
Qed.

(* A more specific one that preserves compatibility with old hint bool_3 *)

Lemma absurd_eq_true : forall b, False -> b = true.forall b : bool, False -> b = true
Proof.forall b : bool, False -> b = true
  contradiction.
Qed.
Hint Resolve absurd_eq_true : core.

(* A specific instance of eq_trans that preserves compatibility with
   old hint bool_2 *)

Lemma trans_eq_bool : forall x y z:bool, x = y -> y = z -> x = z.forall x y z : bool, x = y -> y = z -> x = z
Proof.forall x y z : bool, x = y -> y = z -> x = z
  apply eq_trans.
Qed.
Hint Resolve trans_eq_bool : core.

(*****************************************)

Reflection of bool into Prop

(*****************************************)

Is_true and equality

Hint Unfold Is_true: bool.

Lemma Is_true_eq_true : forall x:bool, Is_true x -> x = true.forall x : bool, Is_true x -> x = true
Proof.forall x : bool, Is_true x -> x = true
  destr_bool; tauto.
Qed.

Lemma Is_true_eq_left : forall x:bool, x = true -> Is_true x.forall x : bool, x = true -> Is_true x
Proof.forall x : bool, x = true -> Is_true x
  intros; subst; auto with bool.
Qed.

Lemma Is_true_eq_right : forall x:bool, true = x -> Is_true x.forall x : bool, true = x -> Is_true x
Proof.forall x : bool, true = x -> Is_true x
  intros; subst; auto with bool.
Qed.

Notation Is_true_eq_true2 := Is_true_eq_right (only parsing).

Hint Immediate Is_true_eq_right Is_true_eq_left: bool.

Lemma eqb_refl : forall x:bool, Is_true (eqb x x).forall x : bool, Is_true (eqb x x)
Proof.forall x : bool, Is_true (eqb x x)
  destr_bool.
Qed.

Lemma eqb_eq : forall x y:bool, Is_true (eqb x y) -> x = y.forall x y : bool, Is_true (eqb x y) -> x = y
Proof.forall x y : bool, Is_true (eqb x y) -> x = y
  destr_bool; tauto.
Qed.

Is_true and connectives

Lemma orb_prop_elim :
  forall a b:bool, Is_true (a || b) -> Is_true a \/ Is_true b.forall a b : bool,
Is_true (a || b) -> Is_true a \/ Is_true b
Proof.forall a b : bool,
Is_true (a || b) -> Is_true a \/ Is_true b
  destr_bool; tauto.
Qed.

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).forall a b : bool,
Is_true a \/ Is_true b -> Is_true (a || b)
Proof.forall a b : bool,
Is_true a \/ Is_true b -> Is_true (a || b)
  destr_bool; tauto.
Qed.

Lemma andb_prop_intro :
  forall b1 b2:bool, Is_true b1 /\ Is_true b2 -> Is_true (b1 && b2).forall b1 b2 : bool,
Is_true b1 /\ Is_true b2 -> Is_true (b1 && b2)
Proof.forall b1 b2 : bool,
Is_true b1 /\ Is_true b2 -> Is_true (b1 && b2)
  destr_bool; tauto.
Qed.
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.forall a b : bool,
Is_true (a && b) -> Is_true a /\ Is_true b
Proof.forall a b : bool,
Is_true (a && b) -> Is_true a /\ Is_true b
  destr_bool; auto.
Qed.
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.forall b1 b2 : bool,
Is_true b1 <-> Is_true b2 -> b1 = b2
Proof.forall b1 b2 : bool,
Is_true b1 <-> Is_true b2 -> b1 = b2
  destr_bool; tauto.
Qed.

Lemma eq_bool_prop_elim : forall b1 b2, b1 = b2 -> (Is_true b1 <-> Is_true b2).forall b1 b2 : bool,
b1 = b2 -> Is_true b1 <-> Is_true b2
Proof.forall b1 b2 : bool,
b1 = b2 -> Is_true b1 <-> Is_true b2
  destr_bool; tauto.
Qed.

Lemma negb_prop_elim : forall b, Is_true (negb b) -> ~ Is_true b.forall b : bool, Is_true (negb b) -> ~ Is_true b
Proof.forall b : bool, Is_true (negb b) -> ~ Is_true b
  destr_bool; tauto.
Qed.

Lemma negb_prop_intro : forall b, ~ Is_true b -> Is_true (negb b).forall b : bool, ~ Is_true b -> Is_true (negb b)
Proof.forall b : bool, ~ Is_true b -> Is_true (negb b)
  destr_bool; tauto.
Qed.

Lemma negb_prop_classical : forall b, ~ Is_true (negb b) -> Is_true b.forall b : bool, ~ Is_true (negb b) -> Is_true b
Proof.forall b : bool, ~ Is_true (negb b) -> Is_true b
  destr_bool; tauto.
Qed.

Lemma negb_prop_involutive : forall b, Is_true b -> ~ Is_true (negb b).forall b : bool, Is_true b -> ~ Is_true (negb b)
Proof.forall b : bool, Is_true b -> ~ Is_true (negb b)
  destr_bool; tauto.
Qed.

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').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')
Proof.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')
  destr_bool.
Qed.

Lemma negb_if : forall (A:Type)(a a':A)(b:bool),
 (if negb b then a else a') =
 (if b then a' else a).forall (A : Type) (a a' : A) (b : bool),
(if negb b then a else a') = (if b then a' else a)
Proof.forall (A : Type) (a a' : A) (b : bool),
(if negb b then a else a') = (if b then a' else a)
  destr_bool.
Qed.

(*****************************************)

Alternative versions of andb and orb

with lazy behavior (for vm_compute)

(*****************************************)

Declare Scope lazy_bool_scope.

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.forall a b : bool, a && b = a &&& b
Proof.forall a b : bool, a && b = a &&& b
  reflexivity.
Qed.

Lemma orb_lazy_alt : forall a b : bool, a || b = a ||| b.forall a b : bool, a || b = a ||| b
Proof.forall a b : bool, a || b = a ||| b
  reflexivity.
Qed.

(*****************************************)

Reflect: a specialized inductive type for

relating propositions and booleans, as popularized by the Ssreflect library.

(*****************************************)

Inductive reflect (P : Prop) : bool -> Set :=
  | ReflectT : P -> reflect P true
  | ReflectF : ~ P -> reflect P false.
Hint Constructors reflect : bool.

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 :

Lemma reflect_iff : forall P b, reflect P b -> (P<->b=true).forall (P : Prop) (b : bool),
reflect P b -> P <-> b = true
Proof.forall (P : Prop) (b : bool),
reflect P b -> P <-> b = true
 destruct 1; intuition; discriminate.
Qed.

Lemma iff_reflect : forall P b, (P<->b=true) -> reflect P b.forall (P : Prop) (b : bool),
P <-> b = true -> reflect P b
Proof.forall (P : Prop) (b : bool),
P <-> b = true -> reflect P b
 destr_bool; intuition.
Defined.

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

Lemma reflect_dec : forall P b, reflect P b -> {P}+{~P}.forall (P : Prop) (b : bool),
reflect P b -> {P} + {~ P}
Proof.forall (P : Prop) (b : bool),
reflect P b -> {P} + {~ P}
 destruct 1; auto.
Defined.

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:

Lemma eqb_spec (b b' : bool) : reflect (b = b') (eqb b b').b, b':bool
reflect (b = b') (eqb b b')
Proof.b, b':bool
reflect (b = b') (eqb b b')
 destruct b, b'; now constructor.
Defined.