#reduce コマンドを紹介する

Seasawher commented 3 months ago

TPiL より https://aconite-ac.github.io/theorem_proving_in_lean4_ja/induction_and_recursion.html#structural-recursion-and-induction-%E6%A7%8B%E9%80%A0%E7%9A%84%E5%86%8D%E5%B8%B0%E3%81%A8%E6%A7%8B%E9%80%A0%E7%9A%84%E5%B8%B0%E7%B4%8D%E6%B3%95

累積再帰の利用は、等式コンパイラがLeanのカーネルに対して特定の関数が停止することを正当に主張するために使うテクニックの一つである。他の関数型プログラミング言語のコンパイラと同様、再帰関数をコンパイルするコードジェネレータに影響を与えることはない。#eval fib n の実行時間は指数 n の指数関数となることを思い出してほしい。一方で、#reduce fib n は brecOn による構築に基づいた定義を使用するため効率的である。

def fib : Nat → Nat
  | 0   => 1
  | 1   => 1
  | n+2 => fib (n+1) + fib n

-- #eval fib 50 -- slow
#reduce fib 50  -- fast

#print fib

Seasawher commented 3 months ago

noncomputable def one : Nat := 1

#eval one -- エラー

#reduce one -- エラーにならない

Seasawher commented 2 months ago

結局 #reduce のやっている内容がよくわからないので，このままでは紹介できない

Seasawher commented 3 weeks ago

文字列を展開できない？

see https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/unexpected.20error.20on.20.23reduce/near/444941290

lean-ja / lean-by-example

#reduce コマンドを紹介する #108