partial を紹介する

resolve #80

Src/Def.lean

@@ -22,18 +22,6 @@ def add (n m : Nat) : Nat := n + m
 
 def threeAdd (n m l : Nat) : Nat := n + m + l
 
-/- ## partial
-再帰関数も再帰的でない関数と同様に定義することができますが，有限回で終了することを Lean が自動的に証明できないとエラーになります．
-エラーを解消するには，停止性を証明するか，定義に `partial` という修飾子を付けます．-/
-
-partial def gcd (n m : Nat) : Nat :=
-  if m = 0 then
-    n
-  else
-    gcd m (n % m)
-
-#guard gcd 12 18 = 6
-
 /- ## where
 `where` キーワードを使うと，定義をする前に変数を使用することができます．主に，ヘルパー関数を宣言するために使用されます．
 -/

Src/Partial.lean

@@ -0,0 +1,54 @@
+/- # partial
+`partial` は部分関数(partial function)を定義するための構文です．
+
+Lean では再帰関数も再帰的でない関数と同様に定義できますが，扱いは異なります．再帰的な関数 `f` を定義すると，Lean は `f` がすべての入力に対して必ず有限回の再帰で停止することを証明しようとします．自動的な証明が失敗すると，エラーになってしまいます．エラーを消すには，
+
+* 停止することを手動で証明するか
+* 停止性は保証しないと明示的にマークするか
+
+どちらかの対応が必要です．関数の定義に `partial` とマークすると, 停止性は保証しないとマークしたことになります．
+-/
+namespace WithoutPartial --#
+
+/--
+error: fail to show termination for
+  WithoutPartial.alternate
+with errors
+argument #2 was not used for structural recursion
+  failed to eliminate recursive application
+    alternate ys xs
+
+argument #3 was not used for structural recursion
+  failed to eliminate recursive application
+    alternate ys xs
+
+structural recursion cannot be used
+
+Could not find a decreasing measure.
+The arguments relate at each recursive call as follows:
+(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
+            xs ys
+1) 38:24-39  ?  ?
+Please use `termination_by` to specify a decreasing measure.
+-/
+#guard_msgs (whitespace := lax) in
+def alternate {α : Type} (xs ys : List α) : List α :=
+  match xs, ys with
+  | [], ys => ys
+  | x :: xs, ys => x :: alternate ys xs
+
+end WithoutPartial --#
+namespace Partial --#
+-- `partial` を使うと，停止性の証明が不要になる
+partial def alternate {α : Type} (xs ys : List α) : List α :=
+  match xs, ys with
+  | [], ys => ys
+  | x :: xs, ys => x :: alternate ys xs
+
+#guard alternate [1, 3, 5] [2, 4, 6] = [1, 2, 3, 4, 5, 6]
+
+/- なお，`partial` とマークされた定義を元に新たに関数を定義するとき，再度 `partial` とマークする必要はありません． -/
+
+def more_alternate := @alternate
+
+end Partial --#

md/SUMMARY.md

@@ -35,6 +35,7 @@
 
 # 修飾子
 
+* [partial: 再帰関数の停止証明をしない](./build/Partial.md)
 * [private: 定義を不可視にする](./build/Private.md)
 * [protected: フルネームを強制する](./build/Protected.md)