58 lines
1.8 KiB
Lean4
58 lines
1.8 KiB
Lean4
import Spa.Lattice
|
||
|
||
namespace Spa
|
||
|
||
namespace Fixedpoint
|
||
|
||
open FiniteHeightLattice (height)
|
||
|
||
variable {α : Type*} [DecidableEq α] [FiniteHeightLattice α]
|
||
|
||
def doStep (f : α → α) (hf : Monotone f) :
|
||
∀ (g : ℕ) (c : LTSeries α), c.length + g = height (α := α) + 1 →
|
||
c.last ≤ f c.last → {a : α // a = f a}
|
||
| 0, c, hlen, _ =>
|
||
absurd (FiniteHeightLattice.chains_bounded c) (by simp only [height] at hlen; omega)
|
||
| g + 1, c, hlen, hle =>
|
||
if heq : c.last = f c.last then
|
||
⟨c.last, heq⟩
|
||
else
|
||
doStep f hf g (c.snoc (f c.last) (lt_of_le_of_ne hle heq))
|
||
(by simp [RelSeries.snoc]; omega)
|
||
(by rw [RelSeries.last_snoc]; exact hf hle)
|
||
|
||
def fix (f : α → α) (hf : Monotone f) : {a : α // a = f a} :=
|
||
doStep f hf (height (α := α) + 1) (RelSeries.singleton _ ⊥)
|
||
(by simp)
|
||
(by simpa [RelSeries.last_singleton]
|
||
using FiniteHeightLattice.bot_le α (f ⊥))
|
||
|
||
def aFix (f : α → α) (hf : Monotone f) : α :=
|
||
(fix f hf).1
|
||
|
||
theorem aFix_eq (f : α → α) (hf : Monotone f) :
|
||
aFix f hf = f (aFix f hf) :=
|
||
(fix f hf).2
|
||
|
||
lemma doStep_le (f : α → α) (hf : Monotone f)
|
||
{b : α} (hb : b = f b) :
|
||
∀ (g : ℕ) (c : LTSeries α) (hlen : c.length + g = height (α := α) + 1)
|
||
(hle : c.last ≤ f c.last), c.last ≤ b →
|
||
(doStep f hf g c hlen hle : α) ≤ b
|
||
| 0, c, hlen, _ => fun _ =>
|
||
absurd (FiniteHeightLattice.chains_bounded c) (by simp only [height] at hlen; omega)
|
||
| g + 1, c, hlen, hle => fun hcb => by
|
||
rw [doStep]
|
||
split
|
||
· exact hcb
|
||
· exact doStep_le f hf hb g _ _ _
|
||
(by rw [RelSeries.last_snoc]; exact le_of_le_of_eq (hf hcb) hb.symm)
|
||
|
||
theorem aFix_le (f : α → α) (hf : Monotone f)
|
||
{a : α} (ha : a = f a) : aFix f hf ≤ a :=
|
||
doStep_le f hf ha _ _ _ _ (by simpa using FiniteHeightLattice.bot_le α a)
|
||
|
||
end Fixedpoint
|
||
|
||
end Spa
|