Compare commits

...

1 Commits

Author SHA1 Message Date
Scott Morrison
30eba379a9 chore: simplify decide (b = true) and variants 2024-02-21 15:05:32 +11:00

View File

@@ -48,6 +48,11 @@ theorem ne_false_iff : {b : Bool} → b ≠ false ↔ b = true := by decide
theorem eq_iff_iff {a b : Bool} : a = b (a b) := by cases b <;> simp
@[simp] theorem decide_eq_true {b : Bool} : decide (b = true) = b := by cases b <;> simp
@[simp] theorem decide_eq_false {b : Bool} : decide (b = false) = !b := by cases b <;> simp
@[simp] theorem decide_true_eq {b : Bool} : decide (true = b) = b := by cases b <;> simp
@[simp] theorem decide_false_eq {b : Bool} : decide (false = b) = !b := by cases b <;> simp
/-! ### and -/
@[simp] theorem not_and_self : (x : Bool), (!x && x) = false := by decide