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

feat: helper simp theorems

Browse source
This commit is contained in:
Leonardo de Moura 2022-02-10 17:06:16 -08:00
parent 1d5da63482
commit 1491253479
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/SimpLemmas.lean
View file

@ -117,9 +117,13 @@ theorem dite_congr {s : Decidable b} [Decidable c]
@[simp] theorem Bool.false_or (b : Bool) : (false || b) = b := by cases b <;> rfl
@[simp] theorem Bool.true_or (b : Bool) : (true || b) = true := by cases b <;> rfl
@[simp] theorem Bool.or_self (b : Bool) : (b || b) = b := by cases b <;> rfl
@[simp] theorem Bool.or_eq_true (a b : Bool) : ((a || b) = true) = (a = true ∨ b = true) := by cases a <;> cases b <;> decide
@[simp] theorem Bool.and_false (b : Bool) : (b && false) = false := by cases b <;> rfl
@[simp] theorem Bool.and_true (b : Bool) : (b && true) = b := by cases b <;> rfl
@[simp] theorem Bool.false_and (b : Bool) : (false && b) = false := by cases b <;> rfl
@[simp] theorem Bool.true_and (b : Bool) : (true && b) = b := by cases b <;> rfl
@[simp] theorem Bool.and_self (b : Bool) : (b && b) = b := by cases b <;> rfl
@[simp] theorem Bool.and_eq_true (a b : Bool) : ((a && b) = true) = (a = true ∧ b = true) := by cases a <;> cases b <;> decide
@[simp] theorem decide_eq_true_eq [Decidable p] : (decide p = true) = p := propext <| Iff.intro of_decide_eq_true decide_eq_true