Lean migration: Phases 0-2 (core lattice/chain, fixpoint, transport)

- lean/ lake project pinned to Lean v4.17.0 + mathlib v4.17.0 - Spa.Lattice: fold monotonicity, FixedHeight/BoundedChains (LTSeries-based), FiniteHeightLattice, chain-bottom-is-least; the rest of Lattice.agda, Chain.agda and Equivalence.agda lift into mathlib (see LEAN_MIGRATION.md) - Spa.Fixedpoint: gas-based least-fixpoint computation (doStep/fix/aFix) - Spa.Isomorphism: FixedHeight transport along monotone inverse pairs Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-06-09 18:36:43 -07:00
parent 1c2bcc2d92
commit ae030386b4
9 changed files with 464 additions and 0 deletions
--- a/LEAN_MIGRATION.md
+++ b/LEAN_MIGRATION.md
@@ -0,0 +1,83 @@
+# Agda → Lean 4 (mathlib) migration plan
+
+Goal: port the static-analysis framework to Lean 4 + mathlib, preserving the
+overall structure and **the same theorems/lemmas** (modulo language details),
+while lifting custom machinery into mathlib wherever a standard counterpart
+exists. Per discussion, the setoid equality (`_≈_`) is **dropped in favor of
+propositional `=`** — it existed mainly so that unordered key-value maps could
+be "equal"; representations below are chosen to be canonical so `=` works.
+
+The Lean project lives in `lean/` (library root `Spa`). Each phase ends with a
+green `lake build` and a correspondence table appended to this file, so you can
+validate phase by phase.
+
+## Design mapping
+
+| Agda | Lean | Notes |
+|---|---|---|
+| `Equivalence.agda` | *lifted*: `Eq`, `Equivalence` | module disappears |
+| `IsDecidable` | *lifted*: `DecidableEq` / `DecidableRel` | mathlib is classical; decidability kept only where functions compute (e.g. the fixpoint iteration) |
+| `Showable.agda` | *lifted*: `ToString` | |
+| `Lattice.agda` `IsSemilattice` (`⊔-assoc/comm/idemp`, `≼`, `≼-refl/trans/antisym`, `x≼x⊔y`, `⊔-Monotonicˡ/ʳ`) | *lifted*: `SemilatticeSup` (`sup_assoc`, `sup_comm`, `sup_idem`, `≤` with `sup_eq_right`, `le_refl`, `le_trans`, `le_antisymm`, `le_sup_left`, `sup_le_sup_left/right`) | `a ≼ b := a ⊔ b ≈ b` becomes `a ≤ b` with bridge lemma `sup_eq_right` |
+| `IsLattice` (`absorb-⊔-⊓`, `absorb-⊓-⊔`) | *lifted*: `Lattice` (`sup_inf_self`, `inf_sup_self`) | |
+| `Monotonic`, `Monotonicˡ/ʳ/₂` | *lifted*: `Monotone` (+ tiny aliases) | |
+| `foldr-Mono`, `foldl-Mono`, `foldr-Mono'`, `foldl-Mono'` | custom, `Spa/Lattice.lean` | stated with `List.Forall₂` (≙ `Utils.Pairwise`) |
+| `Chain.agda` (`Chain`, `concat`, `Chain-map` in `ChainMapping`) | *lifted*: `LTSeries` (`RelSeries.smash`, `LTSeries.map` + `Monotone.strictMono_of_injective`) | with `=`, the ≈-congruence steps in chains vanish |
+| `Chain.Height`, `Bounded`, `Bounded-suc-n` | custom: `Spa.FixedHeight` structure (`⊥`, `⊤`, longest `LTSeries`, `bounded`) | |
+| `IsFiniteHeightLattice`, `FiniteHeightLattice` | custom class `Spa.FiniteHeightLattice` | |
+| `⊥≼` (chain bottom is least, given decidable eq) | custom, same proof shape (prepend `⊥⊓a ≺ ⊥` to longest chain) | decidability hypothesis dropped (classical) |
+| `Fixedpoint.agda` (`doStep` with gas, `aᶠ`, `aᶠ≈faᶠ`, `aᶠ≼`) | custom, `Spa/Fixedpoint.lean`, same gas-based algorithm | **not** replaced by mathlib `lfp` (would change the proof approach and lose computability) |
+| `Isomorphism.agda` (`TransportFiniteHeight`) | custom, `Spa/Isomorphism.lean` | much smaller: with `=`, f/g monotone inverse pair transports `FixedHeight` via `LTSeries.map` |
+| `Lattice/Unit.agda` | *lifted*: mathlib `Lattice PUnit`; custom `FixedHeight PUnit 0` | |
+| `Lattice/Nat.agda` (max/min lattice) | *lifted*: mathlib `Lattice ℕ` (`Nat.instLattice`) | kept only as a remark; file had no fixed-height content |
+| `Lattice/Prod.agda` | instance *lifted* (`Prod.instLattice`); custom: `unzip` + `FixedHeight (A×B) (h₁+h₂)` | same proof: split a product chain into component chains |
+| `Lattice/AboveBelow.agda` (flat lattice ⊥/[x]/⊤) | custom, same datatype; `Plain` module ⇒ `FixedHeight 2` | mathlib has no flat-lattice-on-discrete-type |
+| `Lattice/ExtendBelow.agda` | *lifted*: `WithBot A` lattice instance; custom `FixedHeight (h+1)` | unused by the pipeline; ported for parity (optional) |
+| `Lattice/IterProd.agda` | custom, same induction (`IterProd k = A × … × B`), lattice + height-sum by recursion | the `Everything` record trick survives as a recursive definition of bundled instances |
+| `Lattice/Map.agda` (assoc list with `Unique` keys, setoid) | **deleted**: only existed to support setoid map equality | its consumers move to `Finset` / spine-fixed `FiniteMap` |
+| `Lattice/MapSet.agda` (`StringSet`) | *lifted*: `Finset String` (`∪`, `{·}`, `∅`, `.toList`, `nodup_toList`) | |
+| `Lattice/FiniteMap.agda` | custom: `{ l : List (A × B) // l.map Prod.fst = ks }` — key spine fixed ⇒ `=` is pointwise value equality | same API: `locate`, `_[_]`, `GeneralizedUpdate` (`f'`, `f'-Monotonic`, `f'-k∈ks-≡`, `f'-k∉ks-backward`), `m₁≼m₂⇒m₁[k]≼m₂[k]`, `Provenance-union` analog; fixed height **still via isomorphism to `IterProd`** (same approach) |
+| `Lattice/Builder.agda` | **skipped** — not imported by anything in the repo | flag if you want it |
+| `Utils.agda` | *lifted*: `Unique`→`List.Nodup`, `Pairwise`→`List.Forall₂`, `fins`→`List.finRange`, `∈-cartesianProduct`→`List.product`/`pair_mem_product`, `x∈xs⇒fx∈fxs`→`List.mem_map_of_mem`, `filter-++`→`List.filter_append`, `iterate`→`f^[n]`, `concat-∈`→`List.mem_join`, `All¬-¬Any` etc. → `List.All`/`Any` API | leftovers (if any) in `Spa/Utils.lean` |
+| `Language/Base.agda` | custom; `Expr-vars`/`Stmt-vars : Finset String` | commented-out `∈-vars` lemmas stay omitted |
+| `Language/Semantics.agda` | custom, same big-step relations; `Value`, `Env = List (String × Value)`, custom `∈` | `ℤ` → `Int` |
+| `Language/Graphs.agda` | custom; `Vec` → `Vector` (mathlib `List.Vector`), `Fin._↑ˡ/_↑ʳ` → `Fin.castAdd`/`Fin.natAdd` | same `Graph` record, `∙`/`↦`/`loop`/`skipto`/`singleton`/`wrap`/`buildCfg`, `predecessors` + edge lemmas |
+| `Language/Traces.agda` | custom, same `Trace`/`EndToEndTrace`/`++⟨_⟩` | |
+| `Language/Properties.agda` | custom, same lemma inventory (`Trace-∙ˡ/ʳ`, `Trace-↦ˡ/ʳ`, `Trace-loop`, `EndToEndTrace-*`, `wrap-preds-∅`, `buildCfg-sufficient`) | the "ugly" `↑-≢` Fin-disjointness block should shrink via `Fin.castAdd_ne_natAdd`-style mathlib lemmas |
+| `Language.agda` (`Program` record) | custom, same fields/lemmas (`trace`, `vars`, `states`, `incoming`, `initialState-pred-∅`, …) | |
+| `Analysis/Forward/{Lattices,Evaluation,Adapters}.agda`, `Analysis/Forward.agda` | custom, same structure: `VariableValues`, `StateVariables`, `joinForKey`/`joinAll`, `StmtEvaluator`/`ExprEvaluator` + validity, expr→stmt adapter, `analyze`, `result`, `analyze-correct` | section variables instead of parameterized modules |
+| `Analysis/Sign.agda`, `Analysis/Constant.agda` | custom, same definitions | the four monotonicity **postulates** become real proofs by `decide` (finite lattice, decidable `≤`) |
+| `Main.agda` | `lake exe spa` | same test programs, same printed output |
+
+## Phases & checkpoints
+
+- **Phase 0 — scaffold.** `lean/` lake project, mathlib pinned to toolchain
+  v4.17.0 (already installed). ✅ checkpoint: `lake build` green on empty lib.
+- **Phase 1 — core order theory.** `Spa/Lattice.lean` (Monotone aliases, fold
+  monotonicity, `FixedHeight`, `Bounded`, `FiniteHeightLattice`, chain-bottom-
+  is-least). ✅ checkpoint: build + table below.
+- **Phase 2 — fixpoint & transport.** `Spa/Fixedpoint.lean`,
+  `Spa/Isomorphism.lean`. ✅ checkpoint: `fix`, `fix_eq`, `fix_le`,
+  `TransportFiniteHeight`.
+- **Phase 3 — basic lattice instances.** Unit, Prod (+height), AboveBelow
+  (+`Plain`, height 2), ExtendBelow. ✅ checkpoint.
+- **Phase 4 — map lattices.** IterProd, FiniteMap (+fixed height via IterProd
+  isomorphism), MapSet→`Finset` shims. ✅ checkpoint.
+- **Phase 5 — language.** Base, Semantics, Graphs, Traces, Properties,
+  `Program`. ✅ checkpoint: `buildCfg_sufficient`, `Program.trace`.
+- **Phase 6 — forward analysis framework.** Lattices/Evaluation/Adapters/
+  Forward. ✅ checkpoint: `analyze_correct`.
+- **Phase 7 — concrete analyses + executable.** Sign, Constant, Main.
+  ✅ checkpoint: `lake exe spa` output vs Agda `Main` output; postulates now
+  proved.
+
+## Status
+
+- [x] Phase 0
+- [ ] Phase 1
+- [ ] Phase 2
+- [ ] Phase 3
+- [ ] Phase 4
+- [ ] Phase 5
+- [ ] Phase 6
+- [ ] Phase 7
--- a/lean/.gitignore
+++ b/lean/.gitignore
@@ -0,0 +1 @@
+.lake/
--- a/lean/Spa.lean
+++ b/lean/Spa.lean
@@ -0,0 +1,3 @@
+import Spa.Lattice
+import Spa.Fixedpoint
+import Spa.Isomorphism
--- a/lean/Spa/Fixedpoint.lean
+++ b/lean/Spa/Fixedpoint.lean
@@ -0,0 +1,75 @@
+/-
+Port of `Fixedpoint.agda`.
+
+Same gas-based algorithm: iterate `f` starting at the chain-bottom `⊥`; since
+the lattice has fixed height `h`, a fixed point must be reached within `h + 1`
+steps, or we would build a `<`-chain longer than the longest one. We
+deliberately do *not* use mathlib's `OrderHom.lfp` (different proof approach,
+and not computable).
+
+Correspondence:
+  doStep             ↦ Spa.Fixedpoint.doStep   (the chain argument now carries
+                                                 `a₁ = ⊥` and its length in the
+                                                 `LTSeries` structure itself)
+  fix                ↦ Spa.Fixedpoint.fix
+  aᶠ                 ↦ Spa.Fixedpoint.aFix
+  aᶠ≈faᶠ             ↦ Spa.Fixedpoint.aFix_eq
+  stepPreservesLess  ↦ Spa.Fixedpoint.doStep_le
+  aᶠ≼                ↦ Spa.Fixedpoint.aFix_le
+-/
+import Spa.Lattice
+
+namespace Spa.Fixedpoint
+
+variable {α : Type*} [Lattice α] [DecidableEq α] {h : ℕ}
+
+/-- Agda: `doStep`. `g` is gas; the invariant `c.length + g = h + 1` guarantees
+that when gas runs out the chain contradicts boundedness. -/
+def doStep (fh : FixedHeight α h) (f : α → α) (hf : Monotone f) :
+    ∀ (g : ℕ) (c : LTSeries α), c.length + g = h + 1 →
+      c.last ≤ f c.last → {a : α // a = f a}
+  | 0, c, hlen, _ =>
+    absurd (fh.bounded c) (by omega)
+  | g + 1, c, hlen, hle =>
+    if heq : c.last = f c.last then
+      ⟨c.last, heq⟩
+    else
+      doStep fh 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)
+
+/-- Agda: `fix`. Start iterating from `⊥`. -/
+def fix (fh : FixedHeight α h) (f : α → α) (hf : Monotone f) : {a : α // a = f a} :=
+  doStep fh f hf (h + 1) (RelSeries.singleton _ fh.bot)
+    (by simp)
+    (by simpa [RelSeries.last_singleton] using fh.bot_le (f fh.bot))
+
+/-- Agda: `aᶠ`. -/
+def aFix (fh : FixedHeight α h) (f : α → α) (hf : Monotone f) : α :=
+  (fix fh f hf).1
+
+/-- Agda: `aᶠ≈faᶠ`. -/
+theorem aFix_eq (fh : FixedHeight α h) (f : α → α) (hf : Monotone f) :
+    aFix fh f hf = f (aFix fh f hf) :=
+  (fix fh f hf).2
+
+/-- Agda: `stepPreservesLess` — iteration stays below any fixed point. -/
+theorem doStep_le (fh : FixedHeight α h) (f : α → α) (hf : Monotone f)
+    {b : α} (hb : b = f b) :
+    ∀ (g : ℕ) (c : LTSeries α) (hlen : c.length + g = h + 1)
+      (hle : c.last ≤ f c.last), c.last ≤ b →
+      (doStep fh f hf g c hlen hle : α) ≤ b
+  | 0, c, hlen, _ => fun _ => absurd (fh.bounded c) (by omega)
+  | g + 1, c, hlen, hle => fun hcb => by
+    rw [doStep]
+    split
+    · exact hcb
+    · exact doStep_le fh f hf hb g _ _ _
+        (by rw [RelSeries.last_snoc]; exact le_of_le_of_eq (hf hcb) hb.symm)
+
+/-- Agda: `aᶠ≼` — `aFix` is below every fixed point of `f`. -/
+theorem aFix_le (fh : FixedHeight α h) (f : α → α) (hf : Monotone f)
+    {a : α} (ha : a = f a) : aFix fh f hf ≤ a :=
+  doStep_le fh f hf ha _ _ _ _ (by simpa using fh.bot_le a)
+
+end Spa.Fixedpoint
--- a/lean/Spa/Isomorphism.lean
+++ b/lean/Spa/Isomorphism.lean
@@ -0,0 +1,58 @@
+/-
+Port of `Isomorphism.agda` (`TransportFiniteHeight`).
+
+With propositional equality this module shrinks dramatically: the Agda
+hypotheses `f-preserves-≈`, `g-preserves-≈` are free, and `f-⊔-distr` /
+`g-⊔-distr` (which in the setoid world encoded monotonicity of `f` and `g`
+w.r.t. the derived order) become plain `Monotone` hypotheses. The chain
+transport `portChain₁` / `portChain₂` is mathlib's `LTSeries.map`, using that
+a monotone injective map between partial orders is strictly monotone.
+
+Correspondence:
+  IsInverseˡ / IsInverseʳ     ↦ explicit inverse hypotheses `hfg` / `hgf`
+  f-Injective / g-Injective   ↦ local `Function.LeftInverse.injective`
+  portChain₁ / portChain₂     ↦ LTSeries.map
+  instance fixedHeight        ↦ Spa.FixedHeight.transport
+  isFiniteHeightLattice,
+  finiteHeightLattice         ↦ Spa.FiniteHeightLattice.transport
+-/
+import Spa.Lattice
+
+namespace Spa
+
+namespace FixedHeight
+
+variable {α β : Type*} [PartialOrder α] [PartialOrder β] {h : ℕ}
+
+/-- Agda: `TransportFiniteHeight.fixedHeight`. Transport a `FixedHeight`
+structure along a monotone inverse pair `f : α → β`, `g : β → α`. -/
+def transport (fh : FixedHeight α h) (f : α → β) (g : β → α)
+    (hf : Monotone f) (hg : Monotone g)
+    (hgf : ∀ a, g (f a) = a) (hfg : ∀ b, f (g b) = b) :
+    FixedHeight β h where
+  bot := f fh.bot
+  top := f fh.top
+  longestChain :=
+    fh.longestChain.map f
+      (hf.strictMono_of_injective (Function.LeftInverse.injective hgf))
+  head_longestChain := by
+    rw [LTSeries.head_map, fh.head_longestChain]
+  last_longestChain := by
+    rw [LTSeries.last_map, fh.last_longestChain]
+  length_longestChain := fh.length_longestChain
+  bounded := fun c =>
+    fh.bounded
+      (c.map g (hg.strictMono_of_injective (Function.LeftInverse.injective hfg)))
+
+end FixedHeight
+
+/-- Agda: `TransportFiniteHeight.finiteHeightLattice`. -/
+def FiniteHeightLattice.transport {α β : Type*} [Lattice α] [Lattice β]
+    (I : FiniteHeightLattice α) (f : α → β) (g : β → α)
+    (hf : Monotone f) (hg : Monotone g)
+    (hgf : ∀ a, g (f a) = a) (hfg : ∀ b, f (g b) = b) :
+    FiniteHeightLattice β where
+  height := I.height
+  fixedHeight := I.fixedHeight.transport f g hf hg hgf hfg
+
+end Spa
--- a/lean/Spa/Lattice.lean
+++ b/lean/Spa/Lattice.lean
@@ -0,0 +1,138 @@
+/-
+Port of `Lattice.agda`.
+
+Most of the Agda module is *lifted* into mathlib, since we now work with
+propositional equality instead of a setoid:
+
+  IsSemilattice A _≈_ _⊔_   ↦  SemilatticeSup α
+  IsLattice A _≈_ _⊔_ _⊓_   ↦  Lattice α
+  _≼_ (a ⊔ b ≈ b)           ↦  a ≤ b           (bridge: `sup_eq_right`)
+  _≺_                       ↦  a < b
+  Monotonic                 ↦  Monotone
+  ⊔-assoc/⊔-comm/⊔-idemp    ↦  sup_assoc/sup_comm/sup_idem
+  absorb-⊔-⊓/absorb-⊓-⊔     ↦  sup_inf_self/inf_sup_self
+  ≼-refl/≼-trans/≼-antisym  ↦  le_refl/le_trans/le_antisymm
+  x≼x⊔y                     ↦  le_sup_left
+  ⊔-Monotonicˡ/ʳ            ↦  sup_le_sup_left/sup_le_sup_right
+  id-Mono/const-Mono        ↦  monotone_id/monotone_const
+  IsDecidable               ↦  DecidableEq (kept only where computation needs it)
+  Chain (Chain.agda)        ↦  LTSeries (chains of `<`); concat ↦ RelSeries.smash
+  ChainMapping.Chain-map    ↦  LTSeries.map (Monotone + Injective ⇒ StrictMono)
+
+What remains custom is exactly what mathlib does not have:
+  * monotonicity of folds over pairwise-related lists (foldr-Mono & friends),
+  * the fixed-height machinery (Chain.Height ↦ FixedHeight, Bounded),
+  * the proof that the bottom of the longest chain is a least element (⊥≼).
+-/
+import Mathlib.Order.Lattice
+import Mathlib.Order.RelSeries
+
+namespace Spa
+
+/-! ### Monotonicity helpers (Lattice.agda, `Monotonic₂` and fold lemmas) -/
+
+/-- Agda: `Monotonic₂` (a pair of one-sided monotonicity proofs). -/
+def Monotone₂ {α β γ : Type*} [Preorder α] [Preorder β] [Preorder γ]
+    (f : α → β → γ) : Prop :=
+  (∀ b, Monotone fun a => f a b) ∧ (∀ a, Monotone (f a))
+
+section Folds
+
+variable {α β : Type*} [Preorder α] [Preorder β]
+
+/-- Agda: `foldr-Mono`. `Pairwise _≼₁_` becomes `List.Forall₂ (· ≤ ·)`. -/
+theorem foldr_mono {l₁ l₂ : List α} (f : α → β → β) {b₁ b₂ : β}
+    (hl : List.Forall₂ (· ≤ ·) l₁ l₂) (hb : b₁ ≤ b₂)
+    (hf₁ : ∀ b, Monotone fun a => f a b) (hf₂ : ∀ a, Monotone (f a)) :
+    l₁.foldr f b₁ ≤ l₂.foldr f b₂ := by
+  induction hl with
+  | nil => exact hb
+  | cons hxy _ ih =>
+    exact le_trans (hf₁ _ hxy) (hf₂ _ ih)
+
+/-- Agda: `foldl-Mono`. -/
+theorem foldl_mono {l₁ l₂ : List α} (f : β → α → β) {b₁ b₂ : β}
+    (hl : List.Forall₂ (· ≤ ·) l₁ l₂) (hb : b₁ ≤ b₂)
+    (hf₁ : ∀ a, Monotone fun b => f b a) (hf₂ : ∀ b, Monotone (f b)) :
+    l₁.foldl f b₁ ≤ l₂.foldl f b₂ := by
+  induction hl generalizing b₁ b₂ with
+  | nil => exact hb
+  | cons hxy _ ih =>
+    exact ih (le_trans (hf₁ _ hb) (hf₂ _ hxy))
+
+omit [Preorder α] in
+/-- Agda: `foldr-Mono'` (fixed list, varying accumulator). -/
+theorem foldr_mono' (l : List α) (f : α → β → β)
+    (hf : ∀ a, Monotone (f a)) : Monotone fun b => l.foldr f b := by
+  intro b₁ b₂ hb
+  induction l with
+  | nil => exact hb
+  | cons x xs ih => exact hf x ih
+
+omit [Preorder α] in
+/-- Agda: `foldl-Mono'`. -/
+theorem foldl_mono' (l : List α) (f : β → α → β)
+    (hf : ∀ a, Monotone fun b => f b a) : Monotone fun b => l.foldl f b := by
+  intro b₁ b₂ hb
+  induction l generalizing b₁ b₂ with
+  | nil => exact hb
+  | cons x xs ih => exact ih (hf x hb)
+
+end Folds
+
+/-! ### Fixed height (Chain.agda `Bounded`/`Height`, Lattice.agda `FixedHeight`) -/
+
+/-- Agda: `Chain.Bounded`. Every `<`-chain has length at most `n`. -/
+def BoundedChains (α : Type*) [Preorder α] (n : ℕ) : Prop :=
+  ∀ c : LTSeries α, c.length ≤ n
+
+/-- Agda: `Chain.Height` (with `FixedHeight h = Height h` from Lattice.agda).
+A longest chain runs from `⊥` to `⊤` and has length exactly `height`;
+no chain is longer. -/
+structure FixedHeight (α : Type*) [Preorder α] (height : ℕ) where
+  bot : α
+  top : α
+  longestChain : LTSeries α
+  head_longestChain : longestChain.head = bot
+  last_longestChain : longestChain.last = top
+  length_longestChain : longestChain.length = height
+  bounded : BoundedChains α height
+
+/-- Agda: `Chain.Bounded-suc-n` (a bounded order admits no chain one longer). -/
+theorem BoundedChains.no_longer {α : Type*} [Preorder α] {n : ℕ}
+    (h : BoundedChains α n) (c : LTSeries α) : c.length ≠ n + 1 :=
+  fun hc => absurd (h c) (by omega)
+
+/-- Agda: `IsFiniteHeightLattice` / `FiniteHeightLattice` (bundled). -/
+class FiniteHeightLattice (α : Type*) [Lattice α] where
+  height : ℕ
+  fixedHeight : FixedHeight α height
+
+namespace FixedHeight
+
+variable {α : Type*} [Lattice α] {h : ℕ}
+
+/-- Agda: `Known-⊥`. -/
+def KnownBot (fh : FixedHeight α h) : Prop := ∀ a : α, fh.bot ≤ a
+
+/-- Agda: `Known-⊤`. -/
+def KnownTop (fh : FixedHeight α h) : Prop := ∀ a : α, a ≤ fh.top
+
+/-- Agda: `⊥≼` — the bottom of the longest chain is a least element.
+Same proof: if `⊥ ⊓ a ≠ ⊥` then `⊥ ⊓ a < ⊥` prepends to the longest chain,
+contradicting boundedness. (The decidability hypothesis of the Agda proof is
+not needed classically.) -/
+theorem bot_le (fh : FixedHeight α h) : fh.KnownBot := by
+  intro a
+  by_cases heq : fh.bot ⊓ a = fh.bot
+  · exact inf_eq_left.mp heq
+  · exfalso
+    have hlt : fh.bot ⊓ a < fh.bot :=
+      lt_of_le_of_ne inf_le_left heq
+    exact fh.bounded.no_longer
+      (fh.longestChain.cons (fh.bot ⊓ a) (fh.head_longestChain ▸ hlt))
+      (by simp [RelSeries.cons, fh.length_longestChain])
+
+end FixedHeight
+
+end Spa
--- a/lean/lake-manifest.json
+++ b/lean/lake-manifest.json
@@ -0,0 +1,95 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "5269898d6a51d047931107c8d72d934d8d5d3753",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.17.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "c708be04267e3e995a14ac0d08b1530579c1525a",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "0c169a0d55fef3763cfb3099eafd7b884ec7e41d",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "0447b0a7b7f41f0a1749010db3f222e4a96f9d30",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "799f6986de9f61b784ff7be8f6a8b101045b8ffd",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.52",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "56a2c80b209c253e0281ac4562a92122b457dcc0",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "95561f7a5811fae6a309e4a1bbe22a0a4a98bf03",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "efcc7d9bd9936ecdc625baf0d033b60866565cd5",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "e7fd1a415c80985ade02a021172834ca2139b0ca",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
+ "name": "spa",
+ "lakeDir": ".lake"}
--- a/lean/lakefile.toml
+++ b/lean/lakefile.toml
@@ -0,0 +1,10 @@
+name = "spa"
+defaultTargets = ["Spa"]
+
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4"
+rev = "v4.17.0"
+
+[[lean_lib]]
+name = "Spa"
--- a/lean/lean-toolchain
+++ b/lean/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.17.0