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

feat: helper lemmas for equation compiler

Browse source
This commit is contained in:
Leonardo de Moura 2020-03-13 06:35:00 -07:00
parent a0090b378b
commit 7bb9638ea6
1 changed files with 10 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Init/Core.lean
View file

@ -1019,6 +1019,16 @@ match h with
| (isTrue hc) => absurd hc hnc
| (isFalse hnc) => rfl
theorem difPos {c : Prop} [h : Decidable c] (hc : c) {α : Sort u} {t : c → α} {e : ¬ c → α} : (dite c t e) = t hc :=
match h with
| (isTrue hc) => rfl
| (isFalse hnc) => absurd hc hnc
theorem difNeg {c : Prop} [h : Decidable c] (hnc : ¬c) {α : Sort u} {t : c → α} {e : ¬ c → α} : (dite c t e) = e hnc :=
match h with
| (isTrue hc) => absurd hc hnc
| (isFalse hnc) => rfl
-- Remark: dite and ite are "defally equal" when we ignore the proofs.
theorem difEqIf (c : Prop) [h : Decidable c] {α : Sort u} (t : α) (e : α) : dite c (fun h => t) (fun h => e) = ite c t e :=
match h with