max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: simp theorems for && and ||

Browse source
This commit is contained in:
Leonardo de Moura 2021-03-31 08:12:24 -07:00
parent 9d45ea6721
commit 94e2d0b313
1 changed files with 12 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Init/SimpLemmas.lean
View file

@ -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