theorem Auto.Bool.beq_true {a : Bool} : (a == true) = a

theorem Auto.Bool.beq_false {a : Bool} : (a == false) = !a

theorem Auto.Bool.not_beq_swap {a b : Bool} : (!a == b) = (a == !b)

theorem Auto.Bool.eq_false_of_ne_true {a : Bool} : a ≠ true → a = false

theorem Auto.Bool.ne_true_of_eq_false {a : Bool} : a = false → a ≠ true

theorem Auto.Bool.eq_false_eq_not_eq_true {a : Bool} : (a = false) = (a ≠ true)

theorem Auto.Bool.and_eq_false (a b : Bool) : ((a && b) = false) = (a = false ∨ b = false)

theorem Auto.Bool.or_eq_false (a b : Bool) : ((a || b) = false) = (a = false ∧ b = false)

theorem Auto.Bool.and_comm {a b : Bool} : (a && b) = (b && a)

theorem Auto.Bool.or_comm {a b : Bool} : (a || b) = (b || a)

noncomputable def Auto.Bool.ofProp (c : Prop) : Bool

Equations

• Auto.Bool.ofProp c = match Classical.propDecidable c with | isTrue h => true | isFalse h => false

theorem Auto.Bool.ofProp_spec (c : Prop) : ofProp c = true ↔ c

theorem Auto.Bool.ofProp_spec' (c : Prop) : ofProp c = false ↔ ¬c

theorem Auto.Bool.ite_eq_true {α : Sort u_1} (p : Prop) [inst : Decidable p] (a b : α) : p → (if p then a else b) = a

theorem Auto.Bool.ite_eq_false {α : Sort u_1} (p : Prop) [inst : Decidable p] (a b : α) : ¬p → (if p then a else b) = b

theorem Auto.Bool.dite_eq_true {α : Sort u_1} (p : Prop) [inst : Decidable p] (a : p → α) (b : ¬p → α) (proof : p) : dite p a b = a proof

theorem Auto.Bool.dite_eq_false {α : Sort u_1} (p : Prop) [inst : Decidable p] (a : p → α) (b : ¬p → α) (proof : ¬p) : dite p a b = b proof

noncomputable def Auto.Bool.ite' {α : Sort u} (p : Prop) (x y : α) : α

Similar to ite, but does not have complicated dependent types

Equations

• Auto.Bool.ite' p x y = match Auto.Bool.ofProp p with | true => x | false => y

theorem Auto.Bool.ite_simp : @ite = fun (α : Sort u) (p : Prop) (x : Decidable p) => ite' p

Invoke rw at the beginning of auto

theorem Auto.Bool.ite'_eq_true {α : Sort u_1} (p : Prop) (a b : α) : p → ite' p a b = a

theorem Auto.Bool.ite'_eq_false {α : Sort u_1} (p : Prop) (a b : α) : ¬p → ite' p a b = b

theorem Auto.Bool.cond_simp : @cond = fun (α : Type u) (b : Bool) => ite' (b = true)

Invoke rw at the beginning of auto

theorem Auto.Bool.decide_simp : decide = fun (p : Prop) (x : Decidable p) => ofProp p

Invoke rw at the beginning of auto

theorem Auto.Bool.ite_comm {p : Prop} {α : Sort u_1} {β : Sort u_2} [inst : Decidable p] {x y : α} (f : α → β) : f (if p then x else y) = if p then f x else f y

theorem Auto.Bool.ite'_comm {α : Sort u_1} {β : Sort u_2} {p : Prop} {x y : α} (f : α → β) : f (ite' p x y) = ite' p (f x) (f y)