再帰なんてベースケースと、ベースケースに収束していくステップを末尾再帰で書けばいいのだと思っていたのですが、集合を題材にLeanで簡単な証明を書いてみようと思ったら、そもそも再帰がまわってくれないケースに遭遇したので、そのときの会話内容をベースにAIに記事を書いてもらいました。要点はrepeatは再帰ではなくループである点です。あくまで問題提起的なメモであり、解決策については未着手です。なお、AIのドラマチックな言い回しを抑えきれず、また、数学の小難しい話が勝手に追記されたりして、AIに代筆を頼むのは難しいと思いました。
Lean 4における repeat タクティクの停止要因と全域性の制約
1. 問題の所在
エンジニアがLean 4で有限集合（列挙型）の全要素に対する証明を自動化する際、repeat タクティクが最初のイテレーションのみで停止し、後続の要素が処理されない事象が発生する。
これは、手続き型言語における「一般再帰（General Recursion）」のメンタルモデルと、定理証明系が要求する「全域性（Totality）」および「選言除去（Disjunction Elimination）」の仕様の不一致に起因する。
2. 再現コード
以下のコードは、集合を題材として、仮定 h を replace で更新しつつループ処理を行うことを意図しているが、第2要素以降の処理が行われずに停止する。
集合はLean内部では論理和で表現されているため、証明内で論理和のコンストラクタが使われている。
case h₂ =>
intro c h
repeat (
match h with -- 内部的には cases (Or.elim)
| Or.inl hl =>
subst hl
-- Head側は解決する
repeat (first | apply Or.inl; rfl | apply Or.inr)
| Or.inr hr =>
-- Tail側：仮定を更新して次へ回そうとする
replace h := hr
)
3. 技術的要因
A. 選言除去の閉鎖義務
コード内で使用している cases (または match) は、論理学における選言除去規則（$\lor E$）に対応する。
$$
\frac{\Gamma \vdash A \lor B \quad \Gamma, A \vdash P \quad \Gamma, B \vdash P}{\Gamma \vdash P} (\lor E)
$$
この規則は、分岐した $A$ (Head) と $B$ (Tail) の双方に対して、型 $P$ の項（証明）を構築することを要求する。
手続き的なループとは異なり、論理学的な分岐においては「片方を未解決のまま保留し、状態だけ更新して再帰する」という操作は、証明木の構造上、完結したステップとみなされない場合がある。
B. タクティクの停止条件と partial の排除
Lean 4の repeat t コンビネータは、生成されたすべてのサブゴールに対して $t$ を適用し、進展（Progress）を確認する仕様となっている。
- Head (左分枝): ゴールが解決（Close）される。
- Tail (右分枝): 仮定の型は変化するが、ゴール自体は未解決のまま残存する。
この状態において repeat は「全サブゴールに対する有効な進展が得られなかった」と判定し、停止する。
C. 一般再帰と構造的再帰の乖離
エンジニアが想定する while ループは、計算機科学的には 一般再帰（General Recursion / partial def） に相当する。
-
一般再帰 (
partial): 停止性が保証されなくても記述可能。 - 構造的再帰 (Total): 証明項として許容される唯一の再帰。引数が構造的に縮小していることが型システムによって保証されなければならない。
Leanの証明構築プロセス（カリー＝ハワード同型対応）において、証明項は必ず全域的（Total）でなければならない。タクティクエンジンは、論理的な不整合や無限ループを防ぐため、構造的に閉じていない（partial 的な挙動を含む）証明の構築を拒絶する傾向にある。
4. 結論
repeat タクティクが意図通りに動作しない現象は、実装上の不具合ではなく、**「証明＝全域関数」**という型理論の原則によるものである。
解決には、手続き的な「状態更新ループ」ではなく、データ構造（リストや帰納的型）の構造そのものに基づいた再帰（induction 等）を用いるアプローチが必要となる。