import FormalLab.Mathematics.NaturalNumberInduction
import FormalLab.Mathematics.Orders

/-!
# 第26章：整礎関係・整礎帰納法・停止する一般再帰

自然数の原始再帰では、再帰呼出しは直前の数に限られます。しかしEuclidの互除法は
`gcd(a,b)` から `gcd(b,a mod b)` へ進み、構文上の直部分へ再帰していません。停止を説明するには、
各呼出しで小さくなる量と、無限に下降できない関係を分けて考える必要があります。

本章では接近可能性 `Acc r x` と整礎性 `WellFounded r` を導入します。有限の下降鎖しか持たない点から
帰納原理を得て、自然数値の測度へ写すことで一般の状態上の再帰を正当化します。最後に互除法を実装し、
停止性の証明が最大公約数としての正しさをまだ含まないことを確認します。

## 接近可能性は全ての直前要素にも再帰的に要求される

関係 `r : A → A → Prop` を「第一引数が第二引数より小さい」と読みます。`x` が接近可能であるとは、
`r y x` を満たす全ての `y` が接近可能であることです。

$$
\frac{\prod_{y:A}\bigl(r(y,x)\to\mathsf{Acc}(r,y)\bigr)}
     {\mathsf{Acc}(r,x)}
\quad(\mathsf{acc}).
$$

関係が整礎であるとは全ての点が接近可能であることです。最小元が存在するというだけでなく、任意の点から
始めた下降が無限には続かないという再帰的な構造を与えます。
-/

namespace FormalLab.Recursion.WellFounded

universe u

def Predecessor (smaller larger : Nat) : Prop :=
  smaller < larger

theorem naturalPredecessorWellFounded : WellFounded Predecessor :=
  Nat.lt_wfRel.wf

def decreasesBy {A : Type u} (measure : A → Nat) (smaller larger : A) : Prop :=
  measure smaller < measure larger

theorem measureWellFounded {A : Type u} (measure : A → Nat) :
    WellFounded (decreasesBy measure) := by
  exact InvImage.wf measure Nat.lt_wfRel.wf

/-!
`measureWellFounded` は状態そのものを順序づける代わりに、各状態を自然数へ写します。再帰呼出し
`next` について `measure next < measure current` を示せば、自然数の整礎性を状態へ引き戻せます。
測度が単射である必要はありません。同じ測度を持つ別状態へ移る呼出しは、厳密減少を示せないため
この定理では正当化されません。

## 整礎帰納法は全ての小さい場合を仮定する

通常の自然数帰納法は直前の数に対する仮定を使います。整礎帰納法では、`x` より小さい任意の `y` で
性質 `P y` が成り立つと仮定して `P x` を示します。

$$
\frac{\prod_{x:A}\left(\prod_{y:A}r(y,x)\to P(y)\right)\to P(x)}
     {\prod_{x:A}P(x)}
\quad(\text{整礎帰納法}).
$$
-/

theorem strongInductionOnNat (property : Nat → Prop)
    (step : ∀ n, (∀ m, m < n → property m) → property n) :
    ∀ n, property n := by
  intro n
  exact naturalPredecessorWellFounded.induction n (fun x hypothesis => step x hypothesis)

theorem noInfiniteImmediateDescent (n : Nat) : Acc Predecessor n :=
  naturalPredecessorWellFounded.apply n

/-!
`Acc` は有限な最大長を数値として返すのではなく、どの直前要素を選んでも再び接近可能だという木状の
証拠です。分岐が無限でも各枝が有限であり得ます。「有限集合であること」と「関係が整礎であること」を
同一視しません。

## 互除法では第二引数が減少する

`b>0` なら剰余 `a mod b` は `b` より小さいため、第二引数を測度にできます。Leanの
`termination_by` は返り値の性質でなく、再帰呼出しの停止を検査する指定です。
-/

def gcd : Nat → Nat → Nat
  | a, 0 => a
  | a, b + 1 => gcd (b + 1) (a % (b + 1))
termination_by _ b => b
decreasing_by
  exact Nat.mod_lt _ (Nat.zero_lt_succ _)

theorem gcd_48_18 : gcd 48 18 = 6 := by native_decide
theorem gcd_zero_right (a : Nat) : gcd a 0 = a := by simp [gcd]

/-!
一段の不変条件は `gcd(a,b)=gcd(b,a mod b)`、減少量は第二引数です。本章の定義は計算して停止しますが、
返り値が両入力を割り、全ての公約数の倍数であるという最大公約数の仕様は別に証明しなければなりません。
停止証明を関数の数学的正しさと呼ばないことが重要です。

辞書式順序や多重集合順序を使えば、一成分だけでは毎回減らない再帰も扱えます。その場合も必要なのは、
再帰呼出しが選んだ関係で厳密に下降する証明と、その関係自体の整礎性です。

## 要点

* `Acc r x` は `x` の全ての直前要素が再帰的に接近可能であることを表す。
* `WellFounded r` は全ての点が接近可能であり、整礎帰納法と一般再帰を支える。
* 自然数値の測度が各呼出しで厳密減少すれば、自然数の整礎性を状態へ引き戻せる。
* 停止性は無限の再帰呼出しがないことを保証するが、返り値の仕様は別の不変条件を要する。
* 辞書式順序などは複数成分の減少を一つの整礎関係へまとめる。

## 研究史と文献案内

整礎帰納法は順序論・集合論・再帰理論にまたがる原理です。自然数上の強い帰納法と一般の整礎関係による
再帰の型理論的な扱いは [PFPL16] を参照してください。Lean 4の `termination_by` と整礎再帰の現行仕様は
[LEAN-REF] が対象です。Euclidの互除法の古代史と、現代の停止検査アルゴリズムを同じ発明史にまとめません。

## 問題

### 測度を設計して再帰呼出しを検査する

リストから一要素ずつ除く関数、自然数を二で割り続ける関数、二つの自然数を交互に減らす関数について
状態型と自然数値の測度を定めてください。各再帰呼出しの前後の測度を計算し、厳密不等式をLeanで
証明します。等しいままの分岐があれば、測度または状態遷移を修正できれば完了です。
三例の測度が捨てる状態情報と、停止の証明にはその情報が不要な理由も比較してください。

### 接近可能性から帰納原理を展開する

`Acc.rec` または `WellFounded.induction` の型を調べ、`strongInductionOnNat` の各引数へ対応づけて
ください。通常の後者帰納法から強い帰納法を導く証明とも比較します。帰納仮定の量化範囲と、実際に
利用する小さい数を導出木で示し、循環した仮定がないことを説明すれば完了です。

### 互除法の停止性と正しさを分離する

`gcd 48 18` の呼出し列と第二引数の列を書き、各段の剰余不等式を確認してください。次に「返り値が
両数を割る」と「任意の公約数が返り値を割る」を別補題として定式化します。停止証明のどの行からも
これらが直接は得られないことを指摘し、Euclidの補題を追加した帰納証明の構造を示せば完了です。
-/

end FormalLab.Recursion.WellFounded