Add scoped quotation syntax for object-language programs

Introduce [spa_e| ... ] for Expr and [spa| ... ] for Stmt, scoped to the Spa namespace via a dedicated syntax category and macro_rules. This removes the deeply nested .andThen / .basic (.assign ...) boilerplate when writing programs; Main.lean's test programs are rewritten to use it. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018Yq5SmPQfNfzAEUpUXRo66
Apply some cleanups to Graphs.lean
2026-06-23 14:28:06 -05:00 · 2026-06-23 14:10:54 -05:00 · 2026-06-23 13:29:54 -05:00 · 2026-06-23 13:02:45 -05:00 · 2026-06-23 12:42:53 -05:00 · 2026-06-23 12:29:46 -05:00
24 changed files with 228 additions and 697 deletions
--- a/lean/Main.lean
+++ b/lean/Main.lean
@@ -1,40 +1,35 @@
-/-
-Port of `Main.agda`. Prints the constant- and sign-analysis results for the
-test program (Agda: `putStrLn (output-Const ++ "\n" ++ output-Sign)`).
-/
 import Spa.Analysis.Sign
 import Spa.Analysis.Constant
+import Spa.Language.Notation

 namespace Spa

-/-- Agda: `testCode`. -/
-def testCode : Stmt :=
-  .andThen (.basic (.assign "zero" (.num 0)))
-    (.andThen (.basic (.assign "pos" (.add (.var "zero") (.num 1))))
-      (.andThen (.basic (.assign "neg" (.sub (.var "zero") (.num 1))))
-        (.basic (.assign "unknown" (.add (.var "pos") (.var "neg"))))))
+def testCode : Stmt := [obj_stmt|
+  zero    := 0;
+  pos     := zero + 1;
+  neg     := zero - 1;
+  unknown := pos + neg
+]

-/-- Agda: `testCodeCond₁`. -/
-def testCodeCond₁ : Stmt :=
-  .andThen (.basic (.assign "var" (.num 1)))
-    (.ifElse (.var "var")
-      (.basic (.assign "var" (.add (.var "var") (.num 1))))
-      (.andThen (.basic (.assign "var" (.sub (.var "var") (.num 1))))
-        (.basic (.assign "var" (.num 1)))))
+def testCodeCond₁ : Stmt := [obj_stmt|
+  var := 1;
+  if var {
+    var := var + 1
+  } else {
+    var := var - 1;
+    var := 1
+  }
+]

-/-- Agda: `testCodeCond₂`. -/
-def testCodeCond₂ : Stmt :=
-  .andThen (.basic (.assign "var" (.num 1)))
-    (.ifElse (.var "var")
-      (.basic (.assign "x" (.num 1)))
-      (.basic .noop))
+def testCodeCond₂ : Stmt := [obj_stmt|
+  var := 1;
+  if var { x := 1 } else { noop }
+]

-/-- Agda: `testProgram`. -/
 def testProgram : Program := ⟨testCode⟩

 end Spa

-/-- Agda: `main`. -/
 def main : IO Unit :=
  IO.println (Spa.ConstAnalysis.output Spa.testProgram ++ "\n" ++
              Spa.SignAnalysis.output Spa.testProgram)
--- a/lean/Spa.lean
+++ b/lean/Spa.lean
@@ -7,6 +7,7 @@ import Spa.Lattice.AboveBelow
 import Spa.Lattice.IterProd
 import Spa.Lattice.FiniteMap
 import Spa.Language.Base
+import Spa.Language.Notation
 import Spa.Language.Semantics
 import Spa.Language.Graphs
 import Spa.Language.Traces
--- a/lean/Spa/Analysis/Constant.lean
+++ b/lean/Spa/Analysis/Constant.lean
@@ -1,31 +1,6 @@
-/-
-Port of `Analysis/Constant.agda`.
-
-Correspondence:
-  showable, ≡-equiv, ≡-Decidable-ℤ ↦ (mathlib/derived instances)
-  ConstLattice (AboveBelow ℤ)      ↦ ConstLattice
-  AB.Plain (+ 0)                   ↦ the AboveBelow FiniteHeightLattice instance,
-                                     seeded by `Inhabited ℤ` (default `0`)
-  plus, minus                      ↦ plus, minus
-  plus-Monoˡ/ʳ, minus-Monoˡ/ʳ (postulates in Agda!)
-                                   ↦ plus_mono_left/right, minus_mono_left/right
-                                     — now actually proved, via
-                                     AboveBelow.monotone₂_of_strict
-  plus-Mono₂, minus-Mono₂          ↦ plus_mono₂, minus_mono₂
-  ⟦_⟧ᶜ                             ↦ interpConst
-  ⟦⟧ᶜ-respects-≈ᶜ                  ↦ (trivial with `=`)
-  ⟦⟧ᶜ-⊔ᶜ-∨, ⟦⟧ᶜ-⊓ᶜ-∧               ↦ interpConst_sup, interpConst_inf
-  s₁≢s₂⇒¬s₁∧s₂                     ↦ interpConst_mk_disjoint
-  latticeInterpretationᶜ           ↦ constInterpretation
-  WithProg.eval, eval-Monoʳ        ↦ ConstAnalysis.eval, eval_mono
-  ConstEval                        ↦ ConstAnalysis.exprEvaluator
-  plus-valid, minus-valid          ↦ plus_valid, minus_valid
-  eval-valid, ConstEvalValid       ↦ eval_valid
-  output                           ↦ ConstAnalysis.output
-  analyze-correct                  ↦ ConstAnalysis.analyze_correct
-/
 import Spa.Analysis.Forward
 import Spa.Analysis.Utils
+import Spa.Interp
 import Spa.Showable

 namespace Spa
@@ -35,7 +10,6 @@ abbrev ConstLattice : Type := AboveBelow ℤ
 namespace ConstAnalysis

 open AboveBelow in
-/-- Agda: `plus`. -/
 def plus : ConstLattice → ConstLattice → ConstLattice
  | bot, _ => bot
  | _, bot => bot
@@ -44,7 +18,6 @@ def plus : ConstLattice → ConstLattice → ConstLattice
  | mk z₁, mk z₂ => mk (z₁ + z₂)

 open AboveBelow in
-/-- Agda: `minus`. -/
 def minus : ConstLattice → ConstLattice → ConstLattice
  | bot, _ => bot
  | _, bot => bot
@@ -52,41 +25,23 @@ def minus : ConstLattice → ConstLattice → ConstLattice
  | _, top => top
  | mk z₁, mk z₂ => mk (z₁ - z₂)

-/-- Agda: `plus-Mono₂` (its components were postulates in Agda; `plus` is a
-strict operation on the flat lattice, so monotonicity holds regardless of the
-constant table). -/
 theorem plus_mono₂ : Monotone₂ plus :=
  AboveBelow.monotone₂_of_strict plus
    (fun y => by cases y <;> rfl) (fun x => by cases x <;> rfl)
    (fun y hy => by cases y <;> first | exact absurd rfl hy | rfl)
    (fun x hx => by cases x <;> first | exact absurd rfl hx | rfl)

-/-- Agda: `plus-Monoˡ` — a postulate there, a theorem here. -/
-theorem plus_mono_left (s₂ : ConstLattice) : Monotone (plus · s₂) := plus_mono₂.1 s₂
-
-/-- Agda: `plus-Monoʳ` — a postulate there, a theorem here. -/
-theorem plus_mono_right (s₁ : ConstLattice) : Monotone (plus s₁) := plus_mono₂.2 s₁
-
-/-- Agda: `minus-Mono₂` (likewise from strictness of `minus`). -/
 theorem minus_mono₂ : Monotone₂ minus :=
  AboveBelow.monotone₂_of_strict minus
    (fun y => by cases y <;> rfl) (fun x => by cases x <;> rfl)
    (fun y hy => by cases y <;> first | exact absurd rfl hy | rfl)
    (fun x hx => by cases x <;> first | exact absurd rfl hx | rfl)

-/-- Agda: `minus-Monoˡ` — a postulate there, a theorem here. -/
-theorem minus_mono_left (s₂ : ConstLattice) : Monotone (minus · s₂) := minus_mono₂.1 s₂
-
-/-- Agda: `minus-Monoʳ` — a postulate there, a theorem here. -/
-theorem minus_mono_right (s₁ : ConstLattice) : Monotone (minus s₁) := minus_mono₂.2 s₁
-
-/-- Agda: `⟦_⟧ᶜ`. -/
 def interpConst : ConstLattice → Value → Prop
  | .bot, _ => False
  | .top, _ => True
  | .mk z, v => v = .int z

-/-- Agda: `s₁≢s₂⇒¬s₁∧s₂`. -/
 theorem interpConst_mk_disjoint {z₁ z₂ : ℤ} (hne : z₁ ≠ z₂) {v : Value} :
    ¬(interpConst (.mk z₁) v ∧ interpConst (.mk z₂) v) := by
  rintro ⟨h₁, h₂⟩
@@ -94,25 +49,13 @@ theorem interpConst_mk_disjoint {z₁ z₂ : ℤ} (hne : z₁ ≠ z₂) {v : Val
  injection h₂ with hz
  exact hne hz

-/-- Agda: `⟦⟧ᶜ-⊔ᶜ-∨` (via the factored flat-lattice lemma). -/
-theorem interpConst_sup {s₁ s₂ : ConstLattice} (v : Value)
-    (h : interpConst s₁ v ∨ interpConst s₂ v) : interpConst (s₁ ⊔ s₂) v :=
-  AboveBelow.interp_sup_of (fun _ h => h) (fun _ => trivial) v h
-
-/-- Agda: `⟦⟧ᶜ-⊓ᶜ-∧` (via the factored flat-lattice lemma). -/
-theorem interpConst_inf {s₁ s₂ : ConstLattice} (v : Value)
-    (h : interpConst s₁ v ∧ interpConst s₂ v) : interpConst (s₁ ⊓ s₂) v :=
-  AboveBelow.interp_inf_of (fun hne _ => interpConst_mk_disjoint hne) v h
-
-/-- Agda: `latticeInterpretationᶜ` (an instance there too). -/
 instance constInterpretation : LatticeInterpretation ConstLattice where
  interp := interpConst
-  interp_sup := fun {l₁ l₂} v h => interpConst_sup (s₁ := l₁) (s₂ := l₂) v h
-  interp_inf := fun {l₁ l₂} v h => interpConst_inf (s₁ := l₁) (s₂ := l₂) v h
+  interp_sup := fun v h => AboveBelow.interp_sup_of (fun _ h => h) (fun _ => trivial) v h
+  interp_inf := fun v h => AboveBelow.interp_inf_of (fun hne _ => interpConst_mk_disjoint hne) v h

 variable (prog : Program)

-/-- Agda: `WithProg.eval`. -/
 def eval : Expr → VariableValues ConstLattice prog → ConstLattice
  | .add e₁ e₂, vs => plus (eval e₁ vs) (eval e₂ vs)
  | .sub e₁ e₂, vs => minus (eval e₁ vs) (eval e₂ vs)
@@ -120,7 +63,6 @@ def eval : Expr → VariableValues ConstLattice prog → ConstLattice
    if h : FiniteMap.MemKey k vs then (FiniteMap.locate h).1 else .top
  | .num n, _ => .mk n

-/-- Agda: `WithProg.eval-Monoʳ`. -/
 theorem eval_mono (e : Expr) : Monotone (eval prog e) := by
  induction e with
  | add e₁ e₂ ih₁ ih₂ =>
@@ -143,18 +85,15 @@ theorem eval_mono (e : Expr) : Monotone (eval prog e) := by
    intro vs₁ vs₂ _
    exact le_refl _

-/-- Agda: the `ConstEval` instance. -/
 instance exprEvaluator : ExprEvaluator ConstLattice prog :=
  ⟨eval prog, eval_mono prog⟩

-/-- Agda: `WithProg.result`/`output`. -/
 def output : String :=
  show' (result ConstLattice prog)

-/-- Agda: `plus-valid`. -/
 theorem plus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ}
-    (h₁ : interpConst g₁ (.int z₁)) (h₂ : interpConst g₂ (.int z₂)) :
-    interpConst (plus g₁ g₂) (.int (z₁ + z₂)) := by
+    (h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) :
+    ⟦plus g₁ g₂⟧ (.int (z₁ + z₂)) := by
  rcases g₁ with _ | _ | c₁
  · exact h₁.elim
  · rcases g₂ with _ | _ | c₂
@@ -169,10 +108,9 @@ theorem plus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ}
      show Value.int (z₁ + z₂) = Value.int (c₁ + c₂)
      rw [hz₁, hz₂]

-/-- Agda: `minus-valid`. -/
 theorem minus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ}
-    (h₁ : interpConst g₁ (.int z₁)) (h₂ : interpConst g₂ (.int z₂)) :
-    interpConst (minus g₁ g₂) (.int (z₁ - z₂)) := by
+    (h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) :
+    ⟦minus g₁ g₂⟧ (.int (z₁ - z₂)) := by
  rcases g₁ with _ | _ | c₁
  · exact h₁.elim
  · rcases g₂ with _ | _ | c₂
@@ -187,18 +125,17 @@ theorem minus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ}
      show Value.int (z₁ - z₂) = Value.int (c₁ - c₂)
      rw [hz₁, hz₂]

-/-- Agda: `eval-valid` / the `ConstEvalValid` instance. -/
 instance eval_valid : ValidExprEvaluator ConstLattice prog := by
  constructor
  intro vs ρ e v hev
  induction hev with
  | num n =>
    intro _
-    show interpConst (eval prog (.num n) vs) (.int n)
+    show ⟦eval prog (.num n) vs⟧ (.int n)
    rfl
  | var x v hxv =>
    intro hvs
-    show interpConst (eval prog (.var x) vs) v
+    show ⟦eval prog (.var x) vs⟧ v
    simp only [eval]
    by_cases hk : FiniteMap.MemKey x vs
    · rw [dif_pos hk]
@@ -207,20 +144,19 @@ instance eval_valid : ValidExprEvaluator ConstLattice prog := by
      exact trivial
  | add e₁ e₂ z₁ z₂ _ _ ih₁ ih₂ =>
    intro hvs
