Bool lemmas

@[simp]

theorem decide_eq_not_decide (p q : Prop) [Decidable p] [Decidable q] : (decide p = !decide q) = (decide (p ↔ ¬q) = true)

theorem bif_if_congr {α : Type} {x : Bool} {y : Prop} {a b c d : α} {dy : Decidable y} (xy : x = decide y) (ac : a = c) (bd : b = d) : (bif x then a else b) = if y then c else d

theorem Bool.beq_eq_decide_eq' {α : Type} [BEq α] [DecidableEq α] [LawfulBEq α] (x y : α) : (x == y) = decide (x = y)

Better version of Bool.beq_eq_decide_eq that uses any BEq instance

@[simp]

theorem Bool.beq_not_iff_ne (x y : Bool) : x = !y ↔ x ≠ y

theorem bif_congr {α : Type} {x y : Bool} {a b c d : α} (xy : x = y) (ac : a = c) (bd : b = d) : (bif x then a else b) = bif y then c else d

@[simp]

theorem Bool.beq_not_iff_bne (x y : Bool) : (x == !y) = (x != y)

Change == ! to !=

theorem bif_eq_if {α : Type} {b : Bool} {x y : α} : (bif b then x else y) = if b = true then x else y

Change bif to if

theorem apply_decide {α : Type} {f : Bool → α} {p : Prop} {dp : Decidable p} : f (decide p) = if p then f true else f false

theorem or_decide_eq_if {a : Bool} {p : Prop} {dp : Decidable p} : (a || decide p) = if p then true else a

theorem decide_and_eq_if' {a : Bool} {p : Prop} {dp : Decidable p} : (decide p && a) = if p then a else false

theorem and_decide_eq_if {a : Bool} {p : Prop} {dp : Decidable p} : (a && decide p) = if p then a else false

theorem decide_and_eq_if {p q : Prop} {dp : Decidable (p ∧ q)} : decide (p ∧ q) = if p then decide q else false

theorem decide_eq_if {p : Prop} {dp : Decidable p} : decide p = if p then true else false

theorem if_or {X : Type} {p q : Prop} {dp : Decidable (p ∨ q)} {x y : X} : (if p ∨ q then x else y) = if p then x else if q then x else y

theorem if_and {X : Type} {p q : Prop} {dp : Decidable (p ∧ q)} {x y : X} : (if p ∧ q then x else y) = if p then if q then x else y else y

@[simp]

theorem if_true_false {p : Prop} {dp : Decidable p} : (if p then True else False) = p

@[simp]

theorem Bool.bne_eq_false {x y : Bool} : (x != y) = false ↔ x = y