import FormalLab.Recursion.WellFounded
import FormalLab.Recursion.Lattices
import FormalLab.Recursion.FixedPoints
import FormalLab.Recursion.CoinductivePredicates
import FormalLab.Recursion.DomainTheory

/-!
# 全問題の解答：再帰・不動点・余帰納

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

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

#### ヒント

入力を自然数へ送る測度を選び、すべての再帰呼出しで狭義に減る不等式を示します。

#### 解答

リストを半分ずつ処理する関数なら測度を長さとします。空または一要素で停止し、それ以外では分割した各リストの
長さが元の長さより小さいことを証明します。辞書式再帰では `(m,n)` に辞書式順序を入れ、第一成分が減るか、
第一成分を保って第二成分が減ることを各呼出しで示します。測度の非増加では自己呼出しを排除できないので、
狭義性が必要です。

構文変換では節点数、書換え系では多重集合順序など、計算が実際に消費する資源を測度に選びます。

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

#### ヒント

`Acc r x` の唯一の構成子が、すべての先行者の接近可能性を保持することを使います。

#### 解答

`Acc.intro : (∀y, r y x→Acc r y)→Acc r x` です。`Acc r x` からP xを示すには、その導出へ帰納し、
`h : ∀y,r y x→Acc r y` と各yへの帰納仮定 `P y` を得ます。整礎性 `∀x,Acc r x` があれば、局所ステップ
`∀x,(∀y,r y x→P y)→P x` を任意のxへ適用して `∀x,P x` を得ます。再帰関数でも同じ導出木を辿るため、
無限下降列を作れません。

相互再帰は状態を直和へまとめ、その全体に整礎関係を定義すると一つの原理で扱えます。

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

#### ヒント

停止には剰余の減少、正しさには公約数集合の保存を使います。

#### 解答

`gcd a 0=a`、`gcd a b=gcd b (a%b)` とします。`b>0` なら `a%b<b` なので第二引数を測度にすれば停止します。
正しさは `d∣a ∧ d∣b ↔ d∣b ∧ d∣a%b` を用い、再帰前後で公約数が一致することから示します。停止証明だけでは
返り値が最大公約数だとは分からず、公約数保存だけでも再帰が値を返すとは分かりません。二つは異なる不変条件です。

アルゴリズム検証では変種関数を停止へ、ループ不変量を部分正当性へ割り当てます。

## 第27章：束・完備格子・単調作用素

### 問題1：二項演算から普遍性を復元する

#### ヒント

`x⊓y` が下界である二条件と、任意の下界がそれ以下である条件を書きます。

#### 解答

交わりmは `m≤x`、`m≤y` を満たし、任意のzについて `z≤x∧z≤y→z≤m` を満たします。この三条件からmは一意です。
結びjは順序を反転して `x≤j`、`y≤j`、`x≤z∧y≤z→j≤z` です。吸収則などの代数法則はこの普遍性から、
両辺が同じ下界または上界を分類することにより導けます。演算記号だけでなく比較対象全体への最良性が本体です。

積・余積や極限・余極限でも、候補の構成と任意対象からの一意な比較を同じ順で確認します。

### 問題2：空族を含む任意上限・下限を計算する

#### ヒント

空族の上界・下界条件は空虚に真になることから最小・最大要素を求めます。

#### 解答

完備格子では任意の部分集合Sに `sSup S` と `sInf S` があります。冪集合格子では上限は和集合、下限は共通部分です。
空族の和集合は空集合で、すべての集合の下にある最小元です。空族の共通部分は全体集合で、すべての集合の上にある
最大元です。従って任意上限の存在は底、任意下限の存在は頂を含み、「非空族だけ」の完備性とは異なります。

零項の積と余積が終対象と始対象になることを、空族の極限・余極限として読み替えます。

### 問題3：作用素の単調性を正例と反例で判定する

#### ヒント

`X⊆Y→F X⊆F Y` を要素ごとに示し、否定位置へXが現れる作用素を反例候補にします。

#### 解答

固定集合Aに対する `F(X)=A∪X` は、X⊆YならA∪X⊆A∪Yなので単調です。逆像作用素も所属を関数適用へ展開すれば
単調です。一方 `G(X)=A\X` は反単調です。例えばAが一要素集合で `∅⊆A` ですが、`G(∅)=A` は
`G(A)=∅` に包含されません。述語変数が含意の前件や否定の下に現れると向きが反転します。

帰納的定義の規則形式を設計するとき、定義対象が正の位置だけに現れることを単調性として検査します。

## 第28章：最小・最大不動点とKnaster–Tarski定理

### 問題1：最小不動点証明の二度の単調性を追う

#### ヒント

前固定点全体の下限 `μF` に対し、まず `F(μF)≤μF`、次に逆向きを示します。

#### 解答

`μF=inf {X | F X≤X}` とします。各前固定点Xへ `μF≤X` なので単調性から `F(μF)≤F X≤X` です。従って
`F(μF)` は全前固定点の下界であり `F(μF)≤μF`。この結果へ単調性をもう一度使うと
`F(F(μF))≤F(μF)` なので `F(μF)` 自身が前固定点です。下限の定義から `μF≤F(μF)`。よって等号です。