-    have h₁ : interpConst (eval prog e₁ vs) (.int z₁) := ih₁ hvs
-    have h₂ : interpConst (eval prog e₂ vs) (.int z₂) := ih₂ hvs
-    show interpConst (eval prog (.add e₁ e₂) vs) (.int (z₁ + z₂))
+    have h₁ : ⟦eval prog e₁ vs⟧ (.int z₁) := ih₁ hvs
+    have h₂ : ⟦eval prog e₂ vs⟧ (.int z₂) := ih₂ hvs
+    show ⟦eval prog (.add e₁ e₂) vs⟧ (.int (z₁ + z₂))
    exact plus_valid h₁ h₂
  | sub e₁ e₂ z₁ z₂ _ _ ih₁ ih₂ =>
    intro hvs
-    have h₁ : interpConst (eval prog e₁ vs) (.int z₁) := ih₁ hvs
-    have h₂ : interpConst (eval prog e₂ vs) (.int z₂) := ih₂ hvs
-    show interpConst (eval prog (.sub e₁ e₂) vs) (.int (z₁ - z₂))
+    have h₁ : ⟦eval prog e₁ vs⟧ (.int z₁) := ih₁ hvs
+    have h₂ : ⟦eval prog e₂ vs⟧ (.int z₂) := ih₂ hvs
+    show ⟦eval prog (.sub e₁ e₂) vs⟧ (.int (z₁ - z₂))
    exact minus_valid h₁ h₂

-/-- Agda: `WithProg.analyze-correct`. -/
 theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
-    interpV (variablesAt prog.finalState (result ConstLattice prog)) ρ :=
+    ⟦ variablesAt prog.finalState (result ConstLattice prog) ⟧ ρ :=
  Spa.analyze_correct ConstLattice prog hrun

 end ConstAnalysis
--- a/lean/Spa/Analysis/Forward.lean
+++ b/lean/Spa/Analysis/Forward.lean
@@ -1,30 +1,3 @@
-/-
-Port of `Analysis/Forward.agda` (`WithProg`, `WithStmtEvaluator`,
-`WithValidInterpretation`).
-
-As in Agda, the statement evaluator, the lattice interpretation and the
-evaluator's validity proof are instance arguments (`{{evaluator}}`,
-`{{latticeInterpretationˡ}}`, `{{validEvaluator}}`); `result` and
-`analyze_correct` take `L` and `prog` explicitly, mirroring the Agda call
-shape `WithProg.result L prog`.
-
-Correspondence:
-  updateVariablesForState, -Monoʳ   ↦ updateVariablesForState, _mono
-  updateAll, updateAll-Mono,
-  updateAll-k∈ks-≡                  ↦ updateAll, updateAll_mono, updateAll_mem_eq
-  analyze, analyze-Mono             ↦ analyze, analyze_mono
-  result, result≈analyze-result     ↦ result, result_eq
-  variablesAt-updateAll             ↦ variablesAt_updateAll
-  eval-fold-valid                   ↦ eval_fold_valid
-  updateVariablesForState-matches   ↦ updateVariablesForState_matches
-  updateAll-matches                 ↦ updateAll_matches
-  stepTrace                         ↦ stepTrace   (the `subst`/`⟦⟧ᵛ-respects-≈ᵛ`
-                                       plumbing becomes plain rewriting with `=`)
-  walkTrace                         ↦ walkTrace
-  joinForKey-initialState-⊥ᵛ        ↦ joinForKey_initialState
-  ⟦joinAll-initialState⟧ᵛ∅          ↦ interpV_joinForKey_initialState
-  analyze-correct                   ↦ analyze_correct
-/
 import Spa.Analysis.Forward.Lattices
 import Spa.Analysis.Forward.Evaluation
 import Spa.Analysis.Forward.Adapters
@@ -34,134 +7,113 @@ namespace Spa

 variable {L : Type} [Lattice L] {prog : Program} [E : StmtEvaluator L prog]

-/-- Agda: `updateVariablesForState`. -/
 def updateVariablesForState (s : prog.State) (sv : StateVariables L prog) :
    VariableValues L prog :=
  (prog.code s).foldl (fun vs bs => E.eval s bs vs) (variablesAt s sv)

-/-- Agda: `updateVariablesForState-Monoʳ`. -/
 theorem updateVariablesForState_mono (s : prog.State) :
    Monotone (updateVariablesForState (L := L) s) := fun _ _ hle =>
-  foldl_mono' (prog.code s) _ (fun bs => E.eval_mono s bs) (variablesAt_le hle s)
+  foldl_mono' (prog.code s) _ (E.eval_mono s ·) (variablesAt_le hle s)

-/-- Agda: `updateAll`. -/
 def updateAll (sv : StateVariables L prog) : StateVariables L prog :=
-  FiniteMap.generalizedUpdate id (fun s sv => updateVariablesForState s sv)
+  FiniteMap.generalizedUpdate id updateVariablesForState
    prog.states sv

-/-- Agda: `updateAll-Mono`. -/
 theorem updateAll_mono : Monotone (updateAll (L := L) (prog := prog)) :=
  FiniteMap.generalizedUpdate_monotone monotone_id updateVariablesForState_mono

-/-- Agda: `updateAll-k∈ks-≡`. -/
 theorem updateAll_mem_eq {s : prog.State} {vs : VariableValues L prog}
    {sv : StateVariables L prog} (hmem : (s, vs) ∈ updateAll sv) :
    vs = updateVariablesForState s sv :=
  FiniteMap.generalizedUpdate_mem_eq (prog.states_complete s) hmem

-/-- Agda: `variablesAt-updateAll`. -/
 theorem variablesAt_updateAll (s : prog.State) (sv : StateVariables L prog) :
    variablesAt s (updateAll sv) = updateVariablesForState s sv :=
  updateAll_mem_eq (variablesAt_mem s (updateAll sv))

 variable [FiniteHeightLattice L]

-/-- Agda: `analyze`. -/
 def analyze (sv : StateVariables L prog) : StateVariables L prog :=
  updateAll (joinAll sv)

-/-- Agda: `analyze-Mono`. -/
 theorem analyze_mono : Monotone (analyze (L := L) (prog := prog)) := fun _ _ hle =>
  updateAll_mono (joinAll_mono hle)

 variable [DecidableEq L]

 variable (L prog) in
-/-- Agda: `result` (the least fixpoint of `analyze`). -/
 def result : StateVariables L prog :=
  Fixedpoint.aFix analyze analyze_mono

 variable (L prog) in
-/-- Agda: `result≈analyze-result`. -/
 theorem result_eq : result L prog = analyze (result L prog) :=
  Fixedpoint.aFix_eq analyze analyze_mono

-/-- Agda: `joinForKey-initialState-⊥ᵛ`. -/
 theorem joinForKey_initialState :
    joinForKey prog.initialState (result L prog) = botV L prog := by
  rw [joinForKey, prog.incoming_initialState_eq_nil]
  rfl

-/-! ### Semantic correctness (Agda: `WithValidInterpretation`) -/
-
 variable [I : LatticeInterpretation L] [V : ValidStmtEvaluator L prog]

 omit [FiniteHeightLattice L] [DecidableEq L] in
-/-- Agda: `eval-fold-valid`. -/
 theorem eval_fold_valid {s : prog.State} {bss : List BasicStmt}
    {vs : VariableValues L prog} {ρ₁ ρ₂ : Env}
-    (hbss : EvalBasicStmts ρ₁ bss ρ₂) (hvs : interpV vs ρ₁) :
-    interpV (bss.foldl (fun vs bs => E.eval s bs vs) vs) ρ₂ := by
+    (hbss : EvalBasicStmts ρ₁ bss ρ₂) (hvs : ⟦ vs ⟧ ρ₁) :
+    ⟦ bss.foldl (fun vs bs => E.eval s bs vs) vs ⟧ ρ₂ := by
  induction hbss generalizing vs with
  | nil => exact hvs
  | cons hbs _ ih => exact ih (ValidStmtEvaluator.valid hbs hvs)

 omit [FiniteHeightLattice L] [DecidableEq L] in
-/-- Agda: `updateVariablesForState-matches`. -/
 theorem updateVariablesForState_matches {s : prog.State}
    {sv : StateVariables L prog} {ρ₁ ρ₂ : Env}
    (hbss : EvalBasicStmts ρ₁ (prog.code s) ρ₂)
-    (hvs : interpV (variablesAt s sv) ρ₁) :
-    interpV (updateVariablesForState s sv) ρ₂ :=
+    (hvs : ⟦ variablesAt s sv ⟧ ρ₁) :
+    ⟦ updateVariablesForState s sv ⟧ ρ₂ :=
  eval_fold_valid hbss hvs

 omit [FiniteHeightLattice L] [DecidableEq L] in
-/-- Agda: `updateAll-matches`. -/
 theorem updateAll_matches {s : prog.State} {sv : StateVariables L prog}
    {ρ₁ ρ₂ : Env} (hbss : EvalBasicStmts ρ₁ (prog.code s) ρ₂)
-    (hvs : interpV (variablesAt s sv) ρ₁) :
-    interpV (variablesAt s (updateAll sv)) ρ₂ := by
+    (hvs : ⟦ variablesAt s sv ⟧ ρ₁) :
+    ⟦ variablesAt s (updateAll sv) ⟧ ρ₂ := by
  rw [variablesAt_updateAll]
  exact updateVariablesForState_matches hbss hvs

-/-- Agda: `stepTrace`. -/
 theorem stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env}
-    (hjoin : interpV (joinForKey s₁ (result L prog)) ρ₁)
+    (hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁)
    (hbss : EvalBasicStmts ρ₁ (prog.code s₁) ρ₂) :
-    interpV (variablesAt s₁ (result L prog)) ρ₂ := by
+    ⟦ variablesAt s₁ (result L prog) ⟧ ρ₂ := by
  rw [result_eq L prog]
  refine updateAll_matches hbss ?_
  rw [variablesAt_joinAll]
  exact hjoin

-/-- Agda: `walkTrace`. -/
 theorem walkTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
-    (hjoin : interpV (joinForKey s₁ (result L prog)) ρ₁)
+    (hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁)
    (tr : Trace prog.graph s₁ s₂ ρ₁ ρ₂) :
-    interpV (variablesAt s₂ (result L prog)) ρ₂ := by
+    ⟦ variablesAt s₂ (result L prog) ⟧ ρ₂ := by
  induction tr with
  | single hbss => exact stepTrace hjoin hbss
  | @edge _ ρ' _ i₁ i₂ _ hbss hedge _ ih =>
-    have hstep : interpV (variablesAt i₁ (result L prog)) ρ' :=
+    have hstep : ⟦ variablesAt i₁ (result L prog) ⟧ ρ' :=
      stepTrace hjoin hbss
    have hmem : variablesAt i₁ (result L prog)
        ∈ (result L prog).valuesAt (prog.incoming i₂) :=
      FiniteMap.mem_valuesAt prog.states_nodup
        (prog.mem_incoming_of_edge hedge) (variablesAt_mem i₁ (result L prog))
-    exact ih (interpV_foldr hstep hmem)
+    exact ih (interp_foldr hstep hmem)

 omit V in
-/-- Agda: `⟦joinAll-initialState⟧ᵛ∅`. -/
-theorem interpV_joinForKey_initialState :
-    interpV (joinForKey prog.initialState (result L prog)) [] := by
+theorem interp_joinForKey_initialState :
+    ⟦ joinForKey prog.initialState (result L prog) ⟧ [] := by
  rw [joinForKey_initialState]
-  exact interpV_botV_nil
+  exact interp_botV_nil

 variable (L prog) in
-/-- Agda: `analyze-correct` — the analysis result at the final state soundly
-describes every terminating execution of the program. -/
 theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
-    interpV (variablesAt prog.finalState (result L prog)) ρ :=
-  walkTrace interpV_joinForKey_initialState (prog.trace hrun)
+    ⟦ variablesAt prog.finalState (result L prog) ⟧ ρ :=
+  walkTrace interp_joinForKey_initialState (prog.trace hrun)

 end Spa
--- a/lean/Spa/Analysis/Forward/Adapters.lean
+++ b/lean/Spa/Analysis/Forward/Adapters.lean
@@ -1,53 +1,32 @@
-/-
-Port of `Analysis/Forward/Adapters.agda` (`ExprToStmtAdapter`).
-
-Correspondence:
-  updateVariablesFromExpression           ↦ updateVariablesFromExpression
-  updateVariablesFromExpression-Mono      ↦ updateVariablesFromExpression_mono
-  (the -k∈ks-≡ / -k∉ks-backward renames   ↦ used directly from FiniteMap)
-  evalᵇ, evalᵇ-Monoʳ                      ↦ evalB, evalB_mono
-  stmtEvaluator (instance)                ↦ instance StmtEvaluator L prog
-  evalᵇ-valid, validStmtEvaluator         ↦ instance ValidStmtEvaluator L prog
-                                            (the Agda `k ≟ˢ k'` case split is
-                                            subsumed by `cases` on `Env.Mem`,
-                                            whose `here` case forces `k' = k`)
-/
 import Spa.Analysis.Forward.Evaluation

 namespace Spa

 variable {L : Type} [Lattice L] {prog : Program} [E : ExprEvaluator L prog]

-/-- Agda: `updateVariablesFromExpression` — set the single key `k` to the
-value of `e` (the `GeneralizedUpdate` with `ks = [k]`). -/
 def updateVariablesFromExpression (k : String) (e : Expr)
    (vs : VariableValues L prog) : VariableValues L prog :=
  FiniteMap.generalizedUpdate id (fun _ vs => E.eval e vs) [k] vs

-/-- Agda: `updateVariablesFromExpression-Mono`. -/
 theorem updateVariablesFromExpression_mono (k : String) (e : Expr) :
    Monotone (updateVariablesFromExpression (L := L) (prog := prog) k e) :=
  FiniteMap.generalizedUpdate_monotone monotone_id (fun _ => E.eval_mono e)

-/-- Agda: `evalᵇ`. -/
 def evalB (_ : prog.State) (bs : BasicStmt)
    (vs : VariableValues L prog) : VariableValues L prog :=
  match bs with
  | .assign k e => updateVariablesFromExpression k e vs
  | .noop => vs

