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

feat: add helper theorems

Browse source
This commit is contained in:
Leonardo de Moura 2020-03-16 11:17:41 -07:00
parent fba18edfa3
commit 596a547e57
2 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Init/Core.lean
View file

@ -1739,6 +1739,9 @@ def reduceBool (b : Bool) : Bool := b
We believe `Lean.reduceBool` enables most interesting applications (e.g., proof by reflection). -/
def reduceNat (n : Nat) : Nat := n
def ofReduceBool (a b : Bool) (h : reduceBool a = b) : a = b := h
def ofReduceNat (a b : Nat) (h : reduceNat a = b) : a = b := h
end Lean
/- Classical reasoning support -/

6
tests/lean/run/reduce1.lean
View file

@ -15,3 +15,9 @@ def v2 : Bool := 10000000000000000 < 200000000000000000000
theorem tst2 : Lean.reduceBool v2 = true :=
rfl
theorem tst3 : v1 = 3628800 :=
Lean.ofReduceNat v1 3628800 rfl
theorem tst4 : v2 = true :=
Lean.ofReduceBool v2 true rfl