From 94e2d0b313da2e2d417f5d8df46410bed0f08f27 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 31 Mar 2021 08:12:24 -0700 Subject: [PATCH] feat: simp theorems for `&&` and `||` --- src/Init/SimpLemmas.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/Init/SimpLemmas.lean b/src/Init/SimpLemmas.lean index 9a239a0ed4..ba2016c781 100644 --- a/src/Init/SimpLemmas.lean +++ b/src/Init/SimpLemmas.lean @@ -90,4 +90,16 @@ namespace Lean.Simp @[simp] theorem arrow_True (p : Prop) : (p → True) = True := propext <| Iff.intro (fun _ => trivial) (by intros; trivial) @[simp] theorem True_arrow (p : Prop) : (True → p) = p := propext <| Iff.intro (fun h => h trivial) (by intros; trivial) +@[simp] theorem or_false (b : Bool) : (b || false) = b := by cases b <;> rfl +@[simp] theorem or_true (b : Bool) : (b || true) = true := by cases b <;> rfl +@[simp] theorem false_or (b : Bool) : (false || b) = b := by cases b <;> rfl +@[simp] theorem true_or (b : Bool) : (true || b) = true := by cases b <;> rfl +@[simp] theorem or_self (b : Bool) : (b || b) = b := by cases b <;> rfl + +@[simp] theorem and_false (b : Bool) : (b && false) = false := by cases b <;> rfl +@[simp] theorem and_true (b : Bool) : (b && true) = b := by cases b <;> rfl +@[simp] theorem false_and (b : Bool) : (false && b) = false := by cases b <;> rfl +@[simp] theorem true_and (b : Bool) : (true && b) = b := by cases b <;> rfl +@[simp] theorem and_self (b : Bool) : (b && b) = b := by cases b <;> rfl + end Lean.Simp