From 3d8f73380e270cfb5030bba2ce7e67b58ddce1ba Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Wed, 21 Feb 2024 15:30:25 +1100 Subject: [PATCH] chore: simplify decide (b = true) and variants (#3426) ``` @[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 ``` --- src/Init/Data/Bool.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean index 6068d52258..ae1fe42ce2 100644 --- a/src/Init/Data/Bool.lean +++ b/src/Init/Data/Bool.lean @@ -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