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

chore: add simp helper lemmas

Browse source
This commit is contained in:
Leonardo de Moura 2021-02-15 12:42:13 -08:00
parent 7bdd3ae5a2
commit 51bdf670fa
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Init/SimpLemmas.lean
View file

@ -23,6 +23,12 @@ theorem eqFalse (h : ¬ p) : p = False :=
theorem eqFalse' (h : p → False) : p = False :=
propext <| Iff.intro (fun h' => absurd h' h) (fun h' => False.elim h')
theorem eqTrueOfDecide {p : Prop} {s : Decidable p} (h : decide p = true) : p = True :=
propext <| Iff.intro (fun h => trivial) (fun _ => ofDecideEqTrue h)
theorem eqFalseOfDecide {p : Prop} {s : Decidable p} (h : decide p = false) : p = False :=
propext <| Iff.intro (fun h' => absurd h' (ofDecideEqFalse h)) (fun h => False.elim h)
theorem impCongr {p₁ p₂ : Sort u} {q₁ q₂ : Sort v} (h₁ : p₁ = p₂) (h₂ : q₁ = q₂) : (p₁ → q₁) = (p₂ → q₂) :=
h₁ ▸ h₂ ▸ rfl