証明支援系では前固定点の下限、閉性、最小性を別補題にし、向きの取り違えを型で検出します。

#### 補足

最初の単調性は `F(μF)` が全前固定点の下界であることを作り、二度目の単調性は `F(μF)` 自身が前固定点で
あるという資格を作ります。同じ仮定を二度使っていても、得ている事実の種類は異なります。最大不動点では順序を
反転し、後固定点の上限から始めます。その際も「上界」と「後固定点」という二つの資格を区別します。

### 問題2：帰納的生成を別の規則へ移す

#### ヒント

偶数を0と「2を足す」規則で生成し、その規則作用素の最小不動点として表します。

#### 解答

`F(X)={0}∪{n+2 | n∈X}` と置きます。Fは単調で、最小不動点μFは0を含み、要素へ2を足して閉じています。
帰納法は、集合Pが0を含み2加算で閉じる、すなわち `F(P)⊆P` なら `μF⊆P` という最小性です。これにより
μFの全要素が2で割り切れることを示せます。逆に各 `2k` がμFに属することはkへの自然数帰納法で示します。

到達可能状態や構文の導出可能性も、初期事実と閉包規則が作る最小不動点として扱えます。

### 問題3：最大不動点を直接に特徴づける

#### ヒント

後固定点の上限 `νF=sup {X | X≤F X}` を用い、等式の両方向を追います。

#### 解答

各後固定点Xについて `X≤νF` なので単調性から `X≤F X≤F(νF)`。従ってF(νF)は全後固定点の上界で
`νF≤F(νF)` です。単調性から `F(νF)≤F(F(νF))` となり、F(νF)も後固定点です。上限の定義により
`F(νF)≤νF`、従って不動点です。任意の不動点は後固定点なのでνF以下で、最大性も確認できます。

安全性や無限振る舞いをνFで定義するとき、余帰納法は `X≤F X→X≤νF` という最大性として使います。

## 第29章：最大不動点・余帰納的述語・双模倣

### 問題1：常時安全性を有限観察へ展開する

#### ヒント

安全状態集合Sに対し `F(X)={s∈S | すべての一歩後続がXに属す}` と置きます。

#### 解答

常時安全な状態はνFです。`s∈νF` なら不動点等式からsは安全で、すべての後続が再びνFに属します。これをn回
繰り返すと任意の有限実行接頭辞の全状態がSに属します。逆に、すべての有限接頭辞が安全な状態の集合Xは、
一歩後続から始めた有限接頭辞も安全なので `X⊆F(X)`。余帰納法から `X⊆νF` です。

モデル検査では有限深さ近似を下降列で計算し、有限状態なら安定した段階が最大不動点になります。

### 問題2：余帰納不変量を小さく選ぶ

#### ヒント

証明したい状態だけでなく、その後続として実際に現れる状態を閉じる最小限の集合を候補にします。

#### 解答

二状態が交互に遷移する系 `a→b→a` の常時安全性なら、候補Rを `{a}` にするとaの後続bを含まず
`R⊆F R` が失敗します。`R={a,b}` なら両状態が安全で後続もR内なので後固定点です。全状態集合を選んでもよい
場合がありますが、危険状態を含めれば安全条件で失敗します。到達閉包を基礎に小さい候補を選ぶと、必要な義務が
減り反例も見えます。

双模倣関係でも対象の一対だけで閉じなければ、その遷移先の対を加えて関係を閉じます。

### 問題3：双模倣と単なる観察一致を分ける

#### ヒント

現在の出力は同じでも、次状態の出力が異なる二状態を作ります。

#### 解答

状態pとqがともに0を出力し、pは永遠に0を出す状態へ、qは次に1を出す状態へ遷移するとします。現在の観察だけなら
pとqは一致します。しかし双模倣には出力一致に加え、各遷移を相手が模倣し、後続対も同じ関係に属することが
必要です。後続の出力が0と1なので、この対を含む双模倣はありません。決定的ストリーム系では双模倣から全有限
接頭辞の一致が従い、その逆も成り立ちます。

非決定系では一つの実行列の一致では足りず、分岐する各遷移への往復条件を検査します。

## 第30章：領域理論・連続写像・再帰方程式

### 問題1：反復列の上限が固定される証明を分解する

#### ヒント

`x₀=⊥`、`x_{n+1}=F x_n` とし、連続性がω鎖の上限を保存する式を使います。

#### 解答

単調性から `x₀≤x₁≤…` です。`x=sup_n x_n` と置くと、ω連続性により
`F x=F(sup_n x_n)=sup_n F(x_n)=sup_n x_{n+1}=x` です。最後の等号は先頭の⊥を除いても上限が変わらないためです。
さらに任意の不動点yについて、⊥≤yから帰納的に `x_n≤y`。従ってx≤yであり、xは最小不動点です。

再帰プログラムの有限展開をx_nと見れば、意味はすべての有限近似の上限として構成できます。

### 問題2：平坦順序のω鎖を分類する

#### ヒント

底⊥以外の異なる二値は比較不能であることを使います。

