Merge pull request #556 from lean-ja/Seasawher/issue216

属性: csimp 属性

Examples/Command/Attribute/Csimp.lean

@@ -0,0 +1,62 @@
+/- # csimp
+`csimp` は、コンパイラに単純化を指示する属性です。
+
+`A = B` という形の定理に付与することでコンパイラに `A` の計算を `B` の計算に置き換えさせることができます。非効率な関数を効率的な実装に置き換えるために使用されます。
+-/
+import Lean
+namespace Csimp --#
+
+/-- フィボナッチ数列の非効率な実装 -/
+def fibonacci : Nat → Nat
+  | 0 => 0
+  | 1 => 1
+  | n + 2 => fibonacci n + fibonacci (n+1)
+
+open Lean Elab Command Term Meta in
+
+/-- コマンドが１秒以内に終了することを確かめる -/
+elab "#in_second " stx:command : command => do
+  let start_time ← IO.monoMsNow
+  elabCommand stx
+  let end_time ← IO.monoMsNow
+  let time := end_time - start_time
+  if time <= 1000 then
+    logInfo m!"time: {time}ms"
+  else
+    throwError m!"It took more than one second for the command to run."
+
+-- `#eval fibonacci 32` は１秒以上かかる
+/-- error: It took more than one second for the command to run. -/
+#guard_msgs (error) in #in_second #eval fibonacci 32
+
+/-- フィボナッチ数列のより高速な実装 -/
+def fib (n : Nat) : Nat :=
+  (loop n).1
+where
+  -- ヘルパー関数
+  loop : Nat → Nat × Nat
+    | 0   => (0, 1)
+    | n + 1 =>
+      let p := loop n
+      (p.2, p.1 + p.2)
+
+/-- `fib` は `fibonacci` と同じ漸化式を満たす -/
+theorem fib_add (n : Nat) : fib (n + 2) = fib n + fib (n + 1) := by rfl
+
+/-- `fibonacci` と `fib` は同じ結果を返す。
+`csimp` 属性を与えることで、`fibonacci` の計算を `fib` の計算に置き換えることができる。-/
+@[csimp]
+theorem fib_eq_fibonacci : fibonacci = fib := by
+  ext n
+  induction n using fibonacci.induct
+  case case1 => rfl
+  case case2 => rfl
+  case case3 n ih1 ih2 =>
+    rw [fib_add, fibonacci]
+    simp [ih1, ih2]
+
+-- `fibonacci` の計算が１秒以内に終わるようになった
+#in_second #eval fibonacci 32
+#in_second #eval fibonacci 132
+
+end Csimp --#

src/SUMMARY.md

@@ -55,6 +55,7 @@
     - [variable: 引数を共通化する](./Command/Declarative/Variable.md)
   - [属性](./Command/Attribute/README.md)
     - [cases_eliminator: 独自場合分け](./Command/Attribute/CasesEliminator.md)
+    - [csimp: 効率的な実装に置換](./Command/Attribute/Csimp.md)
     - [induction_eliminator: 独自帰納法](./Command/Attribute/InductionEliminator.md)
     - [simps: simp補題の自動生成](./Command/Attribute/Simps.md)