-/-- Agda: `evalᵇ-Monoʳ`. -/
 theorem evalB_mono (s : prog.State) (bs : BasicStmt) :
    Monotone (evalB (L := L) (prog := prog) s bs) := by
  cases bs with
  | assign k e => exact updateVariablesFromExpression_mono k e
  | noop => exact monotone_id

-/-- Agda: the `stmtEvaluator` instance of `ExprToStmtAdapter`. -/
 instance ExprEvaluator.toStmtEvaluator : StmtEvaluator L prog :=
  ⟨evalB, evalB_mono⟩

-/-- Agda: `evalᵇ-valid` / the `validStmtEvaluator` instance. -/
 instance ExprEvaluator.toStmtEvaluator_valid [LatticeInterpretation L]
    [ValidExprEvaluator L prog] : ValidStmtEvaluator L prog := by
  constructor
--- a/lean/Spa/Analysis/Forward/Evaluation.lean
+++ b/lean/Spa/Analysis/Forward/Evaluation.lean
@@ -1,43 +1,26 @@
-/-
-Port of `Analysis/Forward/Evaluation.agda`.
-
-All four records were consumed through Agda instance arguments (`{{evaluator :
-StmtEvaluator}}`, `{{validEvaluator : ValidStmtEvaluator …}}`), so they are
-typeclasses here as well.
-
-Correspondence:
-  StmtEvaluator (eval, eval-Monoʳ)  ↦ StmtEvaluator (eval, eval_mono)
-  ExprEvaluator (eval, eval-Monoʳ)  ↦ ExprEvaluator (eval, eval_mono)
-  ValidExprEvaluator                ↦ ValidExprEvaluator (valid)
-  ValidStmtEvaluator                ↦ ValidStmtEvaluator (valid)
-/
 import Spa.Analysis.Forward.Lattices

 namespace Spa

 variable (L : Type) [Lattice L] (prog : Program)

-/-- Agda: `StmtEvaluator`. -/
 class StmtEvaluator where
  eval : prog.State → BasicStmt → VariableValues L prog → VariableValues L prog
  eval_mono : ∀ s bs, Monotone (eval s bs)

-/-- Agda: `ExprEvaluator`. -/
 class ExprEvaluator where
  eval : Expr → VariableValues L prog → L
  eval_mono : ∀ e, Monotone (eval e)

-/-- Agda: `ValidExprEvaluator`. -/
 class ValidExprEvaluator [ExprEvaluator L prog] [I : LatticeInterpretation L] :
    Prop where
  valid : ∀ {vs : VariableValues L prog} {ρ : Env} {e : Expr} {v : Value},
-    EvalExpr ρ e v → interpV vs ρ → I.interp (ExprEvaluator.eval e vs) v
+    EvalExpr ρ e v → ⟦ vs ⟧ ρ → I.interp (ExprEvaluator.eval e vs) v

-/-- Agda: `ValidStmtEvaluator`. -/
 class ValidStmtEvaluator [E : StmtEvaluator L prog] [LatticeInterpretation L] :
    Prop where
  valid : ∀ {s : prog.State} {vs : VariableValues L prog} {ρ₁ ρ₂ : Env}
    {bs : BasicStmt},
-    EvalBasicStmt ρ₁ bs ρ₂ → interpV vs ρ₁ → interpV (E.eval s bs vs) ρ₂
+    EvalBasicStmt ρ₁ bs ρ₂ → ⟦ vs ⟧ ρ₁ → ⟦ E.eval s bs vs ⟧ ρ₂

 end Spa
--- a/lean/Spa/Analysis/Forward/Lattices.lean
+++ b/lean/Spa/Analysis/Forward/Lattices.lean
@@ -1,69 +1,34 @@
-/-
-Port of `Analysis/Forward/Lattices.agda`.
-
-The Agda module instantiates `Lattice.FiniteMap` twice (variables ↦ abstract
-values, states ↦ variable maps) and re-exports everything with ᵛ/ᵐ suffixes.
-In Lean the two instantiations are `abbrev`s and the FiniteMap API is used
-directly; the module parameters (the finite-height lattice `L`, the program)
-become section variables, with the finite-height structure and the lattice
-interpretation arriving by instance resolution as in Agda.
-
-Correspondence:
-  VariableValues, StateVariables  ↦ VariableValues, StateVariables
-  isLatticeᵛ/isLatticeᵐ, ⊔ᵛ, ≼ᵛ … ↦ (the FiniteMap Lattice instances)
-  fixedHeightᵛ, fixedHeightᵐ      ↦ (the FiniteMap FiniteHeightLattice instance)
-  ⊥ᵛ, ⊥ᵛ-contains-bottoms         ↦ botV, FiniteMap.bot_contains_bots
-  states-in-Map                   ↦ states_memKey
-  variablesAt                     ↦ variablesAt
-  variablesAt-∈                   ↦ variablesAt_mem
-  variablesAt-≈                   ↦ (congruence, trivial with `=`)
-  joinForKey, joinForKey-Mono     ↦ joinForKey, joinForKey_mono
-  joinAll, joinAll-Mono,
-  joinAll-k∈ks-≡                  ↦ joinAll, joinAll_mono, joinAll_mem_eq
-  variablesAt-joinAll             ↦ variablesAt_joinAll
-  ⟦_⟧ᵛ                            ↦ interpV
-  ⟦⊥ᵛ⟧ᵛ∅                          ↦ interpV_botV_nil
-  ⟦⟧ᵛ-respects-≈ᵛ                 ↦ (trivial with `=`)
-  ⟦⟧ᵛ-⊔ᵛ-∨                        ↦ interpV_sup
-  ⟦⟧ᵛ-foldr                       ↦ interpV_foldr
-/
 import Spa.Language
 import Spa.Lattice.FiniteMap
+import Spa.Interp

 namespace Spa

 variable (L : Type) [Lattice L] (prog : Program)

-/-- Agda: `VariableValues`. -/
 abbrev VariableValues : Type := FiniteMap String L prog.vars

-/-- Agda: `StateVariables`. -/
 abbrev StateVariables : Type := FiniteMap prog.State (VariableValues L prog) prog.states

-/-- Agda: `⊥ᵛ` (the bottom of `fixedHeightᵛ`, now found by instance search). -/
 def botV [FiniteHeightLattice L] : VariableValues L prog :=
  (⊥ : VariableValues L prog)

 variable {L prog}

 omit [Lattice L] in
-/-- Agda: `states-in-Map`. -/
 theorem states_memKey (s : prog.State) (sv : StateVariables L prog) :
    FiniteMap.MemKey s sv :=
  FiniteMap.memKey_iff.mpr (prog.states_complete s)

-/-- Agda: `variablesAt`. -/
 def variablesAt (s : prog.State) (sv : StateVariables L prog) :
    VariableValues L prog :=
  (FiniteMap.locate (states_memKey s sv)).1

 omit [Lattice L] in
-/-- Agda: `variablesAt-∈`. -/
 theorem variablesAt_mem (s : prog.State) (sv : StateVariables L prog) :
    (s, variablesAt s sv) ∈ sv :=
  (FiniteMap.locate (states_memKey s sv)).2

-/-- Agda: `m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ`, specialized the way `Forward.agda` uses it. -/
 theorem variablesAt_le {sv₁ sv₂ : StateVariables L prog} (hle : sv₁ ≤ sv₂)
    (s : prog.State) : variablesAt s sv₁ ≤ variablesAt s sv₂ :=
  FiniteMap.le_of_mem_mem prog.states_nodup hle