#### 解答

平坦領域 `A⊥` では `⊥≤a` だけを追加し、異なるa,bは比較不能です。上昇ω鎖は、すべて⊥であるか、ある段階まで
⊥で、その後は同じ値aに固定されるしかありません。aの後に異なるbへ移れば `a≤b` が必要となり矛盾します。
前者の上限は⊥、後者の上限はaです。この順序は「未定義から一つの確定値へ」という情報増加を表します。

部分関数空間では各入力点で同じ分類を行い、点ごとの情報増加として近似順序を読みます。

### 問題3：燃料近似を意味論的近似へ接続する

#### ヒント

n段まで再帰を展開する評価器を定義し、燃料増加で得られる結果の情報が減らないことを示します。

#### 解答

燃料0では⊥を返し、n+1では関数本体を一段展開して再帰呼出しへ燃料nを渡します。近似 `eval_n` は
`eval_n≤eval_{n+1}` を満たすω鎖です。ある有限段で値vを返せば平坦順序により以後もvで、どの段でも返らなければ
上限は⊥です。意味論的評価を `sup_n eval_n` と定めると、有限停止計算の値と一致し、発散は⊥になります。

ステップ添字付き論理関係でも、燃料を残り観察深度として使い、極限で無限振る舞いを捉えます。

-/

namespace FormalLab.Appendix.Solutions.Chapter026Exercise001

theorem halfDecreases {n : Nat} (positive : 0 < n) : n / 2 < n := by
  omega

theorem alternatingMeasureDecreasesLeft {left right : Nat} (positive : 0 < left) :
    (left - 1) + right < left + right := by
  omega

theorem alternatingMeasureDecreasesRight {left right : Nat} (positive : 0 < right) :
    left + (right - 1) < left + right := by
  omega

end FormalLab.Appendix.Solutions.Chapter026Exercise001

namespace FormalLab.Appendix.Solutions.Chapter026Exercise002

#check Acc.rec
#check WellFounded.induction
#check FormalLab.Recursion.WellFounded.strongInductionOnNat

end FormalLab.Appendix.Solutions.Chapter026Exercise002

namespace FormalLab.Appendix.Solutions.Chapter026Exercise003

open FormalLab.Recursion.WellFounded

#eval gcd 48 18

example : gcd 48 18 = 6 := by native_decide

end FormalLab.Appendix.Solutions.Chapter026Exercise003

namespace FormalLab.Appendix.Solutions.Chapter027Exercise003

open FormalLab.Recursion.Lattices

def reachableStep (start : Nat) (step : Nat → Nat → Prop)
    (set : PredSet Nat) : PredSet Nat :=
  fun y => y = start ∨ ∃ x, set x ∧ step x y

theorem reachableStepMonotone (start : Nat) (step : Nat → Nat → Prop) :
    Monotone (reachableStep start step) := by
  intro left right included y generated
  rcases generated with atStart | ⟨x, member, moves⟩
  · exact Or.inl atStart
  · exact Or.inr ⟨x, included member, moves⟩

end FormalLab.Appendix.Solutions.Chapter027Exercise003

namespace FormalLab.Appendix.Solutions.Chapter029Exercise001

open FormalLab.Recursion.CoinductivePredicates

def iterate (next : A → A) : Nat → A → A
  | 0, state => state
  | time + 1, state => iterate next time (next state)

theorem Always_at {A : Type} {good : A → Prop} {next : A → A} {state : A}
    (always : Always good next state) : ∀ time, good (iterate next time state) := by
  intro time
  induction time generalizing state with
  | zero => exact Always_now always
  | succ time inductionHypothesis =>
      exact inductionHypothesis (Always_next always)

end FormalLab.Appendix.Solutions.Chapter029Exercise001

namespace FormalLab.Appendix.Solutions.Chapter029Exercise002

open FormalLab.Recursion.CoinductivePredicates

inductive Phase where | zero | one | two deriving DecidableEq

def next : Phase → Phase
  | .zero => .one
  | .one => .two
  | .two => .zero

def safe : Phase → Prop
  | .zero | .one => True
  | .two => False

def invariant : Phase → Prop
  | .zero | .one => True
  | .two => False

example : ¬Always safe next .zero := by
  intro always
  have afterTwo := Always_next (Always_next always)
  exact Always_now afterTwo

end FormalLab.Appendix.Solutions.Chapter029Exercise002

namespace FormalLab.Appendix.Solutions.Chapter030Exercise002

open FormalLab.Recursion.DomainTheory

example : FlatLe (none : Option Bool) (some true) := by
  trivial

example : ¬FlatLe (some true) (some false) := by
  simp [FlatLe]

end FormalLab.Appendix.Solutions.Chapter030Exercise002

namespace FormalLab.Appendix.Solutions.Chapter030Exercise003

open FormalLab.Recursion.DomainTheory

example : factorialApproximation 3 3 = none := rfl
example : factorialApproximation 4 3 = some 6 := rfl
example : FlatLe (factorialApproximation 3 3) (factorialApproximation 4 3) := by
  trivial

end FormalLab.Appendix.Solutions.Chapter030Exercise003