agda-spa/LEAN_MIGRATION.md

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

• Phase 0
• Phase 1
• Phase 2
• Phase 3
• Phase 4
• Phase 5
• Phase 6
• Phase 7

All phases complete: lake build is green with zero warnings, zero sorrys and zero axioms, and lake exe spa prints output byte-for-byte identical to the compiled Agda Main (verified with diff). Per-file Agda ↦ Lean correspondence tables live in the header comment of each Lean file.

Wins from the migration

• The four monotonicity postulates in Analysis/Sign.agda and Analysis/Constant.agda are now proved theorems (via AboveBelow.le_cases), so the Lean development is postulate-free.
• ~2200 lines of map machinery (Lattice/Map.agda, Lattice/MapSet.agda, much of Lattice/FiniteMap.agda) collapse into the spine-pinned FiniteMap + Finset; the IterProd isomorphism no longer needs Unique ks (the representation is canonical).
• Equivalence.agda, Chain.agda, the IsSemilattice/IsLattice hierarchy, and most of Utils.agda lift into mathlib.

Deviations & deferred items

• Lattice/Builder.agda: not ported (nothing in the repo imports it).
• Lattice/ExtendBelow.agda, Lattice/Nat.agda: not ported (unused by the pipeline; Nat's lattice is mathlib's, ExtendBelow would be WithBot + a small height proof). Say the word if you want them for parity.
• Program.vars lists variables in sorted order (Finset.sort, since Finset.toList is noncomputable). For the test program this coincides with the Agda MapSet order.
• Chains are mathlib LTSeries, so chain-manipulating proofs (Prod unzip, AboveBelow's isLongest → a rank-based bound) are restated against that API rather than pattern-matching a custom Chain inductive.
• Trace/EndToEndTrace are Prop-valued and destructured in proofs.