@@ -71,12 +36,10 @@ theorem variablesAt_le {sv₁ sv₂ : StateVariables L prog} (hle : sv₁ ≤ sv

 variable [FiniteHeightLattice L]

-/-- Agda: `joinForKey`. -/
 def joinForKey (k : prog.State) (sv : StateVariables L prog) :
    VariableValues L prog :=
  (sv.valuesAt (prog.incoming k)).foldr (· ⊔ ·) (botV L prog)

-/-- Agda: `joinForKey-Mono`. -/
 theorem joinForKey_mono (k : prog.State) :
    Monotone (joinForKey (L := L) k) := by
  intro sv₁ sv₂ hle
@@ -84,21 +47,17 @@ theorem joinForKey_mono (k : prog.State) :
    (fun b _ _ hab => sup_le_sup_right hab b)
    (fun a _ _ hab => sup_le_sup_left hab a)

-/-- Agda: `joinAll` (the "Exercise 4.26" generalized update with `f = id`). -/
 def joinAll (sv : StateVariables L prog) : StateVariables L prog :=
  FiniteMap.generalizedUpdate id joinForKey prog.states sv

-/-- Agda: `joinAll-Mono`. -/
 theorem joinAll_mono : Monotone (joinAll (L := L) (prog := prog)) :=
  FiniteMap.generalizedUpdate_monotone monotone_id joinForKey_mono

-/-- Agda: `joinAll-k∈ks-≡`. -/
 theorem joinAll_mem_eq {s : prog.State} {vs : VariableValues L prog}
    {sv : StateVariables L prog} (h : (s, vs) ∈ joinAll sv) :
    vs = joinForKey s sv :=
  FiniteMap.generalizedUpdate_mem_eq (prog.states_complete s) h

-/-- Agda: `variablesAt-joinAll`. -/
 theorem variablesAt_joinAll (s : prog.State) (sv : StateVariables L prog) :
    variablesAt s (joinAll sv) = joinForKey s sv :=
  joinAll_mem_eq (variablesAt_mem s (joinAll sv))
@@ -108,36 +67,33 @@ theorem variablesAt_joinAll (s : prog.State) (sv : StateVariables L prog) :
 variable [I : LatticeInterpretation L]

 omit [FiniteHeightLattice L] in
-/-- Agda: `⟦_⟧ᵛ`. -/
-def interpV (vs : VariableValues L prog) (ρ : Env) : Prop :=
+instance : Interp (VariableValues L prog) (Env → Prop) where
+  interp (vs : VariableValues L prog) (ρ : Env) : Prop :=
    ∀ (k : String) (l : L), (k, l) ∈ vs →
      ∀ (v : Value), Env.Mem (k, v) ρ → I.interp l v

-/-- Agda: `⟦⊥ᵛ⟧ᵛ∅`. -/
-theorem interpV_botV_nil : interpV (botV L prog) [] := by
+theorem interp_botV_nil : ⟦ botV L prog ⟧ [] := by
  intro k l _ v hmem
  cases hmem

 omit [FiniteHeightLattice L] in
-/-- Agda: `⟦⟧ᵛ-⊔ᵛ-∨`. -/
-theorem interpV_sup {vs₁ vs₂ : VariableValues L prog} {ρ : Env}
-    (h : interpV vs₁ ρ ∨ interpV vs₂ ρ) : interpV (vs₁ ⊔ vs₂) ρ := by
+theorem interp_sup {vs₁ vs₂ : VariableValues L prog} {ρ : Env}
+    (h : ⟦ vs₁⟧ ρ ∨ ⟦ vs₂ ⟧ ρ) : ⟦ vs₁ ⊔ vs₂ ⟧ ρ := by
  intro k l hmem v hv
  obtain ⟨l₁, l₂, rfl, h₁, h₂⟩ := FiniteMap.mem_sup hmem
  rcases h with h | h
  · exact I.interp_sup v (Or.inl (h _ _ h₁ _ hv))
  · exact I.interp_sup v (Or.inr (h _ _ h₂ _ hv))

-/-- Agda: `⟦⟧ᵛ-foldr`. -/
-theorem interpV_foldr {vs : VariableValues L prog}
+theorem interp_foldr {vs : VariableValues L prog}
    {vss : List (VariableValues L prog)} {ρ : Env}
-    (hvs : interpV vs ρ) (hmem : vs ∈ vss) :
-    interpV (vss.foldr (· ⊔ ·) (botV L prog)) ρ := by
+    (hvs : ⟦ vs ⟧ ρ) (hmem : vs ∈ vss) :
+    ⟦ vss.foldr (· ⊔ ·) (botV L prog) ⟧ ρ := by
  induction vss with
  | nil => cases hmem
  | cons vs' vss' ih =>
    rcases List.mem_cons.mp hmem with rfl | hmem'
-    · exact interpV_sup (Or.inl hvs)
-    · exact interpV_sup (Or.inr (ih hmem'))
+    · exact interp_sup (Or.inl hvs)
+    · exact interp_sup (Or.inr (ih hmem'))

 end Spa
--- a/lean/Spa/Analysis/Sign.lean
+++ b/lean/Spa/Analysis/Sign.lean
@@ -1,5 +1,6 @@
 import Spa.Analysis.Forward
 import Spa.Analysis.Utils
+import Spa.Interp
 import Spa.Showable

 namespace Spa
@@ -61,10 +62,6 @@ theorem plus_mono₂ : Monotone₂ plus :=
      rcases x with _ | _ | s <;>
        first | exact absurd rfl hx | rfl | (cases s <;> rfl))

-theorem plus_mono_left (s₂ : SignLattice) : Monotone (plus · s₂) := plus_mono₂.1 s₂
-
-theorem plus_mono_right (s₁ : SignLattice) : Monotone (plus s₁) := plus_mono₂.2 s₁
-
 theorem minus_mono₂ : Monotone₂ minus :=
  AboveBelow.monotone₂_of_strict minus
    (fun y => by cases y <;> rfl)
@@ -74,10 +71,6 @@ theorem minus_mono₂ : Monotone₂ minus :=
      rcases x with _ | _ | s <;>
        first | exact absurd rfl hx | rfl | (cases s <;> rfl))

-theorem minus_mono_left (s₂ : SignLattice) : Monotone (minus · s₂) := minus_mono₂.1 s₂
-
-theorem minus_mono_right (s₁ : SignLattice) : Monotone (minus s₁) := minus_mono₂.2 s₁
-
 def interpSign : SignLattice → Value → Prop
  | .bot, _ => False
  | .top, _ => True
@@ -113,18 +106,10 @@ theorem interpSign_mk_disjoint {s₁ s₂ : Sign} (hne : s₁ ≠ s₂) {v : Val
    injection hv with hz
    omega

-theorem interpSign_sup {s₁ s₂ : SignLattice} (v : Value)
-    (h : interpSign s₁ v ∨ interpSign s₂ v) : interpSign (s₁ ⊔ s₂) v :=
-  AboveBelow.interp_sup_of (fun _ h => h) (fun _ => trivial) v h
-
-theorem interpSign_inf {s₁ s₂ : SignLattice} (v : Value)
-    (h : interpSign s₁ v ∧ interpSign s₂ v) : interpSign (s₁ ⊓ s₂) v :=
-  AboveBelow.interp_inf_of (fun hne _ => interpSign_mk_disjoint hne) v h
-
 instance signInterpretation : LatticeInterpretation SignLattice where
  interp := interpSign
-  interp_sup := fun {l₁ l₂} v h => interpSign_sup (s₁ := l₁) (s₂ := l₂) v h
-  interp_inf := fun {l₁ l₂} v h => interpSign_inf (s₁ := l₁) (s₂ := l₂) v h
+  interp_sup := fun v h => AboveBelow.interp_sup_of (fun _ h => h) (fun _ => trivial) v h
+  interp_inf := fun v h => AboveBelow.interp_inf_of (fun hne _ => interpSign_mk_disjoint hne) v h

 namespace SignAnalysis

@@ -166,78 +151,34 @@ instance exprEvaluator : ExprEvaluator SignLattice prog :=
 def output : String :=
  show' (result SignLattice prog)

+/-- A nonneg-shifted interpretation `∃ n : ℕ, z = n + 1` just means `z` is positive. -/
+private theorem int_pos_iff (z : ℤ) : (∃ n : ℕ, z = (n : ℤ) + 1) ↔ 0 < z := by
+  constructor
+  · rintro ⟨n, rfl⟩; omega
+  · intro h; exact ⟨(z - 1).toNat, by omega⟩
+
+/-- Dually, `∃ n : ℕ, z = -(n + 1)` just means `z` is negative. -/
+private theorem int_neg_iff (z : ℤ) : (∃ n : ℕ, z = -((n : ℤ) + 1)) ↔ z < 0 := by
+  constructor
+  · rintro ⟨n, rfl⟩; omega
+  · intro h; exact ⟨(-z - 1).toNat, by omega⟩
+
 theorem plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
-    (h₁ : interpSign g₁ (.int z₁)) (h₂ : interpSign g₂ (.int z₂)) :
-    interpSign (plus g₁ g₂) (.int (z₁ + z₂)) := by
-  rcases g₁ with _ | _ | s₁
-  · exact h₁.elim
-  · rcases g₂ with _ | _ | s₂
-    · exact h₂.elim
-    · exact trivial
-    · exact trivial
-  · rcases g₂ with _ | _ | s₂
-    · exact h₂.elim
-    · rcases s₁ <;> exact trivial
-    · rcases s₁ <;> rcases s₂ <;>
-        simp only [plus, interpSign, Value.int.injEq] at h₁ h₂ ⊢ <;>
-        try trivial
-      · obtain ⟨n₁, rfl⟩ := h₁
-        obtain ⟨n₂, rfl⟩ := h₂
-        exact ⟨n₁ + n₂ + 1, by omega⟩
-      · obtain ⟨n₁, rfl⟩ := h₁
-        subst h₂
-        exact ⟨n₁, by omega⟩
-      · obtain ⟨n₁, rfl⟩ := h₁
-        obtain ⟨n₂, rfl⟩ := h₂
-        exact ⟨n₁ + n₂ + 1, by omega⟩
-      · obtain ⟨n₁, rfl⟩ := h₁
-        subst h₂
-        exact ⟨n₁, by omega⟩
-      · subst h₁
-        obtain ⟨n₂, rfl⟩ := h₂
-        exact ⟨n₂, by omega⟩
-      · subst h₁
-        obtain ⟨n₂, rfl⟩ := h₂
-        exact ⟨n₂, by omega⟩
-      · subst h₁
-        subst h₂
+    (h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) :
+    ⟦plus g₁ g₂⟧ (.int (z₁ + z₂)) := by
+  rcases g₁ with _ | _ | s₁ <;> rcases g₂ with _ | _ | s₂ <;>
+    (try rcases s₁) <;> (try rcases s₂) <;>
+    simp only [plus, signInterpretation, interpSign, Value.int.injEq, int_pos_iff, int_neg_iff]
+      at h₁ h₂ ⊢ <;>
    omega

 theorem minus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
-    (h₁ : interpSign g₁ (.int z₁)) (h₂ : interpSign g₂ (.int z₂)) :
-    interpSign (minus g₁ g₂) (.int (z₁ - z₂)) := by
-  rcases g₁ with _ | _ | s₁
-  · exact h₁.elim
-  · rcases g₂ with _ | _ | s₂
-    · exact h₂.elim
-    · exact trivial
-    · exact trivial
-  · rcases g₂ with _ | _ | s₂
-    · exact h₂.elim
-    · rcases s₁ <;> exact trivial
-    · rcases s₁ <;> rcases s₂ <;>
-        simp only [minus, interpSign, Value.int.injEq] at h₁ h₂ ⊢ <;>
-        try trivial
-      · obtain ⟨n₁, rfl⟩ := h₁
-        obtain ⟨n₂, rfl⟩ := h₂
-        exact ⟨n₁ + n₂ + 1, by omega⟩
-      · obtain ⟨n₁, rfl⟩ := h₁
-        subst h₂
-        exact ⟨n₁, by omega⟩
-      · obtain ⟨n₁, rfl⟩ := h₁
-        obtain ⟨n₂, rfl⟩ := h₂
-        exact ⟨n₁ + n₂ + 1, by omega⟩
-      · obtain ⟨n₁, rfl⟩ := h₁
-        subst h₂
-        exact ⟨n₁, by omega⟩
-      · subst h₁
-        obtain ⟨n₂, rfl⟩ := h₂
-        exact ⟨n₂, by omega⟩
-      · subst h₁
-        obtain ⟨n₂, rfl⟩ := h₂
-        exact ⟨n₂, by omega⟩
-      · subst h₁
-        subst h₂
+    (h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) :
+    ⟦minus g₁ g₂⟧ (.int (z₁ - z₂)) := by
+  rcases g₁ with _ | _ | s₁ <;> rcases g₂ with _ | _ | s₂ <;>
+    (try rcases s₁) <;> (try rcases s₂) <;>
+    simp only [minus, signInterpretation, interpSign, Value.int.injEq, int_pos_iff, int_neg_iff]
+      at h₁ h₂ ⊢ <;>
    omega

 instance eval_valid : ValidExprEvaluator SignLattice prog := by
@@ -246,13 +187,13 @@ instance eval_valid : ValidExprEvaluator SignLattice prog := by
  induction hev with
  | num n =>
    intro _
-    show interpSign (eval prog (.num n) vs) (.int n)
+    show ⟦eval prog (.num n) vs⟧ (.int n)
    cases n with
    | zero => rfl
    | succ n' => exact ⟨n', congrArg Value.int (by norm_cast)⟩
  | var x v hxv =>
    intro hvs
-    show interpSign (eval prog (.var x) vs) v
+    show ⟦eval prog (.var x) vs⟧ v
    simp only [eval]
    by_cases hk : FiniteMap.MemKey x vs
    · rw [dif_pos hk]
@@ -261,19 +202,19 @@ instance eval_valid : ValidExprEvaluator SignLattice prog := by
      exact trivial
  | add e₁ e₂ z₁ z₂ _ _ ih₁ ih₂ =>
    intro hvs
-    have h₁ : interpSign (eval prog e₁ vs) (.int z₁) := ih₁ hvs
-    have h₂ : interpSign (eval prog e₂ vs) (.int z₂) := ih₂ hvs
-    show interpSign (eval prog (.add e₁ e₂) vs) (.int (z₁ + z₂))
+    have h₁ : ⟦eval prog e₁ vs⟧ (.int z₁) := ih₁ hvs
+    have h₂ : ⟦eval prog e₂ vs⟧ (.int z₂) := ih₂ hvs
+    show ⟦eval prog (.add e₁ e₂) vs⟧ (.int (z₁ + z₂))
    exact plus_valid h₁ h₂
  | sub e₁ e₂ z₁ z₂ _ _ ih₁ ih₂ =>
    intro hvs
-    have h₁ : interpSign (eval prog e₁ vs) (.int z₁) := ih₁ hvs
-    have h₂ : interpSign (eval prog e₂ vs) (.int z₂) := ih₂ hvs
-    show interpSign (eval prog (.sub e₁ e₂) vs) (.int (z₁ - z₂))
+    have h₁ : ⟦eval prog e₁ vs⟧ (.int z₁) := ih₁ hvs
+    have h₂ : ⟦eval prog e₂ vs⟧ (.int z₂) := ih₂ hvs
+    show ⟦eval prog (.sub e₁ e₂) vs⟧ (.int (z₁ - z₂))
    exact minus_valid h₁ h₂

 theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
-    interpV (variablesAt prog.finalState (result SignLattice prog)) ρ :=
+    ⟦ variablesAt prog.finalState (result SignLattice prog) ⟧ ρ :=
  Spa.analyze_correct SignLattice prog hrun

 end SignAnalysis
--- a/lean/Spa/Analysis/Utils.lean
+++ b/lean/Spa/Analysis/Utils.lean
@@ -1,12 +1,7 @@
-/-
-Port of `Analysis/Utils.agda`. The `≼ᴼ-trans` module parameter lifts into the
-`Preorder` instance.
-/
 import Spa.Lattice

 namespace Spa

-/-- Agda: `eval-combine₂`. -/
 theorem eval_combine₂ {O : Type*} [Preorder O] {combine : O → O → O}
    (hmono : Monotone₂ combine) {o₁ o₂ o₃ o₄ : O}
    (h₁ : o₁ ≤ o₃) (h₂ : o₂ ≤ o₄) : combine o₁ o₂ ≤ combine o₃ o₄ :=
--- a/lean/Spa/Interp.lean
+++ b/lean/Spa/Interp.lean
@@ -0,0 +1,10 @@
+import Mathlib.Tactic.TypeStar
+
+namespace Spa
+
+class Interp (α : Type*) (dom : outParam Type*) where
+  interp : α → dom
+
+notation:max (priority := high) "⟦" v "⟧" => Interp.interp v
+
+end Spa
--- a/lean/Spa/Isomorphism.lean
+++ b/lean/Spa/Isomorphism.lean
@@ -2,9 +2,6 @@ import Spa.Lattice

 namespace Spa

-/-- Agda: `TransportFiniteHeight.finiteHeightLattice`. Transport a
-`FiniteHeightLattice` structure along a monotone inverse pair `f : α → β`,
-`g : β → α`. -/
 def FiniteHeightLattice.transport {α β : Type*} [Lattice α] [Lattice β]
    [I : FiniteHeightLattice α] (f : α → β) (g : β → α)
    (hf : Monotone f) (hg : Monotone g)
@@ -13,13 +10,13 @@ def FiniteHeightLattice.transport {α β : Type*} [Lattice α] [Lattice β]
  bot := f ⊥
  top := f ⊤
  height := I.height
-  longest_chain :=
+  longestChain :=
    { series :=
-        I.longest_chain.series.map f
+        I.longestChain.series.map f
          (hf.strictMono_of_injective (Function.LeftInverse.injective hgf))
-      head_series := congrArg f I.longest_chain.head_series
-      last_series := congrArg f I.longest_chain.last_series
-      length_series := I.longest_chain.length_series }
+      head_series := congrArg f I.longestChain.head_series
+      last_series := congrArg f I.longestChain.last_series
+      length_series := I.longestChain.length_series }
  chains_bounded := fun c =>
    I.chains_bounded
      (c.map g (hg.strictMono_of_injective (Function.LeftInverse.injective hfg)))
--- a/lean/Spa/Language.lean
+++ b/lean/Spa/Language.lean
@@ -1,24 +1,3 @@
-/-
-Port of `Language.agda` (the `Program` record and re-exports).
-
-Correspondence:
-  Program record      ↦ structure Program (defs in the `Program` namespace)
-  graph               ↦ Program.graph
-  State               ↦ Program.State
-  initialState        ↦ Program.initialState
-  finalState          ↦ Program.finalState
-  trace               ↦ Program.trace
-  vars, vars-Unique   ↦ Program.vars, Program.vars_nodup
-                        (Finset.toList + Finset.nodup_toList replace
-                        `to-Listˢ` and the intrinsic MapSet uniqueness)
-  states, states-complete, states-Unique
-                      ↦ Program.states, .states_complete, .states_nodup
-  code                ↦ Program.code
-  _≟_, _≟ᵉ_           ↦ (instances, automatic for Fin/products)
-  incoming            ↦ Program.incoming
-  initialState-pred-∅ ↦ Program.incoming_initialState_eq_nil
-  edge⇒incoming       ↦ Program.mem_incoming_of_edge
-/
 import Spa.Language.Base
 import Spa.Language.Semantics
 import Spa.Language.Graphs
@@ -44,7 +23,6 @@ def initialState : p.State := (buildCfg p.rootStmt).wrapInput

 def finalState : p.State := (buildCfg p.rootStmt).wrapOutput

-/-- Agda: `Program.trace`. -/
 theorem trace {ρ : Env} (h : EvalStmt [] p.rootStmt ρ) :
    Trace p.graph p.initialState p.finalState [] ρ := by
  obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := EndToEndTrace.wrap (buildCfg_sufficient h)
@@ -53,34 +31,24 @@ theorem trace {ρ : Env} (h : EvalStmt [] p.rootStmt ρ) :
  subst h₁; subst h₂
  exact tr

-/-- Agda: `vars` (via `vars-Set = Stmt-vars rootStmt`). `Finset.toList` is
-noncomputable, so the variables are listed in sorted order instead — this is
-the computable stand-in for MapSet's `to-List`. -/
 def vars : List String := p.rootStmt.vars.sort (· ≤ ·)

-/-- Agda: `vars-Unique`. -/
 theorem vars_nodup : p.vars.Nodup := Finset.sort_nodup _ _

 def states : List p.State := p.graph.indices

-/-- Agda: `states-complete`. -/
 theorem states_complete (s : p.State) : s ∈ p.states := p.graph.mem_indices s

-/-- Agda: `states-Unique`. -/
 theorem states_nodup : p.states.Nodup := p.graph.nodup_indices

-/-- Agda: `code`. -/
 def code (st : p.State) : List BasicStmt := p.graph.nodes st

-/-- Agda: `incoming`. -/
 def incoming (s : p.State) : List p.State := p.graph.predecessors s

-/-- Agda: `initialState-pred-∅`. -/
 theorem incoming_initialState_eq_nil : p.incoming p.initialState = [] :=
  Graph.wrap_predecessors_eq_nil (buildCfg p.rootStmt) p.initialState
    (by rw [Graph.wrap_inputs]; exact List.mem_singleton_self _)

-/-- Agda: `edge⇒incoming`. -/
 theorem mem_incoming_of_edge {s₁ s₂ : p.State}
    (h : (s₁, s₂) ∈ p.graph.edges) : s₁ ∈ p.incoming s₂ :=
  p.graph.mem_predecessors_of_edge h
--- a/lean/Spa/Language/Base.lean
+++ b/lean/Spa/Language/Base.lean
@@ -1,21 +1,3 @@
-/-
-Port of `Language/Base.agda`.
-
-`StringSet` (built on `Lattice/MapSet.agda`, itself on `Lattice/Map.agda`) is
-lifted to mathlib's `Finset String`: `insertˢ ↦ insert`, `emptyˢ ↦ ∅`,
-`singletonˢ ↦ {·}`, `_⊔ˢ_ ↦ ∪`, `to-List ↦ Finset.toList` (with
-`Finset.nodup_toList` standing in for the intrinsic `Unique` proof).
-
-Constructor renaming (Agda mixfix has no direct Lean counterpart):
-  _+_ ↦ Expr.add      _-_ ↦ Expr.sub     `_ ↦ Expr.var    #_ ↦ Expr.num
-  _←_ ↦ BasicStmt.assign              noop ↦ BasicStmt.noop
-  ⟨_⟩ ↦ Stmt.basic    _then_ ↦ Stmt.andThen
-  if_then_else_ ↦ Stmt.ifElse         while_repeat_ ↦ Stmt.whileLoop
-
-The `_∈ᵉ_` / `_∈ᵇ_` variable-occurrence relations are ported as
-`Expr.HasVar` / `BasicStmt.HasVar`; the commented-out lemmas relating them to
-`Expr-vars` remain unported (they were commented out in the Agda, too).
-/
 import Mathlib.Data.Finset.Basic

 namespace Spa
@@ -39,7 +21,6 @@ inductive Stmt where
  | whileLoop (e : Expr) (s : Stmt)
  deriving DecidableEq

-/-- Agda: `_∈ᵉ_`. -/
 inductive Expr.HasVar : String → Expr → Prop
  | addLeft {e₁ e₂ k} : Expr.HasVar k e₁ → Expr.HasVar k (.add e₁ e₂)
  | addRight {e₁ e₂ k} : Expr.HasVar k e₂ → Expr.HasVar k (.add e₁ e₂)
@@ -47,31 +28,26 @@ inductive Expr.HasVar : String → Expr → Prop
  | subRight {e₁ e₂ k} : Expr.HasVar k e₂ → Expr.HasVar k (.sub e₁ e₂)
  | here {k} : Expr.HasVar k (.var k)

-/-- Agda: `_∈ᵇ_`. -/
 inductive BasicStmt.HasVar : String → BasicStmt → Prop
  | assignLeft {k e} : BasicStmt.HasVar k (.assign k e)
  | assignRight {k k' e} : Expr.HasVar k e → BasicStmt.HasVar k (.assign k' e)

-/-- Agda: `Expr-vars`. -/
 def Expr.vars : Expr → Finset String
  | .add l r => l.vars ∪ r.vars
  | .sub l r => l.vars ∪ r.vars
  | .var s => {s}
  | .num _ => ∅

-/-- Agda: `BasicStmt-vars`. -/
 def BasicStmt.vars : BasicStmt → Finset String
  | .assign x e => {x} ∪ e.vars
  | .noop => ∅

-/-- Agda: `Stmt-vars`. -/
 def Stmt.vars : Stmt → Finset String
  | .basic bs => bs.vars
  | .andThen s₁ s₂ => s₁.vars ∪ s₂.vars
  | .ifElse e s₁ s₂ => (e.vars ∪ s₁.vars) ∪ s₂.vars
  | .whileLoop e s => e.vars ∪ s.vars

-/-- Agda: `Stmts-vars`. -/
 def Stmt.varsList (ss : List Stmt) : Finset String :=
  ss.foldr (fun s acc => s.vars ∪ acc) ∅

--- a/lean/Spa/Language/Graphs.lean
+++ b/lean/Spa/Language/Graphs.lean
@@ -1,34 +1,22 @@
-/-
-Port of `Language/Graphs.agda`.
-
-Representation note: `nodes : Vec (List BasicStmt) size` becomes
-`nodes : Fin size → List BasicStmt`. With that, the `Data.Vec` lookup/append
-lemma stack (`lookup-++ˡ/ʳ`, `cast-is-id`, …) lifts into mathlib's
-`Fin.append` with `Fin.append_left` / `Fin.append_right`.
-
-Correspondence:
-  _↑ˡ_/_↑ʳ_ (on Fin)  ↦ Fin.castAdd / Fin.natAdd (mathlib)
-  _↑ˡⁱ_/_↑ʳⁱ_         ↦ liftIdxL / liftIdxR
-  _↑ˡᵉ_/_↑ʳᵉ_         ↦ liftEdgeL / liftEdgeR
-  _∙_                 ↦ Graph.comp   (scoped notation ∙)
-  _↦_                 ↦ Graph.link   (scoped notation ⤳)
-  loop                ↦ Graph.loop
-  _skipto_            ↦ Graph.skipto
-  _[_]                ↦ Graph.nodes (plain application)
-  singleton, wrap     ↦ Graph.singleton, Graph.wrap
-  buildCfg            ↦ buildCfg
-  indices             ↦ List.finRange (mathlib; `fins` from Utils.agda)
-  indices-complete    ↦ List.mem_finRange
-  indices-Unique      ↦ List.nodup_finRange
-  predecessors        ↦ Graph.predecessors
-  edge⇒predecessor    ↦ Graph.mem_predecessors_of_edge
-  predecessor⇒edge    ↦ Graph.edge_of_mem_predecessors
-/
 import Spa.Language.Base
 import Mathlib.Data.Fin.Tuple.Basic
 import Mathlib.Data.List.ProdSigma
 import Mathlib.Data.List.FinRange

+def List.finCastAdd {n : ℕ} (l : List (Fin n)) (m : ℕ) : List (Fin (n + m)) :=
+  l.map (Fin.castAdd m)
+
+def List.finNatAdd {m : ℕ} (l : List (Fin m)) (n : ℕ) : List (Fin (n + m)) :=
+  l.map (Fin.natAdd n)
+
+def List.finCastAddProd {n : ℕ} (l : List (Fin n × Fin n)) (m : ℕ) :
+    List (Fin (n + m) × Fin (n + m)) :=
+  l.map (fun e => (e.1.castAdd m, e.2.castAdd m))
+
+def List.finNatAddProd {m : ℕ} (l : List (Fin m × Fin m)) (n : ℕ) :
+    List (Fin (n + m) × Fin (n + m)) :=
+  l.map (fun e => (e.1.natAdd n, e.2.natAdd n))
+
 namespace Spa

 structure Graph where
@@ -44,42 +32,22 @@ abbrev Index (g : Graph) : Type := Fin g.size

 abbrev Edge (g : Graph) : Type := g.Index × g.Index

-/-- Agda: `_↑ˡⁱ_`. -/
-def liftIdxL {n : ℕ} (l : List (Fin n)) (m : ℕ) : List (Fin (n + m)) :=
-  l.map (Fin.castAdd m)
-
-/-- Agda: `_↑ʳⁱ_`. -/
-def liftIdxR (n : ℕ) {m : ℕ} (l : List (Fin m)) : List (Fin (n + m)) :=
-  l.map (Fin.natAdd n)
-
-/-- Agda: `_↑ˡᵉ_` (with `_↑ˡ_` on pairs inlined). -/
-def liftEdgeL {n : ℕ} (l : List (Fin n × Fin n)) (m : ℕ) :
-    List (Fin (n + m) × Fin (n + m)) :=
-  l.map (fun e => (e.1.castAdd m, e.2.castAdd m))
-
-/-- Agda: `_↑ʳᵉ_` (with `_↑ʳ_` on pairs inlined). -/
-def liftEdgeR (n : ℕ) {m : ℕ} (l : List (Fin m × Fin m)) :
-    List (Fin (n + m) × Fin (n + m)) :=
-  l.map (fun e => (e.1.natAdd n, e.2.natAdd n))
-
-/-- Agda: `_∙_` — disjoint union. -/
 def comp (g₁ g₂ : Graph) : Graph where
  size := g₁.size + g₂.size
  nodes := Fin.append g₁.nodes g₂.nodes
-  edges := liftEdgeL g₁.edges g₂.size ++ liftEdgeR g₁.size g₂.edges
-  inputs := liftIdxL g₁.inputs g₂.size ++ liftIdxR g₁.size g₂.inputs
-  outputs := liftIdxL g₁.outputs g₂.size ++ liftIdxR g₁.size g₂.outputs
+  edges := g₁.edges.finCastAddProd g₂.size ++ g₂.edges.finNatAddProd g₁.size
+  inputs := g₁.inputs.finCastAdd g₂.size ++ g₂.inputs.finNatAdd g₁.size
+  outputs := g₁.outputs.finCastAdd g₂.size ++ g₂.outputs.finNatAdd g₁.size

@[inherit_doc] scoped infixr:70 " ∙ " => Graph.comp

-/-- Agda: `_↦_` — sequencing: all outputs of `g₁` feed all inputs of `g₂`. -/
 def link (g₁ g₂ : Graph) : Graph where
  size := g₁.size + g₂.size
  nodes := Fin.append g₁.nodes g₂.nodes
-  edges := liftEdgeL g₁.edges g₂.size ++ liftEdgeR g₁.size g₂.edges ++
-    (liftIdxL g₁.outputs g₂.size).product (liftIdxR g₁.size g₂.inputs)
-  inputs := liftIdxL g₁.inputs g₂.size
-  outputs := liftIdxR g₁.size g₂.outputs
+  edges := g₁.edges.finCastAddProd g₂.size ++ g₂.edges.finNatAddProd g₁.size ++
+    (g₁.outputs.finCastAdd g₂.size).product (g₂.inputs.finNatAdd g₁.size)
+  inputs := g₁.inputs.finCastAdd g₂.size
+  outputs := g₂.outputs.finNatAdd g₁.size

@[inherit_doc] scoped infixr:70 " ⤳ " => Graph.link

@@ -89,13 +57,12 @@ def loopIn (g : Graph) : Fin (2 + g.size) := (0 : Fin 2).castAdd g.size
 /-- The exit node of a `loop` graph. -/
 def loopOut (g : Graph) : Fin (2 + g.size) := (1 : Fin 2).castAdd g.size

-/-- Agda: `loop`. -/
 def loop (g : Graph) : Graph where
  size := 2 + g.size
  nodes := Fin.append (fun _ : Fin 2 => []) g.nodes
-  edges := liftEdgeR 2 g.edges ++
-    (liftIdxR 2 g.inputs).map (g.loopIn, ·) ++
-    (liftIdxR 2 g.outputs).map (·, g.loopOut) ++
+  edges := g.edges.finNatAddProd 2 ++
+    (g.inputs.finNatAdd 2).map (g.loopIn, ·) ++
+    (g.outputs.finNatAdd 2).map (·, g.loopOut) ++
    [(g.loopOut, g.loopIn), (g.loopIn, g.loopOut)]
  inputs := [g.loopIn]
  outputs := [g.loopOut]
@@ -104,16 +71,14 @@ def loop (g : Graph) : Graph where

@[simp] theorem loop_outputs (g : Graph) : (loop g).outputs = [g.loopOut] := rfl

-/-- Agda: `_skipto_` (unused by `buildCfg`, ported for parity). -/
 def skipto (g₁ g₂ : Graph) : Graph where
  size := g₁.size + g₂.size
  nodes := Fin.append g₁.nodes g₂.nodes
-  edges := liftEdgeL g₁.edges g₂.size ++ liftEdgeR g₁.size g₂.edges ++
-    (liftIdxL g₁.inputs g₂.size).product (liftIdxR g₁.size g₂.inputs)
-  inputs := liftIdxL g₁.inputs g₂.size
-  outputs := liftIdxR g₁.size g₂.inputs
+  edges := g₁.edges.finCastAddProd g₂.size ++ g₂.edges.finNatAddProd g₁.size ++
+    (g₁.inputs.finCastAdd g₂.size).product (g₂.inputs.finNatAdd g₁.size)
+  inputs := g₁.inputs.finCastAdd g₂.size
+  outputs := g₂.inputs.finNatAdd g₁.size

-/-- Agda: `singleton`. -/
 def singleton (bss : List BasicStmt) : Graph where
  size := 1
  nodes := fun _ => bss
@@ -121,14 +86,12 @@ def singleton (bss : List BasicStmt) : Graph where
  inputs := [0]
  outputs := [0]

-/-- Agda: `wrap`. -/
 def wrap (g : Graph) : Graph :=
  singleton [] ⤳ g ⤳ singleton []

 end Graph

 open Graph in
-/-- Agda: `buildCfg`. -/
 def buildCfg : Stmt → Graph
  | .basic bs => Graph.singleton [bs]
  | .andThen s₁ s₂ => buildCfg s₁ ⤳ buildCfg s₂
@@ -139,27 +102,21 @@ namespace Graph

 variable (g : Graph)

-/-- Agda: `indices` (`fins` is mathlib's `List.finRange`). -/
 def indices : List g.Index := List.finRange g.size

-/-- Agda: `indices-complete`. -/
 theorem mem_indices (idx : g.Index) : idx ∈ g.indices :=
  List.mem_finRange idx

-/-- Agda: `indices-Unique`. -/
 theorem nodup_indices : g.indices.Nodup :=
  List.nodup_finRange g.size

-/-- Agda: `predecessors`. -/
 def predecessors (idx : g.Index) : List g.Index :=
  g.indices.filter (fun idx' => (idx', idx) ∈ g.edges)

-/-- Agda: `edge⇒predecessor`. -/
 theorem mem_predecessors_of_edge {idx₁ idx₂ : g.Index}
    (h : (idx₁, idx₂) ∈ g.edges) : idx₁ ∈ g.predecessors idx₂ :=
  List.mem_filter.mpr ⟨g.mem_indices idx₁, by simpa using h⟩

-/-- Agda: `predecessor⇒edge`. -/
 theorem edge_of_mem_predecessors {idx₁ idx₂ : g.Index}
    (h : idx₁ ∈ g.predecessors idx₂) : (idx₁, idx₂) ∈ g.edges := by
  simpa using (List.mem_filter.mp h).2
--- a/lean/Spa/Language/Notation.lean
+++ b/lean/Spa/Language/Notation.lean
@@ -0,0 +1,60 @@
+import Spa.Language.Base
+
+namespace Spa
+
+/-!
+Scoped quotation syntax for writing object-language programs.
+
+`[obj_expr| … ]` builds an `Expr`, `[obj_stmt| … ]` builds a `Stmt`.
+
+Example:
+```
+[obj_stmt|
+  zero := 0;
+  pos  := zero + 1;
+  if pos { x := 1 } else { noop };
+  while x { x := x - 1 }
+]
+```
+-/
+
+/-- Expressions of the object language. -/
+declare_syntax_cat obj_expr
+
+syntax num                              : obj_expr
+syntax ident                           : obj_expr
+syntax:65 obj_expr:65 " + " obj_expr:66 : obj_expr
+syntax:65 obj_expr:65 " - " obj_expr:66 : obj_expr
+syntax "(" obj_expr ")"                 : obj_expr
+
+/-- Statements of the object language. -/
+declare_syntax_cat obj_stmt
+
+syntax "noop"                                          : obj_stmt
+syntax ident " := " obj_expr                           : obj_stmt
+syntax "if " obj_expr " { " obj_stmt " } " "else" " { " obj_stmt " } " : obj_stmt
+syntax "while " obj_expr " { " obj_stmt " } "          : obj_stmt
+syntax:50 obj_stmt:51 "; " obj_stmt:50                 : obj_stmt
+syntax "(" obj_stmt ")"                                : obj_stmt
+
+scoped syntax "[obj_expr| " obj_expr " ]" : term
+scoped syntax "[obj_stmt| " obj_stmt " ]" : term
+
+scoped macro_rules
+  | `([obj_expr| $n:num])        => `(Expr.num $n)
+  | `([obj_expr| $x:ident])      => `(Expr.var $(Lean.quote x.getId.toString))
+  | `([obj_expr| $a + $b])       => `(Expr.add [obj_expr| $a] [obj_expr| $b])
+  | `([obj_expr| $a - $b])       => `(Expr.sub [obj_expr| $a] [obj_expr| $b])
+  | `([obj_expr| ($e:obj_expr)]) => `([obj_expr| $e])
+
+scoped macro_rules
+  | `([obj_stmt| noop])           => `(Stmt.basic .noop)
+  | `([obj_stmt| $x:ident := $e]) =>
+      `(Stmt.basic (.assign $(Lean.quote x.getId.toString) [obj_expr| $e]))
+  | `([obj_stmt| $s₁ ; $s₂])      => `(Stmt.andThen [obj_stmt| $s₁] [obj_stmt| $s₂])
+  | `([obj_stmt| if $e { $s₁ } else { $s₂ }]) =>
+      `(Stmt.ifElse [obj_expr| $e] [obj_stmt| $s₁] [obj_stmt| $s₂])
+  | `([obj_stmt| while $e { $s }]) => `(Stmt.whileLoop [obj_expr| $e] [obj_stmt| $s])
+  | `([obj_stmt| ($s:obj_stmt)])  => `([obj_stmt| $s])
+
+end Spa
--- a/lean/Spa/Language/Properties.lean
+++ b/lean/Spa/Language/Properties.lean
@@ -1,36 +1,9 @@
-/-
-Port of `Language/Properties.agda`.
-
-Correspondence:
-  ↑-≢ (and the whole "ugly" Fin-disjointness block:
-    idx→f∉↑ʳᵉ, idx→f∉pair, idx→f∉cart, help, helpAll)
-                          ↦ Fin.castAdd_ne_natAdd + not_mem_edges_castAdd_link
-                            (mathlib `List.mem_append`/`mem_map`/`mem_product`
-                            replace the hand-rolled membership eliminations)
-  wrap-preds-∅            ↦ wrap_predecessors_eq_nil
-  wrap-input, wrap-output ↦ Graph.wrapInput/wrapOutput + wrap_inputs/wrap_outputs
-  Trace-∙ˡ/ʳ              ↦ Trace.comp_left / Trace.comp_right
-  Trace-↦ˡ/ʳ              ↦ Trace.link_left / Trace.link_right
-  Trace-loop              ↦ Trace.loop
-  EndToEndTrace-∙ˡ/ʳ      ↦ EndToEndTrace.comp_left / .comp_right
-  loop-edge-groups,
-  loop-edge-help          ↦ (inlined: the four edge groups are reached through
-                            `List.mem_append` directly)
-  EndToEndTrace-loop      ↦ EndToEndTrace.loop
-  EndToEndTrace-loop²     ↦ EndToEndTrace.loop_concat
-  EndToEndTrace-loop⁰     ↦ EndToEndTrace.loop_empty
-  _++_                    ↦ EndToEndTrace.concat
-  EndToEndTrace-singleton ↦ EndToEndTrace.singleton (+ .singleton_nil)
-  EndToEndTrace-wrap      ↦ EndToEndTrace.wrap
-  buildCfg-sufficient     ↦ buildCfg_sufficient
-/
 import Spa.Language.Traces

 namespace Spa

 open Graph

-/-- Agda: `↑-≢`. -/
 theorem Fin.castAdd_ne_natAdd {n m : ℕ} (i : Fin n) (j : Fin m) :
    Fin.castAdd m i ≠ Fin.natAdd n j := by
  intro h
@@ -44,7 +17,6 @@ section Embeddings

 variable {g₁ g₂ : Graph} {ρ₁ ρ₂ : Env}

-/-- Agda: `Trace-∙ˡ`. -/
 theorem Trace.comp_left {idx₁ idx₂ : g₁.Index}
    (tr : Trace g₁ idx₁ idx₂ ρ₁ ρ₂) :
    Trace (g₁ ∙ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by
@@ -57,7 +29,6 @@ theorem Trace.comp_left {idx₁ idx₂ : g₁.Index}
    · rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_left]
    · exact List.mem_append_left _ (List.mem_map_of_mem _ he)

-/-- Agda: `Trace-∙ʳ`. -/
 theorem Trace.comp_right {idx₁ idx₂ : g₂.Index}
    (tr : Trace g₂ idx₁ idx₂ ρ₁ ρ₂) :
    Trace (g₁ ∙ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ := by
@@ -70,7 +41,6 @@ theorem Trace.comp_right {idx₁ idx₂ : g₂.Index}
    · rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_right]
    · exact List.mem_append_right _ (List.mem_map_of_mem _ he)

-/-- Agda: `Trace-↦ˡ`. -/
 theorem Trace.link_left {idx₁ idx₂ : g₁.Index}
    (tr : Trace g₁ idx₁ idx₂ ρ₁ ρ₂) :
    Trace (g₁ ⤳ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by
@@ -83,7 +53,6 @@ theorem Trace.link_left {idx₁ idx₂ : g₁.Index}
    · rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_left]
    · exact List.mem_append_left _ (List.mem_append_left _ (List.mem_map_of_mem _ he))

-/-- Agda: `Trace-↦ʳ`. -/
 theorem Trace.link_right {idx₁ idx₂ : g₂.Index}
    (tr : Trace g₂ idx₁ idx₂ ρ₁ ρ₂) :
    Trace (g₁ ⤳ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ := by
@@ -97,7 +66,6 @@ theorem Trace.link_right {idx₁ idx₂ : g₂.Index}
    · exact List.mem_append_left _
        (List.mem_append_right _ (List.mem_map_of_mem _ he))

-/-- Agda: `EndToEndTrace-∙ˡ`. -/
 theorem EndToEndTrace.comp_left (etr : EndToEndTrace g₁ ρ₁ ρ₂) :
    EndToEndTrace (g₁ ∙ g₂) ρ₁ ρ₂ := by
  obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := etr
@@ -105,7 +73,6 @@ theorem EndToEndTrace.comp_left (etr : EndToEndTrace g₁ ρ₁ ρ₂) :
         i₂.castAdd g₂.size, List.mem_append_left _ (List.mem_map_of_mem _ h₂),
         tr.comp_left⟩

-/-- Agda: `EndToEndTrace-∙ʳ`. -/
 theorem EndToEndTrace.comp_right (etr : EndToEndTrace g₂ ρ₁ ρ₂) :
    EndToEndTrace (g₁ ∙ g₂) ρ₁ ρ₂ := by
  obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := etr
@@ -113,7 +80,6 @@ theorem EndToEndTrace.comp_right (etr : EndToEndTrace g₂ ρ₁ ρ₂) :
         i₂.natAdd g₁.size, List.mem_append_right _ (List.mem_map_of_mem _ h₂),
         tr.comp_right⟩

-/-- Agda: `_++_` — sequencing end-to-end traces over `⤳`. -/
 theorem EndToEndTrace.concat {ρ₃ : Env} (etr₁ : EndToEndTrace g₁ ρ₁ ρ₂)
    (etr₂ : EndToEndTrace g₂ ρ₂ ρ₃) : EndToEndTrace (g₁ ⤳ g₂) ρ₁ ρ₃ := by
  obtain ⟨i₁, h₁, i₂, h₂, tr₁⟩ := etr₁
@@ -132,7 +98,6 @@ section Loop

 variable {g : Graph} {ρ₁ ρ₂ ρ₃ : Env}

-/-- Agda: `Trace-loop`. -/
 theorem Trace.loop {idx₁ idx₂ : g.Index} (tr : Trace g idx₁ idx₂ ρ₁ ρ₂) :
    Trace (Graph.loop g) (idx₁.natAdd 2) (idx₂.natAdd 2) ρ₁ ρ₂ := by
  induction tr with
@@ -155,7 +120,6 @@ private theorem loop_nodes_at_out :
    (Graph.loop g).nodes g.loopOut = [] :=
  Fin.append_left (fun _ : Fin 2 => []) g.nodes 1

-/-- Agda: `EndToEndTrace-loop`. -/
 theorem EndToEndTrace.loop (etr : EndToEndTrace g ρ₁ ρ₂) :
    EndToEndTrace (Graph.loop g) ρ₁ ρ₂ := by
  obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := etr
@@ -176,7 +140,6 @@ private theorem loop_edge_out_in :
  refine List.mem_append_right _ ?_
  exact List.mem_cons_self _ _

-/-- Agda: `EndToEndTrace-loop²`. -/
 theorem EndToEndTrace.loop_concat (etr₁ : EndToEndTrace (Graph.loop g) ρ₁ ρ₂)
    (etr₂ : EndToEndTrace (Graph.loop g) ρ₂ ρ₃) :
    EndToEndTrace (Graph.loop g) ρ₁ ρ₃ := by
@@ -187,7 +150,6 @@ theorem EndToEndTrace.loop_concat (etr₁ : EndToEndTrace (Graph.loop g) ρ₁
  exact ⟨g.loopIn, List.mem_singleton_self _, g.loopOut, List.mem_singleton_self _,
    Trace.concat tr₁ loop_edge_out_in tr₂⟩

-/-- Agda: `EndToEndTrace-loop⁰`. -/
 theorem EndToEndTrace.loop_empty {ρ : Env} : EndToEndTrace (Graph.loop g) ρ ρ := by
  have hedge : ((g.loopIn, g.loopOut) : (Graph.loop g).Edge) ∈ (Graph.loop g).edges :=
    List.mem_append_right _ (List.mem_cons_of_mem _ (List.mem_cons_self _ _))
@@ -199,24 +161,19 @@ end Loop

 /-! ### Singletons, wrap, and the main result -/

-/-- Agda: `EndToEndTrace-singleton`. -/
 theorem EndToEndTrace.singleton {bss : List BasicStmt} {ρ₁ ρ₂ : Env}
    (h : EvalBasicStmts ρ₁ bss ρ₂) : EndToEndTrace (Graph.singleton bss) ρ₁ ρ₂ :=
  ⟨(0 : Fin 1), List.mem_singleton_self _, (0 : Fin 1), List.mem_singleton_self _,
   Trace.single h⟩

-/-- Agda: `EndToEndTrace-singleton[]`. -/
 theorem EndToEndTrace.singleton_nil (ρ : Env) :
    EndToEndTrace (Graph.singleton []) ρ ρ :=
  EndToEndTrace.singleton EvalBasicStmts.nil

-/-- Agda: `EndToEndTrace-wrap`. -/
 theorem EndToEndTrace.wrap {g : Graph} {ρ₁ ρ₂ : Env}
    (etr : EndToEndTrace g ρ₁ ρ₂) : EndToEndTrace (Graph.wrap g) ρ₁ ρ₂ :=
  (EndToEndTrace.singleton_nil ρ₁).concat (etr.concat (EndToEndTrace.singleton_nil ρ₂))

-/-- Agda: `buildCfg-sufficient` — every terminating execution is witnessed by
-an end-to-end trace through the control-flow graph. -/
 theorem buildCfg_sufficient {s : Stmt} {ρ₁ ρ₂ : Env}
    (h : EvalStmt ρ₁ s ρ₂) : EndToEndTrace (buildCfg s) ρ₁ ρ₂ := by
  induction h with
@@ -235,11 +192,9 @@ theorem buildCfg_sufficient {s : Stmt} {ρ₁ ρ₂ : Env}

 /-! ### The wrapped graph's entry has no predecessors (Agda's "ugly" block) -/

-/-- The input of `wrap g` (Agda: `wrap-input`). -/
 def Graph.wrapInput (g : Graph) : (Graph.wrap g).Index :=
  (0 : Fin 1).castAdd ((g ⤳ Graph.singleton []).size)

-/-- The output of `wrap g` (Agda: `wrap-output`). -/
 def Graph.wrapOutput (g : Graph) : (Graph.wrap g).Index :=
  Fin.natAdd 1 ((Fin.natAdd g.size (0 : Fin 1)))

@@ -249,8 +204,6 @@ theorem Graph.wrap_inputs (g : Graph) :
 theorem Graph.wrap_outputs (g : Graph) :
    (Graph.wrap g).outputs = [g.wrapOutput] := rfl

-/-- Agda: `help`/`helpAll` — no edge of `singleton [] ⤳ g₂` ends at a
-`castAdd`-injected node (all edge targets are `natAdd`s). -/
 private theorem not_mem_edges_castAdd_link {g₂ : Graph} (i : Fin 1)
    (idx : (Graph.singleton [] ⤳ g₂).Index) :
    ((idx, i.castAdd g₂.size) : (Graph.singleton [] ⤳ g₂).Edge)
@@ -259,7 +212,7 @@ private theorem not_mem_edges_castAdd_link {g₂ : Graph} (i : Fin 1)
  rcases List.mem_append.mp h with h' | h'
  · rcases List.mem_append.mp h' with h'' | h''
    · -- lifted edges of `singleton []`: there are none
-      simp [Graph.singleton, Graph.liftEdgeL] at h''
+      simp [Graph.singleton, List.finCastAddProd] at h''
    · -- lifted edges of g₂: targets are natAdd
      obtain ⟨e, _, heq⟩ := List.mem_map.mp h''
      exact Fin.castAdd_ne_natAdd i e.2 (congrArg Prod.snd heq).symm
@@ -268,8 +221,6 @@ private theorem not_mem_edges_castAdd_link {g₂ : Graph} (i : Fin 1)
    obtain ⟨j, -, heq⟩ := List.mem_map.mp hb
    exact Fin.castAdd_ne_natAdd i j heq.symm

-/-- Agda: `wrap-preds-∅` — the entry node of a wrapped graph has no
-incoming edges. -/
 theorem Graph.wrap_predecessors_eq_nil (g : Graph) (idx : (Graph.wrap g).Index)
    (h : idx ∈ (Graph.wrap g).inputs) :
    (Graph.wrap g).predecessors idx = [] := by
--- a/lean/Spa/Language/Semantics.lean
+++ b/lean/Spa/Language/Semantics.lean
@@ -1,23 +1,6 @@
-/-
-Port of `Language/Semantics.agda`.
-
-Correspondence:
-  Value (↑ᶻ)        ↦ Value.int
-  Env               ↦ Env (= List (String × Value))
-  _∈_ (env lookup)  ↦ Env.Mem
-  _,_⇒ᵉ_            ↦ EvalExpr
-  _,_⇒ᵇ_            ↦ EvalBasicStmt
-  _,_⇒ᵇˢ_           ↦ EvalBasicStmts
-  _,_⇒ˢ_            ↦ EvalStmt
-  LatticeInterpretation:
-    ⟦_⟧             ↦ interp
-    ⟦⟧-respects-≈   ↦ (trivial with `=`; field dropped)
-    ⟦⟧-⊔-∨          ↦ interp_sup
-    ⟦⟧-⊓-∧          ↦ interp_inf
-    (the `Utils` combinators `_⇒_`, `_∨_`, `_∧_` are inlined as plain logic)
-/
 import Spa.Language.Base
 import Spa.Lattice
+import Spa.Interp

 namespace Spa

@@ -27,13 +10,11 @@ inductive Value where

 def Env : Type := List (String × Value)

-/-- Agda: `_∈_` on environments — lookup respecting shadowing. -/
 inductive Env.Mem : String × Value → Env → Prop
  | here (s : String) (v : Value) (ρ : Env) : Env.Mem (s, v) ((s, v) :: ρ)
  | there (s s' : String) (v v' : Value) (ρ : Env) :
      ¬(s = s') → Env.Mem (s, v) ρ → Env.Mem (s, v) ((s', v') :: ρ)

-/-- Agda: `_,_⇒ᵉ_`. -/
 inductive EvalExpr : Env → Expr → Value → Prop
  | num (ρ : Env) (n : ℕ) : EvalExpr ρ (.num n) (.int n)
  | var (ρ : Env) (x : String) (v : Value) :
@@ -45,20 +26,17 @@ inductive EvalExpr : Env → Expr → Value → Prop
      EvalExpr ρ e₁ (.int z₁) → EvalExpr ρ e₂ (.int z₂) →
      EvalExpr ρ (.sub e₁ e₂) (.int (z₁ - z₂))

-/-- Agda: `_,_⇒ᵇ_`. -/
 inductive EvalBasicStmt : Env → BasicStmt → Env → Prop
  | noop (ρ : Env) : EvalBasicStmt ρ .noop ρ
  | assign (ρ : Env) (x : String) (e : Expr) (v : Value) :
      EvalExpr ρ e v → EvalBasicStmt ρ (.assign x e) ((x, v) :: ρ)

-/-- Agda: `_,_⇒ᵇˢ_`. -/
 inductive EvalBasicStmts : Env → List BasicStmt → Env → Prop
  | nil {ρ : Env} : EvalBasicStmts ρ [] ρ
  | cons {ρ₁ ρ₂ ρ₃ : Env} {bs : BasicStmt} {bss : List BasicStmt} :
      EvalBasicStmt ρ₁ bs ρ₂ → EvalBasicStmts ρ₂ bss ρ₃ →
      EvalBasicStmts ρ₁ (bs :: bss) ρ₃

-/-- Agda: `_,_⇒ˢ_`. -/
 inductive EvalStmt : Env → Stmt → Env → Prop
  | basic (ρ₁ ρ₂ : Env) (bs : BasicStmt) :
      EvalBasicStmt ρ₁ bs ρ₂ → EvalStmt ρ₁ (.basic bs) ρ₂
@@ -79,10 +57,7 @@ inductive EvalStmt : Env → Stmt → Env → Prop
      EvalExpr ρ e (.int 0) →
      EvalStmt ρ (.whileLoop e s) ρ

-/-- Agda: `LatticeInterpretation` (used there as an instance argument `⦃·⦄`,
-hence a typeclass here). -/
-class LatticeInterpretation (L : Type*) [Lattice L] where
-  interp : L → Value → Prop
+class LatticeInterpretation (L : Type*) [Lattice L] extends Interp L (Value → Prop) where
  interp_sup : ∀ {l₁ l₂ : L} (v : Value),
    interp l₁ v ∨ interp l₂ v → interp (l₁ ⊔ l₂) v
  interp_inf : ∀ {l₁ l₂ : L} (v : Value),
--- a/lean/Spa/Language/Traces.lean
+++ b/lean/Spa/Language/Traces.lean
@@ -1,18 +1,8 @@
-/-
-Port of `Language/Traces.agda`.
-
-Correspondence:
-  Trace          ↦ Trace (a `Prop`-valued inductive; only used in proofs)
-  _++⟨_⟩_        ↦ Trace.concat
-  EndToEndTrace  ↦ EndToEndTrace (a `Prop`-valued structure, like `∃`; its
-                   fields are accessed by destructuring inside proofs)
-/
 import Spa.Language.Semantics
 import Spa.Language.Graphs

 namespace Spa

-/-- Agda: `Trace`. -/
 inductive Trace (g : Graph) : g.Index → g.Index → Env → Env → Prop
  | single {ρ₁ ρ₂ : Env} {idx : g.Index} :
      EvalBasicStmts ρ₁ (g.nodes idx) ρ₂ → Trace g idx idx ρ₁ ρ₂
@@ -20,7 +10,6 @@ inductive Trace (g : Graph) : g.Index → g.Index → Env → Env → Prop
      EvalBasicStmts ρ₁ (g.nodes idx₁) ρ₂ → (idx₁, idx₂) ∈ g.edges →
      Trace g idx₂ idx₃ ρ₂ ρ₃ → Trace g idx₁ idx₃ ρ₁ ρ₃

-/-- Agda: `_++⟨_⟩_`. -/
 theorem Trace.concat {g : Graph} {idx₁ idx₂ idx₃ idx₄ : g.Index}
    {ρ₁ ρ₂ ρ₃ : Env} (tr₁ : Trace g idx₁ idx₂ ρ₁ ρ₂)
    (he : (idx₂, idx₃) ∈ g.edges) (tr₂ : Trace g idx₃ idx₄ ρ₂ ρ₃) :
@@ -29,7 +18,6 @@ theorem Trace.concat {g : Graph} {idx₁ idx₂ idx₃ idx₄ : g.Index}
  | single hbs => exact Trace.edge hbs he tr₂
  | edge hbs he' _ ih => exact Trace.edge hbs he' (ih he tr₂)

-/-- Agda: `EndToEndTrace` (an existential package, destructured in proofs). -/
 inductive EndToEndTrace (g : Graph) (ρ₁ ρ₂ : Env) : Prop
  | intro (idx₁ : g.Index) (idx₁_mem : idx₁ ∈ g.inputs)
      (idx₂ : g.Index) (idx₂_mem : idx₂ ∈ g.outputs)
--- a/lean/Spa/Lattice.lean
+++ b/lean/Spa/Lattice.lean
@@ -58,7 +58,7 @@ structure PointedLTSeries (α : Type*) (f t : α)(n : ℕ) [Preorder α] where

 class FiniteHeightLattice (α : Type*) [Lattice α] extends Bot α, Top α where
  height : ℕ
-  longest_chain : PointedLTSeries α ⊥ ⊤ height
+  longestChain : PointedLTSeries α ⊥ ⊤ height
  chains_bounded : BoundedChains α height

 namespace FixedHeight
@@ -70,7 +70,7 @@ theorem bot_le [FiniteHeightLattice α] : ∀ (a : α), ⊥ ≤ a := by
  by_cases heq : ⊥ ⊓ a = ⊥
  · exact inf_eq_left.mp heq
  · exfalso
-    have lc := FiniteHeightLattice.longest_chain (α := α)
+    have lc := FiniteHeightLattice.longestChain (α := α)
    have hlt : ⊥ ⊓ a < lc.series.head := by
      rw [lc.head_series]
      exact lt_of_le_of_ne inf_le_left heq
--- a/lean/Spa/Lattice/AboveBelow.lean
+++ b/lean/Spa/Lattice/AboveBelow.lean
@@ -1,25 +1,7 @@
-/-
-Port of `Lattice/AboveBelow.agda`: the flat lattice obtained by adjoining a
-top and bottom element to an (unordered, decidable-equality) type.
-
-With propositional equality the `_≈_` data type and its equivalence/decidability
-proofs disappear (`deriving DecidableEq`). The lattice itself cannot be lifted:
-mathlib has no "flat lattice on a discrete type". The `Lattice` instance is
-built with `Lattice.mk'`, which — exactly like the Agda module — consumes the
-two semilattices (comm/assoc, idempotence derived) plus the absorption laws,
-and defines `a ≤ b ↔ a ⊔ b = b` (Agda's `_≼_`).
-
-The Agda module's `Plain x` submodule (the witness `x` seeds the longest chain
-`⊥ ≺ [x] ≺ ⊤`) becomes `plainFixedHeight x`; the boundedness proof `isLongest`
-is restated through a rank function since chains are mathlib `LTSeries` rather
-than a pattern-matchable inductive (the `¬-Chain-⊤`-style case analysis lives
-in `rank_strictMono`).
-/
 import Spa.Lattice

 namespace Spa

-/-- Agda: `AboveBelow` with constructors `⊥`, `⊤`, `[_]`. -/
 inductive AboveBelow (α : Type*) where
  | bot
  | top
@@ -28,7 +10,6 @@ inductive AboveBelow (α : Type*) where

 namespace AboveBelow

-/-- Agda: the `Showable` instance. -/
 instance {α : Type*} [ToString α] : ToString (AboveBelow α) where
  toString
    | bot => "⊥"
@@ -53,9 +34,6 @@ instance : Min (AboveBelow α) where
    | mk _, bot => bot
    | mk x, top => mk x

-/-! Agda: `⊥⊔x≡x`, `⊤⊔x≡⊤`, `x⊔⊥≡x`, `x⊔⊤≡⊤`, and the `[x]⊔[y]` reductions
-(`x≈y⇒[x]⊔[y]≡[x]` / `x̷≈y⇒[x]⊔[y]≡⊤` are the two branches of `mk_sup_mk`). -/
-
@[simp] theorem bot_sup (x : AboveBelow α) : bot ⊔ x = x := rfl
@[simp] theorem top_sup (x : AboveBelow α) : top ⊔ x = top := rfl
@[simp] theorem sup_bot (x : AboveBelow α) : x ⊔ bot = x := by cases x <;> rfl
@@ -70,46 +48,38 @@ instance : Min (AboveBelow α) where
@[simp] theorem mk_inf_mk (x y : α) :
    (mk x ⊓ mk y : AboveBelow α) = if x = y then mk x else bot := rfl

-/-- Agda: `⊔-comm`. -/
 protected theorem sup_comm (a b : AboveBelow α) : a ⊔ b = b ⊔ a := by
  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> simp only
    [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk]
  split_ifs with h₁ h₂ h₂ <;> simp_all

-/-- Agda: `⊔-assoc`. -/
 protected theorem sup_assoc (a b c : AboveBelow α) : a ⊔ b ⊔ c = a ⊔ (b ⊔ c) := by
  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> rcases c with _ | _ | z <;>
    simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk]
  split_ifs <;> simp_all

-/-- Agda: `⊓-comm`. -/
 protected theorem inf_comm (a b : AboveBelow α) : a ⊓ b = b ⊓ a := by
  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> simp only
    [bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk]
  split_ifs with h₁ h₂ h₂ <;> simp_all

-/-- Agda: `⊓-assoc`. -/
 protected theorem inf_assoc (a b c : AboveBelow α) : a ⊓ b ⊓ c = a ⊓ (b ⊓ c) := by
  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> rcases c with _ | _ | z <;>
    simp only [bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk]
  split_ifs <;> simp_all

-/-- Agda: `absorb-⊔-⊓`. -/
 protected theorem sup_inf_self (a b : AboveBelow α) : a ⊔ a ⊓ b = a := by
  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;>
    simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk,
               bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk] <;>
    try (split_ifs <;> simp_all)

-/-- Agda: `absorb-⊓-⊔`. -/
 protected theorem inf_sup_self (a b : AboveBelow α) : a ⊓ (a ⊔ b) = a := by
  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;>
    simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk,
               bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk] <;>
    try (split_ifs <;> simp_all)

