search

lean-ja / lean-by-example

コード例で学ぶ Lean 言語
https://lean-ja.github.io/lean-by-example/
MIT License
51 stars 7 forks source link

induction タクティクで induction' タクティクの真似をする #1065

Closed Seasawher closed 3 weeks ago

Seasawher commented 3 weeks ago 
def fac (n : Nat) :=
  match n with
  | 0 => 1
  | n + 1 => (n + 1) * fac n

theorem foo (n : Nat) : n = 0 := by
  generalize h : fac n = m
  induction m with
  | zero => sorry
  | succ => sorry