partial_fixpoint の登場により「定義の後から停止性を示す」ことができるようになった

[Seasawher]

Rocq ではできるそうなので、Lean のデメリットが少なくなったと言える。

[Seasawher]

GPTによるコメント

はい。ただし正確には、「後から termination_by を追加する」というより、先に Option を返す部分関数として定義し、後から = some ... や .isSome を証明するという形です。partial_fixpoint は Option などの適切なモナドを返す再帰関数を受理でき、Lean は等式的に推論できる定理や partial correctness theorem を生成します。Option の場合、非停止に対応する値は none として扱われます。

典型例は McCarthy 91 関数です。これは停止性証明がやや厄介ですが、partial_fixpoint ならまず定義できます。あとから「実は常に some を返す」と証明します。以下はその形です。

import Mathlib
def f91 (n : Nat) : Option Nat :=
if n > 100 then
some (n - 10)
else
f91 (n + 11) >>= f91
partial_fixpoint
#eval f91 42
-- some 91

ここでは、定義時に停止性証明を書いていません。戻り値を Option Nat にしているので、停止すれば some v、停止しなければ論理上は none 側に落ちる、という扱いです。

その後で仕様を証明します。

theorem f91_spec_high (n : Nat) (h : 100 < n) :
f91 n = some (n - 10) := by
unfold f91
simp [h]
theorem f91_spec_low (n : Nat) (h : n ≤ 100) :
f91 n = some 91 := by
unfold f91
rw [if_neg (by omega)]
by_cases hn : n < 90
· rw [f91_spec_low (n + 11) (by omega)]
simp only [Option.bind_eq_bind, Option.some_bind]
rw [f91_spec_low 91 (by omega)]
· rw [f91_spec_high (n + 11) (by omega)]
simp only [Nat.reduceSubDiff, Option.some_bind]
by_cases h100 : n = 100
· simp [f91, h100]
· exact f91_spec_low (n + 1) (by omega)
theorem f91_spec (n : Nat) :
f91 n = some (if n ≤ 100 then 91 else n - 10) := by
by_cases h : n ≤ 100
· simp [f91_spec_low, h]
· simp [f91_spec_high, Nat.lt_of_not_le h, h]

ここまで来ると、全域性はこう言えます。

theorem f91_total (n : Nat) : (f91 n).isSome := by
simp [f91_spec]

そして Option を外した普通の関数も作れます。

def f91! (n : Nat) : Nat :=
(f91 n).get (f91_total n)
theorem f91!_spec (n : Nat) :
f91! n = if n ≤ 100 then 91 else n - 10 := by
simp [f91!, f91_spec]

要するに：

def f : α → Option β := ...
partial_fixpoint

として先に定義し、後から

theorem f_total (x : α) : (f x).isSome := ...

または

theorem f_spec (x : α) : f x = some (...) := ...

を証明する。この f_spec が、実質的に「停止性」と「返り値の正しさ」を同時に言っています。