-/-- Agda: `isLattice` (via the two semilattices + absorption, like the Agda
-record; `Lattice.mk'` derives idempotence and sets `a ≤ b ↔ a ⊔ b = b`). -/
 instance : Lattice (AboveBelow α) :=
  Lattice.mk' AboveBelow.sup_comm AboveBelow.sup_assoc
    AboveBelow.inf_comm AboveBelow.inf_assoc
@@ -117,11 +87,9 @@ instance : Lattice (AboveBelow α) :=

 theorem le_iff {a b : AboveBelow α} : a ≤ b ↔ a ⊔ b = b := sup_eq_right.symm

-/-- Agda: `⊥≺[x]` (the `≤` part; `⊥` is least). -/
 theorem bot_le' (a : AboveBelow α) : (bot : AboveBelow α) ≤ a :=
  le_iff.mpr (bot_sup a)

-/-- Agda: `[x]≺⊤` (the `≤` part; `⊤` is greatest). -/
 theorem le_top' (a : AboveBelow α) : a ≤ (top : AboveBelow α) :=
  le_iff.mpr (sup_top a)

@@ -134,9 +102,6 @@ theorem mk_lt_top (x : α) : (mk x : AboveBelow α) < top :=
 theorem bot_lt_top : (bot : AboveBelow α) < top :=
  lt_of_le_of_ne (bot_le' _) (by simp)

-/-- The order of the flat lattice, by cases (used to discharge the
-monotonicity obligations that were `postulate`d in `Analysis/Sign.agda` and
-`Analysis/Constant.agda`). -/
 theorem le_cases {a b : AboveBelow α} (h : a ≤ b) :
    a = bot ∨ b = top ∨ a = b := by
  have hsup := le_iff.mp h
@@ -183,18 +148,12 @@ theorem monotone₂_of_strict {β γ : Type*} [DecidableEq β] [DecidableEq γ]
      · rw [htopr x hx]; exact le_top' _
    · exact le_rfl

-/-! ### Interpretations of flat lattices
-
-The `⟦⟧-⊔-∨` / `⟦⟧-⊓-∧` proofs of `Analysis/Sign.agda` and
-`Analysis/Constant.agda` are the same case analysis; only the meaning of the
-plain elements differs. Factored here, they need just `P ⊥ ↦ False`,
-`P ⊤ ↦ True`, and (for `⊓`) disjointness of distinct plain elements. -/
+/-! ### Interpretations of flat lattices -/

 section Interp

 variable {V : Type*} {P : AboveBelow α → V → Prop}

-/-- Agda: `⟦⟧ᵍ-⊔ᵍ-∨` / `⟦⟧ᶜ-⊔ᶜ-∨`, generalized. -/
 theorem interp_sup_of (hbot : ∀ v, ¬P bot v) (htop : ∀ v, P top v)
    {s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∨ P s₂ v) : P (s₁ ⊔ s₂) v := by
  rcases s₁ with _ | _ | x
@@ -208,7 +167,6 @@ theorem interp_sup_of (hbot : ∀ v, ¬P bot v) (htop : ∀ v, P top v)
      · next heq => subst heq; exact h.elim id id
      · exact htop v

-/-- Agda: `⟦⟧ᵍ-⊓ᵍ-∧` / `⟦⟧ᶜ-⊓ᶜ-∧`, generalized. -/
 theorem interp_inf_of
    (hdisj : ∀ {x y : α}, x ≠ y → ∀ v, ¬(P (mk x) v ∧ P (mk y) v))
    {s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∧ P s₂ v) : P (s₁ ⊓ s₂) v := by
@@ -258,22 +216,17 @@ theorem rank_strictMono : StrictMono (rank : AboveBelow α → ℕ) := by
  · simp [rank]
  · exact absurd hab (not_mk_lt_mk x y)

-/-- Agda: `isLongest` — no chain is longer than 2. -/
 theorem boundedChains : BoundedChains (AboveBelow α) 2 := fun c => by
  have h := LTSeries.head_add_length_le_nat (c.map rank rank_strictMono)
  rw [LTSeries.head_map, LTSeries.last_map, LTSeries.map_length] at h
  have h2 : rank c.last ≤ 2 := by cases c.last <;> simp [rank]
  omega

-/-- Agda: `Plain.longestChain`/`Plain.fixedHeight` and
-`Plain.isFiniteHeightLattice`/`Plain.finiteHeightLattice` — the witness
-(`default`, playing the role of the Agda module parameter `x`) seeds the chain
-`⊥ ≺ [x] ≺ ⊤` of length 2. -/
 instance [Inhabited α] : FiniteHeightLattice (AboveBelow α) where
  bot := bot
  top := top
  height := 2
-  longest_chain :=
+  longestChain :=
    { series :=
        ((RelSeries.singleton _ bot).snoc (mk default)
            (by rw [RelSeries.last_singleton]; exact bot_lt_mk default)).snoc top
--- a/lean/Spa/Lattice/IterProd.lean
+++ b/lean/Spa/Lattice/IterProd.lean
@@ -1,21 +1,3 @@
-/-
-Port of `Lattice/IterProd.agda`: the `k`-fold product `A × (A × ⋯ × B)`.
-
-With propositional equality and typeclasses, the Agda `Everything` record
-(which threaded the lattice operations and the conditional fixed-height proof
-through one recursion, so that the operations built by separate recursions
-would agree) is no longer needed: the `Lattice` instance is one recursive
-definition, and the fixed-height structure is another recursion over it.
-
-Correspondence:
-  IterProd            ↦ Spa.IterProd
-  build               ↦ Spa.IterProd.build
-  isLattice/lattice   ↦ instance Spa.IterProd.instLattice
-  fixedHeight,
-  isFiniteHeightLattice,
-  finiteHeightLattice ↦ Spa.IterProd.fixedHeight (+ instFiniteHeight instance)
-  ⊥-built             ↦ Spa.IterProd.bot_fixedHeight
-/
 import Spa.Lattice.Prod
 import Spa.Lattice.Unit

@@ -23,8 +5,6 @@ namespace Spa

 universe u

-/-- Agda: `IterProd k = iterate k (A × ·) B`. (As in the Agda module, `A` and
-`B` are constrained to the same universe to keep the recursion simple.) -/
 def IterProd (A B : Type u) : ℕ → Type u
  | 0 => B
  | k + 1 => A × IterProd A B k
@@ -43,7 +23,6 @@ instance instDecidableEq [DecidableEq A] [DecidableEq B] :
  | 0 => inferInstanceAs (DecidableEq B)
  | k + 1 => @instDecidableEqProd A (IterProd A B k) _ (instDecidableEq k)

-/-- Agda: `build`. -/
 def build (a : A) (b : B) : (k : ℕ) → IterProd A B k
  | 0 => b
  | k + 1 => (a, build a b k)
--- a/lean/Spa/Lattice/Prod.lean
+++ b/lean/Spa/Lattice/Prod.lean
@@ -68,25 +68,25 @@ instance prod [A : FiniteHeightLattice α] [B : FiniteHeightLattice β] :
  bot := ((⊥ : α), (⊥ : β))
  top := ((⊤ : α), (⊤ : β))
  height := A.height + B.height
-  longest_chain :=
+  longestChain :=
    { series :=
        RelSeries.smash
-          (A.longest_chain.series.map (fun a => (a, (⊥ : β)))
+          (A.longestChain.series.map (fun a => (a, (⊥ : β)))
            (fun _ _ h => Prod.mk_lt_mk_iff_left.mpr h))
-          (B.longest_chain.series.map (fun b => ((⊤ : α), b))
+          (B.longestChain.series.map (fun b => ((⊤ : α), b))
            (fun _ _ h => Prod.mk_lt_mk_iff_right.mpr h))
-          (by simp [A.longest_chain.last_series, B.longest_chain.head_series])
+          (by simp [A.longestChain.last_series, B.longestChain.head_series])
      head_series :=
        (RelSeries.head_smash _).trans
          ((LTSeries.head_map _ _ _).trans
-            (congrArg (·, (⊥ : β)) A.longest_chain.head_series))
+            (congrArg (·, (⊥ : β)) A.longestChain.head_series))
      last_series :=
        (RelSeries.last_smash _).trans
          ((LTSeries.last_map _ _ _).trans
-            (congrArg ((⊤ : α), ·) B.longest_chain.last_series))
+            (congrArg ((⊤ : α), ·) B.longestChain.last_series))
      length_series := by
-        show A.longest_chain.series.length + B.longest_chain.series.length = _
-        rw [A.longest_chain.length_series, B.longest_chain.length_series] }
+        show A.longestChain.series.length + B.longestChain.series.length = _
+        rw [A.longestChain.length_series, B.longestChain.length_series] }
  chains_bounded := fun c => by
    obtain ⟨c₁, c₂, -, -, -, -, hlen⟩ := LTSeries.exists_unzip c
    have h₁ := A.chains_bounded c₁
--- a/lean/Spa/Lattice/Unit.lean
+++ b/lean/Spa/Lattice/Unit.lean
@@ -1,28 +1,18 @@
-/-
-Port of `Lattice/Unit.agda`.
-
-The lattice structure itself (`_⊔_`, `_⊓_`, all semilattice/lattice laws) is
-lifted into mathlib: `PUnit.instLinearOrder` provides `Lattice PUnit`.
-What remains is the fixed-height structure: the unit lattice has height 0.
-/
 import Spa.Lattice

 namespace Spa

-/-- Chains in a subsingleton order are bounded by any `n` (Agda: the `bounded`
-field of `Lattice/Unit.agda`'s `fixedHeight`, generalized). -/
 theorem boundedChains_of_subsingleton (α : Type*) [Preorder α] [Subsingleton α]
    (n : ℕ) : BoundedChains α n := fun c => by
  by_contra hc
  push_neg at hc
  exact (c.step ⟨0, by omega⟩).ne (Subsingleton.elim _ _)

-/-- Agda: `Lattice/Unit.agda`'s `fixedHeight`. -/
 instance : FiniteHeightLattice PUnit where
  bot := PUnit.unit
  top := PUnit.unit
  height := 0
-  longest_chain := { series := RelSeries.singleton _ PUnit.unit, head_series := refl _, last_series := refl _, length_series := refl _ }
+  longestChain := { series := RelSeries.singleton _ PUnit.unit, head_series := refl _, last_series := refl _, length_series := refl _ }
  chains_bounded := boundedChains_of_subsingleton PUnit 0

 end Spa
--- a/lean/Spa/Showable.lean
+++ b/lean/Spa/Showable.lean
@@ -1,16 +1,8 @@
-/-
-Port of `Showable.agda` (plus the `Showable` instances that lived on
-`Lattice/Map.agda` and `Lattice/AboveBelow.agda`).
-
-Lean has `ToString`, but its `String` instance does not quote (the Agda one
-does), so to reproduce the Agda output exactly we port the class as-is.
-/
 import Spa.Lattice.FiniteMap
 import Spa.Lattice.AboveBelow

 namespace Spa

-/-- Agda: `Showable` (`show` is a Lean keyword, hence `show'`). -/
 class Showable (α : Type*) where
  show' : α → String

@@ -29,15 +21,12 @@ instance {α β : Type*} [Showable α] [Showable β] : Showable (α × β) :=

 instance : Showable PUnit := ⟨fun _ => "()"⟩

-/-- Agda: the `Showable` instance of `Lattice/AboveBelow.agda`. -/
 instance {α : Type*} [Showable α] : Showable (AboveBelow α) :=
  ⟨fun
    | .bot => "⊥"
    | .top => "⊤"
    | .mk x => show' x⟩

-/-- Agda: the `Showable` instance of `Lattice/Map.agda` (inherited by
-`FiniteMap`). -/
 instance {α β : Type*} {ks : List α} [Showable α] [Showable β] :
    Showable (FiniteMap α β ks) :=
  ⟨fun fm =>
Author	SHA1	Message	Date
Danila Fedorin	30d2960fca	Add scoped quotation syntax for object-language programs Introduce [spa_e\| ... ] for Expr and [spa\| ... ] for Stmt, scoped to the Spa namespace via a dedicated syntax category and macro_rules. This removes the deeply nested .andThen / .basic (.assign ...) boilerplate when writing programs; Main.lean's test programs are rewritten to use it. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018Yq5SmPQfNfzAEUpUXRo66	2026-06-23 14:28:06 -05:00
Danila Fedorin	b1dc725ced	Apply some cleanups to Graphs.lean	2026-06-23 14:10:54 -05:00
Danila Fedorin	ed88f4ce94	Use 'interp' to add [[ bla ]] notation for analysis Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-06-23 13:29:54 -05:00
Danila Fedorin	8ce6e5e4e4	Have LatticeInterpretation extend Interp LatticeInterpretation now extends Interp L (Value → Prop), so each analysis defines only its LatticeInterpretation instance and gets the ⟦⟧ notation for free. Drops the standalone per-analysis Interp instances (signInterp and the anonymous constInterp). The Interp class is kept for other uses. The interp*_mk_disjoint bootstrap lemmas now state on the raw interp function since they feed the instance and run before any Interp instance exists; the trivial sup/inf wrappers are inlined into the instance. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>	2026-06-23 13:02:45 -05:00
Danila Fedorin	6afa7df444	Remove unused plus/minus mono_left/mono_right projections These eight one-line projections of plus_mono₂/minus_mono₂ were never referenced; eval_mono uses the bundled Monotone₂ facts directly. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>	2026-06-23 12:42:53 -05:00
Danila Fedorin	7f753a4f38	Delete more LLM-generated comments from the migration	2026-06-23 12:29:46 -05:00
Danila Fedorin	21b2e3dd98	Rename longest_chain to longestChain for convention	2026-06-23 11:49:45 -05:00
Danila Fedorin	5e0c002fd5	Delete 'Agda:' migration comments from Forward Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-06-23 11:44:50 -05:00
Danila Fedorin	20daf817e4	Clean up Sign correctness proofs Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>	2026-06-23 11:44:33 -05:00
Danila Fedorin	2044d4b2b6	Start working on notation for formalization Per convention, create a new instance for 'interpretable' thing, with an fundep'ed semantic domain. I feel at peace with this notation even though it conflicts with Mathlib's quotients. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>	2026-06-23 10:23:44 -05:00