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

lean/Main.lean

@@ -1,6 +1,5 @@
 import Spa.Analysis.Sign
 import Spa.Analysis.Constant
-import Spa.Analysis.Reaching
 import Spa.Language.Notation
 
 namespace Spa
@@ -27,11 +26,10 @@ def testCodeCond₂ : Stmt := [obj_stmt|
   if var { x := 1 } else { noop }
 ]
 
-def testProgram : Program := { rootStmt := testCode }
+def testProgram : Program := ⟨testCode⟩
 
 end Spa
 
 def main : IO Unit :=
   IO.println (Spa.ConstAnalysis.output Spa.testProgram ++ "\n" ++
-              Spa.SignAnalysis.output Spa.testProgram ++ "\n" ++
+              Spa.SignAnalysis.output Spa.testProgram)
-              Spa.ReachingAnalysis.output Spa.testProgram)

lean/Spa.lean

@@ -1,9 +1,11 @@
 import Spa.Lattice
 import Spa.Fixedpoint
+import Spa.Isomorphism
 import Spa.Lattice.Unit
+import Spa.Lattice.Prod
 import Spa.Lattice.AboveBelow
+import Spa.Lattice.IterProd
 import Spa.Lattice.FiniteMap
-import Spa.Lattice.Bool
 import Spa.Language.Base
 import Spa.Language.Notation
 import Spa.Language.Semantics
@@ -19,10 +21,3 @@ import Spa.Showable
 import Spa.Analysis.Utils
 import Spa.Analysis.Sign
 import Spa.Analysis.Constant
-import Spa.Language.Tagged.Id
-import Spa.Language.Tagged.Derive
-import Spa.Language.Tagged.Basic
-import Spa.Language.Tagged.Properties
-import Spa.Language.Tagged.Graphs
-import Spa.Analysis.Reaching
-import Spa.Transformation.Licm

lean/Spa/Analysis/Constant.lean

@@ -5,8 +5,6 @@ import Spa.Showable
 
 namespace Spa
 
-open Forward
-
 abbrev ConstLattice : Type := AboveBelow ℤ
 
 namespace ConstAnalysis
@@ -27,22 +25,24 @@ def minus : ConstLattice → ConstLattice → ConstLattice
   | _, top => top
   | mk z₁, mk z₂ => mk (z₁ - z₂)
 
-lemma plus_mono₂ : Monotone₂ plus :=
+theorem plus_mono₂ : Monotone₂ plus :=
   AboveBelow.monotone₂_of_strict plus
-    (fun y => by aesop) (fun x => by aesop)
+    (fun y => by cases y <;> rfl) (fun x => by cases x <;> rfl)
-    (fun y hy => by aesop) (fun x hx => by aesop)
+    (fun y hy => by cases y <;> first | exact absurd rfl hy | rfl)
+    (fun x hx => by cases x <;> first | exact absurd rfl hx | rfl)
 
-lemma minus_mono₂ : Monotone₂ minus :=
+theorem minus_mono₂ : Monotone₂ minus :=
   AboveBelow.monotone₂_of_strict minus
-    (fun y => by aesop) (fun x => by aesop)
+    (fun y => by cases y <;> rfl) (fun x => by cases x <;> rfl)
-    (fun y hy => by aesop) (fun x hx => by aesop)
+    (fun y hy => by cases y <;> first | exact absurd rfl hy | rfl)
+    (fun x hx => by cases x <;> first | exact absurd rfl hx | rfl)
 
 def interpConst : ConstLattice → Value → Prop
   | .bot, _ => False
   | .top, _ => True
   | .mk z, v => v = .int z
 
-lemma interpConst_mk_disjoint {z₁ z₂ : ℤ} (hne : z₁ ≠ z₂) {v : Value} :
+theorem interpConst_mk_disjoint {z₁ z₂ : ℤ} (hne : z₁ ≠ z₂) {v : Value} :
     ¬(interpConst (.mk z₁) v ∧ interpConst (.mk z₂) v) := by
   rintro ⟨h₁, h₂⟩
   rw [h₁] at h₂
@@ -63,7 +63,7 @@ def eval : Expr → VariableValues ConstLattice prog → ConstLattice
     if h : FiniteMap.MemKey k vs then (FiniteMap.locate h).1 else .top
   | .num n, _ => .mk n
 
-lemma eval_mono (e : Expr) : Monotone (eval prog e) := by
+theorem eval_mono (e : Expr) : Monotone (eval prog e) := by
   induction e with
   | add e₁ e₂ ih₁ ih₂ =>
     intro vs₁ vs₂ h
@@ -75,12 +75,12 @@ lemma eval_mono (e : Expr) : Monotone (eval prog e) := by
     intro vs₁ vs₂ h
     simp only [eval]
     by_cases hk : k ∈ prog.vars
-    · rw [dif_pos (FiniteMap.MemKey_iff.mpr hk),
+    · rw [dif_pos (FiniteMap.memKey_iff.mpr hk),
-          dif_pos (FiniteMap.MemKey_iff.mpr hk)]
+          dif_pos (FiniteMap.memKey_iff.mpr hk)]
       exact FiniteMap.le_of_mem_mem prog.vars_nodup h
         (FiniteMap.locate _).2 (FiniteMap.locate _).2
-    · rw [dif_neg (fun hm => hk (FiniteMap.MemKey_iff.mp hm)),
+    · rw [dif_neg (fun hm => hk (FiniteMap.memKey_iff.mp hm)),
-          dif_neg (fun hm => hk (FiniteMap.MemKey_iff.mp hm))]
+          dif_neg (fun hm => hk (FiniteMap.memKey_iff.mp hm))]
   | num n =>
     intro vs₁ vs₂ _
     exact le_refl _
@@ -91,17 +91,39 @@ instance exprEvaluator : ExprEvaluator ConstLattice prog :=
 def output : String :=
   show' (result ConstLattice prog)
 
-lemma plus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ}
+theorem plus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ}
     (h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) :
     ⟦plus g₁ g₂⟧ (.int (z₁ + z₂)) := by
-  rcases g₁ with _ | _ | c₁ <;> rcases g₂ with _ | _ | c₂ <;>
+  rcases g₁ with _ | _ | c₁
-    simp_all [plus, constInterpretation, interpConst]
+  · exact h₁.elim
+  · rcases g₂ with _ | _ | c₂
+    · exact h₂.elim
+    · exact trivial
+    · exact trivial
+  · rcases g₂ with _ | _ | c₂
+    · exact h₂.elim
+    · exact trivial
+    · injection h₁ with hz₁
+      injection h₂ with hz₂
+      show Value.int (z₁ + z₂) = Value.int (c₁ + c₂)
+      rw [hz₁, hz₂]
 
-lemma minus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ}
+theorem minus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ}
     (h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) :
     ⟦minus g₁ g₂⟧ (.int (z₁ - z₂)) := by
-  rcases g₁ with _ | _ | c₁ <;> rcases g₂ with _ | _ | c₂ <;>
+  rcases g₁ with _ | _ | c₁
-    simp_all [minus, constInterpretation, interpConst]
+  · exact h₁.elim
+  · rcases g₂ with _ | _ | c₂
+    · exact h₂.elim
+    · exact trivial
+    · exact trivial
+  · rcases g₂ with _ | _ | c₂
+    · exact h₂.elim
+    · exact trivial
+    · injection h₁ with hz₁
+      injection h₂ with hz₂
+      show Value.int (z₁ - z₂) = Value.int (c₁ - c₂)
+      rw [hz₁, hz₂]
 
 instance eval_valid : ValidExprEvaluator ConstLattice prog := by
   constructor
@@ -135,14 +157,7 @@ instance eval_valid : ValidExprEvaluator ConstLattice prog := by
 
 theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
     ⟦ variablesAt prog.finalState (result ConstLattice prog) ⟧ ρ :=
-  Forward.analyze_correct ConstLattice prog hrun
+  Spa.analyze_correct ConstLattice prog hrun
-
-theorem analyze_correct_at {ρf : Env} (hrun : EvalStmt [] prog.rootStmt ρf)
-    {s : prog.State} {ρin ρout : Env}
-    (hr : Reaches (prog.trace hrun) s ρin ρout) :
-    ⟦ joinForKey s (result ConstLattice prog) ⟧ ρin
-      ∧ ⟦ variablesAt s (result ConstLattice prog) ⟧ ρout :=
-  Forward.analyze_correct_at ConstLattice prog hrun hr
 
 end ConstAnalysis
 

lean/Spa/Analysis/Forward.lean

@@ -5,37 +5,38 @@ import Spa.Fixedpoint
 
 namespace Spa
 
-namespace Forward
+variable {L : Type} [Lattice L] {prog : Program} [E : StmtEvaluator L prog]
-
-variable {L : Type} [FiniteHeightLattice L] {prog : Program} [E : StmtEvaluator L prog]
 
 def updateVariablesForState (s : prog.State) (sv : StateVariables L prog) :
-    VariableValues L prog := E.eval s (variablesAt s sv)
+    VariableValues L prog :=
+  (prog.code s).foldl (fun vs bs => E.eval s bs vs) (variablesAt s sv)
 
-lemma updateVariablesForState_mono (s : prog.State) :
+theorem updateVariablesForState_mono (s : prog.State) :
     Monotone (updateVariablesForState (L := L) s) := fun _ _ hle =>
-  E.eval_mono s (variablesAt_le hle s)
+  foldl_mono' (prog.code s) _ (E.eval_mono s ·) (variablesAt_le hle s)
 
 def updateAll (sv : StateVariables L prog) : StateVariables L prog :=
   FiniteMap.generalizedUpdate id updateVariablesForState
     prog.states sv
 
-lemma updateAll_mono : Monotone (updateAll (L := L) (prog := prog)) :=
+theorem updateAll_mono : Monotone (updateAll (L := L) (prog := prog)) :=
   FiniteMap.generalizedUpdate_monotone monotone_id updateVariablesForState_mono
 
-lemma updateAll_mem_eq {s : prog.State} {vs : VariableValues L prog}
+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
 
-lemma variablesAt_updateAll (s : prog.State) (sv : StateVariables L prog) :
+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]
+
 def analyze (sv : StateVariables L prog) : StateVariables L prog :=
   updateAll (joinAll sv)
 
-lemma analyze_mono : Monotone (analyze (L := L) (prog := prog)) := fun _ _ hle =>
+theorem analyze_mono : Monotone (analyze (L := L) (prog := prog)) := fun _ _ hle =>
   updateAll_mono (joinAll_mono hle)
 
 variable [DecidableEq L]
@@ -45,130 +46,74 @@ def result : StateVariables L prog :=
   Fixedpoint.aFix analyze analyze_mono
 
 variable (L prog) in
-lemma result_eq : result L prog = analyze (result L prog) :=
+theorem result_eq : result L prog = analyze (result L prog) :=
   Fixedpoint.aFix_eq analyze analyze_mono
 
-lemma joinForKey_initialState :
+theorem joinForKey_initialState :
     joinForKey prog.initialState (result L prog) = botV L prog := by
   rw [joinForKey, prog.incoming_initialState_eq_nil]
   rfl
 
-class ValidStateEvaluator (L : Type) [FiniteHeightLattice L] (prog : Program)
+variable [I : LatticeInterpretation L] [V : ValidStmtEvaluator L prog]
-    [E : StmtEvaluator L prog] [S : StateInterpretation L prog] where
-  valid : ∀ (s₁ s₂ : prog.State) {ρ₁ ρ₂ ρ₃: Env}
-    {vs : VariableValues L prog},
-    (tr : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂) →
-    (hbs : EvalBasicStmtOpt ρ₂ (prog.cfg.nodes s₂) ρ₃) → ⟦ vs ⟧ (S.Pre tr) →
-    ⟦ E.eval s₂ vs ⟧ (S.Post (tr ++ hbs))
-  botV_init : ⟦ botV L prog ⟧ (S.Pre (Traceₗ.single prog.cfg prog.initialState []))
 
-instance [LatticeInterpretation L] [ValidStmtEvaluator L prog] :
+omit [FiniteHeightLattice L] [DecidableEq L] in
-    ValidStateEvaluator L prog where
+theorem eval_fold_valid {s : prog.State} {bss : List BasicStmt}
-  valid := by intro _ _ _ _ _ _ tr hbs hvs; exact ValidStmtEvaluator.valid hbs hvs
+    {vs : VariableValues L prog} {ρ₁ ρ₂ : Env}
-  botV_init := by intro k l _ v hmem; cases hmem
+    (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)
 
-section
+omit [FiniteHeightLattice L] [DecidableEq L] in
-variable [S : StateInterpretation L prog] [V : ValidStateEvaluator L prog]
+theorem updateVariablesForState_matches {s : prog.State}
+    {sv : StateVariables L prog} {ρ₁ ρ₂ : Env}
+    (hbss : EvalBasicStmts ρ₁ (prog.code s) ρ₂)
+    (hvs : ⟦ variablesAt s sv ⟧ ρ₁) :
+    ⟦ updateVariablesForState s sv ⟧ ρ₂ :=
+  eval_fold_valid hbss hvs
 
-omit [DecidableEq L] in
+omit [FiniteHeightLattice L] [DecidableEq L] in
-lemma updateAll_matches {s₁ s₂ : prog.State} {sv : StateVariables L prog}
+theorem updateAll_matches {s : prog.State} {sv : StateVariables L prog}
-    {ρ₁ ρ₂ ρ₃ : Env}
+    {ρ₁ ρ₂ : Env} (hbss : EvalBasicStmts ρ₁ (prog.code s) ρ₂)
-    (tr : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂)
+    (hvs : ⟦ variablesAt s sv ⟧ ρ₁) :
-    (hnode : EvalBasicStmtOpt ρ₂ (prog.code s₂) ρ₃)
+    ⟦ variablesAt s (updateAll sv) ⟧ ρ₂ := by
-    (hvs : ⟦ variablesAt s₂ sv ⟧ (S.Pre tr)) :
-    ⟦ variablesAt s₂ (updateAll sv) ⟧ (S.Post (tr ++ hnode)) := by
   rw [variablesAt_updateAll]
-  exact V.valid s₁ s₂ tr hnode hvs
+  exact updateVariablesForState_matches hbss hvs
 
-lemma stepTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
+theorem stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env}
-    (tr : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂)
+    (hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁)
-    (hjoin : ⟦ joinForKey s₂ (result L prog) ⟧ (S.Pre tr))
+    (hbss : EvalBasicStmts ρ₁ (prog.code s₁) ρ₂) :
-    (hnode : EvalBasicStmtOpt ρ₂ (prog.code s₂) ρ₃) :
+    ⟦ variablesAt s₁ (result L prog) ⟧ ρ₂ := by
-    ⟦ variablesAt s₂ (result L prog) ⟧ (S.Post (tr ++ hnode)) := by
   rw [result_eq L prog]
-  refine updateAll_matches tr hnode ?_
+  refine updateAll_matches hbss ?_
   rw [variablesAt_joinAll]
   exact hjoin
 
-/-- Soundness at *every* visited node: if the analysis result over-approximates the
+theorem walkTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
-    incoming environment at the start of the trace, then at each node reached along the
+    (hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁)
-    way it over-approximates both the environment entering that node (via `joinForKey`)
+    (tr : Trace prog.graph s₁ s₂ ρ₁ ρ₂) :
-    and the environment leaving it (via `variablesAt`). The intermediate `variablesAt`
+    ⟦ variablesAt s₂ (result L prog) ⟧ ρ₂ := by
-    evidence used to be computed and discarded inside `walkTrace`; here it is returned. -/
-lemma walkTrace_reaches {s₁ s₂ s₃: prog.State} {ρ₁ ρ₂ ρ₃: Env}
-    {s : prog.State} {ρin ρout : Env}
-    {tr : Trace prog.cfg s₂ s₃ ρ₂ ρ₃}
-    (hr : Reaches tr s ρin ρout)
-    (trₗ : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂)
-    (hjoin : ⟦ joinForKey s₂ (result L prog) ⟧ (S.Pre trₗ)) :
-    ⟦ joinForKey s (result L prog) ⟧ (S.Pre (trₗ ++ hr.pre))
-      ∧ ⟦ variablesAt s (result L prog) ⟧ (S.Post (trₗ ++ hr.post)) := by
-  induction hr with
-  | single_here hnode =>
-    simp [Reaches.pre, Reaches.post]
-    refine ⟨?_, ?_⟩ <;> try simpa [HAppend.hAppend]
-    exact stepTrace trₗ hjoin hnode
-  | edge_here hnode hedge rest =>
-    simp [Reaches.pre, Reaches.post]
-    refine ⟨?_, ?_⟩ <;> try simpa [HAppend.hAppend]
-    exact stepTrace trₗ hjoin hnode
-  | edge_there hnode hedge rest hr' ih =>
-    have hstep := stepTrace trₗ hjoin hnode
-    have hmem := FiniteMap.mem_valuesAt prog.states_nodup
-      (prog.mem_incoming_of_edge hedge) (variablesAt_mem _ (result L prog))
-    simpa [Reaches.pre, Reaches.post, HAppend.hAppend] using
-      ih ((trₗ ++ hnode).addEdge hedge)
-        (interp_foldr (S.post_pre (trₗ ++ hnode) hedge hstep) hmem)
-
-omit [DecidableEq L] in
-/-- The final node of a trace is always reached, with the environment/state the trace
-    ends in. Used to recover the final-state soundness theorem from `walkTrace_reaches`. -/
-def reaches_final {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
-    (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) :
-    Σ ρin, Reaches tr s₂ ρin ρ₂ :=
-  match tr with
-  | .single hnode => ⟨_, .single_here hnode⟩
-  | .edge hnode hedge rest =>
-    let ⟨ρin, r'⟩ := reaches_final rest; ⟨ρin, .edge_there hnode hedge _ r'⟩
-
-omit [DecidableEq L] in
-/-- Reaching the final node covers the whole trace. -/
-@[simp] lemma reaches_final_post {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
-    (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) :
-    (reaches_final tr).2.post = tr := by
   induction tr with
-  | single hnode => rfl
+  | single hbss => exact stepTrace hjoin hbss
-  | edge hnode hedge rest ih => simp [reaches_final, Reaches.post, ih]
+  | @edge _ ρ' _ i₁ i₂ _ hbss hedge _ ih =>
+    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 (interp_foldr hstep hmem)
 
-variable (L prog) in
+omit V in
-/-- Soundness at every program point reached during execution: for any node `s` visited
+theorem interp_joinForKey_initialState :
-    by the run `hrun` (witnessed by `hr`), the analysis result over-approximates both the
+    ⟦ joinForKey prog.initialState (result L prog) ⟧ [] := by
-    environment entering `s` and the one leaving it. The final-state theorem
-    `analyze_correct_state` is the special case where `s` is `prog.finalState`. -/
-theorem analyze_correct_at {ρf : Env} (hrun : EvalStmt [] prog.rootStmt ρf)
-    {s : prog.State} {ρin ρout : Env}
-    (hr : Reaches (prog.trace hrun) s ρin ρout) :
-    ⟦ joinForKey s (result L prog) ⟧ (S.Pre hr.pre)
-      ∧ ⟦ variablesAt s (result L prog) ⟧ (S.Post hr.post) := by
-  refine walkTrace_reaches hr (Traceₗ.single _ _ []) ?_
   rw [joinForKey_initialState]
-  exact ValidStateEvaluator.botV_init
+  exact interp_botV_nil
 
 variable (L prog) in
-theorem analyze_correct'
+theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
-    {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
-    ⟦ variablesAt prog.finalState (result L prog) ⟧ (S.Post (prog.trace hrun)) := by
-  have h := (analyze_correct_at L prog hrun (reaches_final (prog.trace hrun)).2).2
-  rwa [reaches_final_post] at h
-
-end
-
-variable (L prog) in
-theorem analyze_correct [LatticeInterpretation L] [ValidStmtEvaluator L prog]
-    {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
     ⟦ variablesAt prog.finalState (result L prog) ⟧ ρ :=
-  analyze_correct' L prog hrun
+  walkTrace interp_joinForKey_initialState (prog.trace hrun)
-
-end Forward
 
 end Spa

lean/Spa/Analysis/Forward/Adapters.lean

@@ -2,63 +2,53 @@ import Spa.Analysis.Forward.Evaluation
 
 namespace Spa
 
-namespace Forward
-
 variable {L : Type} [Lattice L] {prog : Program} [E : ExprEvaluator L prog]
 
 def updateVariablesFromExpression (k : String) (e : Expr)
     (vs : VariableValues L prog) : VariableValues L prog :=
   FiniteMap.generalizedUpdate id (fun _ vs => E.eval e vs) [k] vs
 
-lemma updateVariablesFromExpression_mono (k : String) (e : Expr) :
+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)
 
-def evalBasicStmt (bs : BasicStmt)
+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
 
-lemma evalBasicStmt_mono (bs : BasicStmt) :
+theorem evalB_mono (s : prog.State) (bs : BasicStmt) :
-    Monotone (evalBasicStmt (L := L) (prog := prog) bs) := by
+    Monotone (evalB (L := L) (prog := prog) s bs) := by
   cases bs with
   | assign k e => exact updateVariablesFromExpression_mono k e
   | noop => exact monotone_id
 
-def evalBasicStmtOpt (obs : Option BasicStmt)
-    (vs : VariableValues L prog) : VariableValues L prog :=
-  match obs with
-  | none => vs
-  | some bs => evalBasicStmt bs vs
-
-lemma evalBasicStmtOpt_mono (obs : Option BasicStmt) :
-    Monotone (evalBasicStmtOpt (L := L) (prog := prog) obs) := by
-  cases obs <;> unfold evalBasicStmtOpt
-  · exact monotone_id
-  · apply evalBasicStmt_mono
-
 instance ExprEvaluator.toStmtEvaluator : StmtEvaluator L prog :=
-  ⟨evalBasicStmtOpt ∘ prog.code,
+  ⟨evalB, evalB_mono⟩
-   by intro s; simp; exact (evalBasicStmtOpt_mono (prog.code s))⟩
 
 instance ExprEvaluator.toStmtEvaluator_valid [LatticeInterpretation L]
     [ValidExprEvaluator L prog] : ValidStmtEvaluator L prog := by
   constructor
-  simp [StmtEvaluator.eval, evalBasicStmtOpt]
+  intro s vs ρ₁ ρ₂ bs hbs hvs
-  intro s vs ρ₁ ρ₂; generalize prog.code s = obs; intro hev hvs
+  cases hbs with
-  rcases hev with _ | @⟨_,bs,hev⟩ <;> try simpa
+  | noop => exact hvs
-  rcases hev with _ | @⟨k, e, v, hev⟩ <;> try simpa
+  | assign k e v hev =>
-  intros k' l' hkl' v' hρ
+    intro k' l hk'l v' hv'
-  rcases hρ with _ | ⟨_,_,_,_,_,hne,hmem⟩ <;> simp [evalBasicStmt] at hkl'
+    cases hv' with
-  · have hl := FiniteMap.generalizedUpdate_mem_eq (f := id)
+    | here =>
-        (g := fun _ vs => E.eval e vs) (List.mem_singleton_self k) hkl'
+      have hk'l₀ : (k, l) ∈ FiniteMap.generalizedUpdate (ks := prog.vars) id
-    rewrite [hl]; simp
+          (fun _ vs => E.eval e vs) [k] vs := hk'l
-    exact ValidExprEvaluator.valid hev hvs
+      have hl := FiniteMap.generalizedUpdate_mem_eq (f := id)
-  · have hl := FiniteMap.generalizedUpdate_not_mem_backward
+        (g := fun _ vs => E.eval e vs) (List.mem_singleton_self k) hk'l₀
-        (fun hmem => hne (List.mem_singleton.mp hmem)) hkl'
+      rw [hl]
-    apply hvs _ _ hl _ hmem
+      exact ValidExprEvaluator.valid hev hvs
-
+    | there _ _ _ _ _ hne hmem' =>
-end Forward
+      have hk'l₀ : (k', l) ∈ FiniteMap.generalizedUpdate (ks := prog.vars) id
+          (fun _ vs => E.eval e vs) [k] vs := hk'l
+      have hk'l' : (k', l) ∈ (id vs : VariableValues L prog) :=
+        FiniteMap.generalizedUpdate_not_mem_backward
+          (fun hmem => hne (List.mem_singleton.mp hmem)) hk'l₀
+      exact hvs _ _ hk'l' _ hmem'
 
 end Spa

lean/Spa/Analysis/Forward/Evaluation.lean

@@ -2,13 +2,11 @@ import Spa.Analysis.Forward.Lattices
 
 namespace Spa
 
-namespace Forward
-
 variable (L : Type) [Lattice L] (prog : Program)
 
 class StmtEvaluator where
-  eval : prog.State → VariableValues L prog → VariableValues L prog
+  eval : prog.State → BasicStmt → VariableValues L prog → VariableValues L prog
-  eval_mono : ∀ s, Monotone (eval s)
+  eval_mono : ∀ s bs, Monotone (eval s bs)
 
 class ExprEvaluator where
   eval : Expr → VariableValues L prog → L
@@ -21,9 +19,8 @@ class ValidExprEvaluator [ExprEvaluator L prog] [I : LatticeInterpretation L] :
 
 class ValidStmtEvaluator [E : StmtEvaluator L prog] [LatticeInterpretation L] :
     Prop where
-  valid : ∀ {s : prog.State} {vs : VariableValues L prog} {ρ₁ ρ₂ : Env},
+  valid : ∀ {s : prog.State} {vs : VariableValues L prog} {ρ₁ ρ₂ : Env}
-    EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂ → ⟦ vs ⟧ ρ₁ → ⟦ E.eval s vs ⟧ ρ₂
+    {bs : BasicStmt},
-
+    EvalBasicStmt ρ₁ bs ρ₂ → ⟦ vs ⟧ ρ₁ → ⟦ E.eval s bs vs ⟧ ρ₂
-end Forward
 
 end Spa

lean/Spa/Analysis/Forward/Lattices.lean

@@ -4,8 +4,6 @@ import Spa.Interp
 
 namespace Spa
 
-namespace Forward
-
 variable (L : Type) [Lattice L] (prog : Program)
 
 abbrev VariableValues : Type := FiniteMap String L prog.vars
@@ -18,20 +16,20 @@ def botV [FiniteHeightLattice L] : VariableValues L prog :=
 variable {L prog}
 
 omit [Lattice L] in
-lemma states_memKey (s : prog.State) (sv : StateVariables L prog) :
+theorem states_memKey (s : prog.State) (sv : StateVariables L prog) :
     FiniteMap.MemKey s sv :=
-  FiniteMap.MemKey_iff.mpr (prog.states_complete s)
+  FiniteMap.memKey_iff.mpr (prog.states_complete s)
 
 def variablesAt (s : prog.State) (sv : StateVariables L prog) :
     VariableValues L prog :=
   (FiniteMap.locate (states_memKey s sv)).1
 
 omit [Lattice L] in
-lemma variablesAt_mem (s : prog.State) (sv : StateVariables L prog) :
+theorem variablesAt_mem (s : prog.State) (sv : StateVariables L prog) :
     (s, variablesAt s sv) ∈ sv :=
   (FiniteMap.locate (states_memKey s sv)).2
 
-lemma variablesAt_le {sv₁ sv₂ : StateVariables L prog} (hle : sv₁ ≤ sv₂)
+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
     (variablesAt_mem s sv₁) (variablesAt_mem s sv₂)
@@ -42,7 +40,7 @@ def joinForKey (k : prog.State) (sv : StateVariables L prog) :
     VariableValues L prog :=
   (sv.valuesAt (prog.incoming k)).foldr (· ⊔ ·) (botV L prog)
 
-lemma joinForKey_mono (k : prog.State) :
+theorem joinForKey_mono (k : prog.State) :
     Monotone (joinForKey (L := L) k) := by
   intro sv₁ sv₂ hle
   exact foldr_mono _ (FiniteMap.valuesAt_le hle (prog.incoming k)) (le_refl _)
@@ -52,70 +50,50 @@ lemma joinForKey_mono (k : prog.State) :
 def joinAll (sv : StateVariables L prog) : StateVariables L prog :=
   FiniteMap.generalizedUpdate id joinForKey prog.states sv
 
-lemma joinAll_mono : Monotone (joinAll (L := L) (prog := prog)) :=
+theorem joinAll_mono : Monotone (joinAll (L := L) (prog := prog)) :=
   FiniteMap.generalizedUpdate_monotone monotone_id joinForKey_mono
 
-lemma joinAll_mem_eq {s : prog.State} {vs : VariableValues L prog}
+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
 
-lemma variablesAt_joinAll (s : prog.State) (sv : StateVariables L prog) :
+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))
 
-class StateInterpretation (L : Type) [Lattice L] (prog : Program) where
+/-! ### Lifting an interpretation to variable maps -/
-  Proj : Type
-  Pre : ∀ {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}, Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂ → Proj
-  Post : ∀ {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}, Trace prog.cfg s₁ s₂ ρ₁ ρ₂ → Proj
 
-  interp : VariableValues L prog → (p : Proj) → Prop
+variable [I : LatticeInterpretation L]
-  interp_sup : ∀ {vs₁ vs₂ : VariableValues L prog} {p : Proj},
-    interp vs₁ p ∨ interp vs₂ p → interp (vs₁ ⊔ vs₂) p
-  interp_inf : ∀ {vs₁ vs₂ : VariableValues L prog} {p : Proj},
-    interp vs₁ p ∧ interp vs₂ p → interp (vs₁ ⊓ vs₂) p
 
-  post_pre : ∀ {vs} {s₁ s₂ s₃: prog.State} {ρ₁ ρ₂ : Env}
+omit [FiniteHeightLattice L] in
-    (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) (hedge : (s₂, s₃) ∈ prog.cfg.edges),
+instance : Interp (VariableValues L prog) (Env → Prop) where
-    interp vs (Post tr) → interp vs (Pre (tr.addEdge hedge))
+  interp (vs : VariableValues L prog) (ρ : Env) : Prop :=
+    ∀ (k : String) (l : L), (k, l) ∈ vs →
+      ∀ (v : Value), Env.Mem (k, v) ρ → I.interp l v
 
-instance [S : StateInterpretation L prog] :
+theorem interp_botV_nil : ⟦ botV L prog ⟧ [] := by
-    Interp (VariableValues L prog) (S.Proj → Prop) :=
+  intro k l _ v hmem
-  ⟨S.interp⟩
+  cases hmem
 
-lemma interp_foldr [S : StateInterpretation L prog]
+omit [FiniteHeightLattice L] in
-    {vs : VariableValues L prog} {vss : List (VariableValues L prog)}
+theorem interp_sup {vs₁ vs₂ : VariableValues L prog} {ρ : Env}
-    {p : S.Proj} (hvs : ⟦ vs ⟧ p) (hmem : vs ∈ vss) :
+    (h : ⟦ vs₁⟧ ρ ∨ ⟦ vs₂ ⟧ ρ) : ⟦ vs₁ ⊔ vs₂ ⟧ ρ := by
-    ⟦ vss.foldr (· ⊔ ·) (botV L prog) ⟧ p := 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))
+
+theorem interp_foldr {vs : VariableValues L prog}
+    {vss : List (VariableValues L prog)} {ρ : Env}
+    (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 S.interp_sup (Or.inl hvs)
+    · exact interp_sup (Or.inl hvs)
-    · exact S.interp_sup (Or.inr (ih hmem'))
+    · exact interp_sup (Or.inr (ih hmem'))
-
-variable [I : LatticeInterpretation L]
-
-instance : StateInterpretation L prog where
-  Proj := Env
-  Pre := fun {_ _ _ ρ₂} _ => ρ₂
-  Post := fun {_ _ _ ρ₂} _ => ρ₂
-
-  interp vs ρ := ∀ (k : String) (l : L), (k, l) ∈ vs →
-    ∀ (v : Value), Env.Mem (k, v) ρ → I.interp l v
-  interp_sup := by
-    intro vs₁ vs₂ ρ h 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))
-  interp_inf := by
-    intro vs₁ vs₂ ρ h k l hmem v hv
-    obtain ⟨l₁, l₂, rfl, h₁, h₂⟩ := FiniteMap.mem_inf hmem
-    exact I.interp_inf v ⟨h.1 _ _ h₁ _ hv, h.2 _ _ h₂ _ hv⟩
-  post_pre := by simp
-
-
-end Forward
 
 end Spa

lean/Spa/Analysis/Reaching.lean

@@ -1,135 +0,0 @@
-import Spa.Analysis.Forward
-import Spa.Lattice.Finset
-import Spa.Language.Tagged.Graphs
-import Spa.Showable
-
-namespace Spa
-
-open Forward
-
-instance {n : ℕ} : Showable (Finset (Fin n)) :=
-  ⟨fun s =>
-    "{" ++ (List.finRange n).foldr
-        (fun i rest => if i ∈ s then show' i ++ ", " ++ rest else rest) ""
-        ++ "}"⟩
-
-abbrev DefSet (prog : Program) : Type := Finset prog.NodeId
-
-namespace ReachingAnalysis
-
-variable (prog : Program)
-
-def genSet (s : prog.State) : DefSet prog := (prog.nodeIdOf s).elim {} (fun x => {x})
-
-def eval (s : prog.State) (vs : VariableValues (DefSet prog) prog) : VariableValues (DefSet prog) prog :=
-  match prog.code s with
-  | none => vs
-  | some bs =>
-    match bs with
-    | .assign k _ => FiniteMap.generalizedUpdate id (fun _ _ => genSet prog s) [k] vs
-    | .noop => vs
-
-lemma eval_mono (s : prog.State) :
-    Monotone (eval prog s) := by
-  intros vs₁ vs₂ hle
-  unfold eval; split <;> try simpa
-  split <;> try simpa
-  apply FiniteMap.generalizedUpdate_monotone monotone_id (fun _ => monotone_const)
-  assumption
-
-instance stmtEvaluator : StmtEvaluator (DefSet prog) prog :=
-  ⟨eval prog, eval_mono prog⟩
-
-def output : String :=
-  show' (result (DefSet prog) prog)
-
-/-- The statements a trace executed, paired with the state each executed at,
-    most recent first (matching `LastAssign`, which scans for the most recent
-    assignment). This is `Trace.steps` (chronological) reversed, so facts about
-    concatenating traces reduce to mathlib's `List.append`/`List.reverse` lemmas. -/
-abbrev Run (prog : Program) : Type := List (prog.State × BasicStmt)
-
-@[aesop unsafe cases]
-inductive LastAssign (prog : Program) (x : String) : Run prog → prog.NodeId → Prop
-  | here (s : prog.State) (e : Expr) (hc : prog.code s = some (.assign x e))
-      (rest : Run prog) :
-      LastAssign prog x ((s, .assign x e) :: rest) (prog.nodeIdOfNonempty s hc)
-  | there (s : prog.State) (bs : BasicStmt) (hc : prog.code s = some bs)
-      (rest : Run prog) {n : prog.NodeId} :
-      (∀ e, bs ≠ .assign x e) → LastAssign prog x rest n →
-      LastAssign prog x ((s, bs) :: rest) n
-
-def runOfTraceₗ {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
-    (tr : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂) : Run prog :=
-  tr.steps.reverse
-
-def runOfTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
-    (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) : Run prog :=
-  tr.steps.reverse
-
-instance stateInterp : StateInterpretation (DefSet prog) prog where
-  Proj := Run prog
-  Pre := @runOfTraceₗ prog
-  Post := @runOfTrace prog
-
-  interp vs run := ∀ (x : String) (assigners : DefSet prog), (x, assigners) ∈ vs →
-    ∀ (n : prog.NodeId), LastAssign prog x run n → n ∈ assigners
-  interp_sup := by
-    intro vs₁ vs₂ run h x assigners hmem n hla
-    obtain ⟨a₁, a₂, rfl, h₁, h₂⟩ := FiniteMap.mem_sup hmem
-    aesop (add simp Finset.mem_union)
-  interp_inf := by
-    intro vs₁ vs₂ run h x assigners hmem n hla
-    obtain ⟨a₁, a₂, rfl, h₁, h₂⟩ := FiniteMap.mem_inf hmem
-    aesop (add simp Finset.mem_inter)
-
-  post_pre := by
-    intro vs s₁ s₂ s₃ ρ₁ ρ₂ tr hedge hvs
-    simpa [runOfTrace, runOfTraceₗ] using hvs
-
-private lemma valid_step (s : prog.State) {ρ₁ ρ₂ : Env}
-    {obs : Option BasicStmt} (hcode : prog.code s = obs)
-    (hbs : EvalBasicStmtOpt ρ₁ obs ρ₂)
-    {vs : VariableValues (DefSet prog) prog} {run : Run prog}
-    (hvs : ⟦vs⟧ run) :
-    ⟦eval prog s vs⟧ ((hbs.steps s).reverse ++ run) := by
-  cases hbs with
-  | none => simpa [eval, hcode, EvalBasicStmtOpt.steps] using hvs
-  | some hbs =>
-  cases hbs with
-  | noop =>
-    simp [eval, hcode, EvalBasicStmtOpt.steps]
-    intro x assigners hmem n hla; aesop
-  | assign x e v hev =>
-    simp [eval, hcode, EvalBasicStmtOpt.steps]; intro k assigners hmem n hla
-    by_cases hx : k = x
-    · subst hx
-      have hd := FiniteMap.generalizedUpdate_mem_eq (List.mem_singleton.mpr rfl) hmem
-      rcases hla
-        <;> simp [Program.nodeIdOfNonempty, hd, genSet, Option.get] <;> aesop
-    · have hmem' := FiniteMap.generalizedUpdate_not_mem_backward
-        (fun hc => hx (List.mem_singleton.mp hc)) hmem
-      aesop
-
-instance validStateEvaluator : ValidStateEvaluator (DefSet prog) prog where
-  valid := by
-    intro s₁ s₂ ρ₁ ρ₂ ρ₃ vs tr hbs hvs
-    show ⟦eval prog s₂ vs⟧ (runOfTrace prog (tr ++ hbs))
-    simpa [runOfTrace, runOfTraceₗ] using valid_step prog s₂ rfl hbs hvs
-  botV_init := by intro x assigners _ n hla; cases hla
-
-theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
-    ⟦ variablesAt prog.finalState (result (DefSet prog) prog) ⟧
-      (runOfTrace prog (prog.trace hrun)) :=
-  Forward.analyze_correct' (DefSet prog) prog hrun
-
-theorem analyze_correct_at {ρf : Env} (hrun : EvalStmt [] prog.rootStmt ρf)
-    {s : prog.State} {ρin ρout : Env}
-    (hr : Reaches (prog.trace hrun) s ρin ρout) :
-    ⟦ joinForKey s (result (DefSet prog) prog) ⟧ (runOfTraceₗ prog hr.pre)
-      ∧ ⟦ variablesAt s (result (DefSet prog) prog) ⟧ (runOfTrace prog hr.post) :=
-  Forward.analyze_correct_at (DefSet prog) prog hrun hr
-
-end ReachingAnalysis
-
-end Spa

lean/Spa/Analysis/Sign.lean

@@ -5,16 +5,12 @@ import Spa.Showable
 
 namespace Spa
 
-open Forward
-
 inductive Sign where
   | plus
   | minus
   | zero
   deriving DecidableEq
 
-attribute [aesop safe cases] Sign
-
 instance : Showable Sign :=
   ⟨fun
     | .plus => "+"
@@ -57,15 +53,23 @@ def minus : SignLattice → SignLattice → SignLattice
   | mk .zero, mk .minus => mk .plus
   | mk .zero, mk .zero => mk .zero
 
-lemma plus_mono₂ : Monotone₂ plus :=
+theorem plus_mono₂ : Monotone₂ plus :=
   AboveBelow.monotone₂_of_strict plus
-    (fun y => by aesop) (fun x => by aesop)
+    (fun y => by cases y <;> rfl)
-    (fun y hy => by aesop) (fun x hx => by aesop)
+    (fun x => by rcases x with _ | _ | s <;> first | rfl | (cases s <;> rfl))
+    (fun y hy => by cases y <;> first | exact absurd rfl hy | rfl)
+    (fun x hx => by
+      rcases x with _ | _ | s <;>
+        first | exact absurd rfl hx | rfl | (cases s <;> rfl))
 
-lemma minus_mono₂ : Monotone₂ minus :=
+theorem minus_mono₂ : Monotone₂ minus :=
   AboveBelow.monotone₂_of_strict minus
-    (fun y => by aesop) (fun x => by aesop)
+    (fun y => by cases y <;> rfl)
-    (fun y hy => by aesop) (fun x hx => by aesop)
+    (fun x => by rcases x with _ | _ | s <;> first | rfl | (cases s <;> rfl))
+    (fun y hy => by cases y <;> first | exact absurd rfl hy | rfl)
+    (fun x hx => by
+      rcases x with _ | _ | s <;>
+        first | exact absurd rfl hx | rfl | (cases s <;> rfl))
 
 def interpSign : SignLattice → Value → Prop
   | .bot, _ => False
@@ -74,7 +78,7 @@ def interpSign : SignLattice → Value → Prop
   | .mk .zero, v => v = .int 0
   | .mk .minus, v => ∃ n : ℕ, v = .int (-(n + 1))
 
-lemma interpSign_mk_disjoint {s₁ s₂ : Sign} (hne : s₁ ≠ s₂) {v : Value} :
+theorem interpSign_mk_disjoint {s₁ s₂ : Sign} (hne : s₁ ≠ s₂) {v : Value} :
     ¬(interpSign (.mk s₁) v ∧ interpSign (.mk s₂) v) := by
   rintro ⟨h₁, h₂⟩
   rcases s₁ <;> rcases s₂ <;> try exact hne rfl
@@ -119,7 +123,7 @@ def eval : Expr → VariableValues SignLattice prog → SignLattice
   | .num 0, _ => .mk .zero
   | .num (_ + 1), _ => .mk .plus
 
-lemma eval_mono (e : Expr) : Monotone (eval prog e) := by
+theorem eval_mono (e : Expr) : Monotone (eval prog e) := by
   induction e with
   | add e₁ e₂ ih₁ ih₂ =>
     intro vs₁ vs₂ h
@@ -131,12 +135,12 @@ lemma eval_mono (e : Expr) : Monotone (eval prog e) := by
     intro vs₁ vs₂ h
     simp only [eval]
     by_cases hk : k ∈ prog.vars
-    · rw [dif_pos (FiniteMap.MemKey_iff.mpr hk),
+    · rw [dif_pos (FiniteMap.memKey_iff.mpr hk),
-          dif_pos (FiniteMap.MemKey_iff.mpr hk)]
+          dif_pos (FiniteMap.memKey_iff.mpr hk)]
       exact FiniteMap.le_of_mem_mem prog.vars_nodup h
         (FiniteMap.locate _).2 (FiniteMap.locate _).2
-    · rw [dif_neg (fun hm => hk (FiniteMap.MemKey_iff.mp hm)),
+    · rw [dif_neg (fun hm => hk (FiniteMap.memKey_iff.mp hm)),
-          dif_neg (fun hm => hk (FiniteMap.MemKey_iff.mp hm))]
+          dif_neg (fun hm => hk (FiniteMap.memKey_iff.mp hm))]
   | num n =>
     intro vs₁ vs₂ _
     cases n <;> exact le_refl _
@@ -148,18 +152,18 @@ def output : String :=
   show' (result SignLattice prog)
 
 /-- A nonneg-shifted interpretation `∃ n : ℕ, z = n + 1` just means `z` is positive. -/
-private lemma int_pos_iff (z : ℤ) : (∃ n : ℕ, z = (n : ℤ) + 1) ↔ 0 < z := by
+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 lemma int_neg_iff (z : ℤ) : (∃ n : ℕ, z = -((n : ℤ) + 1)) ↔ z < 0 := by
+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⟩
 
-lemma plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
+theorem plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
     (h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) :
     ⟦plus g₁ g₂⟧ (.int (z₁ + z₂)) := by
   rcases g₁ with _ | _ | s₁ <;> rcases g₂ with _ | _ | s₂ <;>
@@ -168,7 +172,7 @@ lemma plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
       at h₁ h₂ ⊢ <;>
     omega
 
-lemma minus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
+theorem minus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
     (h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) :
     ⟦minus g₁ g₂⟧ (.int (z₁ - z₂)) := by
   rcases g₁ with _ | _ | s₁ <;> rcases g₂ with _ | _ | s₂ <;>
@@ -211,14 +215,7 @@ instance eval_valid : ValidExprEvaluator SignLattice prog := by
 
 theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
     ⟦ variablesAt prog.finalState (result SignLattice prog) ⟧ ρ :=
-  Forward.analyze_correct SignLattice prog hrun
+  Spa.analyze_correct SignLattice prog hrun
-
-theorem analyze_correct_at {ρf : Env} (hrun : EvalStmt [] prog.rootStmt ρf)
-    {s : prog.State} {ρin ρout : Env}
-    (hr : Reaches (prog.trace hrun) s ρin ρout) :
-    ⟦ joinForKey s (result SignLattice prog) ⟧ ρin
-      ∧ ⟦ variablesAt s (result SignLattice prog) ⟧ ρout :=
-  Forward.analyze_correct_at SignLattice prog hrun hr
 
 end SignAnalysis
 

lean/Spa/Analysis/Utils.lean

@@ -2,7 +2,7 @@ import Spa.Lattice
 
 namespace Spa
 
-lemma eval_combine₂ {O : Type*} [Preorder O] {combine : O → O → O}
+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₄ :=
   le_trans (hmono.1 o₂ h₁) (hmono.2 o₃ h₂)

lean/Spa/Fixedpoint.lean

@@ -1,12 +1,10 @@
 import Spa.Lattice
 
-namespace Spa
+namespace Spa.Fixedpoint
-
-namespace Fixedpoint
 
 open FiniteHeightLattice (height)
 
-variable {α : Type*} [DecidableEq α] [FiniteHeightLattice α]
+variable {α : Type*} [Lattice α] [DecidableEq α] [FiniteHeightLattice α]
 
 def doStep (f : α → α) (hf : Monotone f) :
     ∀ (g : ℕ) (c : LTSeries α), c.length + g = height (α := α) + 1 →
@@ -24,7 +22,8 @@ def doStep (f : α → α) (hf : Monotone f) :
 def fix (f : α → α) (hf : Monotone f) : {a : α // a = f a} :=
   doStep f hf (height (α := α) + 1) (RelSeries.singleton _ ⊥)
     (by simp)
-    (by simp)
+    (by simpa [RelSeries.last_singleton]
+          using FiniteHeightLattice.bot_le α (f ⊥))
 
 def aFix (f : α → α) (hf : Monotone f) : α :=
   (fix f hf).1
@@ -33,13 +32,12 @@ theorem aFix_eq (f : α → α) (hf : Monotone f) :
     aFix f hf = f (aFix f hf) :=
   (fix f hf).2
 
-lemma doStep_le (f : α → α) (hf : Monotone f)
+theorem doStep_le (f : α → α) (hf : Monotone f)
     {b : α} (hb : b = f b) :
     ∀ (g : ℕ) (c : LTSeries α) (hlen : c.length + g = height (α := α) + 1)
       (hle : c.last ≤ f c.last), c.last ≤ b →
       (doStep f hf g c hlen hle : α) ≤ b
-  | 0, c, hlen, _ => fun _ =>
+  | 0, c, hlen, _ => fun _ => absurd (FiniteHeightLattice.chains_bounded c) (by omega)
-    absurd (FiniteHeightLattice.chains_bounded c) (by omega)
   | g + 1, c, hlen, hle => fun hcb => by
     rw [doStep]
     split
@@ -49,8 +47,6 @@ lemma doStep_le (f : α → α) (hf : Monotone f)
 
 theorem aFix_le (f : α → α) (hf : Monotone f)
     {a : α} (ha : a = f a) : aFix f hf ≤ a :=
-  doStep_le f hf ha _ _ _ _ (by simp)
+  doStep_le f hf ha _ _ _ _ (by simpa using FiniteHeightLattice.bot_le α a)
 
-end Fixedpoint
+end Spa.Fixedpoint
-
-end Spa

lean/Spa/Interp.lean

@@ -1,17 +1,7 @@
 import Mathlib.Tactic.TypeStar
 
-/-!
-
-# Interpretation to a Semantic Domain
-
-This file serves to introduce the double-angle-bracket "denotation"
-notation by prodiving a class instance `Interp`, whose single
-method `interp` is what the double brackets map to. -/
-
 namespace Spa
 
-/-- A type `α` that implements this class has denotation / meaning
-   in the semantic domain `dom`. -/
 class Interp (α : Type*) (dom : outParam Type*) where
   interp : α → dom
 

lean/Spa/Isomorphism.lean

@@ -0,0 +1,24 @@
+import Spa.Lattice
+
+namespace Spa
+
+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
+  bot := f ⊥
+  top := f ⊤
+  height := I.height
+  longestChain :=
+    { series :=
+        I.longestChain.series.map f
+          (hf.strictMono_of_injective (Function.LeftInverse.injective hgf))
+      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)))
+
+end Spa

lean/Spa/Language.lean

@@ -3,4 +3,56 @@ import Spa.Language.Semantics
 import Spa.Language.Graphs
 import Spa.Language.Traces
 import Spa.Language.Properties
-import Spa.Language.Program
+import Mathlib.Data.Finset.Sort
+import Mathlib.Data.String.Basic
+
+namespace Spa
+
+structure Program where
+  rootStmt : Stmt
+
+namespace Program
+
+variable (p : Program)
+
+def graph : Graph := Graph.wrap (buildCfg p.rootStmt)
+
+abbrev State : Type := p.graph.Index
+
+def initialState : p.State := (buildCfg p.rootStmt).wrapInput
+
+def finalState : p.State := (buildCfg p.rootStmt).wrapOutput
+
+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)
+  rw [Graph.wrap_inputs, List.mem_singleton] at h₁
+  rw [Graph.wrap_outputs, List.mem_singleton] at h₂
+  subst h₁; subst h₂
+  exact tr
+
+def vars : List String := p.rootStmt.vars.sort (· ≤ ·)
+
+theorem vars_nodup : p.vars.Nodup := Finset.sort_nodup _ _
+
+def states : List p.State := p.graph.indices
+
+theorem states_complete (s : p.State) : s ∈ p.states := p.graph.mem_indices s
+
+theorem states_nodup : p.states.Nodup := p.graph.nodup_indices
+
+def code (st : p.State) : List BasicStmt := p.graph.nodes st
+
+def incoming (s : p.State) : List p.State := p.graph.predecessors s
+
+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 _)
+
+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
+
+end Program
+
+end Spa

lean/Spa/Language/Base.lean

@@ -1,19 +1,7 @@
 import Mathlib.Data.Finset.Basic
 
-/-!
-
-# Base Language
-
-This file defines the core object language for the program analysis and
-transformation. It's a very basic imperative language. The `Spa/Language/Tagged/Basic.lean`
-file provides an auto-derived version of the `Expr`, `BasicStmt`, and `Stmt` data
-types with unique IDs per condtructor, enabling in-AST pointers.
-
--/
-
 namespace Spa
 
-/-- A value-producing expression. Currently, this cannot have side effects. -/
 inductive Expr where
   | add (e₁ e₂ : Expr)
   | sub (e₁ e₂ : Expr)
@@ -21,15 +9,11 @@ inductive Expr where
   | num (n : ℕ)
   deriving DecidableEq
 
-/-- A statement that cannot alter control flow (and thus, can be part of a basic block).
-
-    This differs from, e.g., a loop, which can cause execution to jump to its top several times. -/
 inductive BasicStmt where
   | assign (x : String) (e : Expr)
   | noop
   deriving DecidableEq
 
-/-- Any statements, which may or may not change program state (variable assignments). -/
 inductive Stmt where
   | basic (bs : BasicStmt)
   | andThen (s₁ s₂ : Stmt)
@@ -37,23 +21,34 @@ inductive Stmt where
   | whileLoop (e : Expr) (s : Stmt)
   deriving DecidableEq
 
-/-- Variables mentioned in this expression. -/
+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₂)
+  | subLeft {e₁ e₂ k} : Expr.HasVar k e₁ → Expr.HasVar k (.sub e₁ e₂)
+  | subRight {e₁ e₂ k} : Expr.HasVar k e₂ → Expr.HasVar k (.sub e₁ e₂)
+  | here {k} : Expr.HasVar k (.var k)
+
+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)
+
 def Expr.vars : Expr → Finset String
   | .add l r => l.vars ∪ r.vars
   | .sub l r => l.vars ∪ r.vars
   | .var s => {s}
   | .num _ => ∅
 
-/-- Variables assigned or mentioned in this basic statement. -/
 def BasicStmt.vars : BasicStmt → Finset String
   | .assign x e => {x} ∪ e.vars
   | .noop => ∅
 
-/-- Variables assigned or mentioned in this statement. -/
 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
 
+def Stmt.varsList (ss : List Stmt) : Finset String :=
+  ss.foldr (fun s acc => s.vars ∪ acc) ∅
+
 end Spa

lean/Spa/Language/Graphs.lean

@@ -3,113 +3,45 @@ import Mathlib.Data.Fin.Tuple.Basic
 import Mathlib.Data.List.ProdSigma
 import Mathlib.Data.List.FinRange
 
-/-!
-
-# Algebraic Control Flow Graphs
-
-This file defines control flow graphs and operations to naturally compose them,
-making it possible to inductively covnert a program in the object language
-(see `Spa.Stmt` in `Spa/Language/Base.lean`) into its corresponding graph.
-
-Graphs are, in general, parameterized by their "payload" (the per-node data); see `GGraph`.
-This is useful because other operations, such as finding the CFG node corresponding
-to an AST node, are performed by embellishing a graph's basic blocks with their AST
-identifiers.
-
-The operations are deliberately a little bit sloppy here, creating empty / statement-less
-CFG nodes. Additionally, the current CFG construction algorithm doesn't group
-consecutive statements in a single notional basic block into one node.
-This makes graph construction much easier to define, and might save us the
-trouble of (when trying to find the CFG node for an AST node) doing
-indexing into a list.
-
--/
-
-/-- Logically, when combining `Fin`s from two distinct pools,
-    the combination is disjoint. -/
-lemma Fin.castAdd_ne_natAdd {n m : ℕ} (i : Fin n) (j : Fin m) :
-    Fin.castAdd m i ≠ Fin.natAdd n j := by
-  intro h
-  have := congrArg Fin.val h
-  simp only [Fin.coe_castAdd, Fin.coe_natAdd] at this
-  omega
-
-/-- Bump the upper bound of a list of `Fin`s without changing their value. -/
 def List.finCastAdd {n : ℕ} (l : List (Fin n)) (m : ℕ) : List (Fin (n + m)) :=
   l.map (Fin.castAdd m)
 
-/-- Bump the upper bound of a list of `Fin`s by adding the amount to their value. -/
 def List.finNatAdd {m : ℕ} (l : List (Fin m)) (n : ℕ) : List (Fin (n + m)) :=
   l.map (Fin.natAdd n)
 
-/-- Bump the upper bound of a list of `Fin` pairs without changing their value. -/
 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))
 
-/-- Bump the upper bound of a list of `Fin` pairs by adding the amount to their value. -/
 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
 
-/-- Graph with general (`α`-labeled) nodes. By using a tuple `Fin size → α`
+structure Graph where
-    and writing `edges` over the `Fin size`, guarantees all edges are between real nodes.
-
-    To make graph composition via operations not force a
-    [`alga`](https://hackage.haskell.org/package/algebraic-graphs)-style "connect"-based
-    algebra, explicitly defines `inputs` and `outputs`, which are the only nodes that
-    get connected when graphs are sequenced. This makes the graph construction
-    operations more naturally fit with how CFGs are created from `Stmt`s. -/
-structure GGraph (α : Type) where
   size : ℕ
-  nodes : Fin size → α
+  nodes : Fin size → List BasicStmt
   edges : List (Fin size × Fin size)
   inputs : List (Fin size)
   outputs : List (Fin size)
 
-namespace GGraph
+namespace Graph
 
-variable {α β : Type}
+abbrev Index (g : Graph) : Type := Fin g.size
 
-/-- An index (node) in the CFG. -/
+abbrev Edge (g : Graph) : Type := g.Index × g.Index
-abbrev Index (g : GGraph α) : Type := Fin g.size
 
-/-- An edge in the CFG. -/
+def comp (g₁ g₂ : Graph) : Graph where
-abbrev Edge (g : GGraph α) : Type := g.Index × g.Index
-
-instance : Functor GGraph where
-  map {α β : Type} (f : α → β) (g : GGraph α) : GGraph β :=
-    { size := g.size,
-      nodes := f ∘ g.nodes
-      edges := g.edges,
-      inputs := g.inputs,
-      outputs := g.outputs }
-
-@[simp] lemma map_size (f : α → β) (g : GGraph α) : (f <$> g).size = g.size := rfl
-@[simp] lemma map_edges (f : α → β) (g : GGraph α) : (f <$> g).edges = g.edges := rfl
-@[simp] lemma map_inputs (f : α → β) (g : GGraph α) : (f <$> g).inputs = g.inputs := rfl
-@[simp] lemma map_outputs (f : α → β) (g : GGraph α) : (f <$> g).outputs = g.outputs := rfl
-
-/-- Overlay two graphs: create a new graph whose nodes and edges come from two
-    sub-graphs, without inserting any additional edges. Also combines the
-    input and output node sets. -/
-def overlay (g₁ g₂ : GGraph α) : GGraph α where
   size := g₁.size + g₂.size
   nodes := Fin.append g₁.nodes g₂.nodes
   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 " ∙ " => GGraph.overlay
+@[inherit_doc] scoped infixr:70 " ∙ " => Graph.comp
 
-/-- Sequence two CFGs: create a combined graph whose nodes and edges come
+def link (g₁ g₂ : Graph) : Graph where
-    from two subgraphs, __and__ make all the outputs of the left graph have edges to
-    all the inputs of the right graph. By the semantics of CFGs, this
-    encodes the fact that code first traverses the basic blocks in theleft
-    graph, and does the same for the right graph. -/
-def sequence (g₁ g₂ : GGraph α) : GGraph α where
   size := g₁.size + g₂.size
   nodes := Fin.append g₁.nodes g₂.nodes
   edges := g₁.edges.finCastAddProd g₂.size ++ g₂.edges.finNatAddProd g₁.size ++
@@ -117,244 +49,78 @@ def sequence (g₁ g₂ : GGraph α) : GGraph α where
   inputs := g₁.inputs.finCastAdd g₂.size
   outputs := g₂.outputs.finNatAdd g₁.size
 
-@[inherit_doc] scoped infixr:70 " ⤳ " => GGraph.sequence
+@[inherit_doc] scoped infixr:70 " ⤳ " => Graph.link
 
-/-- When a graph `g` is wrapped in a `loop`, the index / node corresponding
+/-- The entry node of a `loop` graph. -/
-    to the input of the new loop. -/
+def loopIn (g : Graph) : Fin (2 + g.size) := (0 : Fin 2).castAdd g.size
-def loopIn (g : GGraph α) : Fin (2 + g.size) := (0 : Fin 2).castAdd g.size
 
-/-- When a graph `g` is wrapped in a `loop`, the index / node corresponding
+/-- The exit node of a `loop` graph. -/
-    to the output of the new loop. -/
+def loopOut (g : Graph) : Fin (2 + g.size) := (1 : Fin 2).castAdd g.size
-def loopOut (g : GGraph α) : Fin (2 + g.size) := (1 : Fin 2).castAdd g.size
 
-/-- Creates a zero-or-more loop loop in the CFG: connects all the output
+def loop (g : Graph) : Graph where
-    nodes of the CFG back to the graph's beginning, and also introduces a path
-    to a new ending node (see `loopOut`) which bypasses the entire graph.
-
-    Notably, both the new input (`loopIn`) and new output (`loopOut`)
-    nodes are necessary for correctness: adding a path from inputs to a
-    hypothetical no-op end node encodes something like "just the first statement is executed".
-    Similarly, just adding a path from a a hypothetical no-op beginning node
-    to the outputs encodes "just the last statement is executed".
-
-    This is technically sloppy (see module comment), but it's simple.
--/
-def loop (g : GGraph (Option β)) : GGraph (Option β) where
   size := 2 + g.size
-  nodes := Fin.append (fun _ : Fin 2 => none) g.nodes
+  nodes := Fin.append (fun _ : Fin 2 => []) g.nodes
   edges := g.edges.finNatAddProd 2 ++
-    ((g.loopIn, ·) <$> g.inputs.finNatAdd 2)  ++
+    (g.inputs.finNatAdd 2).map (g.loopIn, ·) ++
-    ((·, g.loopOut) <$> g.outputs.finNatAdd 2) ++
+    (g.outputs.finNatAdd 2).map (·, g.loopOut) ++
     [(g.loopOut, g.loopIn), (g.loopIn, g.loopOut)]
   inputs := [g.loopIn]
   outputs := [g.loopOut]
 
-@[simp] lemma loop_inputs (g : GGraph (Option β)) : (loop g).inputs = [g.loopIn] := rfl
+@[simp] theorem loop_inputs (g : Graph) : (loop g).inputs = [g.loopIn] := rfl
 
-@[simp] lemma loop_outputs (g : GGraph (Option β)) : (loop g).outputs = [g.loopOut] := rfl
+@[simp] theorem loop_outputs (g : Graph) : (loop g).outputs = [g.loopOut] := rfl
 
-/-- Creates a single-node graph whose node contains the given value. -/
+def skipto (g₁ g₂ : Graph) : Graph where
-def singleton (a : α) : GGraph α where
+  size := g₁.size + g₂.size
+  nodes := Fin.append g₁.nodes g₂.nodes
+  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
+
+def singleton (bss : List BasicStmt) : Graph where
   size := 1
-  nodes := fun _ => a
+  nodes := fun _ => bss
   edges := []
   inputs := [0]
   outputs := [0]
 
-/-- Creates a new graph with a single input and single output node. Useful to ensure there's
+def wrap (g : Graph) : Graph :=
-    a single point of entry and single point of exit. -/
+  singleton [] ⤳ g ⤳ singleton []
-def wrap (g : GGraph (Option β)) : GGraph (Option β) :=
-  singleton none ⤳ g ⤳ singleton none
-
-/-- The input / entry node generated by `GGraph.wrap`. -/
-def wrapInput (g : GGraph (Option β)) : (wrap g).Index :=
-  (0 : Fin 1).castAdd ((g ⤳ singleton none).size)
-
-/-- The output / exit node generated by `GGraph.wrap`. -/
-def wrapOutput (g : GGraph (Option β)) : (wrap g).Index :=
-  Fin.natAdd 1 ((Fin.natAdd g.size (0 : Fin 1)))
-
-/-- The `wrapInput` is, indeed, the graph's only input after `wrap`. -/
-lemma wrap_inputs (g : GGraph (Option β)) :
-    (wrap g).inputs = [g.wrapInput] := rfl
-
-/-- The `wrapInput` is, indeed, the graph's only output after `wrap`. -/
-lemma wrap_outputs (g : GGraph (Option β)) :
-    (wrap g).outputs = [g.wrapOutput] := rfl
-
-@[simp] lemma map_singleton (f : α → β) (a : α) :
-    f <$> singleton a = singleton (f a) := rfl
-
-@[simp] lemma map_overlay (f : α → β) (g₁ g₂ : GGraph α) :
-    f<$> (g₁ ∙ g₂) = f <$> g₁ ∙ f <$> g₂ := by
-  rcases g₁ with ⟨n₁, nd₁, e₁, i₁, o₁⟩; rcases g₂ with ⟨n₂, nd₂, e₂, i₂, o₂⟩
-  simp only [Functor.map, GGraph.overlay]
-  congr 1
-  funext i
-  refine Fin.addCases ?_ ?_ i <;> intro j <;> simp [Fin.append_left, Fin.append_right]
-
-@[simp] lemma map_sequence (f : α → β) (g₁ g₂ : GGraph α) :
-    f <$> (g₁ ⤳ g₂) = (f <$> g₁) ⤳  (f <$> g₂) := by
-  rcases g₁ with ⟨n₁, nd₁, e₁, i₁, o₁⟩; rcases g₂ with ⟨n₂, nd₂, e₂, i₂, o₂⟩
-  simp only [Functor.map, GGraph.sequence]
-  congr 1
-  funext i
-  refine Fin.addCases ?_ ?_ i <;> intro j <;> simp [Fin.append_left, Fin.append_right]
-
-@[simp] lemma map_loop (h : β → γ) (g : GGraph (Option β)) :
-    (Option.map h) <$> (loop g) = loop (Option.map h <$> g) := by
-  rcases g with ⟨n, nd, e, i, o⟩
-  simp only [Functor.map, GGraph.loop]
-  congr 1
-  funext i
-  refine Fin.addCases ?_ ?_ i <;> intro j <;> simp [Fin.append_left, Fin.append_right]
-
-@[simp] lemma map_wrap (h : β → γ) (g : GGraph (Option β)) :
-    (Option.map h) <$> wrap g = wrap (Option.map h <$> g) := by
-  simp [GGraph.wrap, GGraph.map_sequence, GGraph.map_singleton]
-
-/-! ### Embeddings
-
-Each composition operator includes its operands into the result via an index
-translation that preserves node payloads and edges. `Embed` captures exactly
-those two facts, so anything defined from `nodes` and `edges` (traces, node
-labels, …) can be transported along an embedding once, instead of once per
-operator.
-
-`Embed` is deliberately a structure rather than a class: for `g ⤳ g`, both the
-left and the right inclusion inhabit the same type `Embed g (g ⤳ g)`, so
-instance resolution could silently pick the wrong copy. Embeddings into a
-composed graph are non-canonical by design; a named witness says which
-inclusion is meant. -/
-
-/-- An embedding of graph `g` into graph `h`: an index translation that
-    preserves node payloads and edges. -/
-structure Embed (g h : GGraph α) where
-  f : g.Index → h.Index
-  nodes_eq : ∀ i, h.nodes (f i) = g.nodes i
-  edges_mem : ∀ {e : g.Edge}, e ∈ g.edges → (f e.1, f e.2) ∈ h.edges
-
-/-- Embeddings compose. -/
-def Embed.trans {g₁ g₂ g₃ : GGraph α} (e₁ : Embed g₁ g₂) (e₂ : Embed g₂ g₃) :
-    Embed g₁ g₃ where
-  f := e₂.f ∘ e₁.f
-  nodes_eq i := (e₂.nodes_eq (e₁.f i)).trans (e₁.nodes_eq i)
-  edges_mem he := e₂.edges_mem (e₁.edges_mem he)
-
-/-- The left operand's inclusion into a sequenced graph. -/
-def Embed.sequenceLeft (g₁ g₂ : GGraph α) : Embed g₁ (g₁ ⤳ g₂) where
-  f i := i.castAdd g₂.size
-  nodes_eq i := Fin.append_left g₁.nodes g₂.nodes i
-  edges_mem he := List.mem_append_left _ (List.mem_append_left _ (List.mem_map_of_mem _ he))
-
-/-- The right operand's inclusion into a sequenced graph. -/
-def Embed.sequenceRight (g₁ g₂ : GGraph α) : Embed g₂ (g₁ ⤳ g₂) where
-  f i := i.natAdd g₁.size
-  nodes_eq i := Fin.append_right g₁.nodes g₂.nodes i
-  edges_mem he := List.mem_append_left _ (List.mem_append_right _ (List.mem_map_of_mem _ he))
-
-/-- The left operand's inclusion into an overlaid graph. -/
-def Embed.overlayLeft (g₁ g₂ : GGraph α) : Embed g₁ (g₁ ∙ g₂) where
-  f i := i.castAdd g₂.size
-  nodes_eq i := Fin.append_left g₁.nodes g₂.nodes i
-  edges_mem he := List.mem_append_left _ (List.mem_map_of_mem _ he)
-
-/-- The right operand's inclusion into an overlaid graph. -/
-def Embed.overlayRight (g₁ g₂ : GGraph α) : Embed g₂ (g₁ ∙ g₂) where
-  f i := i.natAdd g₁.size
-  nodes_eq i := Fin.append_right g₁.nodes g₂.nodes i
-  edges_mem he := List.mem_append_right _ (List.mem_map_of_mem _ he)
-
-/-- The body's inclusion into a `loop` graph. -/
-def Embed.loop (g : GGraph (Option β)) : Embed g (loop g) where
-  f i := i.natAdd 2
-  nodes_eq i := Fin.append_right (fun _ : Fin 2 => none) g.nodes i
-  edges_mem he := List.mem_append_left _ (List.mem_append_left _
-    (List.mem_append_left _ (List.mem_map_of_mem _ he)))
-
-variable (g : GGraph α)
-
-/-- All the nodes in the graph. -/
-def indices : List g.Index := List.finRange g.size
-
-/-- All of the graph's indices are listed in `indices`. -/
-lemma mem_indices (idx : g.Index) : idx ∈ g.indices :=
-  List.mem_finRange idx
-
-/-- `indices` does not have duplicates. -/
-lemma nodup_indices : g.indices.Nodup :=
-  List.nodup_finRange g.size
-
-/-- Predecessors of a particular node in the graph. --/
-def predecessors (idx : g.Index) : List g.Index :=
-  g.indices.filter (fun idx' => (idx', idx) ∈ g.edges)
-
-/-- When sequencing (proven here with `Graph.singleton` on the left), no edges
-    exist from the right-hand graph back to the left. -/
-private lemma not_mem_edges_castAdd_sequence {g₂ : GGraph (Option β)} (i : Fin 1)
-    (idx : (singleton none ⤳ g₂).Index) :
-    ((idx, i.castAdd g₂.size) : (singleton none ⤳ g₂).Edge)
-      ∉ (singleton none ⤳ g₂).edges := by
-  intro h
-  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 [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
-  · -- product edges: targets are natAdd'd inputs of g₂
-    obtain ⟨-, hb⟩ := List.mem_product.mp h'
-    obtain ⟨j, -, heq⟩ := List.mem_map.mp hb
-    exact Fin.castAdd_ne_natAdd i j heq.symm
-
-/-- The input node of a graph after `Graph.wrap` has no predecessors. -/
-lemma wrap_predecessors_eq_nil (g : GGraph (Option β)) (idx : (wrap g).Index)
-    (h : idx ∈ (wrap g).inputs) :
-    (wrap g).predecessors idx = [] := by
-  rw [wrap_inputs, List.mem_singleton] at h
-  subst h
-  rw [GGraph.predecessors, List.filter_eq_nil_iff]
-  intro idx' _
-  simpa using not_mem_edges_castAdd_sequence (g₂ := g ⤳ singleton none) 0 idx'
-
-/-- There's there's an edge between two nodes `idx₁` and `idx₂`,
-    then `idx₁` is the predecessor of `idx₂`. -/
-lemma 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⟩
-
-/-- A node is a predecessor of another node only if there's an
-    edge between them. -/
-lemma 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
-
-end GGraph
-
-/-- "Normal" graphs, for the purposes of the analyses in this
-    framework, have basic statements in their nodes, and nothing else. -/
-abbrev Graph : Type := GGraph (Option BasicStmt)
-
-namespace Graph
-
-export GGraph (overlay sequence loop singleton wrap loop_inputs loop_outputs wrapInput wrapOutput wrap_inputs wrap_outputs)
-
-@[inherit_doc] scoped infixr:70 " ∙ " => GGraph.overlay
-@[inherit_doc] scoped infixr:70 " ⤳ " => GGraph.sequence
 
 end Graph
 
 open Graph in
-def Stmt.cfg : Stmt → Graph
+def buildCfg : Stmt → Graph
-  -- A basic statement goes into a single basic block
+  | .basic bs => Graph.singleton [bs]
-  | .basic bs => singleton (some bs)
+  | .andThen s₁ s₂ => buildCfg s₁ ⤳ buildCfg s₂
-  -- Sequencing of statements corresponds naturally to CFG sequencing
+  | .ifElse _ s₁ s₂ => buildCfg s₁ ∙ buildCfg s₂
-  | .andThen s₁ s₂ => s₁.cfg ⤳  s₂.cfg
+  | .whileLoop _ s => Graph.loop (buildCfg s)
-  -- An if can execute either one branch or the other; overlap them.
+
-  -- Subsequent sequencing (etc.) will end up creating the forks and joins.
+namespace Graph
-  | .ifElse _ s₁ s₂ => s₁.cfg ∙ s₂.cfg
+
-  -- The `loop` construct was developed specifically for zero-or-more loops like this.
+variable (g : Graph)
-  | .whileLoop _ s => loop s.cfg
+
+def indices : List g.Index := List.finRange g.size
+
+theorem mem_indices (idx : g.Index) : idx ∈ g.indices :=
+  List.mem_finRange idx
+
+theorem nodup_indices : g.indices.Nodup :=
+  List.nodup_finRange g.size
+
+def predecessors (idx : g.Index) : List g.Index :=
+  g.indices.filter (fun idx' => (idx', idx) ∈ g.edges)
+
+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⟩
+
+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
+
+end Graph
 
 end Spa

lean/Spa/Language/Program.lean

@@ -1,77 +0,0 @@
-import Spa.Language.Base
-import Spa.Language.Semantics
-import Spa.Language.Graphs
-import Mathlib.Data.Finset.Sort
-import Mathlib.Data.String.Basic
-
-namespace Spa
-
-/-- A self-contained program to be evaluated, analyzed, and transformed. -/
-structure Program where
-  /-- The statement at the top level of the program. Since `Spa.Stmt` contains
-      sequencing via `Spa.Stmt.andThen`, this can encode any number of
-      statements. -/
-  rootStmt : Stmt
-  /-- A memoized copy of the control-flow graph. This field is an
-      implementation detail to avoid re-computing `Spa.GGraph.wrap` and `Spa.Stmt.cfg`
-      every time the program's control flow graph is needed -/
-  cfgCache : Thunk Graph := Thunk.mk fun _ => Graph.wrap rootStmt.cfg
-
-namespace Program
-
-variable (p : Program)
-
--- Runtime implementation of `cfg`: read the memoized graph.
-private def cfgImpl : Graph := p.cfgCache.get
-
-/-- The control flow graph corresponding to this graph. -/
-@[implemented_by cfgImpl]
-def cfg : Graph := Graph.wrap p.rootStmt.cfg
-
-/-- A state in the control flow `Spa.Graph` of this program. -/
-abbrev State : Type := p.cfg.Index
-
-/-- Variables mentioned or defined in this program. -/
-def vars : List String := p.rootStmt.vars.sort (· ≤ ·)
-
-/-- `vars` has no duplicates. -/
-lemma vars_nodup : p.vars.Nodup := Finset.sort_nodup _ _
-
-/-- All the states in the program's control flow `Spa.Graph`. -/
-def states : List p.State := p.cfg.indices
-
-/-- All states in the CFG are contained in `states`. -/
-lemma states_complete (s : p.State) : s ∈ p.states := p.cfg.mem_indices s
-
-/-- `states` has no duplicates. -/
-lemma states_nodup : p.states.Nodup := p.cfg.nodup_indices
-
-/-- Given a node of the program's CFG, return the code at that node.
-    At this time, for convenience of proofs, the CFGs have at most
-    one basic statement, and multi-statement basic blocks are encoded
-    as chains of blocks. Thus, this returns at most one `Spa.BasicStmt`. -/
-@[reducible]
-def code (st : p.State) : Option BasicStmt := p.cfg.nodes st
-
-/-- Get the predecessors of a particular CFG node / program state. -/
-def incoming (s : p.State) : List p.State := p.cfg.predecessors s
-
-/-- The entry point of the program's CFG. -/
-def initialState : p.State := Graph.wrapInput p.rootStmt.cfg
-
-/-- The exit point of the program's CFG. -/
-def finalState : p.State := Graph.wrapOutput p.rootStmt.cfg
-
-/-- `incoming` is a faithful representation of edges in the CFG. -/
-lemma mem_incoming_of_edge {s₁ s₂ : p.State}
-    (h : (s₁, s₂) ∈ p.cfg.edges) : s₁ ∈ p.incoming s₂ :=
-  p.cfg.mem_predecessors_of_edge h
-
-/-- The `initialState` has no incoming edges (it's the program start). -/
-lemma incoming_initialState_eq_nil : p.incoming p.initialState = [] :=
-  GGraph.wrap_predecessors_eq_nil p.rootStmt.cfg p.initialState
-    (by rw [Graph.wrap_inputs]; exact List.mem_singleton_self _)
-
-end Program
-
-end Spa

lean/Spa/Language/Properties.lean

@@ -1,126 +1,126 @@
 import Spa.Language.Traces
 
-/-!
-
-# Properties of the Object Language, CFGs, and Traces
-
-This module encodes some properties of the language, mostly those having to do
-with connecting the computational view (the `Spa.Graph`s, on which static
-analyses are executed) to the semantic view (such as `EvalStmt`, which
-encodes the expected formal behavior of the language). In particular,
-to prove that our computationally-implemented static analyses are correct,
-we need to show that our computational model of their execution (the CFG)
-matches the formal description. Thus, the key result `cfg_sufficient`.
-
-Many lemmas and definitions here aim are used to prove that result,
-by allowing inductive proofs on the construction of the CFG:
-the bits where we _build up_ the trace corresponding to each
-proof tree are exactly those when we have two graphs (through
-which traces exist) and we want to combine these graphs, while
-showing also that a combined trace exists as well. -/
-
 namespace Spa
 
 open Graph
 
+theorem Fin.castAdd_ne_natAdd {n m : ℕ} (i : Fin n) (j : Fin m) :
+    Fin.castAdd m i ≠ Fin.natAdd n j := by
+  intro h
+  have := congrArg Fin.val h
+  simp only [Fin.coe_castAdd, Fin.coe_natAdd] at this
+  omega
+
+/-! ### Trace embeddings -/
+
 section Embeddings
 
 variable {g₁ g₂ : Graph} {ρ₁ ρ₂ : Env}
 
-/-- Transport a trace along a graph embedding: an embedding preserves node
+theorem Trace.comp_left {idx₁ idx₂ : g₁.Index}
-    payloads and edges, which is everything a trace is made of. This is the
+    (tr : Trace g₁ idx₁ idx₂ ρ₁ ρ₂) :
-    single induction behind all the per-operator lifting corollaries below. -/
+    Trace (g₁ ∙ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by
-noncomputable def Trace.embed {g h : Graph} (e : GGraph.Embed g h)
-    {idx₁ idx₂ : g.Index} (tr : Trace g idx₁ idx₂ ρ₁ ρ₂) :
-    Trace h (e.f idx₁) (e.f idx₂) ρ₁ ρ₂ := by
   induction tr with
-  | single hbs => exact Trace.single (by rwa [e.nodes_eq])
+  | single hbs =>
-  | edge hbs he _ ih => exact Trace.edge (by rwa [e.nodes_eq]) (e.edges_mem he) ih
+    exact Trace.single (by rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl,
+      Fin.append_left])
+  | edge hbs he _ ih =>
+    refine Trace.edge ?_ ?_ ih
+    · 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)
 
-/-- When two graphs are overlaid, for each trace in the left graph,
+theorem Trace.comp_right {idx₁ idx₂ : g₂.Index}
-    a corresponding trace exists in the combined graph. -/
-noncomputable def Trace.overlay_left {idx₁ idx₂ : g₁.Index}
-    (tr : Trace g₁ idx₁ idx₂ ρ₁ ρ₂) :
-    Trace (g₁ ∙ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ :=
-  tr.embed (GGraph.Embed.overlayLeft g₁ g₂)
-
-/-- When two graphs are overlaid, for each trace in the right graph,
-    a corresponding trace exists in the combined graph. -/
-noncomputable def Trace.overlay_right {idx₁ idx₂ : g₂.Index}
     (tr : Trace g₂ idx₁ idx₂ ρ₁ ρ₂) :
-    Trace (g₁ ∙ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ :=
+    Trace (g₁ ∙ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ := by
-  tr.embed (GGraph.Embed.overlayRight g₁ g₂)
+  induction tr with
+  | single hbs =>
+    exact Trace.single (by rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl,
+      Fin.append_right])
+  | edge hbs he _ ih =>
+    refine Trace.edge ?_ ?_ ih
+    · 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)
 
-/-- When two graphs are sequenced, for each trace in the first graph,
+theorem Trace.link_left {idx₁ idx₂ : g₁.Index}
-    a corresponding trace exists in the combined graph. -/
-noncomputable def Trace.sequence_left {idx₁ idx₂ : g₁.Index}
     (tr : Trace g₁ idx₁ idx₂ ρ₁ ρ₂) :
-    Trace (g₁ ⤳ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ :=
+    Trace (g₁ ⤳ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by
-  tr.embed (GGraph.Embed.sequenceLeft g₁ g₂)
+  induction tr with
+  | single hbs =>
+    exact Trace.single (by rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl,
+      Fin.append_left])
+  | edge hbs he _ ih =>
+    refine Trace.edge ?_ ?_ ih
+    · 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))
 
-/-- When two graphs are sequenced, for each trace in the second graph,
+theorem Trace.link_right {idx₁ idx₂ : g₂.Index}
-   a corresponding trace exists in the combined graph. -/
-noncomputable def Trace.sequence_right {idx₁ idx₂ : g₂.Index}
     (tr : Trace g₂ idx₁ idx₂ ρ₁ ρ₂) :
-    Trace (g₁ ⤳ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ :=
+    Trace (g₁ ⤳ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ := by
-  tr.embed (GGraph.Embed.sequenceRight g₁ g₂)
+  induction tr with
+  | single hbs =>
+    exact Trace.single (by rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl,
+      Fin.append_right])
+  | edge hbs he _ ih =>
+    refine Trace.edge ?_ ?_ ih
+    · rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_right]
+    · exact List.mem_append_left _
+        (List.mem_append_right _ (List.mem_map_of_mem _ he))
 
-/-- Equivalent of `Trace.overlay_left` for end-to-end traces. -/
+theorem EndToEndTrace.comp_left (etr : EndToEndTrace g₁ ρ₁ ρ₂) :
-noncomputable def EndToEndTrace.overlay_left (etr : EndToEndTrace g₁ ρ₁ ρ₂) :
     EndToEndTrace (g₁ ∙ g₂) ρ₁ ρ₂ := by
   obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := etr
   exact ⟨i₁.castAdd g₂.size, List.mem_append_left _ (List.mem_map_of_mem _ h₁),
          i₂.castAdd g₂.size, List.mem_append_left _ (List.mem_map_of_mem _ h₂),
-         tr.overlay_left⟩
+         tr.comp_left⟩
 
-/-- Equivalent of `Trace.overlay_right` for end-to-end traces. -/
+theorem EndToEndTrace.comp_right (etr : EndToEndTrace g₂ ρ₁ ρ₂) :
-noncomputable def EndToEndTrace.overlay_right (etr : EndToEndTrace g₂ ρ₁ ρ₂) :
     EndToEndTrace (g₁ ∙ g₂) ρ₁ ρ₂ := by
   obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := etr
   exact ⟨i₁.natAdd g₁.size, List.mem_append_right _ (List.mem_map_of_mem _ h₁),
          i₂.natAdd g₁.size, List.mem_append_right _ (List.mem_map_of_mem _ h₂),
-         tr.overlay_right⟩
+         tr.comp_right⟩
 
-/-- When two graphs are sequenced, two end-to-end traces through the respective
+theorem EndToEndTrace.concat {ρ₃ : Env} (etr₁ : EndToEndTrace g₁ ρ₁ ρ₂)
-    graphs can be sequenced to create an end-to-end trace in the combined
-    graph. This is only possible for end-to-end traces and not for general
-    `Trace`s, because sequencing only introduces edges from the output nodes
-    of one graph to the input nodes of another graph. A non-end-to-end trace
-    need to conclude at the output node, so it cannot necessarily be sequenced
-    with a trace in another graph. -/
-noncomputable def EndToEndTrace.concat {ρ₃ : Env} (etr₁ : EndToEndTrace g₁ ρ₁ ρ₂)
     (etr₂ : EndToEndTrace g₂ ρ₂ ρ₃) : EndToEndTrace (g₁ ⤳ g₂) ρ₁ ρ₃ := by
   obtain ⟨i₁, h₁, i₂, h₂, tr₁⟩ := etr₁
   obtain ⟨j₁, k₁, j₂, k₂, tr₂⟩ := etr₂
   refine ⟨i₁.castAdd g₂.size, List.mem_map_of_mem _ h₁,
           j₂.natAdd g₁.size, List.mem_map_of_mem _ k₂,
-          tr₁.sequence_left ++< ?_ >++ tr₂.sequence_right⟩
+          Trace.concat tr₁.link_left ?_ tr₂.link_right⟩
   exact List.mem_append_right _
     (List.mem_product.mpr ⟨List.mem_map_of_mem _ h₂, List.mem_map_of_mem _ k₁⟩)
 
 end Embeddings
 
+/-! ### Loops -/
+
 section Loop
 
 variable {g : Graph} {ρ₁ ρ₂ ρ₃ : Env}
 
-/-- A trace through a body CFG still exists (up to reindexing) in a zero-or-more loop CFG. -/
+theorem Trace.loop {idx₁ idx₂ : g.Index} (tr : Trace g idx₁ idx₂ ρ₁ ρ₂) :
-noncomputable def Trace.loop {idx₁ idx₂ : g.Index} (tr : Trace g idx₁ idx₂ ρ₁ ρ₂) :
+    Trace (Graph.loop g) (idx₁.natAdd 2) (idx₂.natAdd 2) ρ₁ ρ₂ := by
-    Trace (Graph.loop g) (idx₁.natAdd 2) (idx₂.natAdd 2) ρ₁ ρ₂ :=
+  induction tr with
-  tr.embed (GGraph.Embed.loop g)
+  | single hbs =>
+    exact Trace.single (by
+      rwa [show (Graph.loop g).nodes = Fin.append (fun _ : Fin 2 => []) g.nodes from rfl,
+        Fin.append_right])
+  | edge hbs he _ ih =>
+    refine Trace.edge ?_ ?_ ih
+    · rwa [show (Graph.loop g).nodes = Fin.append (fun _ : Fin 2 => []) g.nodes from rfl,
+        Fin.append_right]
+    · exact List.mem_append_left _ (List.mem_append_left _
+        (List.mem_append_left _ (List.mem_map_of_mem _ he)))
 
-/-- The beginning node of a loop graph is empty. -/
+private theorem loop_nodes_at_in :
-private lemma loop_nodes_at_in :
+    (Graph.loop g).nodes g.loopIn = [] :=
-    (Graph.loop g).nodes g.loopIn = none :=
+  Fin.append_left (fun _ : Fin 2 => []) g.nodes 0
-  Fin.append_left (fun _ : Fin 2 => none) g.nodes 0
 
-/-- The ending node of a loop graph is empty. -/
+private theorem loop_nodes_at_out :
-private lemma loop_nodes_at_out :
+    (Graph.loop g).nodes g.loopOut = [] :=
-    (Graph.loop g).nodes g.loopOut = none :=
+  Fin.append_left (fun _ : Fin 2 => []) g.nodes 1
-  Fin.append_left (fun _ : Fin 2 => none) g.nodes 1
 
-/-- Equivlaent of `Trace.loop` for end-to-end traces. -/
+theorem EndToEndTrace.loop (etr : EndToEndTrace g ρ₁ ρ₂) :
-noncomputable def EndToEndTrace.loop (etr : EndToEndTrace g ρ₁ ρ₂) :
     EndToEndTrace (Graph.loop g) ρ₁ ρ₂ := by
   obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := etr
   -- the edge in → (2 ↑ʳ i₁), reached through the second edge group
@@ -132,17 +132,15 @@ noncomputable def EndToEndTrace.loop (etr : EndToEndTrace g ρ₁ ρ₂) :
     refine List.mem_append_left _ (List.mem_append_right _ ?_)
     exact List.mem_map_of_mem _ (List.mem_map_of_mem _ h₂)
   refine ⟨g.loopIn, List.mem_singleton_self _, g.loopOut, List.mem_singleton_self _, ?_⟩
-  exact Trace.single (loop_nodes_at_in ▸ EvalBasicStmtOpt.none) ++< hin >++
+  exact Trace.concat (Trace.single (loop_nodes_at_in ▸ EvalBasicStmts.nil)) hin
-    tr.loop ++< hout >++ Trace.single (loop_nodes_at_out ▸ EvalBasicStmtOpt.none)
+    (Trace.concat tr.loop hout (Trace.single (loop_nodes_at_out ▸ EvalBasicStmts.nil)))
 
-/-- The zero-or-more times loop has an edge to return back to the top, to continue after an iteration. -/
+private theorem loop_edge_out_in :
-private lemma loop_edge_out_in :
     ((g.loopOut, g.loopIn) : (Graph.loop g).Edge) ∈ (Graph.loop g).edges := by
   refine List.mem_append_right _ ?_
   exact List.mem_cons_self _ _
 
-/-- Two traces through a loop can be combined, since a loop can be executed any number of times. -/
+theorem EndToEndTrace.loop_concat (etr₁ : EndToEndTrace (Graph.loop g) ρ₁ ρ₂)
-noncomputable def EndToEndTrace.loop_concat (etr₁ : EndToEndTrace (Graph.loop g) ρ₁ ρ₂)
     (etr₂ : EndToEndTrace (Graph.loop g) ρ₂ ρ₃) :
     EndToEndTrace (Graph.loop g) ρ₁ ρ₃ := by
   obtain ⟨i₁, h₁, i₂, h₂, tr₁⟩ := etr₁
@@ -150,77 +148,86 @@ noncomputable def EndToEndTrace.loop_concat (etr₁ : EndToEndTrace (Graph.loop
   simp only [Graph.loop_inputs, Graph.loop_outputs, List.mem_singleton] at h₁ h₂ k₁ k₂
   subst h₁; subst h₂; subst k₁; subst k₂
   exact ⟨g.loopIn, List.mem_singleton_self _, g.loopOut, List.mem_singleton_self _,
-    tr₁ ++< loop_edge_out_in >++ tr₂⟩
+    Trace.concat tr₁ loop_edge_out_in tr₂⟩
 
-/-- A loop can be executed zero times. -/
+theorem EndToEndTrace.loop_empty {ρ : Env} : EndToEndTrace (Graph.loop g) ρ ρ := by
-noncomputable def 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 _ _))
   exact ⟨g.loopIn, List.mem_singleton_self _, g.loopOut, List.mem_singleton_self _,
-    Trace.single (loop_nodes_at_in ▸ EvalBasicStmtOpt.none) ++< hedge >++
+    Trace.concat (Trace.single (loop_nodes_at_in ▸ EvalBasicStmts.nil)) hedge
-      Trace.single (loop_nodes_at_out ▸ EvalBasicStmtOpt.none)⟩
+      (Trace.single (loop_nodes_at_out ▸ EvalBasicStmts.nil))⟩
 
 end Loop
 
-/-- A CFG consisting of only a single node has a trace through it corresponding to that node. -/
+/-! ### Singletons, wrap, and the main result -/
-noncomputable def EndToEndTrace.singleton {o : Option BasicStmt} {ρ₁ ρ₂ : Env}
+
-    (h : EvalBasicStmtOpt ρ₁ o ρ₂) : EndToEndTrace (Graph.singleton o) ρ₁ ρ₂ :=
+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⟩
 
-/-- If a CFG's only node is empty, the no-op trace exists through it. -/
+theorem EndToEndTrace.singleton_nil (ρ : Env) :
-noncomputable def EndToEndTrace.singleton_nil (ρ : Env) :
+    EndToEndTrace (Graph.singleton []) ρ ρ :=
-    EndToEndTrace (Graph.singleton none) ρ ρ :=
+  EndToEndTrace.singleton EvalBasicStmts.nil
-  EndToEndTrace.singleton EvalBasicStmtOpt.none
 
-/-- Invoking 'Graph.wrap` (which ensures a single entry and exit node for a CFG)
+theorem EndToEndTrace.wrap {g : Graph} {ρ₁ ρ₂ : Env}
-    does not invalidate traces in the original graph. -/
-noncomputable def EndToEndTrace.wrap {g : Graph} {ρ₁ ρ₂ : Env}
     (etr : EndToEndTrace g ρ₁ ρ₂) : EndToEndTrace (Graph.wrap g) ρ₁ ρ₂ :=
   (EndToEndTrace.singleton_nil ρ₁).concat (etr.concat (EndToEndTrace.singleton_nil ρ₂))
 
-/-- Key result: the control flow graph admits every execution that's made
+theorem buildCfg_sufficient {s : Stmt} {ρ₁ ρ₂ : Env}
-    possible by a language's semantics. Thus, the CFG encodes _at least_ all
+    (h : EvalStmt ρ₁ s ρ₂) : EndToEndTrace (buildCfg s) ρ₁ ρ₂ := by
-    semantically-possible executions. Informally, we can conclude from this
-    that if we compute a result that using the graph's edges to determine
-    what's possible, this result will not disagree with the semantics.
-
-    Note that a CFG like $K_4$ (where the nodes are basic blocks) is
-    technically also a sufficient graph, but is very likely meaningless in that
-    it grossly overestimates the possible execution paths in the language, and
-    thus is bound to produce less-than-specific results. There is as yet no
-    result in this framework that the CFG we produce is _minimal_: loosely,
-    posessing only edges for things that are admitted by the semantics.
-    This is difficult to state (in its strongest form, this would
-    require the CFG to be able to detect something like `while (alwaysFalse)`,
-    and so remains a TODO. -/
-noncomputable def Stmt.cfg_sufficient {s : Stmt} {ρ₁ ρ₂ : Env}
-    (h : EvalStmt ρ₁ s ρ₂) : EndToEndTrace s.cfg ρ₁ ρ₂ := by
   induction h with
   | basic ρ₁ ρ₂ bs hbs =>
-    exact EndToEndTrace.singleton (EvalBasicStmtOpt.some hbs)
+    exact EndToEndTrace.singleton (EvalBasicStmts.cons hbs EvalBasicStmts.nil)
   | andThen ρ₁ ρ₂ ρ₃ s₁ s₂ _ _ ih₁ ih₂ =>
     exact ih₁.concat ih₂
   | ifTrue ρ₁ ρ₂ e z s₁ s₂ _ _ _ ih =>
-    exact ih.overlay_left
+    exact ih.comp_left
   | ifFalse ρ₁ ρ₂ e s₁ s₂ _ _ ih =>
-    exact ih.overlay_right
+    exact ih.comp_right
   | whileTrue ρ₁ ρ₂ ρ₃ e z s _ _ _ _ ih₁ ih₂ =>
     exact (ih₁.loop).loop_concat ih₂
   | whileFalse ρ e s _ =>
     exact EndToEndTrace.loop_empty
 
-namespace Program
+/-! ### The wrapped graph's entry has no predecessors (Agda's "ugly" block) -/
 
-noncomputable def trace (p : Program) {ρ : Env} (h : EvalStmt [] p.rootStmt ρ) :
+def Graph.wrapInput (g : Graph) : (Graph.wrap g).Index :=
-    Trace p.cfg p.initialState p.finalState [] ρ := by
+  (0 : Fin 1).castAdd ((g ⤳ Graph.singleton []).size)
-  obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := EndToEndTrace.wrap (Stmt.cfg_sufficient h)
-  rw [Graph.wrap_inputs, List.mem_singleton] at h₁
-  rw [Graph.wrap_outputs, List.mem_singleton] at h₂
-  subst h₁; subst h₂
-  exact tr
 
-end Program
+def Graph.wrapOutput (g : Graph) : (Graph.wrap g).Index :=
+  Fin.natAdd 1 ((Fin.natAdd g.size (0 : Fin 1)))
 
+theorem Graph.wrap_inputs (g : Graph) :
+    (Graph.wrap g).inputs = [g.wrapInput] := rfl
+
+theorem Graph.wrap_outputs (g : Graph) :
+    (Graph.wrap g).outputs = [g.wrapOutput] := rfl
+
+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)
+      ∉ (Graph.singleton [] ⤳ g₂).edges := by
+  intro h
+  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, 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
+  · -- product edges: targets are natAdd'd inputs of g₂
+    obtain ⟨-, hb⟩ := List.mem_product.mp h'
+    obtain ⟨j, -, heq⟩ := List.mem_map.mp hb
+    exact Fin.castAdd_ne_natAdd i j heq.symm
+
+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
+  rw [Graph.wrap_inputs, List.mem_singleton] at h
+  subst h
+  rw [Graph.predecessors, List.filter_eq_nil_iff]
+  intro idx' _
+  simpa using not_mem_edges_castAdd_link (g₂ := g ⤳ Graph.singleton []) 0 idx'
 
 end Spa

lean/Spa/Language/Semantics.lean

@@ -2,27 +2,12 @@ import Spa.Language.Base
 import Spa.Lattice
 import Spa.Interp
 
-/-!
-
-# Operational Semantics
-
-This file contains the operational semantics for the object language defined in
-`Spa.Language.Base`. Right now, all values in the language are integers.
-The semantics are big-step, and lead to a fully constructed proof tree
-containing the derivation connecting the initial and final states.
-All pretty standard.
-
--/
-
 namespace Spa
 
-/-- A value in the object language. Currently, the only possible case is
-    an integer. -/
 inductive Value where
   | int (z : ℤ)
   deriving DecidableEq
 
-/-- An environment mapping variables to their values. -/
 def Env : Type := List (String × Value)
 
 inductive Env.Mem : String × Value → Env → Prop
@@ -30,8 +15,6 @@ inductive Env.Mem : String × Value → Env → Prop
   | there (s s' : String) (v v' : Value) (ρ : Env) :
       ¬(s = s') → Env.Mem (s, v) ρ → Env.Mem (s, v) ((s', v') :: ρ)
 
-/-- Inference rules for evaluating an expression (`Spa.Expr`) in a given
-    environment. Pretty standard big-step expression evaluation. -/
 inductive EvalExpr : Env → Expr → Value → Prop
   | num (ρ : Env) (n : ℕ) : EvalExpr ρ (.num n) (.int n)
   | var (ρ : Env) (x : String) (v : Value) :
@@ -43,25 +26,18 @@ inductive EvalExpr : Env → Expr → Value → Prop
       EvalExpr ρ e₁ (.int z₁) → EvalExpr ρ e₂ (.int z₂) →
       EvalExpr ρ (.sub e₁ e₂) (.int (z₁ - z₂))
 
-/-- Inference rules for evaluating a basic statement (`Spa.BasicStmt`) in
+inductive EvalBasicStmt : Env → BasicStmt → Env → Prop
-    a given environment, potentially changing the environment.
-    Pretty standard big-step evaluation. -/
-inductive EvalBasicStmt : Env → BasicStmt → Env → Type
   | noop (ρ : Env) : EvalBasicStmt ρ .noop ρ
   | assign (ρ : Env) (x : String) (e : Expr) (v : Value) :
       EvalExpr ρ e v → EvalBasicStmt ρ (.assign x e) ((x, v) :: ρ)
 
-/-- Inference rules for evaluating a basic-statement-or-nothing,
+inductive EvalBasicStmts : Env → List BasicStmt → Env → Prop
-    which is the current representation of CFGs nodes. -/
+  | nil {ρ : Env} : EvalBasicStmts ρ [] ρ
-inductive EvalBasicStmtOpt : Env → Option BasicStmt → Env → Type
+  | cons {ρ₁ ρ₂ ρ₃ : Env} {bs : BasicStmt} {bss : List BasicStmt} :
-  | none {ρ : Env} : EvalBasicStmtOpt ρ Option.none ρ
+      EvalBasicStmt ρ₁ bs ρ₂ → EvalBasicStmts ρ₂ bss ρ₃ →
-  | some {ρ₁ ρ₂ : Env} {bs : BasicStmt} :
+      EvalBasicStmts ρ₁ (bs :: bss) ρ₃
-      EvalBasicStmt ρ₁ bs ρ₂ → EvalBasicStmtOpt ρ₁ (Option.some bs) ρ₂
 
-/-- Inference rules for evaluating statements (`Spa.Stmt`) in a given
+inductive EvalStmt : Env → Stmt → Env → Prop
-    environment, potentially changing the environment.
-    Pretty standard big-step evaluation. -/
-inductive EvalStmt : Env → Stmt → Env → Type
   | basic (ρ₁ ρ₂ : Env) (bs : BasicStmt) :
       EvalBasicStmt ρ₁ bs ρ₂ → EvalStmt ρ₁ (.basic bs) ρ₂
   | andThen (ρ₁ ρ₂ ρ₃ : Env) (s₁ s₂ : Stmt) :
@@ -81,15 +57,6 @@ inductive EvalStmt : Env → Stmt → Env → Type
       EvalExpr ρ e (.int 0) →
       EvalStmt ρ (.whileLoop e s) ρ
 
-/-- For the purpose of static analysis, lattices we define describe program
-    state, or better yet, they describe _values_ in the program.
-    This class should be provided by each analysis' lattice (see also `Spa/Analysis/Forward.lean`)
-    to describe what each lattice value means in terms of the language.
-
-    In addition to providing the interpretation (`Spa.Interp`), the lattice
-    combinators `⊔` and `⊓` must respect disjunction and conjunction respectively.
-    This is because possible paths through a control flow graph (`Spa/Language/Graphs.lean`),
-    are tied to lattice operations used by the analysis engine. -/
 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

lean/Spa/Language/Tagged/Basic.lean

@@ -1,18 +0,0 @@
-import Spa.Language.Base
-import Spa.Language.Tagged.Id
-import Spa.Language.Tagged.Derive
-
-derive_tagged Spa.Expr Spa.BasicStmt Spa.Stmt
-
-namespace Spa
-
-def tagStmt (s : Stmt) : Stmt.Tagged RawId := (s.tag 0).1
-
-def Stmt.Tagged.subtreeIds {τ : Type} (s : Stmt.Tagged τ) : List τ :=
-  s.foldTags (· :: ·) []
-
-def Stmt.Tagged.isInLoopBody {τ : Type} [DecidableEq τ]
-    (body : Stmt.Tagged τ) (id : τ) : Bool :=
-  decide (id ∈ body.subtreeIds)
-
-end Spa

lean/Spa/Language/Tagged/DESCENDANT-TRACKING.md

@@ -1,417 +0,0 @@
-# Descendant tracking (parked)
-
-This is the formally-verified **interval-labeling / descendant** machinery that
-used to live in `Id.lean` and `Properties.lean`. It let you decide "is node `a`
-a descendant of node `b`?" with two integer comparisons on their identifiers,
-and *proved* that numeric test equivalent to structural subtree containment.
-
-It was removed because the descendant test is a *computational optimization*:
-the same question can be answered by walking the AST, and nothing in the current
-pipeline needs the fast test yet. The proofs (a rose-tree flattening + a
-postorder `Good` invariant) are a real mechanization cost to carry. Parked here
-so it can be restored verbatim when LICM actually wants it.
-
-## What stays in the live code
-
-- `NodeId` collapses to a single unique index (`{ post : ℕ }`); `tag` still
-  assigns each node a distinct postorder number.
-- The bidirectional mapping (`erase`/`tag` + `erase_tagStmt`) stays in
-  `Properties.lean`.
-- The labelled-CFG id↔state mapping (`Cfg.lean`) is independent of this and is
-  unaffected.
-
-## Revival checklist
-
-1. In `Id.lean`, give `NodeId` back its descendant-count field and the test:
-
-   ```lean
-   structure NodeId where
-     post : ℕ
-     desc : ℕ          -- number of proper descendants (subtree size − 1); leaf = 0
-     deriving DecidableEq, Repr
-
-   namespace NodeId
-
-   /-- Left endpoint of the node's postorder interval `[lo, post]`. -/
-   def lo (a : NodeId) : ℕ := a.post - a.desc
-
-   /-- `a` is a descendant-or-self of `b`: `a.post` lies in `b`'s interval. -/
-   def DescendantOf (a b : NodeId) : Prop := b.lo ≤ a.post ∧ a.post ≤ b.post
-
-   instance (a b : NodeId) : Decidable (DescendantOf a b) := by
-     unfold DescendantOf; infer_instance
-
-   end NodeId
-   ```
-
-2. In `Derive.lean`, make the generated `tag` store the descendant count again:
-   change the emitted identifier in `mkTag` from `(⟨$last⟩ : $nId)` back to
-   `(⟨$last, $last - n⟩ : $nId)`.
-
-3. Paste the Lean block below back into `Properties.lean` (after the round-trip
-   theorems). It builds against the `id.lo = lo`-premise form of `Good` and the
-   childcount (`desc`) identifier. The headline result is
-   `descendant_iff_tagStmt`; everything else is supporting machinery.
-
-## The parked proofs
-
-```lean
-/-- A rose tree of identifiers: the uniform shape underlying all three tagged
-AST types, used to reason about the postorder labeling generically. -/
-inductive IdTree where
-  | node (id : NodeId) (children : List IdTree)
-
-namespace IdTree
-
-def rootId : IdTree → NodeId
-  | .node id _ => id
-
-@[simp] theorem rootId_node (id : NodeId) (cs : List IdTree) :
-    (IdTree.node id cs).rootId = id := rfl
-
-mutual
-def subtrees : IdTree → List IdTree
-  | .node id cs => .node id cs :: subtreesList cs
-def subtreesList : List IdTree → List IdTree
-  | [] => []
-  | c :: cs => subtrees c ++ subtreesList cs
-end
-
-@[simp] theorem subtrees_node (id : NodeId) (cs : List IdTree) :
-    subtrees (.node id cs) = .node id cs :: subtreesList cs := rfl
-
-@[simp] theorem subtreesList_nil : subtreesList [] = [] := rfl
-
-@[simp] theorem subtreesList_cons (c : IdTree) (cs : List IdTree) :
-    subtreesList (c :: cs) = subtrees c ++ subtreesList cs := rfl
-
-def posts (t : IdTree) : List ℕ := (subtrees t).map (fun s => s.rootId.post)
-
-def postsList (cs : List IdTree) : List ℕ := (subtreesList cs).map (fun s => s.rootId.post)
-
-@[simp] theorem posts_node (id : NodeId) (cs : List IdTree) :
-    posts (.node id cs) = id.post :: postsList cs := rfl
-
-@[simp] theorem postsList_nil : postsList [] = [] := rfl
-
-@[simp] theorem postsList_cons (c : IdTree) (cs : List IdTree) :
-    postsList (c :: cs) = posts c ++ postsList cs := by
-  simp [posts, postsList]
-
-end IdTree
-
-def Expr.Tagged.toIdTree : Expr.Tagged NodeId → IdTree
-  | .add t a b => .node t [a.toIdTree, b.toIdTree]
-  | .sub t a b => .node t [a.toIdTree, b.toIdTree]
-  | .var t _ => .node t []
-  | .num t _ => .node t []
-
-def BasicStmt.Tagged.toIdTree : BasicStmt.Tagged NodeId → IdTree
-  | .assign t _ e => .node t [e.toIdTree]
-  | .noop t => .node t []
-
-def Stmt.Tagged.toIdTree : Stmt.Tagged NodeId → IdTree
-  | .basic t bs => .node t [bs.toIdTree]
-  | .andThen t a b => .node t [a.toIdTree, b.toIdTree]
-  | .ifElse t e a b => .node t [e.toIdTree, a.toIdTree, b.toIdTree]
-  | .whileLoop t e s => .node t [e.toIdTree, s.toIdTree]
-
-mutual
-inductive Good : ℕ → IdTree → Prop
-  | mk {lo : ℕ} {id : NodeId} {cs : List IdTree} :
-      id.lo = lo → GoodChildren lo cs id.post →
-      Good lo (.node id cs)
-inductive GoodChildren : ℕ → List IdTree → ℕ → Prop
-  | nil {pos : ℕ} : GoodChildren pos [] pos
-  | cons {cur : ℕ} {c : IdTree} {cs : List IdTree} {pos : ℕ} :
-      Good cur c → GoodChildren (c.rootId.post + 1) cs pos →
-      GoodChildren cur (c :: cs) pos
-end
-
-theorem Good.lo_le_post {lo : ℕ} {t : IdTree} (h : Good lo t) : lo ≤ t.rootId.post := by
-  cases h with
-  | mk hlo _ => simp only [NodeId.lo] at hlo; simp only [IdTree.rootId_node]; omega
-
-theorem GoodChildren.cur_le_pos : ∀ {cur : ℕ} (cs : List IdTree) {pos : ℕ},
-    GoodChildren cur cs pos → cur ≤ pos
-  | _, [], _, h => by cases h; exact le_rfl
-  | _, c :: cs, _, h => by
-      cases h with
-      | cons hc hcs =>
-        have := hc.lo_le_post
-        have := GoodChildren.cur_le_pos cs hcs
-        omega
-
-mutual
-theorem Good.mem_posts : ∀ {lo : ℕ} (t : IdTree), Good lo t →
-    ∀ x, x ∈ IdTree.posts t ↔ lo ≤ x ∧ x ≤ t.rootId.post
-  | _, .node id cs, h, x => by
-      cases h with
-      | mk hlo hch =>
-        simp only [IdTree.posts_node, List.mem_cons, IdTree.rootId_node]
-        rw [GoodChildren.mem_postsList cs hch x]
-        simp only [NodeId.lo] at hlo
-        omega
-theorem GoodChildren.mem_postsList : ∀ {cur : ℕ} (cs : List IdTree) {pos : ℕ},
-    GoodChildren cur cs pos → ∀ x, x ∈ IdTree.postsList cs ↔ cur ≤ x ∧ x < pos
-  | _, [], _, h, x => by
-      cases h
-      simp only [IdTree.postsList_nil]
-      constructor
-      · intro hx; exact absurd hx (List.not_mem_nil x)
-      · rintro ⟨h1, h2⟩; exfalso; omega
-  | _, c :: cs, _, h, x => by
-      cases h with
-      | cons hc hcs =>
-        simp only [IdTree.postsList_cons, List.mem_append]
-        rw [Good.mem_posts c hc x, GoodChildren.mem_postsList cs hcs x]
-        have := hc.lo_le_post
-        have := GoodChildren.cur_le_pos cs hcs
-        omega
-end
-
-mutual
-theorem Good.nodup_posts : ∀ {lo : ℕ} (t : IdTree), Good lo t → (IdTree.posts t).Nodup
-  | _, .node id cs, h => by
-      cases h with
-      | mk hlo hch =>
-        simp only [IdTree.posts_node, List.nodup_cons]
-        refine ⟨?_, GoodChildren.nodup_postsList cs hch⟩
-        intro hmem
-        rw [GoodChildren.mem_postsList cs hch id.post] at hmem
-        omega
-theorem GoodChildren.nodup_postsList : ∀ {cur : ℕ} (cs : List IdTree) {pos : ℕ},
-    GoodChildren cur cs pos → (IdTree.postsList cs).Nodup
-  | _, [], _, h => by cases h; simp only [IdTree.postsList_nil, List.nodup_nil]
-  | _, c :: cs, _, h => by
-      cases h with
-      | cons hc hcs =>
-        simp only [IdTree.postsList_cons, List.nodup_append]
-        refine ⟨Good.nodup_posts c hc, GoodChildren.nodup_postsList cs hcs, ?_⟩
-        intro x hx1 hx2
-        rw [Good.mem_posts c hc x] at hx1
-        rw [GoodChildren.mem_postsList cs hcs x] at hx2
-        omega
-end
-
-mutual
-theorem Good.subtree_good : ∀ {lo : ℕ} (t : IdTree), Good lo t →
-    ∀ s ∈ IdTree.subtrees t, Good s.rootId.lo s
-  | _, .node id cs, h, s, hs => by
-      cases h with
-      | mk hlo hch =>
-        rw [IdTree.subtrees_node, List.mem_cons] at hs
-        rcases hs with rfl | hs
-        · simp only [IdTree.rootId_node]; rw [hlo]; exact Good.mk hlo hch
-        · exact GoodChildren.subtree_good cs hch s hs
-theorem GoodChildren.subtree_good : ∀ {cur : ℕ} (cs : List IdTree) {pos : ℕ},
-    GoodChildren cur cs pos → ∀ s ∈ IdTree.subtreesList cs, Good s.rootId.lo s
-  | _, [], _, _, s, hs => by simp only [IdTree.subtreesList_nil, List.not_mem_nil] at hs
-  | _, c :: cs, _, h, s, hs => by
-      cases h with
-      | cons hc hcs =>
-        rw [IdTree.subtreesList_cons, List.mem_append] at hs
-        rcases hs with hs | hs
-        · exact Good.subtree_good c hc s hs
-        · exact GoodChildren.subtree_good cs hcs s hs
-end
-
-mutual
-theorem IdTree.subtrees_subset : ∀ (t : IdTree) {b : IdTree},
-    b ∈ subtrees t → subtrees b ⊆ subtrees t
-  | .node id cs, b, hb => by
-      rw [subtrees_node, List.mem_cons] at hb
-      rcases hb with rfl | hb
-      · exact fun _ h => h
-      · intro x hx
-        rw [subtrees_node, List.mem_cons]
-        exact Or.inr (IdTree.subtreesList_subset cs hb hx)
-theorem IdTree.subtreesList_subset : ∀ (cs : List IdTree) {b : IdTree},
-    b ∈ subtreesList cs → subtrees b ⊆ subtreesList cs
-  | [], b, hb => by simp only [subtreesList_nil, List.not_mem_nil] at hb
-  | c :: cs, b, hb => by
-      rw [subtreesList_cons, List.mem_append] at hb
-      intro x hx
-      rw [subtreesList_cons, List.mem_append]
-      rcases hb with hb | hb
-      · exact Or.inl (IdTree.subtrees_subset c hb hx)
-      · exact Or.inr (IdTree.subtreesList_subset cs hb hx)
-end
-
-theorem IdTree.eq_of_post_eq {l : List IdTree}
-    (h : (l.map (fun s => s.rootId.post)).Nodup) {a c : IdTree}
-    (ha : a ∈ l) (hc : c ∈ l) (hpost : a.rootId.post = c.rootId.post) : a = c := by
-  induction l with
-  | nil => exact absurd ha (List.not_mem_nil a)
-  | cons d ds ih =>
-    simp only [List.map_cons, List.nodup_cons] at h
-    obtain ⟨hd, htl⟩ := h
-    simp only [List.mem_cons] at ha hc
-    rcases ha with rfl | ha <;> rcases hc with rfl | hc
-    · rfl
-    · exfalso; apply hd; rw [hpost]; exact List.mem_map_of_mem _ hc
-    · exfalso; apply hd; rw [← hpost]; exact List.mem_map_of_mem _ ha
-    · exact ih htl ha hc
-
-theorem descendant_iff_of_good {lo : ℕ} {t : IdTree} (hg : Good lo t)
-    {a b : IdTree} (ha : a ∈ IdTree.subtrees t) (hb : b ∈ IdTree.subtrees t) :
-    a.rootId.DescendantOf b.rootId ↔ a ∈ IdTree.subtrees b := by
-  have hgb : Good b.rootId.lo b := Good.subtree_good t hg b hb
-  constructor
-  · rintro ⟨h1, h2⟩
-    have hmem : a.rootId.post ∈ IdTree.posts b := by
-      rw [Good.mem_posts b hgb a.rootId.post]; exact ⟨h1, h2⟩
-    rw [IdTree.posts, List.mem_map] at hmem
-    obtain ⟨c, hc_mem, hc_post⟩ := hmem
-    have hc_t : c ∈ IdTree.subtrees t := IdTree.subtrees_subset t hb hc_mem
-    have hac : a = c :=
-      IdTree.eq_of_post_eq (hg.nodup_posts t) ha hc_t hc_post.symm
-    rw [hac]; exact hc_mem
-  · intro hsub
-    have hmem : a.rootId.post ∈ IdTree.posts b := by
-      rw [IdTree.posts, List.mem_map]; exact ⟨a, hsub, rfl⟩
-    rw [Good.mem_posts b hgb a.rootId.post] at hmem
-    exact hmem
-
-/-! ### Tagging produces a good tree
-
-We bridge from the `tag` traversal to the abstract `Good` invariant, by induction
-on the plain AST.  Each lemma also records that the returned counter is one past
-the root's postorder index. -/
-
-theorem Expr.tag_spec : ∀ (e : Expr) (n : ℕ),
-    Good n (e.tag n).1.toIdTree ∧ (e.tag n).1.toIdTree.rootId.post + 1 = (e.tag n).2 := by
-  intro e
-  induction e with
-  | num k =>
-      intro n
-      refine ⟨?_, ?_⟩
-      · simp only [Expr.tag, Expr.Tagged.toIdTree]
-        exact Good.mk (by simp only [NodeId.lo]; omega) GoodChildren.nil
-      · simp only [Expr.tag, Expr.Tagged.toIdTree, IdTree.rootId_node]
-  | var x =>
-      intro n
-      refine ⟨?_, ?_⟩
-      · simp only [Expr.tag, Expr.Tagged.toIdTree]
-        exact Good.mk (by simp only [NodeId.lo]; omega) GoodChildren.nil
-      · simp only [Expr.tag, Expr.Tagged.toIdTree, IdTree.rootId_node]
-  | add a b iha ihb =>
-      intro n
-      obtain ⟨gA, pA⟩ := iha n
-      obtain ⟨gB, pB⟩ := ihb (a.tag n).2
-      have lA := gA.lo_le_post
-      have lB := gB.lo_le_post
-      refine ⟨?_, ?_⟩
-      · simp only [Expr.tag, Expr.Tagged.toIdTree]
-        refine Good.mk ?_ ?_
-        · simp only [NodeId.lo]; omega
-        · refine GoodChildren.cons gA ?_
-          rw [pA]; refine GoodChildren.cons gB ?_; rw [pB]; exact GoodChildren.nil
-      · simp only [Expr.tag, Expr.Tagged.toIdTree, IdTree.rootId_node]
-  | sub a b iha ihb =>
-      intro n
-      obtain ⟨gA, pA⟩ := iha n
-      obtain ⟨gB, pB⟩ := ihb (a.tag n).2
-      have lA := gA.lo_le_post
-      have lB := gB.lo_le_post
-      refine ⟨?_, ?_⟩
-      · simp only [Expr.tag, Expr.Tagged.toIdTree]
-        refine Good.mk ?_ ?_
-        · simp only [NodeId.lo]; omega
-        · refine GoodChildren.cons gA ?_
-          rw [pA]; refine GoodChildren.cons gB ?_; rw [pB]; exact GoodChildren.nil
-      · simp only [Expr.tag, Expr.Tagged.toIdTree, IdTree.rootId_node]
-
-theorem BasicStmt.tag_spec : ∀ (bs : BasicStmt) (n : ℕ),
-    Good n (bs.tag n).1.toIdTree ∧ (bs.tag n).1.toIdTree.rootId.post + 1 = (bs.tag n).2 := by
-  intro bs
-  cases bs with
-  | noop =>
-      intro n
-      refine ⟨?_, ?_⟩
-      · simp only [BasicStmt.tag, BasicStmt.Tagged.toIdTree]
-        exact Good.mk (by simp only [NodeId.lo]; omega) GoodChildren.nil
-      · simp only [BasicStmt.tag, BasicStmt.Tagged.toIdTree, IdTree.rootId_node]
-  | assign x e =>
-      intro n
-      obtain ⟨gE, pE⟩ := Expr.tag_spec e n
-      have lE := gE.lo_le_post
-      refine ⟨?_, ?_⟩
-      · simp only [BasicStmt.tag, BasicStmt.Tagged.toIdTree]
-        refine Good.mk ?_ ?_
-        · simp only [NodeId.lo]; omega
-        · refine GoodChildren.cons gE ?_
-          rw [pE]; exact GoodChildren.nil
-      · simp only [BasicStmt.tag, BasicStmt.Tagged.toIdTree, IdTree.rootId_node]
-
-theorem Stmt.tag_spec : ∀ (s : Stmt) (n : ℕ),
-    Good n (s.tag n).1.toIdTree ∧ (s.tag n).1.toIdTree.rootId.post + 1 = (s.tag n).2 := by
-  intro s
-  induction s with
-  | basic bs =>
-      intro n
-      obtain ⟨gBs, pBs⟩ := BasicStmt.tag_spec bs n
-      have lBs := gBs.lo_le_post
-      refine ⟨?_, ?_⟩
-      · simp only [Stmt.tag, Stmt.Tagged.toIdTree]
-        refine Good.mk ?_ ?_
-        · simp only [NodeId.lo]; omega
-        · refine GoodChildren.cons gBs ?_
-          rw [pBs]; exact GoodChildren.nil
-      · simp only [Stmt.tag, Stmt.Tagged.toIdTree, IdTree.rootId_node]
-  | andThen a b iha ihb =>
-      intro n
-      obtain ⟨gA, pA⟩ := iha n
-      obtain ⟨gB, pB⟩ := ihb (a.tag n).2
-      have lA := gA.lo_le_post
-      have lB := gB.lo_le_post
-      refine ⟨?_, ?_⟩
-      · simp only [Stmt.tag, Stmt.Tagged.toIdTree]
-        refine Good.mk ?_ ?_
-        · simp only [NodeId.lo]; omega
-        · refine GoodChildren.cons gA ?_
-          rw [pA]; refine GoodChildren.cons gB ?_; rw [pB]; exact GoodChildren.nil
-      · simp only [Stmt.tag, Stmt.Tagged.toIdTree, IdTree.rootId_node]
-  | ifElse e a b iha ihb =>
-      intro n
-      obtain ⟨gE, pE⟩ := Expr.tag_spec e n
-      obtain ⟨gA, pA⟩ := iha (e.tag n).2
-      obtain ⟨gB, pB⟩ := ihb (a.tag (e.tag n).2).2
-      have lE := gE.lo_le_post
-      have lA := gA.lo_le_post
-      have lB := gB.lo_le_post
-      refine ⟨?_, ?_⟩
-      · simp only [Stmt.tag, Stmt.Tagged.toIdTree]
-        refine Good.mk ?_ ?_
-        · simp only [NodeId.lo]; omega
-        · refine GoodChildren.cons gE ?_
-          rw [pE]; refine GoodChildren.cons gA ?_
-          rw [pA]; refine GoodChildren.cons gB ?_; rw [pB]; exact GoodChildren.nil
-      · simp only [Stmt.tag, Stmt.Tagged.toIdTree, IdTree.rootId_node]
-  | whileLoop e s ih =>
-      intro n
-      obtain ⟨gE, pE⟩ := Expr.tag_spec e n
-      obtain ⟨gS, pS⟩ := ih (e.tag n).2
-      have lE := gE.lo_le_post
-      have lS := gS.lo_le_post
-      refine ⟨?_, ?_⟩
-      · simp only [Stmt.tag, Stmt.Tagged.toIdTree]
-        refine Good.mk ?_ ?_
-        · simp only [NodeId.lo]; omega
-        · refine GoodChildren.cons gE ?_
-          rw [pE]; refine GoodChildren.cons gS ?_; rw [pS]; exact GoodChildren.nil
-      · simp only [Stmt.tag, Stmt.Tagged.toIdTree, IdTree.rootId_node]
-
-/-- A freshly tagged program is a well-tagged tree (rooted at postorder start `0`). -/
-theorem good_tagStmt (s : Stmt) : Good 0 (tagStmt s).toIdTree :=
-  (Stmt.tag_spec s 0).1
-
-/-- **Descendant characterization.** The numeric `NodeId.DescendantOf` relation on
-two nodes of a tagged program holds exactly when one is structurally contained in
-the other's subtree. -/
-theorem descendant_iff_tagStmt (s : Stmt) {a b : IdTree}
-    (ha : a ∈ IdTree.subtrees (tagStmt s).toIdTree)
-    (hb : b ∈ IdTree.subtrees (tagStmt s).toIdTree) :
-    a.rootId.DescendantOf b.rootId ↔ a ∈ IdTree.subtrees b :=
-  descendant_iff_of_good (good_tagStmt s) ha hb
-```

lean/Spa/Language/Tagged/Derive.lean

@@ -1,509 +0,0 @@
-import Lean
-import Mathlib.Tactic.DeriveTraversable
-import Spa.Language.Base
-import Spa.Language.Tagged.Id
-
-/-!
-# The `derive_tagged` command
-
-`derive_tagged T₁ T₂ … Tₙ` takes a family of (possibly mutually recursive)
-inductive types and generates, for each `Tᵢ`:
-
-* a *tagged* mirror inductive `Tᵢ.Tagged (τ : Type)`, in which every constructor
-  carries a leading `tag : τ` field and every field whose type is a family
-  member is retyped to its `.Tagged τ` counterpart;
-* `Tᵢ.Tagged.erase : Tᵢ.Tagged τ → Tᵢ`, forgetting all tags;
-* `Tᵢ.tag : Tᵢ → ℕ → Tᵢ.Tagged RawId × ℕ`, assigning every node a unique
-  `RawId` (its postorder index) by a single unified traversal that threads a
-  counter; the whole family shares one counter, so identifiers are unique across
-  types.
-
-The generated declarations have exactly the shape of the hand-written reference;
-see `Spa/Language/Tagged/Basic.lean` (which invokes this command) and the proofs
-in `Spa/Language/Tagged/Properties.lean`.
-
-Scope: the generator handles non-indexed inductives whose constructor fields are
-either scalars or *direct* references to a family member (which covers the object
-language).  Nested occurrences such as `List Tᵢ` are not supported.
--/
-
-open Lean Elab Command Meta
-
-namespace Spa.DeriveTagged
-
-/-- One constructor field, classified as a recursive family reference or a scalar
-(whose type syntax we keep verbatim for the mirror inductive). -/
-structure FieldData where
-  isRec : Bool
-  recType : Name
-  typeStx : Term
-
-/-- A constructor: its original (full) name, short name, and fields. -/
-structure CtorData where
-  origName : Name
-  shortName : Name
-  fields : Array FieldData
-
-/-- A family member together with its constructors. -/
-structure TypeData where
-  name : Name
-  ctors : Array CtorData
-
-def taggedOf (n : Name) : Name := n ++ `Tagged
-def eraseOf (n : Name) : Name := n ++ `Tagged ++ `erase
-def rootTagOf (n : Name) : Name := n ++ `Tagged ++ `rootTag
-def tagOf (n : Name) : Name := n ++ `tag
-def foldTagsOf (n : Name) : Name := n ++ `Tagged ++ `foldTags
-def wfOf (n : Name) : Name := n ++ `Tagged ++ `WF
-def narrowOf (n : Name) : Name := n ++ `Tagged ++ `narrow
-def narrowEraseOf (n : Name) : Name := n ++ `Tagged ++ `narrow_erase
-def tagLeOf (n : Name) : Name := n ++ `tag_le
-def tagRootTagPostOf (n : Name) : Name := n ++ `tag_rootTag_post
-def tagWfOf (n : Name) : Name := n ++ `tag_wf
-
-/-- Project the `i`-th conjunct (1-based) out of `hyp`, which has type a
-right-nested `And` of `total` conjuncts, e.g. `hyp |>.2 |>.2 |>.1`. -/
-def projAnd {m : Type → Type} [Monad m] [MonadQuotation m]
-    (hyp : Term) (i total : Nat) : m Term := do
-  let mut t := hyp
-  for _ in [0:i-1] do
-    t ← `($t |>.2)
-  if i < total then
-    t ← `($t |>.1)
-  return t
-
-/-- Combine a non-empty array of propositions into a right-nested conjunction. -/
-def mkAndR {m : Type → Type} [Monad m] [MonadQuotation m]
-    (cs : Array Term) : m Term := do
-  let mut t := cs.back!
-  for c in cs.pop.reverse do
-    t ← `($c ∧ $t)
-  return t
-
-/-- For a constructor, return one entry per *recursive* field: its argument
-identifier, the family member it references, and the start-counter expression at
-which it is tagged (`n`, then `(a.tag n).2`, …) — the same threading `mkTag`
-uses. -/
-def recChildren (cd : CtorData) (argNames : Array Ident) (nStart : Term) :
-    CommandElabM (Array (Ident × Name × Term)) := do
-  let mut res : Array (Ident × Name × Term) := #[]
-  let mut cur := nStart
-  for (f, a) in cd.fields.zip argNames do
-    if f.isRec then
-      res := res.push (a, f.recType, cur)
-      cur ← `(($(mkIdent (tagOf f.recType)) $a $cur) |>.2)
-  return res
-
-/-- Inspect the family, classifying each constructor field. -/
-def gather (family : Array Name) (τ : Ident) : TermElabM (Array TypeData) := do
-  let famSet : NameSet := family.foldl (·.insert ·) {}
-  family.mapM fun tn => do
-    let iv ← getConstInfoInduct tn
-    let ctors ← iv.ctors.toArray.mapM fun cn => do
-      let cv ← getConstInfoCtor cn
-      let fields ← forallTelescopeReducing cv.type fun args _ => do
-        let fieldArgs := args.extract iv.numParams args.size
-        fieldArgs.mapM fun a => do
-          let ty ← inferType a
-          match ty.getAppFn.constName? with
-          | some hn =>
-            if famSet.contains hn then
-              return { isRec := true, recType := hn, typeStx := ← `($(mkIdent (taggedOf hn)) $τ) }
-            else
-              return { isRec := false, recType := default, typeStx := ← Lean.PrettyPrinter.delab ty }
-          | none =>
-            return { isRec := false, recType := default, typeStx := ← Lean.PrettyPrinter.delab ty }
-      return { origName := cn, shortName := cn.componentsRev.head!, fields }
-    return { name := tn, ctors }
-
-/-- The arrow type `τ → <fields…> → Self τ` of a tagged constructor. -/
-def ctorArrow (cd : CtorData) (self : Term) (τ : Ident) : TermElabM Term := do
-  let mut t := self
-  for f in cd.fields.reverse do
-    t ← `($(f.typeStx) → $t)
-  `($τ → $t)
-
-/-- The tagged mirror inductives, one per family member.  The family is a DAG
-(`Expr ← BasicStmt ← Stmt`), not genuinely mutual, so they are emitted as
-separate inductives in dependency order rather than a `mutual` block.
-
-`Functor`/`Traversable` instances are derived separately by `mkDeriveInstances`
-below rather than via an inline `deriving` clause. -/
-def mkInductives (tds : Array TypeData) (τ : Ident) :
-    CommandElabM (Array (TSyntax `command)) := do
-  tds.mapM fun td => do
-    let self ← `($(mkIdent (taggedOf td.name)) $τ)
-    let ctors ← td.ctors.mapM fun cd => do
-      let aty ← Command.liftTermElabM (ctorArrow cd self τ)
-      `(Lean.Parser.Command.ctor| | $(mkIdent cd.shortName):ident : $aty)
-    `(command| inductive $(mkIdent (taggedOf td.name)):ident ($τ : Type) where $ctors*)
-
-/-- A `deriving instance Functor, Traversable for Tᵢ.Tagged` command per family
-member.  Since every tagged type is a single-parameter, direct-recursive
-inductive in `τ`, Mathlib's deriving handler produces clean (`sorry`-free)
-instances, giving `map`, `traverse`, and the `Traversable.foldr`/`toList` folds
-for free.
-
-These are emitted as *separate* commands in dependency order (rather than an
-inline `deriving` clause on each inductive) for two reasons: deriving
-`Stmt.Tagged` needs the `Expr.Tagged`/`BasicStmt.Tagged` instances already in
-scope, and — because every member's type name ends in `.Tagged` — the handler's
-auto-generated instance name (`instFunctorTagged`, built from the type's last
-component) collides across the family unless each derive sees the environment
-the previous one updated; separate commands give it that, so the names
-disambiguate to `instFunctorTagged`, `instFunctorTagged_1`, ….
-
-The hand-written `foldTags` is retained alongside these: it is a
-structural-recursion fold that `simp`/`decide` reduce cleanly, unlike the
-abstract `Traversable.foldr` (defined via the `FreeMonoid`/`Const` applicative),
-which reduces under `decide`/`rfl` but not naive `simp` unfolding. -/
-def mkDeriveInstances (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
-  tds.mapM fun td =>
-    `(command| deriving instance Functor, Traversable for $(mkIdent (taggedOf td.name)))
-
-/-- The `erase` functions, one per family member (separate defs in dependency
-order — each calls only already-defined lower members). -/
-def mkErase (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
-  tds.mapM fun td => do
-    let mut pats : Array Term := #[]
-    let mut rhss : Array Term := #[]
-    for cd in td.ctors do
-      let argNames := (Array.range cd.fields.size).map (fun i => mkIdent (.mkSimple s!"a{i}"))
-      let pat ← `($(mkIdent (taggedOf td.name ++ cd.shortName)) _ $argNames*)
-      let eraseArgs ← (cd.fields.zip argNames).mapM fun (f, a) =>
-        if f.isRec then `($(mkIdent (eraseOf f.recType)) $a) else pure a
-      let rhs ← `($(mkIdent cd.origName) $eraseArgs*)
-      pats := pats.push pat
-      rhss := rhss.push rhs
-    `(command| def $(mkIdent (eraseOf td.name)) {τ : Type} :
-        $(mkIdent (taggedOf td.name)) τ → $(mkIdent td.name) :=
-        fun x => match x with $[| $pats => $rhss]*)
-
-/-- The `rootTag` accessors (one non-recursive `def` per type). -/
-def mkRootTag (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
-  let tIdent := mkIdent `t
-  tds.mapM fun td => do
-    let mut pats : Array Term := #[]
-    let mut rhss : Array Term := #[]
-    for cd in td.ctors do
-      let hole ← `(_)
-      let wilds := Array.mkArray cd.fields.size hole
-      pats := pats.push (← `($(mkIdent (taggedOf td.name ++ cd.shortName)) $tIdent $wilds*))
-      rhss := rhss.push tIdent
-    `(command| def $(mkIdent (rootTagOf td.name)) {τ : Type} :
-        $(mkIdent (taggedOf td.name)) τ → τ :=
-        fun x => match x with $[| $pats => $rhss]*)
-
-/-- The postorder `tag` functions, one per family member (separate defs in
-dependency order). -/
-def mkTag (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
-  let nId := mkIdent ``Spa.RawId
-  tds.mapM fun td => do
-    let mut pats : Array Term := #[]
-    let mut rhss : Array Term := #[]
-    for cd in td.ctors do
-      let argNames := (Array.range cd.fields.size).map (fun i => mkIdent (.mkSimple s!"a{i}"))
-      let pat ← `($(mkIdent cd.origName) $argNames*)
-      let mut cur : Term ← `(n)
-      let mut lets : Array (Ident × Term) := #[]
-      let mut taggedArgs : Array Term := #[]
-      let mut ri := 0
-      for (f, a) in cd.fields.zip argNames do
-        if f.isRec then
-          let rName := mkIdent (.mkSimple s!"r{ri}")
-          let rhsCall ← `($(mkIdent (tagOf f.recType)) $a $cur)
-          lets := lets.push (rName, rhsCall)
-          taggedArgs := taggedArgs.push (← `($rName |>.1))
-          cur ← `($rName |>.2)
-          ri := ri + 1
-        else
-          taggedArgs := taggedArgs.push a
-      let last := cur
-      let tagged ← `($(mkIdent (taggedOf td.name ++ cd.shortName))
-          (⟨$last⟩ : $nId) $taggedArgs*)
-      let mut body ← `(($tagged, $last + 1))
-      for (rName, rhs) in lets.reverse do
-        body ← `(let $rName := $rhs; $body)
-      pats := pats.push pat
-      rhss := rhss.push body
-    `(command| def $(mkIdent (tagOf td.name)) :
-        $(mkIdent td.name) → Nat → $(mkIdent (taggedOf td.name)) $nId × Nat :=
-        fun e n => match e with $[| $pats => $rhss]*)
-
-/-- The tag-fold functions: `foldTags f acc t` applies `f` to every tag in `t`,
-right-to-left, threading `acc`.  This is the `Foldable`/`foldr`-over-tags the
-hand-written collectors (e.g. `subtreeIds`) reduce to.  One separate def per
-family member (the family is a DAG, so no `mutual` block is needed). -/
-def mkFoldTags (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
-  let τ := mkIdent `τ
-  let m := mkIdent `M
-  let fId := mkIdent `f
-  let accId := mkIdent `acc
-  let tagId := mkIdent `t
-  tds.mapM fun td => do
-    let mut pats : Array Term := #[]
-    let mut rhss : Array Term := #[]
-    for cd in td.ctors do
-      let argNames := (Array.range cd.fields.size).map (fun i => mkIdent (.mkSimple s!"a{i}"))
-      let pat ← `($(mkIdent (taggedOf td.name ++ cd.shortName)) $tagId $argNames*)
-      let mut body : Term := accId
-      for (fld, a) in (cd.fields.zip argNames).reverse do
-        if fld.isRec then
-          body ← `($(mkIdent (foldTagsOf fld.recType)) $fId $body $a)
-      body ← `($fId $tagId $body)
-      pats := pats.push pat
-      rhss := rhss.push body
-    `(command| def $(mkIdent (foldTagsOf td.name)) {$τ:ident : Type} {$m:ident : Type}
-        ($fId : $τ → $m → $m) ($accId : $m) :
-        $(mkIdent (taggedOf td.name)) $τ → $m :=
-        fun x => match x with $[| $pats => $rhss]*)
-
-/-- The well-formedness predicate `T.Tagged.WF : T.Tagged RawId → Prop`: every
-recursive child's root tag has a strictly smaller postorder index than the node's
-own tag, and each child is itself well-formed.  Leaf constructors are `True`. -/
-def mkWF (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
-  let tId := mkIdent `t
-  let rawId := mkIdent ``Spa.RawId
-  tds.mapM fun td => do
-    let mut pats : Array Term := #[]
-    let mut rhss : Array Term := #[]
-    for cd in td.ctors do
-      let hasRec := cd.fields.any (·.isRec)
-      let mut patArgs : Array Term := #[]
-      let mut recArgs : Array Ident := #[]
-      let mut i := 0
-      for f in cd.fields do
-        if f.isRec then
-          let a := mkIdent (.mkSimple s!"a{i}")
-          patArgs := patArgs.push a
-          recArgs := recArgs.push a
-        else
-          patArgs := patArgs.push (← `(_))
-        i := i + 1
-      let tagBind : Term ← if hasRec then `($tId) else `(_)
-      let pat ← `($(mkIdent (taggedOf td.name ++ cd.shortName)) $tagBind $patArgs*)
-      let rhs ← if recArgs.isEmpty then `(True) else do
-        let bounds ← recArgs.mapM fun a => `($(a).rootTag.post < $(tId).post)
-        let wfs ← recArgs.mapM fun a => `($(a).WF)
-        mkAndR (bounds ++ wfs)
-      pats := pats.push pat
-      rhss := rhss.push rhs
-    `(command| def $(mkIdent (wfOf td.name)) :
-        $(mkIdent (taggedOf td.name)) $rawId → Prop :=
-        fun x => match x with $[| $pats => $rhss]*)
-
-/-- The `narrow` coercion `T.Tagged RawId → T.Tagged (Fin N)`, given a bound on
-the root tag and a well-formedness proof.  Each node's tag becomes the `Fin N`
-built from its postorder index, and recursion threads the bound through `lt_trans`
-and the (definitionally unfolded) `WF` conjunction. -/
-def mkNarrow (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
-  let rawId := mkIdent ``Spa.RawId
-  let tId := mkIdent `t
-  let nId := mkIdent `N
-  let hId := mkIdent `h
-  let hwfId := mkIdent `hwf
-  let tgId := mkIdent `tg
-  tds.mapM fun td => do
-    let self ← `($(mkIdent (taggedOf td.name)) $rawId)
-    let mut patss : Array (Array Term) := #[]
-    let mut rhss : Array Term := #[]
-    for cd in td.ctors do
-      let argNames := (Array.range cd.fields.size).map fun i => mkIdent (.mkSimple s!"a{i}")
-      let ctorPat ← `($(mkIdent (taggedOf td.name ++ cd.shortName)) $tgId $argNames*)
-      let k := (cd.fields.filter (·.isRec)).size
-      let mut newArgs : Array Term := #[]
-      let mut ri := 0
-      for (f, a) in cd.fields.zip argNames do
-        if f.isRec then
-          let bound ← projAnd hwfId (ri + 1) (2 * k)
-          let wf ← projAnd hwfId (k + ri + 1) (2 * k)
-          newArgs := newArgs.push (← `($(a).narrow (lt_trans $bound $hId) $wf))
-          ri := ri + 1
-        else
-          newArgs := newArgs.push a
-      let built ← `($(mkIdent (taggedOf td.name ++ cd.shortName)) ⟨$(tgId).post, $hId⟩ $newArgs*)
-      let nPat ← `(_)
-      let hPat ← `($hId)
-      let hwfPat : Term ← if k == 0 then `(_) else `($hwfId)
-      patss := patss.push #[ctorPat, nPat, hPat, hwfPat]
-      rhss := rhss.push built
-    `(command| def $(mkIdent (narrowOf td.name)) : ($tId : $self) → {$nId : ℕ} →
-        $(tId).rootTag.post < $nId → $(tId).WF → $(mkIdent (taggedOf td.name)) (Fin $nId)
-        $[| $[$patss],* => $rhss]*)
-
-/-- `T.tag_rootTag_post`: the root tag of a freshly tagged node is exactly one
-below the threaded-out counter, i.e. the node itself is numbered last (postorder).
-A uniform `cases <;> simp` discharges every constructor. -/
-def mkTagRootTagPost (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
-  let eId := mkIdent `e
-  let nId := mkIdent `n
-  tds.mapM fun td =>
-    `(command| theorem $(mkIdent (tagRootTagPostOf td.name))
-        ($eId : $(mkIdent td.name)) ($nId : ℕ) :
-        ($(eId).tag $nId).1.rootTag.post + 1 = ($(eId).tag $nId).2 := by
-        cases $eId:ident <;>
-          simp [$(mkIdent (tagOf td.name)):ident, $(mkIdent (rootTagOf td.name)):ident])
-
-/-- `T.tag_le`: tagging only ever advances the counter (`n ≤ (e.tag n).2`).
-Proved by induction; each arm threads the counter through its recursive children
-(using the relevant `tag_le`/induction hypothesis) and closes with `omega`. -/
-def mkTagLe (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
-  let eId := mkIdent `e
-  let nId := mkIdent `n
-  tds.mapM fun td => do
-    let mut ctorLabels : Array Ident := #[]
-    let mut binderss : Array (Array Ident) := #[]
-    let mut tacs : Array (TSyntax ``Lean.Parser.Tactic.tacticSeq) := #[]
-    for cd in td.ctors do
-      let argNames := (Array.range cd.fields.size).map fun i => mkIdent (.mkSimple s!"a{i}")
-      let mut ihBinders : Array Ident := #[]
-      let mut haveTacs : Array (TSyntax `tactic) := #[]
-      let mut cur : Term ← `($nId)
-      let mut i := 0
-      for (f, a) in cd.fields.zip argNames do
-        if f.isRec then
-          let fact ← if f.recType == td.name then
-              `($(mkIdent (.mkSimple s!"ih{i}")) $cur)
-            else
-              `($(mkIdent (tagLeOf f.recType)) $a $cur)
-          if f.recType == td.name then
-            ihBinders := ihBinders.push (mkIdent (.mkSimple s!"ih{i}"))
-          haveTacs := haveTacs.push (← `(tactic| have := $fact))
-          cur ← `(($(mkIdent (tagOf f.recType)) $a $cur) |>.2)
-        i := i + 1
-      let simpTac ← `(tactic| simp only [$(mkIdent (tagOf td.name)):ident])
-      let omegaTac ← `(tactic| omega)
-      let allTacs := #[simpTac] ++ haveTacs ++ #[omegaTac]
-      ctorLabels := ctorLabels.push (mkIdent cd.shortName)
-      binderss := binderss.push (argNames ++ ihBinders)
-      tacs := tacs.push (← `(tacticSeq| $[$allTacs]*))
-    `(command| theorem $(mkIdent (tagLeOf td.name)) ($eId : $(mkIdent td.name)) ($nId : ℕ) :
-        $nId ≤ ($(eId).tag $nId).2 := by
-        induction $eId:ident generalizing $nId:ident with
-          $[| $ctorLabels:ident $binderss* => $tacs]*)
-
-/-- `T.tag_wf`: a freshly tagged term is well-formed.  Each recursive child's
-bound conjunct is closed by `omega` from that child's `tag_rootTag_post` plus the
-`tag_le` of every later child (which bounds the threaded-out counter), and each
-well-formedness conjunct is the child's induction hypothesis / `tag_wf`. -/
-def mkTagWf (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
-  let eId := mkIdent `e
-  let nId := mkIdent `n
-  tds.mapM fun td => do
-    let mut ctorLabels : Array Ident := #[]
-    let mut binderss : Array (Array Ident) := #[]
-    let mut tacs : Array (TSyntax ``Lean.Parser.Tactic.tacticSeq) := #[]
-    for cd in td.ctors do
-      let argNames := (Array.range cd.fields.size).map fun i => mkIdent (.mkSimple s!"a{i}")
-      -- recursive children: (arg, recType, startCounter, sameType?, fieldIndex)
-      let mut recs : Array (Ident × Name × Term × Bool × Nat) := #[]
-      let mut cur : Term ← `($nId)
-      let mut i := 0
-      for (f, a) in cd.fields.zip argNames do
-        if f.isRec then
-          recs := recs.push (a, f.recType, cur, f.recType == td.name, i)
-          cur ← `(($(mkIdent (tagOf f.recType)) $a $cur) |>.2)
-        i := i + 1
-      let k := recs.size
-      let ihBinders := (recs.filter (·.2.2.2.1)).map fun r => mkIdent (.mkSimple s!"ih{r.2.2.2.2}")
-      let tac : TSyntax ``Lean.Parser.Tactic.tacticSeq ← if k == 0 then
-          `(tacticSeq| exact True.intro)
-        else do
-          let mut comps : Array Term := #[]
-          -- bound conjuncts
-          for idx in [0:k] do
-            let (a, rt, s, _, _) := recs[idx]!
-            let mut bHaves : Array (TSyntax `tactic) :=
-              #[← `(tactic| have := $(mkIdent (tagRootTagPostOf rt)) $a $s)]
-            for j in [idx+1:k] do
-              let (aj, rtj, sj, _, _) := recs[j]!
-              bHaves := bHaves.push (← `(tactic| have := $(mkIdent (tagLeOf rtj)) $aj $sj))
-            bHaves := bHaves.push (← `(tactic| omega))
-            comps := comps.push (← `(by $(← `(tacticSeq| $[$bHaves]*))))
-          -- well-formedness conjuncts
-          for idx in [0:k] do
-            let (a, rt, s, same, fi) := recs[idx]!
-            comps := comps.push <| ← if same then `($(mkIdent (.mkSimple s!"ih{fi}")) $s)
-              else `($(mkIdent (tagWfOf rt)) $a $s)
-          let simpTac ← `(tactic| simp only
-            [$(mkIdent (tagOf td.name)):ident, $(mkIdent (wfOf td.name)):ident])
-          let exactTac ← `(tactic| exact ⟨$comps,*⟩)
-          `(tacticSeq| $[$(#[simpTac, exactTac])]*)
-      ctorLabels := ctorLabels.push (mkIdent cd.shortName)
-      binderss := binderss.push (argNames ++ ihBinders)
-      tacs := tacs.push tac
-    `(command| theorem $(mkIdent (tagWfOf td.name)) ($eId : $(mkIdent td.name)) ($nId : ℕ) :
-        ($(eId).tag $nId).1.WF := by
-        induction $eId:ident generalizing $nId:ident with
-          $[| $ctorLabels:ident $binderss* => $tacs]*)
-
-/-- `T.Tagged.narrow_erase`: narrowing the tag type does not change the erased
-(untagged) term.  A per-constructor `simp` with the local `narrow`/`erase`
-equations, the lower members' `narrow_erase`, and the induction hypotheses. -/
-def mkNarrowErase (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
-  let rawId := mkIdent ``Spa.RawId
-  let tId := mkIdent `t
-  let nId := mkIdent `N
-  let hId := mkIdent `h
-  let hwfId := mkIdent `hwf
-  let tgId := mkIdent `tg
-  tds.mapM fun td => do
-    let mut ctorLabels : Array Ident := #[]
-    let mut binderss : Array (Array Ident) := #[]
-    let mut tacs : Array (TSyntax ``Lean.Parser.Tactic.tacticSeq) := #[]
-    for cd in td.ctors do
-      let argNames := (Array.range cd.fields.size).map fun i => mkIdent (.mkSimple s!"a{i}")
-      let mut lemmas : Array Term :=
-        #[← `($(mkIdent (narrowOf td.name))), ← `($(mkIdent (eraseOf td.name)))]
-      let mut ihBinders : Array Ident := #[]
-      let mut seenLower : Array Name := #[]
-      let mut i := 0
-      for f in cd.fields do
-        if f.isRec then
-          if f.recType == td.name then
-            let ih := mkIdent (.mkSimple s!"ih{i}")
-            ihBinders := ihBinders.push ih
-            lemmas := lemmas.push (← `($ih))
-          else if !seenLower.contains f.recType then
-            seenLower := seenLower.push f.recType
-            lemmas := lemmas.push (← `($(mkIdent (narrowEraseOf f.recType))))
-        i := i + 1
-      let introTac ← `(tactic| intro $nId $hId $hwfId)
-      let simpTac ← `(tactic| simp [$[$lemmas:term],*])
-      ctorLabels := ctorLabels.push (mkIdent cd.shortName)
-      binderss := binderss.push (#[tgId] ++ argNames ++ ihBinders)
-      tacs := tacs.push (← `(tacticSeq| $[$(#[introTac, simpTac])]*))
-    `(command| theorem $(mkIdent (narrowEraseOf td.name)) :
-        ($tId : $(mkIdent (taggedOf td.name)) $rawId) → ∀ {$nId : ℕ}
-          ($hId : $(tId).rootTag.post < $nId) ($hwfId : $(tId).WF),
-          ($(tId).narrow $hId $hwfId).erase = $(tId).erase := by
-        intro $tId:ident
-        induction $tId:ident with
-          $[| $ctorLabels:ident $binderss* => $tacs]*)
-
-/-- `derive_tagged T₁ … Tₙ` — generate tagged mirrors, `erase`, and `tag` for the
-given family of inductives. -/
-syntax (name := deriveTaggedCmd) "derive_tagged " ident+ : command
-
-@[command_elab deriveTaggedCmd]
-def elabDeriveTagged : CommandElab := fun stx => do
-  match stx with
-  | `(derive_tagged $ids*) =>
-    let family ← ids.mapM fun i => Command.liftCoreM (realizeGlobalConstNoOverload i)
-    let τ := mkIdent `τ
-    let tds ← Command.liftTermElabM (gather family τ)
-    for d in (← mkInductives tds τ) do elabCommand d
-    for d in (← mkDeriveInstances tds) do elabCommand d
-    for d in (← mkRootTag tds) do elabCommand d
-    for d in (← mkErase tds) do elabCommand d
-    for d in (← mkTag tds) do elabCommand d
-    for d in (← mkFoldTags tds) do elabCommand d
-    for d in (← mkWF tds) do elabCommand d
-    for d in (← mkNarrow tds) do elabCommand d
-    for d in (← mkTagRootTagPost tds) do elabCommand d
-    for d in (← mkTagLe tds) do elabCommand d
-    for d in (← mkTagWf tds) do elabCommand d
-    for d in (← mkNarrowErase tds) do elabCommand d
-  | _ => throwUnsupportedSyntax
-
-end Spa.DeriveTagged

lean/Spa/Language/Tagged/Graphs.lean

@@ -1,104 +0,0 @@
-import Spa.Language
-import Spa.Language.Graphs
-import Spa.Language.Tagged.Basic
-import Spa.Language.Tagged.Properties
-
-namespace Spa
-
-open GGraph
-
-def Stmt.Tagged.cfg {τ : Type} : Stmt.Tagged τ → GGraph (Option (BasicStmt.Tagged τ))
-  | .basic _ bs => GGraph.singleton (some bs)
-  | .andThen _ s₁ s₂ => s₁.cfg ⤳  s₂.cfg
-  | .ifElse _ _ s₁ s₂ => s₁.cfg ∙ s₂.cfg
-  | .whileLoop _ _ s => GGraph.loop s.cfg
-
-theorem Stmt.Tagged.cfg_graph {τ : Type} : ∀ (t : Stmt.Tagged τ),
-    (Option.map BasicStmt.Tagged.erase) <$> t.cfg = t.erase.cfg
-  | .basic _ bs => by simp [Stmt.Tagged.cfg, Stmt.cfg, Stmt.Tagged.erase, BasicStmt.Tagged.erase]
-  | .andThen _ s₁ s₂ => by
-      simp [Stmt.Tagged.cfg, Stmt.cfg, Stmt.Tagged.erase, Stmt.Tagged.cfg_graph s₁, Stmt.Tagged.cfg_graph s₂]
-  | .ifElse _ _ s₁ s₂ => by
-      simp [Stmt.Tagged.cfg, Stmt.cfg, Stmt.Tagged.erase, Stmt.Tagged.cfg_graph s₁, Stmt.Tagged.cfg_graph s₂]
-  | .whileLoop _ _ s => by
-      simp [Stmt.Tagged.cfg, Stmt.cfg, Stmt.Tagged.erase, Stmt.Tagged.cfg_graph s]
-
-def GGraph.nodeLabel {τ : Type} (g : GGraph (Option (BasicStmt.Tagged τ))) (i : g.Index) :
-    Option τ :=
-  (g.nodes i).map BasicStmt.Tagged.rootTag
-
-def GGraph.stateOf {τ : Type} [DecidableEq τ] (g : GGraph (Option (BasicStmt.Tagged τ)))
-    (id : τ) : Option g.Index :=
-  g.indices.find? (fun i => decide (g.nodeLabel i = some id))
-
-theorem GGraph.stateOf_label {τ : Type} [DecidableEq τ]
-    {g : GGraph (Option (BasicStmt.Tagged τ))} {id : τ}
-    {i : g.Index} (h : g.stateOf id = some i) : g.nodeLabel i = some id := by
-  rw [GGraph.stateOf] at h
-  simpa using List.find?_some h
-
-namespace Program
-
-variable (p : Program)
-
-def tagged : Stmt.Tagged RawId := tagStmt p.rootStmt
-
-def size : ℕ := p.tagged.rootTag.post + 1
-
-theorem size_pos : 0 < p.size := Nat.succ_pos _
-
-abbrev NodeId : Type := Fin p.size
-
-theorem tagged_wf : p.tagged.WF := Stmt.tag_wf p.rootStmt 0
-
-def taggedFin : Stmt.Tagged p.NodeId :=
-  p.tagged.narrow (Nat.lt_succ_self _) p.tagged_wf
-
-def taggedCfg : GGraph (Option (BasicStmt.Tagged p.NodeId)) :=
-  GGraph.wrap p.taggedFin.cfg
-
-theorem taggedCfg_erase :
-    (Option.map BasicStmt.Tagged.erase) <$> p.taggedCfg = p.cfg := by
-  rw [taggedCfg, GGraph.map_wrap, Stmt.Tagged.cfg_graph, taggedFin,
-    Stmt.Tagged.narrow_erase, tagged, erase_tagStmt]
-  rfl
-
-theorem taggedCfg_size : p.taggedCfg.size = p.cfg.size := by
-  conv_rhs => rw [← p.taggedCfg_erase]
-  rfl
-
-def nodeIdOf (s : p.State) : Option p.NodeId :=
-  p.taggedCfg.nodeLabel (Fin.cast p.taggedCfg_size.symm s)
-
-def stateOfNodeId (id : p.NodeId) : Option p.State :=
-  (p.taggedCfg.stateOf id).map (Fin.cast p.taggedCfg_size)
-
-theorem cfg_nodes_eq (s : p.State) :
-    p.cfg.nodes s = Option.map BasicStmt.Tagged.erase
-      (p.taggedCfg.nodes (Fin.cast p.taggedCfg_size.symm s)) := by
-  have key : ∀ (g : Graph) (hsz : p.taggedCfg.size = g.size),
-      (Option.map BasicStmt.Tagged.erase) <$> p.taggedCfg = g →
-      ∀ i : Fin g.size,
-        g.nodes i = Option.map BasicStmt.Tagged.erase
-          (p.taggedCfg.nodes (Fin.cast hsz.symm i)) := by
-    intro g hsz hg i
-    subst hg
-    rfl
-  exact key p.cfg p.taggedCfg_size p.taggedCfg_erase s
-
-theorem nodeIdOf_isSome_of_code {s : p.State} {bs : BasicStmt}
-    (h : p.code s = some bs) : (p.nodeIdOf s).isSome = true := by
-  have hc : Option.map BasicStmt.Tagged.erase
-      (p.taggedCfg.nodes (Fin.cast p.taggedCfg_size.symm s)) = some bs := by
-    rw [← p.cfg_nodes_eq s]; exact h
-  unfold Program.nodeIdOf GGraph.nodeLabel
-  cases hcase : p.taggedCfg.nodes (Fin.cast p.taggedCfg_size.symm s) with
-  | none => rw [hcase] at hc; simp at hc
-  | some tbs => simp
-
-def nodeIdOfNonempty (s : p.State) {bs : BasicStmt} (h : p.code s = some bs) : p.NodeId :=
-  (p.nodeIdOf s).get (p.nodeIdOf_isSome_of_code h)
-
-end Program
-
-end Spa

lean/Spa/Language/Tagged/Id.lean

@@ -1,9 +0,0 @@
-import Mathlib.Data.Nat.Notation
-
-namespace Spa
-
-structure RawId where
-  post : ℕ
-  deriving DecidableEq, Repr
-
-end Spa

lean/Spa/Language/Tagged/Properties.lean

@@ -1,29 +0,0 @@
-import Spa.Language.Tagged.Basic
-
-namespace Spa
-
-@[simp] theorem Expr.erase_tag (e : Expr) (n : ℕ) : (e.tag n).1.erase = e := by
-  induction e generalizing n with
-  | add a b iha ihb => simp [Expr.tag, Expr.Tagged.erase, iha, ihb]
-  | sub a b iha ihb => simp [Expr.tag, Expr.Tagged.erase, iha, ihb]
-  | var x => simp [Expr.tag, Expr.Tagged.erase]
-  | num k => simp [Expr.tag, Expr.Tagged.erase]
-
-@[simp] theorem BasicStmt.erase_tag (bs : BasicStmt) (n : ℕ) :
-    (bs.tag n).1.erase = bs := by
-  cases bs with
-  | assign x e => simp [BasicStmt.tag, BasicStmt.Tagged.erase]
-  | noop => simp [BasicStmt.tag, BasicStmt.Tagged.erase]
-
-@[simp] theorem Stmt.erase_tag (s : Stmt) (n : ℕ) : (s.tag n).1.erase = s := by
-  induction s generalizing n with
-  | basic bs => simp [Stmt.tag, Stmt.Tagged.erase]
-  | andThen a b iha ihb => simp [Stmt.tag, Stmt.Tagged.erase, iha, ihb]
-  | ifElse e a b iha ihb => simp [Stmt.tag, Stmt.Tagged.erase, iha, ihb]
-  | whileLoop e s ih => simp [Stmt.tag, Stmt.Tagged.erase, ih]
-
-/-- Erasing a freshly tagged program recovers it. -/
-theorem erase_tagStmt (s : Stmt) : (tagStmt s).erase = s := by
-  simp [tagStmt]
-
-end Spa

lean/Spa/Language/Tagged/TODO.md

@@ -1,46 +0,0 @@
-# Tagged AST — follow-ups
-
-## Descendant tracking — parked
-
-The interval-labeling descendant test and its correctness proof
-(`descendant_iff_tagStmt` and supporting rose-tree/`Good` machinery) have been
-removed from the live code and parked in `DESCENDANT-TRACKING.md`, with a revival
-checklist. It's a computational optimization not yet needed; revive it (and the
-`NodeId.desc` field) when LICM wants fast ancestor queries.
-
-## ID → CFG-state mapping — plan part B — DONE
-
-`Graphs.lean` now defines a payload-generic `GGraph α` (with `Graph := GGraph
-(List BasicStmt)` as the concrete CFG), so the labelled CFG **reuses** the graph
-combinators instead of mirroring them. In `Cfg.lean`:
-`buildCfgL : Stmt.Tagged NodeId → GGraph (List (BasicStmt.Tagged NodeId))` is just
-`buildCfg` at the tagged payload; `buildCfgL_graph :
-(buildCfgL t).map (List.map erase) = buildCfg t.erase` connects it to the real
-CFG; and `GGraph.nodeLabel`/`GGraph.stateOf` read a node's id straight from its
-payload (`stateOf_label` is the soundness). No `LGraph`, no separate `label`
-field, no duplicated combinators.
-
-## ID → CFG-state mapping — totality — DONE
-
-The `Option`-valued `nodeIdOf`/`stateOfNodeId` are now proven total on the inputs
-that matter (`Graphs.lean`), via a payload-list characterization of the CFG:
-
-- `GGraph.nodeList` flattens `nodes` into the list of payloads, with combinator
-  lemmas (`nodeList_comp/link/loop/wrap`) reducing it through the CFG builders.
-- `Stmt.Tagged.basics` lists a program's basic statements; the master lemma
-  `Stmt.Tagged.cfg_nodeList_filter` (and its program-level
-  `taggedCfg_nodeList_filter`) shows the non-empty CFG nodes are *exactly* the
-  singletons `[bs]` for `bs ∈ basics`.
-- AST ⇒ CFG: `exists_state_of_mem_basics` (a state with payload `[bs]`) and
-  `stateOfNodeId_isSome` (the search succeeds).
-- CFG ⇒ AST: `exists_basic_of_code_ne_nil` (a non-empty node is `[bs]`, with
-  `code = [bs.erase]` and `nodeIdOf = some bs.rootTag`) and `nodeIdOf_isSome`.
-
-All `propext`/`Quot.sound`-only (no `sorry`, no choice).
-
-Remaining nice-to-have:
-- Injectivity: distinct basic-statement ids map to distinct states, giving a
-  two-sided id ↔ state correspondence (upgrading the existence results above to a
-  genuine bijection, and pinning `stateOfNodeId (bs.rootTag)` to *the* state
-  holding `bs`). The `tag`-uniqueness fact this needs (`Nodup` of postorder tags)
-  was part of the parked descendant machinery in `DESCENDANT-TRACKING.md`.

lean/Spa/Language/Traces.lean

@@ -1,266 +1,26 @@
 import Spa.Language.Semantics
 import Spa.Language.Graphs
-import Spa.Language.Program
-
-/-!
-
-# Program Traces
-
-This module defines program traces tied to Control Flow Graphs, or CFGs
-(see `Spa.GGraph` and `Spa.Graph`). These traces boil town to sequences of
-basic-block executions (really, `Spa.BasicStmt` executions), each of which must
-have an actual basic block in the graph _and_ be connected to the previous
-basic block by an edge. In this way, traces encode executions admitted
-by the CFG.
-
-While the regular `Trace` is just _any_ path through the graph, an
-`EndToEndTrace` is a path from the entry node to the exit node, denoting
-full program execution.
-
-Properties about graphs and language semantics (especially,
-the fact that the graph contains the proper basic block and edges
-to represent any program execution according to the
-language's big-step semantics `EvalStmt`) is found
-in `Spa/Language/Properties.lean`.
-
--/
 
 namespace Spa
 
-/-- A partial trace through a graph `g`, starting right before
+inductive Trace (g : Graph) : g.Index → g.Index → Env → Env → Prop
-    the execution of the basic block at the first index, and
-    ending right after the execution of the basic block at the last index. -/
-inductive Trace (g : Graph) : g.Index → g.Index → Env → Env → Type
   | single {ρ₁ ρ₂ : Env} {idx : g.Index} :
-      EvalBasicStmtOpt ρ₁ (g.nodes idx) ρ₂ → Trace g idx idx ρ₁ ρ₂
+      EvalBasicStmts ρ₁ (g.nodes idx) ρ₂ → Trace g idx idx ρ₁ ρ₂
   | edge {ρ₁ ρ₂ ρ₃ : Env} {idx₁ idx₂ idx₃ : g.Index} :
-      EvalBasicStmtOpt ρ₁ (g.nodes idx₁) ρ₂ → (idx₁, idx₂) ∈ g.edges →
+      EvalBasicStmts ρ₁ (g.nodes idx₁) ρ₂ → (idx₁, idx₂) ∈ g.edges →
       Trace g idx₂ idx₃ ρ₂ ρ₃ → Trace g idx₁ idx₃ ρ₁ ρ₃
 
-/-!
+theorem Trace.concat {g : Graph} {idx₁ idx₂ idx₃ idx₄ : g.Index}
-
-## Open Traces
-
-A normal `Trace` starts right before one state, and ends right after another.
-This is convenient for inductively proving correctness / sufficience, but
-awkward because 1) no empty traces exist and 2) concatenation requires an extra
-edge.
-
-However, when attempting an "empty" trace, two types are equally possible:
-traces that end _right before_ executing a state (`Traceₗ`) and
-traces that begin _right after_ executing a state (`Traceᵣ`). They
-are symmetric and can be concatenated with full traces on the left
-and right, respectively. -/
-
-/-- Left-open trace, representing execution that ends right before `idx₂`. -/
-inductive Traceₗ (g : Graph) : g.Index → g.Index → Env → Env → Type where
-  | nil {idx : g.Index} {ρ : Env} : Traceₗ g idx idx ρ ρ
-  | cons {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} :
-      EvalBasicStmtOpt ρ₁ (g.nodes idx₁) ρ₂ →
-      (idx₁, idx₂) ∈ g.edges →
-      Traceₗ g idx₂ idx₃ ρ₂ ρ₃ → Traceₗ g idx₁ idx₃ ρ₁ ρ₃
-
-def Traceₗ.single (g : Graph) (idx : g.Index) (ρ : Env) : Traceₗ g idx idx ρ ρ := .nil
-
-/-- Right-open trace, representing execution that starts right after `idx₁`. -/
-inductive Traceᵣ (g : Graph) : g.Index → g.Index → Env → Env → Type where
-  | nil {idx : g.Index} {ρ : Env} : Traceᵣ g idx idx ρ ρ
-  | cons {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} :
-      Traceᵣ g idx₁ idx₂ ρ₁ ρ₂ →
-      (idx₂, idx₃) ∈ g.edges →
-      EvalBasicStmtOpt ρ₂ (g.nodes idx₃) ρ₃ → Traceᵣ g idx₁ idx₃ ρ₁ ρ₃
-
-def Traceᵣ.single (g : Graph) (idx : g.Index) (ρ : Env) : Traceᵣ g idx idx ρ ρ := .nil
-
-/-- Sequence two traces together. Since the endpoint of the first trace
-    is _after_ its last basic block's execution, and the beginning of
-    the next trace is _before_ its first basic block's execution,
-    there must be an edge to connect the two. -/
-def 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₄ ρ₂ ρ₃) :
-    Trace g idx₁ idx₄ ρ₁ ρ₃ :=
+    Trace g idx₁ idx₄ ρ₁ ρ₃ := by
-  match tr₁ with
+  induction tr₁ with
-  | single hbs => edge hbs he tr₂
+  | single hbs => exact Trace.edge hbs he tr₂
-  | edge hbs he' tr₁' => edge hbs he' (tr₁'.concat he tr₂)
+  | edge hbs he' _ ih => exact Trace.edge hbs he' (ih he tr₂)
 
-scoped notation:65 tr₁:66 " ++< " he " >++ " tr₂:65 => Trace.concat tr₁ he tr₂
+inductive EndToEndTrace (g : Graph) (ρ₁ ρ₂ : Env) : Prop
-
-def Trace.addEdge {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ : Env} :
-    Trace g idx₁ idx₂ ρ₁ ρ₂ →
-    (idx₂, idx₃) ∈ g.edges →
-    Traceₗ g idx₁ idx₃ ρ₁ ρ₂
-  | .single hnode, hedge => .cons hnode hedge .nil
-  | .edge hnode hedge' rest, hedge => .cons hnode hedge' (rest.addEdge hedge)
-
-@[aesop simp]
-def Traceₗ.append {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} :
-    Traceₗ g idx₁ idx₂ ρ₁ ρ₂ → Traceₗ g idx₂ idx₃ ρ₂ ρ₃ →
-    Traceₗ g idx₁ idx₃ ρ₁ ρ₃
-  | .nil, rhs => rhs
-  | .cons hnode hedge rest, rhs => .cons hnode hedge (rest.append rhs)
-
-@[simp] def traceₗ_append_nil {g : Graph} {idx₁ idx₂ : g.Index} {ρ₁ ρ₂ : Env}
-    {trₗ : Traceₗ g idx₁ idx₂ ρ₁ ρ₂} : trₗ.append Traceₗ.nil = trₗ := by
-  induction trₗ <;> aesop
-
-def Traceₗ.appendTrace {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} :
-    Traceₗ g idx₁ idx₂ ρ₁ ρ₂ → Trace g idx₂ idx₃ ρ₂ ρ₃ →
-    Trace g idx₁ idx₃ ρ₁ ρ₃
-  | .nil, rhs => rhs
-  | .cons hnode hedge rest, rhs => .edge hnode hedge (rest.appendTrace rhs)
-
-def Traceₗ.appendStep {g : Graph} {idx₁ idx₂ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} :
-    Traceₗ g idx₁ idx₂ ρ₁ ρ₂ → EvalBasicStmtOpt ρ₂ (g.nodes idx₂) ρ₃ →
-    Trace g idx₁ idx₂ ρ₁ ρ₃ := fun trₗ hbs => trₗ.appendTrace (Trace.single hbs)
-
-def Trace.appendRight {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} :
-    Trace g idx₁ idx₂ ρ₁ ρ₂ → Traceᵣ g idx₂ idx₃ ρ₂ ρ₃ →
-    Trace g idx₁ idx₃ ρ₁ ρ₃
-  | lhs, .nil => lhs
-  | lhs, .cons rest hedge hnode => Trace.concat (lhs.appendRight rest) hedge (.single hnode)
-
-instance instHAppendTraceLTraceL {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} :
-    HAppend (Traceₗ g idx₁ idx₂ ρ₁ ρ₂) (Traceₗ g idx₂ idx₃ ρ₂ ρ₃) (Traceₗ g idx₁ idx₃ ρ₁ ρ₃) where
-  hAppend := Traceₗ.append
-
-instance instHAppendTraceLTrace {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} :
-    HAppend (Traceₗ g idx₁ idx₂ ρ₁ ρ₂) (Trace g idx₂ idx₃ ρ₂ ρ₃) (Trace g idx₁ idx₃ ρ₁ ρ₃) where
-  hAppend := Traceₗ.appendTrace
-
-instance instHAppendTraceLStep {g : Graph} {idx₁ idx₂ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} :
-    HAppend (Traceₗ g idx₁ idx₂ ρ₁ ρ₂) (EvalBasicStmtOpt ρ₂ (g.nodes idx₂) ρ₃) (Trace g idx₁ idx₂ ρ₁ ρ₃) where
-  hAppend := Traceₗ.appendStep
-
-instance instHAppendTraceTraceR {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} :
-    HAppend (Trace g idx₁ idx₂ ρ₁ ρ₂) (Traceᵣ g idx₂ idx₃ ρ₂ ρ₃) (Trace g idx₁ idx₃ ρ₁ ρ₃) where
-  hAppend := Trace.appendRight
-
-/-!
-
-## Trace Steps
-
-Analyses that care about *which statements executed* (e.g. reaching
-definitions) need to project a trace down to its list of executed statements.
-Defining that projection here, once, as a chronological mathlib `List` means
-all the re-association facts about concatenating traces come for free from
-`List.append_assoc` and friends, instead of being re-proven per analysis. -/
-
-/-- The (index, statement) pairs executed by a single optional-statement step:
-    none if the node is empty, and the node's statement otherwise. -/
-def EvalBasicStmtOpt.steps {α : Type*} (idx : α) {ρ₁ ρ₂ : Env} {obs : Option BasicStmt} :
-    EvalBasicStmtOpt ρ₁ obs ρ₂ → List (α × BasicStmt)
-  | .none => []
-  | .some (bs := bs) _ => [(idx, bs)]
-
-/-- The statements executed by a left-open trace, in chronological order. -/
-def Traceₗ.steps {g : Graph} {idx₁ idx₂ : g.Index} {ρ₁ ρ₂ : Env} :
-    Traceₗ g idx₁ idx₂ ρ₁ ρ₂ → List (g.Index × BasicStmt)
-  | .nil => []
-  | .cons (idx₁ := idx) hnode _ rest => hnode.steps idx ++ rest.steps
-
-/-- The statements executed by a trace, in chronological order. -/
-def Trace.steps {g : Graph} {idx₁ idx₂ : g.Index} {ρ₁ ρ₂ : Env} :
-    Trace g idx₁ idx₂ ρ₁ ρ₂ → List (g.Index × BasicStmt)
-  | .single (idx := idx) hnode => hnode.steps idx
-  | .edge (idx₁ := idx) hnode _ rest => hnode.steps idx ++ rest.steps
-
-@[simp] lemma Traceₗ.steps_append {g : Graph} {idx₁ idx₂ idx₃ : g.Index}
-    {ρ₁ ρ₂ ρ₃ : Env} (tr₁ : Traceₗ g idx₁ idx₂ ρ₁ ρ₂)
-    (tr₂ : Traceₗ g idx₂ idx₃ ρ₂ ρ₃) :
-    (tr₁ ++ tr₂).steps = tr₁.steps ++ tr₂.steps := by
-  show (tr₁.append tr₂).steps = _
-  induction tr₁ <;> simp [Traceₗ.append, Traceₗ.steps, *]
-
-@[simp] lemma Traceₗ.steps_appendTrace {g : Graph} {idx₁ idx₂ idx₃ : g.Index}
-    {ρ₁ ρ₂ ρ₃ : Env} (tr₁ : Traceₗ g idx₁ idx₂ ρ₁ ρ₂)
-    (tr₂ : Trace g idx₂ idx₃ ρ₂ ρ₃) :
-    (tr₁ ++ tr₂).steps = tr₁.steps ++ tr₂.steps := by
-  show (tr₁.appendTrace tr₂).steps = _
-  induction tr₁ <;> simp [Traceₗ.appendTrace, Traceₗ.steps, Trace.steps, *]
-
-@[simp] lemma Traceₗ.steps_appendStep {g : Graph} {idx₁ idx₂ : g.Index}
-    {ρ₁ ρ₂ ρ₃ : Env} (tr : Traceₗ g idx₁ idx₂ ρ₁ ρ₂)
-    (hbs : EvalBasicStmtOpt ρ₂ (g.nodes idx₂) ρ₃) :
-    (tr ++ hbs).steps = tr.steps ++ hbs.steps idx₂ :=
-  Traceₗ.steps_appendTrace tr (Trace.single hbs)
-
-@[simp] lemma Trace.steps_addEdge {g : Graph} {idx₁ idx₂ idx₃ : g.Index}
-    {ρ₁ ρ₂ : Env} (tr : Trace g idx₁ idx₂ ρ₁ ρ₂)
-    (hedge : (idx₂, idx₃) ∈ g.edges) :
-    (tr.addEdge hedge).steps = tr.steps := by
-  induction tr <;> simp [Trace.addEdge, Trace.steps, Traceₗ.steps, *]
-
-@[simp] lemma Traceₗ.append_addEdge {g : Graph}
-    {idx₁ idx₂ idx₃ idx₄ : g.Index} {ρ₁ ρ₂ ρ₃ ρ₄ : Env}
-    (trₗ : Traceₗ g idx₁ idx₂ ρ₁ ρ₂)
-    (hnode : EvalBasicStmtOpt ρ₂ (g.nodes idx₂) ρ₃)
-    (hedge : (idx₂, idx₃) ∈ g.edges)
-    (rest : Traceₗ g idx₃ idx₄ ρ₃ ρ₄) :
-    trₗ.append (Traceₗ.cons hnode hedge rest) =
-      (Trace.addEdge (trₗ.appendStep hnode) hedge).append rest := by
-  induction trₗ <;> simp [Traceₗ.append, Traceₗ.appendStep, Traceₗ.appendTrace, Trace.addEdge, *]
-
-@[simp] lemma Traceₗ.appendTrace_addEdge {g : Graph}
-    {idx₁ idx₂ idx₃ idx₄ : g.Index} {ρ₁ ρ₂ ρ₃ ρ₄ : Env}
-    (trₗ : Traceₗ g idx₁ idx₂ ρ₁ ρ₂)
-    (hnode : EvalBasicStmtOpt ρ₂ (g.nodes idx₂) ρ₃)
-    (hedge : (idx₂, idx₃) ∈ g.edges)
-    (rest : Trace g idx₃ idx₄ ρ₃ ρ₄) :
-    trₗ.appendTrace (Trace.edge hnode hedge rest) =
-      (Trace.addEdge (trₗ.appendStep hnode) hedge).appendTrace rest := by
-  induction trₗ <;> simp [Traceₗ.appendTrace, Traceₗ.appendStep, Trace.addEdge, *]
-
-/-- A beginning-to-end trace corresponding to the CFG `g`. -/
-inductive EndToEndTrace (g : Graph) (ρ₁ ρ₂ : Env) : Type
   | intro (idx₁ : g.Index) (idx₁_mem : idx₁ ∈ g.inputs)
       (idx₂ : g.Index) (idx₂_mem : idx₂ ∈ g.outputs)
       (trace : Trace g idx₁ idx₂ ρ₁ ρ₂) : EndToEndTrace g ρ₁ ρ₂
 
-inductive Reaches {prog : Program} : {s₁ s₂ : prog.State} → {ρ₁ ρ₂ : Env} →
-    Trace prog.cfg s₁ s₂ ρ₁ ρ₂ →
-    (s : prog.State) → (ρin ρout : Env) → Type
-  | single_here {s₁ : prog.State} {ρ₁ ρ₂ : Env}
-      (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂) :
-      Reaches (.single hnode) s₁ ρ₁ ρ₂
-  | edge_here {s₁ s₂ s₃ : prog.State} {ρ₁ ρ₂ ρ₃ : Env}
-      (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂)
-      (hedge : (s₁, s₂) ∈ prog.cfg.edges) (rest : Trace prog.cfg s₂ s₃ ρ₂ ρ₃) :
-      Reaches (.edge hnode hedge rest) s₁ ρ₁ ρ₂
-  | edge_there {s₁ s₂ s₃ : prog.State} {ρ₁ ρ₂ ρ₃ : Env}
-      (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂)
-      (hedge : (s₁, s₂) ∈ prog.cfg.edges) (rest : Trace prog.cfg s₂ s₃ ρ₂ ρ₃)
-      {s : prog.State} {ρin ρout : Env} :
-      Reaches rest s ρin ρout →
-      Reaches (.edge hnode hedge rest) s ρin ρout
-
-def Reaches.pre {prog : Program} {s₁ s₂ s: prog.State}
-    {ρ₁ ρ₂ ρin ρout : Env} {tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂} :
-    (r : Reaches tr s ρin ρout) → Traceₗ prog.cfg s₁ s ρ₁ ρin
-  | .single_here _ => .nil
-  | .edge_here _ _ _ => .nil
-  | .edge_there hnode hedge _ r => .cons hnode hedge r.pre
-
-def Reaches.post {prog : Program} {s₁ s₂ s: prog.State}
-    {ρ₁ ρ₂ ρin ρout : Env} {tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂} :
-    (r : Reaches tr s ρin ρout) → Trace prog.cfg s₁ s ρ₁ ρout
-  | .single_here hnode => .single hnode
-  | .edge_here hnode _ _ => .single hnode
-  | .edge_there hnode hedge _ r => .edge hnode hedge r.post
-
-def Reaches.first {prog : Program} {s₁ s₂ s: prog.State}
-    {ρ₁ ρ₂ ρin ρout : Env} {tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂} :
-    (r : Reaches tr s ρin ρout) → Σ ρ₁', Reaches tr s₁ ρ₁ ρ₁'
-  | .single_here hnode => ⟨_, .single_here hnode⟩
-  | .edge_here hnode hedge hrest => ⟨_, .edge_here hnode hedge hrest⟩
-  | .edge_there hnode hedge hrest tmp' => ⟨_, .edge_here hnode hedge hrest⟩
-
-def Reaches.step {prog : Program} {s₁ s₂ s: prog.State}
-    {ρ₁ ρ₂ ρin ρout : Env} {tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂} :
-    (r : Reaches tr s ρin ρout) → EvalBasicStmtOpt ρin (prog.code s) ρout
-  | .single_here hnode => hnode
-  | .edge_here hnode hedge hrest => hnode
-  | .edge_there hnode hedge hrest tmp' => tmp'.step
-
-
 end Spa

lean/Spa/Lattice.lean

@@ -1,32 +1,8 @@
 import Mathlib.Order.Lattice
 import Mathlib.Order.RelSeries
 
-/-!
-
-# Lattice Definitions
-
-This file provides some definitions for lattices. It used to be more critical
-when this was an Agda project, since it defined (semi)lattices, the ordering
-relation, etc. However, these have been lifted into `Mathlib.Order.Lattice`
-etc.. What remains are a couple of theorems about folds, as well
-as `FiniteHeightLattice`, the core concept of lattice-based static
-program analyses. See the documentation on that class for more information. -/
-
-namespace Option
-
-/-- Equality-sensitive eliminator for options in which the `some` case
-    is sensitive to the base `β`. This makes it mirror a one-element fold
-    more closely. -/
-def elimEq {α : Type*} {β : Sort*} :
-    (o : Option α) → β → ((a : α) → o = some a → β → β) → β
-  | none, b, _ => b
-  | some a, b, f => f a rfl b
-
-end Option
-
 namespace Spa
 
-/-- Predicate for binary functions independently monotone in both their arguments. -/
 def Monotone₂ {α β γ : Type*} [Preorder α] [Preorder β] [Preorder γ]
     (f : α → β → γ) : Prop :=
   (∀ b, Monotone (f · b)) ∧ (∀ a, Monotone (f a ·))
@@ -35,20 +11,18 @@ section Folds
 
 variable {α β : Type*} [Preorder α] [Preorder β]
 
-/-- (right) folds are monotonic in both their arguments if the underlying accumulator function is. -/
+theorem foldr_mono {l₁ l₂ : List α} (f : α → β → β) {b₁ b₂ : β}
-lemma foldr_mono {l₁ l₂ : List α} (f : α → β → β) {b₁ b₂ : β}
     (hl : List.Forall₂ (· ≤ ·) l₁ l₂) (hb : b₁ ≤ b₂)
-    (hf₁ : ∀ b, Monotone (f · b)) (hf₂ : ∀ a, Monotone (f a ·)) :
+    (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)
 
-/-- (left) folds are monotinic in both their arguments if the underlying accumulator function is. -/
+theorem foldl_mono {l₁ l₂ : List α} (f : β → α → β) {b₁ b₂ : β}
-lemma foldl_mono {l₁ l₂ : List α} (f : β → α → β) {b₁ b₂ : β}
     (hl : List.Forall₂ (· ≤ ·) l₁ l₂) (hb : b₁ ≤ b₂)
-    (hf₁ : ∀ a, Monotone (f · a)) (hf₂ : ∀ b, Monotone (f 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
@@ -56,96 +30,61 @@ lemma foldl_mono {l₁ l₂ : List α} (f : β → α → β) {b₁ b₂ : β}
     exact ih (le_trans (hf₁ _ hb) (hf₂ _ hxy))
 
 omit [Preorder α] in
-/-- (right) folds on a particular list are monotonic if the underlying accumulator is monotonic in its accumulator argument. -/
+theorem foldr_mono' (l : List α) (f : α → β → β)
-lemma foldr_mono' (l : List α) (f : α → β → β)
+    (hf : ∀ a, Monotone (f a ·)) : Monotone fun b => l.foldr f b := by
-    (hf : ∀ a, Monotone (f a ·)) : Monotone (l.foldr f ·) := by
   intro b₁ b₂ hb
   induction l with
   | nil => exact hb
   | cons x xs ih => exact hf x ih
 
 omit [Preorder α] in
-/-- (left) folds on a particular list are monotonic if the underlying accumulator is monotonic in its accumulator argument. -/
+theorem foldl_mono' (l : List α) (f : β → α → β)
-lemma foldl_mono' (l : List α) (f : β → α → β)
     (hf : ∀ a, Monotone (f · 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)
 
-omit [Preorder α] in
-/-- The equality-aware eliminator (that also alters its behavior dependent on base case)
-    for option is monotonic. -/
-lemma elimEq_self_mono (o : Option α) (g : (a : α) → o = some a → β → β)
-    (hg : ∀ a h, Monotone (g a h)) :
-    Monotone (o.elimEq · g) := by
-  cases o with
-  | none => exact monotone_id
-  | some a => exact hg a rfl
-
 end Folds
 
-/-- Predicate on types with `Preorder` that claims all $<$ chains in the type have at most `n` comparisons. -/
 def BoundedChains (α : Type*) [Preorder α] (n : ℕ) : Prop :=
   ∀ c : LTSeries α, c.length ≤ n
 
-/-- Since a singleton type's preorder has no nonempty `<` chains,
+structure PointedLTSeries (α : Type*) (f t : α)(n : ℕ) [Preorder α] where
-    they are vacuously bounded by any minimum height. -/
+  series : LTSeries α
-lemma boundedChains_of_subsingleton (α : Type*) [Preorder α] [Subsingleton α]
+  head_series : series.head = f
-    (n : ℕ) : BoundedChains α n := fun c => by
+  last_series : series.last = t
-  by_contra hc
+  length_series : series.length = n
-  push_neg at hc
-  exact (c.step ⟨0, by omega⟩).ne (Subsingleton.elim _ _)
 
-/-- A finite height lattice is a lattice in which all chains $a < \ldots < z$ have a maximum height `height`. -/
+class FiniteHeightLattice (α : Type*) [Lattice α] extends Bot α, Top α where
-class FiniteHeightLattice (α : Type*) extends Lattice α, OrderBot α, OrderTop α where
   height : ℕ
+  longestChain : PointedLTSeries α ⊥ ⊤ height
   chains_bounded : BoundedChains α height
 
--- a < ... < z
+namespace FixedHeight
--- ----------- length <= height
+
+variable {α : Type*} [Lattice α] {h : ℕ}
+
+theorem bot_le [FiniteHeightLattice α] : ∀ (a : α), ⊥ ≤ a := by
+  intro a
+  by_cases heq : ⊥ ⊓ a = ⊥
+  · exact inf_eq_left.mp heq
+  · exfalso
+    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
+    have hbound := FiniteHeightLattice.chains_bounded (lc.series.cons (⊥ ⊓ a) hlt)
+    rw [RelSeries.cons_length, lc.length_series] at hbound
+    omega
+
+end FixedHeight
 
 namespace FiniteHeightLattice
 
-/-- This is something like a lemma about isomorphic types having the same height.
+variable (α : Type*) [Lattice α] [FiniteHeightLattice α]
-    Given a finite-height lattice `α`, lattice `β`, and a `Monotone` bijection
-    between the two, we can show that lattice `β` also has a finite height.
 
-    The proof is fairly trivial: any chain in `β` can be transported to a chain in `α`,
+theorem bot_le (a : α) : (⊥ : α) ≤ a := FixedHeight.bot_le a
-    and must be bounded by the same height by `FiniteHeightLattice.chains_bounded`. -/
-def transport {α β : Type*} [Lattice β]
-    [I : FiniteHeightLattice α] (f : α → β) (g : β → α)
-    (hf : Monotone f) (hg : Monotone g)
-    (hfg : Function.LeftInverse f g) :
-    FiniteHeightLattice β where
-  toLattice := inferInstance
-  toOrderBot := {
-    bot := f (⊥ : α)
-    bot_le := fun b => by
-      rw [← hfg b]
-      exact hf (_root_.bot_le : (⊥ : α) ≤ g b) }
-  toOrderTop := {
-    top := f (⊤ : α)
-    le_top := fun b => by
-      rw [← hfg b]
-      exact hf (_root_.le_top : g b ≤ (⊤ : α)) }
-  height := I.height
-  chains_bounded := fun c =>
-    I.chains_bounded (c.map g (hg.strictMono_of_injective hfg.injective))
-
-/-- A `Unique` lattice trivially has finite height: its only chain is the singleton
-    `[default]`, and there are no nontrivial `<` chains in a subsingleton. -/
-def ofUnique (α : Type*) [Lattice α] [Unique α] :
-    FiniteHeightLattice α where
-  toLattice := inferInstance
-  toOrderBot := {
-    bot := default
-    bot_le := fun _ => le_of_eq (Subsingleton.elim _ _) }
-  toOrderTop := {
-    top := default
-    le_top := fun _ => le_of_eq (Subsingleton.elim _ _) }
-  height := 0
-  chains_bounded := boundedChains_of_subsingleton α 0
 
 end FiniteHeightLattice
 

lean/Spa/Lattice/AboveBelow.lean

@@ -1,38 +1,7 @@
 import Spa.Lattice
 
-/-!
-
-# The Above-Below Lattice
-
-This file defines the `AboveBelow` lattice, which takes a flat domain
-$a_1, \ldots, a_n \in \alpha$ and lifts it into a lattice bounded
-above by a synthetic $\top$ element, and below by a synthetic $\bot$
-element.
-
-$$
-\begin{array}{ccccc}
-  && \top && \\
-  & \swarrow & \downarrow & \searrow & \\
-  a_1 & & … & & a_n \\
-  & \searrow & \downarrow & \swarrow & \\
-  && \bot &&
-\end{array}
-$$
-
-This lattice is also a `Spa.FiniteHeightLattice`, because no chain can
-exceed the bottom-to-top chain $\bot < a_i < \top$.
-
-The above-below lattice is helpful for for analyses such as
-`Spa/Analysis/Sign.lean` and `Spa/Analysis/Constant.lean`, whose
-classifications of values (by sign or by exact value) do not have
-any inherent structure beyond "matching exactly".
-
--/
-
 namespace Spa
 
-/-- The above-below lattice, with bottom element `bot` and top element `top`. -/
-@[aesop safe cases]
 inductive AboveBelow (α : Type*) where
   | bot
   | top
@@ -65,125 +34,206 @@ instance : Min (AboveBelow α) where
     | mk _, bot => bot
     | mk x, top => mk x
 
-@[simp] lemma bot_sup (x : AboveBelow α) : bot ⊔ x = x := rfl
+@[simp] theorem bot_sup (x : AboveBelow α) : bot ⊔ x = x := rfl
-@[simp] lemma top_sup (x : AboveBelow α) : top ⊔ x = top := rfl
+@[simp] theorem top_sup (x : AboveBelow α) : top ⊔ x = top := rfl
-@[simp] lemma sup_bot (x : AboveBelow α) : x ⊔ bot = x := by cases x <;> rfl
+@[simp] theorem sup_bot (x : AboveBelow α) : x ⊔ bot = x := by cases x <;> rfl
-@[simp] lemma sup_top (x : AboveBelow α) : x ⊔ top = top := by cases x <;> rfl
+@[simp] theorem sup_top (x : AboveBelow α) : x ⊔ top = top := by cases x <;> rfl
-@[simp] lemma mk_sup_mk (x y : α) :
+@[simp] theorem mk_sup_mk (x y : α) :
     (mk x ⊔ mk y : AboveBelow α) = if x = y then mk x else top := rfl
 
-@[simp] lemma bot_inf (x : AboveBelow α) : bot ⊓ x = bot := rfl
+@[simp] theorem bot_inf (x : AboveBelow α) : bot ⊓ x = bot := rfl
-@[simp] lemma top_inf (x : AboveBelow α) : top ⊓ x = x := rfl
+@[simp] theorem top_inf (x : AboveBelow α) : top ⊓ x = x := rfl
-@[simp] lemma inf_bot (x : AboveBelow α) : x ⊓ bot = bot := by cases x <;> rfl
+@[simp] theorem inf_bot (x : AboveBelow α) : x ⊓ bot = bot := by cases x <;> rfl
-@[simp] lemma inf_top (x : AboveBelow α) : x ⊓ top = x := by cases x <;> rfl
+@[simp] theorem inf_top (x : AboveBelow α) : x ⊓ top = x := by cases x <;> rfl
-@[simp] lemma mk_inf_mk (x y : α) :
+@[simp] theorem mk_inf_mk (x y : α) :
     (mk x ⊓ mk y : AboveBelow α) = if x = y then mk x else bot := rfl
 
-protected lemma sup_comm (a b : AboveBelow α) : a ⊔ b = b ⊔ a := by aesop
+protected theorem sup_comm (a b : AboveBelow α) : a ⊔ b = b ⊔ a := by
-protected lemma sup_assoc (a b c : AboveBelow α) : a ⊔ b ⊔ c = a ⊔ (b ⊔ c) := by aesop
+  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> simp only
-protected lemma inf_comm (a b : AboveBelow α) : a ⊓ b = b ⊓ a := by aesop
+    [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk]
-protected lemma inf_assoc (a b c : AboveBelow α) : a ⊓ b ⊓ c = a ⊓ (b ⊓ c) := by aesop
+  split_ifs with h₁ h₂ h₂ <;> simp_all
-protected lemma sup_inf_self (a b : AboveBelow α) : a ⊔ a ⊓ b = a := by aesop
+
-protected lemma inf_sup_self (a b : AboveBelow α) : a ⊓ (a ⊔ b) = a := by aesop
+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
+
+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
+
+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
+
+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)
+
+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)
 
 instance : Lattice (AboveBelow α) :=
   Lattice.mk' AboveBelow.sup_comm AboveBelow.sup_assoc
     AboveBelow.inf_comm AboveBelow.inf_assoc
     AboveBelow.sup_inf_self AboveBelow.inf_sup_self
 
-lemma le_iff {a b : AboveBelow α} : a ≤ b ↔ a ⊔ b = b := sup_eq_right.symm
+theorem le_iff {a b : AboveBelow α} : a ≤ b ↔ a ⊔ b = b := sup_eq_right.symm
 
-lemma bot_le' (a : AboveBelow α) : (bot : AboveBelow α) ≤ a :=
+theorem bot_le' (a : AboveBelow α) : (bot : AboveBelow α) ≤ a :=
   le_iff.mpr (bot_sup a)
 
-lemma le_top' (a : AboveBelow α) : a ≤ (top : AboveBelow α) :=
+theorem le_top' (a : AboveBelow α) : a ≤ (top : AboveBelow α) :=
   le_iff.mpr (sup_top a)
 
-instance : OrderBot (AboveBelow α) where
+theorem bot_lt_mk (x : α) : (bot : AboveBelow α) < mk x :=
-  bot := bot
+  lt_of_le_of_ne (bot_le' _) (by simp)
-  bot_le := bot_le'
 
-instance : OrderTop (AboveBelow α) where
+theorem mk_lt_top (x : α) : (mk x : AboveBelow α) < top :=
-  top := top
+  lt_of_le_of_ne (le_top' _) (by simp)
-  le_top := le_top'
 
-lemma bot_lt_mk (x : α) : (bot : AboveBelow α) < mk x := lt_of_le_of_ne (bot_le' _) (by simp)
+theorem bot_lt_top : (bot : AboveBelow α) < top :=
-lemma mk_lt_top (x : α) : (mk x : AboveBelow α) < top := lt_of_le_of_ne (le_top' _) (by simp)
+  lt_of_le_of_ne (bot_le' _) (by simp)
-lemma bot_lt_top : (bot : AboveBelow α) < top := lt_of_le_of_ne (bot_le' _) (by simp)
 
-lemma le_cases {a b : AboveBelow α} (h : a ≤ b) :
+theorem le_cases {a b : AboveBelow α} (h : a ≤ b) :
     a = bot ∨ b = top ∨ a = b := by
-  rw [le_iff] at h
+  have hsup := le_iff.mp h
-  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> simp_all
+  rcases a with _ | _ | x <;> rcases b with _ | _ | y
+  · exact Or.inl rfl
+  · exact Or.inr (Or.inl rfl)
+  · exact Or.inl rfl
+  · exact absurd hsup (by simp)
+  · exact Or.inr (Or.inl rfl)
+  · exact absurd hsup (by simp)
+  · exact absurd hsup (by simp)
+  · exact Or.inr (Or.inl rfl)
+  · rw [mk_sup_mk] at hsup
+    by_cases hxy : x = y
+    · exact Or.inr (Or.inr (by rw [hxy]))
+    · rw [if_neg hxy] at hsup
+      exact absurd hsup (by simp)
 
-/-- If `f` sends `⊥` to `⊥` (in both arguments) and `⊤` to `⊤`
+/-- Monotonicity for *strict* operations on flat lattices: if `f` sends `⊥` to
-    (against any non-`⊥` argument), it is monotone in both arguments.
+`⊥` (in either argument) and `⊤` to `⊤` (against any non-`⊥` argument), it is
-    The values of the the elements in `α` are irrelevant since they
+monotone in both arguments — regardless of its values on plain elements.
-    are always incomparable. This makes it easy to prove monotonicity
+`Analysis/Sign.agda` and `Analysis/Constant.agda` postulated exactly these
-    for operations that "just" combine their flat elements, or give up. -/
+monotonicity facts for their `plus`/`minus`, all of which have this shape. -/
-lemma monotone₂_of_strict {β γ : Type*} [DecidableEq β] [DecidableEq γ]
+theorem monotone₂_of_strict {β γ : Type*} [DecidableEq β] [DecidableEq γ]
     (f : AboveBelow α → AboveBelow β → AboveBelow γ)
     (hbotl : ∀ y, f bot y = bot) (hbotr : ∀ x, f x bot = bot)
     (htopl : ∀ y, y ≠ bot → f top y = top)
     (htopr : ∀ x, x ≠ bot → f x top = top) : Monotone₂ f := by
-  constructor <;> intro c a b hab <;>
+  constructor
-    rcases eq_or_ne c bot with rfl | hc <;>
+  · intro y a b hab
-    rcases le_cases hab with rfl | rfl | rfl <;>
+    show f a y ≤ f b y
-    simp [hbotl, hbotr, htopl, htopr, bot_le', le_top', *]
+    rcases le_cases hab with rfl | rfl | rfl
+    · rw [hbotl]; exact bot_le' _
+    · rcases eq_or_ne y bot with rfl | hy
+      · rw [hbotr, hbotr]
+      · rw [htopl y hy]; exact le_top' _
+    · exact le_rfl
+  · intro x a b hab
+    show f x a ≤ f x b
+    rcases le_cases hab with rfl | rfl | rfl
+    · rw [hbotr]; exact bot_le' _
+    · rcases eq_or_ne x bot with rfl | hx
+      · rw [hbotl, hbotl]
+      · rw [htopr x hx]; exact le_top' _
+    · exact le_rfl
+
+/-! ### Interpretations of flat lattices -/
 
 section Interp
 
 variable {V : Type*} {P : AboveBelow α → V → Prop}
 
-/-- As long as the interpretation of a the above-below lattice respects the
+theorem interp_sup_of (hbot : ∀ v, ¬P bot v) (htop : ∀ v, P top v)
-    fact that `bot` means "impossible", interpreting the above-below
+    {s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∨ P s₂ v) : P (s₁ ⊔ s₂) v := by
-    lattice agrees with its `⊔`. -/
+  rcases s₁ with _ | _ | x
-lemma interp_sup_of (hbot : ∀ v, ¬P bot v) (htop : ∀ v, P top v)
+  · rw [bot_sup]; exact h.resolve_left (hbot v)
-    {s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∨ P s₂ v) : P (s₁ ⊔ s₂) v := by aesop
+  · rw [top_sup]; exact htop v
+  · rcases s₂ with _ | _ | y
+    · rw [sup_bot]; exact h.resolve_right (hbot v)
+    · rw [sup_top]; exact htop v
+    · rw [mk_sup_mk]
+      split
+      · next heq => subst heq; exact h.elim id id
+      · exact htop v
 
-/-- As long as two distinct values in the flat domain don't overlap,
+theorem interp_inf_of
-    interpreting the above-below lattice agrees with its `⊔` -/
-lemma 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
-  rcases s₁ with _ | _ | x <;> rcases s₂ with _ | _ | y <;> simp_all
+  rcases s₁ with _ | _ | x
-  split
+  · rw [bot_inf]; exact h.1
-  · exact h.2
+  · rw [top_inf]; exact h.2
-  · next hne => exact (hdisj hne v h.1 h.2).elim
+  · rcases s₂ with _ | _ | y
+    · rw [inf_bot]; exact h.2
+    · rw [inf_top]; exact h.1
+    · rw [mk_inf_mk]
+      split
+      · next heq => subst heq; exact h.1
+      · next hne => exact absurd h (hdisj hne v)
 
 end Interp
 
-/-- synthetic rank of an element, used to prove chain bounds. -/
+/-- Rank of an element: `⊥ ↦ 0`, `[x] ↦ 1`, `⊤ ↦ 2`. Used to bound chains
-private def rank : AboveBelow α → ℕ
+(Agda's `isLongest` / `x≺[y]⇒x≡⊥` / `[x]≺y⇒y≡⊤` case analysis lives here). -/
+def rank : AboveBelow α → ℕ
   | bot => 0
   | mk _ => 1
   | top => 2
 
-/-- It's not possible for any two lifted flat-domain elements to be less
+/-- Agda: the impossibility of `[x] ≺ [y]` (combines `x≺[y]⇒x≡⊥` and
-    than one another. -/
+`[x]≺y⇒y≡⊤`: the flat middle layer is an antichain). -/
-lemma not_mk_lt_mk (x y : α) : ¬(mk x : AboveBelow α) < mk y := by
+theorem not_mk_lt_mk (x y : α) : ¬(mk x : AboveBelow α) < mk y := by
   intro h
   obtain ⟨hle, hne⟩ := lt_iff_le_and_ne.mp h
-  rcases le_cases hle with h | h | h <;> simp_all
+  have hsup := le_iff.mp hle
+  rw [mk_sup_mk] at hsup
+  by_cases hxy : x = y
+  · rw [if_pos hxy] at hsup
+    exact hne hsup
+  · rw [if_neg hxy] at hsup
+    exact absurd hsup (by simp)
 
-/-- The rank of elements is strictly monotonic. -/
+theorem rank_strictMono : StrictMono (rank : AboveBelow α → ℕ) := by
-lemma rank_strictMono : StrictMono (rank : AboveBelow α → ℕ) := by
   intro a b hab
-  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;>
+  rcases a with _ | _ | x <;> rcases b with _ | _ | y
-    simp_all [rank, not_mk_lt_mk, (bot_le' _).not_lt, (le_top' _).not_lt]
+  · exact absurd hab (lt_irrefl _)
+  · simp [rank]
+  · simp [rank]
+  · exact absurd hab (bot_le' _).not_lt
+  · exact absurd hab (lt_irrefl _)
+  · exact absurd hab (le_top' _).not_lt
+  · exact absurd hab (bot_le' _).not_lt
+  · simp [rank]
+  · exact absurd hab (not_mk_lt_mk x y)
 
-/-- All chains in the above-below lattice have at most 2 comparisons. -/
+theorem boundedChains : BoundedChains (AboveBelow α) 2 := fun c => by
-lemma 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
 
 instance [Inhabited α] : FiniteHeightLattice (AboveBelow α) where
-  toLattice := inferInstance
+  bot := bot
-  toOrderBot := inferInstance
+  top := top
-  toOrderTop := inferInstance
   height := 2
+  longestChain :=
+    { series :=
+        ((RelSeries.singleton _ bot).snoc (mk default)
+            (by rw [RelSeries.last_singleton]; exact bot_lt_mk default)).snoc top
+          (by rw [RelSeries.last_snoc]; exact mk_lt_top default)
+      head_series := by simp
+      last_series := by simp
+      length_series := by simp [RelSeries.snoc, RelSeries.append] }
   chains_bounded := boundedChains
 
 end AboveBelow

lean/Spa/Lattice/Bool.lean

@@ -1,39 +0,0 @@
-import Spa.Lattice
-import Mathlib.Order.BooleanAlgebra
-
-namespace Spa
-
-/-! ### `Bool` as a finite-height lattice
-
-`Bool` is the two-element lattice `false ≤ true` (with `⊥ = false`, `⊤ = true`).
-It is the building block of the "power set" lattice `FiniteMap A Bool ks`, used by
-the reaching-definitions analysis to represent sets of definition sites. -/
-
-namespace Bool
-
-/-- Rank of a boolean: `false ↦ 0`, `true ↦ 1`. Used to bound chains, mirroring
-`AboveBelow.rank`. -/
-def rank : Bool → ℕ
-  | false => 0
-  | true => 1
-
-lemma rank_strictMono : StrictMono rank := by
-  intro a b hab
-  cases a <;> cases b <;> revert hab <;> decide
-
-lemma boundedChains : BoundedChains Bool 1 := 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 ≤ 1 := by cases c.last <;> simp [rank]
-  omega
-
-instance : FiniteHeightLattice Bool where
-  toLattice := inferInstance
-  toOrderBot := inferInstance
-  toOrderTop := inferInstance
-  height := 1
-  chains_bounded := boundedChains
-
-end Bool
-
-end Spa

lean/Spa/Lattice/FiniteMap.lean

@@ -1,207 +1,425 @@
-import Spa.Lattice.Tuple
+import Spa.Lattice.IterProd
-import Mathlib.Data.List.Nodup
+import Spa.Isomorphism
-
-/-!
-
-# Finite Maps
-
-This file defines _finite maps_, or key-value maps with a finite domain. This
-is encoded as a map from `Fin` into the value type. Finite maps form a
-lattice from pointwise composition: $(f \land g) k = f k \land g k$,
-and, provided the domain `\beta` is of finite height, so is the map
-lattice as a whole.
-
-In fact, the isomorphism is described and proven in `Spa/Lattice/Tuple.lean`.
-
--/
 
 namespace Spa
 
-/-- Key-value map with domain `α` and codomain `β`, with possible keys $\textit{ks} \subseteq \alpha$. -/
+def FiniteMap (A B : Type*) (ks : List A) : Type _ :=
-def FiniteMap (α β : Type*) (ks : List α) : Type _ := Fin ks.length → β
+  { l : List (A × B) // l.map Prod.fst = ks }
 
 namespace FiniteMap
 
-variable {α β : Type*} {ks : List α}
+variable {A B : Type*} {ks : List A}
 
-instance [Lattice β] : Lattice (FiniteMap α β ks) :=
+instance [DecidableEq A] [DecidableEq B] : DecidableEq (FiniteMap A B ks) :=
-  inferInstanceAs (Lattice (Fin ks.length → β))
+  fun a b => decidable_of_iff (a.val = b.val) Subtype.ext_iff.symm
 
-instance [FiniteHeightLattice β] : FiniteHeightLattice (FiniteMap α β ks) :=
+theorem spine_eq (fm₁ fm₂ : FiniteMap A B ks) :
-  inferInstanceAs (FiniteHeightLattice (Fin ks.length → β))
+    fm₁.val.map Prod.fst = fm₂.val.map Prod.fst :=
+  fm₁.property.trans fm₂.property.symm
 
-instance [DecidableEq β] : DecidableEq (FiniteMap α β ks) :=
+def combine (f : B → B → B) (l₁ l₂ : List (A × B)) : List (A × B) :=
-  inferInstanceAs (DecidableEq (Fin ks.length → β))
+  List.zipWith (fun p q => (p.1, f p.2 q.2)) l₁ l₂
 
-instance : Membership (α × β) (FiniteMap α β ks) :=
+theorem combine_spine (f : B → B → B) : ∀ {l₁ l₂ : List (A × B)},
-  ⟨fun fm p => ∃ i : Fin ks.length, ks.get i = p.1 ∧ fm i = p.2⟩
+    l₁.map Prod.fst = l₂.map Prod.fst →
+    (combine f l₁ l₂).map Prod.fst = l₁.map Prod.fst
+  | [], [], _ => rfl
+  | p :: l₁, q :: l₂, h => by
+    simp only [List.map_cons, List.cons.injEq] at h
+    simp only [combine, List.zipWith_cons_cons, List.map_cons]
+    exact congrArg _ (combine_spine f h.2)
+  | [], _ :: _, h => by simp at h
+  | _ :: _, [], h => by simp at h
 
-lemma mem_iff {fm : FiniteMap α β ks} {p : α × β} :
+theorem combine_comm (f : B → B → B) (hf : ∀ a b, f a b = f b a) :
-    p ∈ fm ↔ ∃ i : Fin ks.length, ks.get i = p.1 ∧ fm i = p.2 := Iff.rfl
+    ∀ {l₁ l₂ : List (A × B)}, l₁.map Prod.fst = l₂.map Prod.fst →
+      combine f l₁ l₂ = combine f l₂ l₁
+  | [], [], _ => rfl
+  | p :: l₁, q :: l₂, h => by
+    simp only [List.map_cons, List.cons.injEq] at h
+    simp only [combine, List.zipWith_cons_cons]
+    rw [h.1, hf]
+    exact congrArg _ (combine_comm f hf h.2)
+  | [], _ :: _, h => by simp at h
+  | _ :: _, [], h => by simp at h
 
-def MemKey (k : α) (_fm : FiniteMap α β ks) : Prop := k ∈ ks
+theorem combine_assoc (f : B → B → B) (hf : ∀ a b c, f (f a b) c = f a (f b c)) :
+    ∀ {l₁ l₂ l₃ : List (A × B)},
+      l₁.map Prod.fst = l₂.map Prod.fst → l₂.map Prod.fst = l₃.map Prod.fst →
+      combine f (combine f l₁ l₂) l₃ = combine f l₁ (combine f l₂ l₃)
+  | [], [], [], _, _ => rfl
+  | p :: l₁, q :: l₂, r :: l₃, h₁₂, h₂₃ => by
+    simp only [List.map_cons, List.cons.injEq] at h₁₂ h₂₃
+    simp only [combine, List.zipWith_cons_cons]
+    rw [hf]
+    exact congrArg _ (combine_assoc f hf h₁₂.2 h₂₃.2)
+  | [], [], _ :: _, _, h => by simp at h
+  | [], _ :: _, _, h, _ => by simp at h
+  | _ :: _, [], _, h, _ => by simp at h
+  | _ :: _, _ :: _, [], _, h => by simp at h
 
-lemma MemKey_iff {k : α} {fm : FiniteMap α β ks} : MemKey k fm ↔ k ∈ ks := Iff.rfl
+theorem combine_absorb (f g : B → B → B) (hfg : ∀ a b, f a (g a b) = a) :
+    ∀ {l₁ l₂ : List (A × B)}, l₁.map Prod.fst = l₂.map Prod.fst →
+      combine f l₁ (combine g l₁ l₂) = l₁
+  | [], [], _ => rfl
+  | p :: l₁, q :: l₂, h => by
+    simp only [List.map_cons, List.cons.injEq] at h
+    simp only [combine, List.zipWith_cons_cons, hfg]
+    exact congrArg _ (combine_absorb f g hfg h.2)
+  | [], _ :: _, h => by simp at h
+  | _ :: _, [], h => by simp at h
 
-instance {k : α} {fm : FiniteMap α β ks} [DecidableEq α] : Decidable (MemKey k fm) :=
+variable [Lattice B]
-  decidable_of_iff _ MemKey_iff.symm
 
-lemma mem_key_of_mem {k : α} {v : β} {fm : FiniteMap α β ks}
+instance : Max (FiniteMap A B ks) where
-    (h : (k, v) ∈ fm) : MemKey k fm := by
+  max fm₁ fm₂ :=
-  obtain ⟨i, hi, _⟩ := h
+    ⟨combine (· ⊔ ·) fm₁.val fm₂.val,
-  have hik : ks.get i = k := hi
+     (combine_spine _ (spine_eq fm₁ fm₂)).trans fm₁.property⟩
-  exact hik ▸ ks.get_mem i
 
-def toList (fm : FiniteMap α β ks) : List (α × β) :=
+instance : Min (FiniteMap A B ks) where
-  (List.finRange ks.length).map fun i => (ks.get i, fm i)
+  min fm₁ fm₂ :=
+    ⟨combine (· ⊓ ·) fm₁.val fm₂.val,
+     (combine_spine _ (spine_eq fm₁ fm₂)).trans fm₁.property⟩
 
-lemma le_def [Lattice β] {fm₁ fm₂ : FiniteMap α β ks} :
+@[simp] theorem sup_val (fm₁ fm₂ : FiniteMap A B ks) :
-    fm₁ ≤ fm₂ ↔ ∀ i, fm₁ i ≤ fm₂ i := Iff.rfl
+    (fm₁ ⊔ fm₂).val = combine (· ⊔ ·) fm₁.val fm₂.val := rfl
+
+@[simp] theorem inf_val (fm₁ fm₂ : FiniteMap A B ks) :
+    (fm₁ ⊓ fm₂).val = combine (· ⊓ ·) fm₁.val fm₂.val := rfl
+
+instance : Lattice (FiniteMap A B ks) :=
+  Lattice.mk'
+    (fun a b => Subtype.ext (combine_comm _ sup_comm (spine_eq a b)))
+    (fun a b c => Subtype.ext (combine_assoc _ sup_assoc (spine_eq a b) (spine_eq b c)))
+    (fun a b => Subtype.ext (combine_comm _ inf_comm (spine_eq a b)))
+    (fun a b c => Subtype.ext (combine_assoc _ inf_assoc (spine_eq a b) (spine_eq b c)))
+    (fun a b => Subtype.ext (combine_absorb _ _ (fun _ _ => sup_inf_self) (spine_eq a b)))
+    (fun a b => Subtype.ext (combine_absorb _ _ (fun _ _ => inf_sup_self) (spine_eq a b)))
+
+instance : Membership (A × B) (FiniteMap A B ks) :=
+  ⟨fun fm p => p ∈ fm.val⟩
+
+omit [Lattice B] in
+theorem mem_def {p : A × B} {fm : FiniteMap A B ks} : p ∈ fm ↔ p ∈ fm.val :=
+  Iff.rfl
+
+def MemKey (k : A) (fm : FiniteMap A B ks) : Prop :=
+  k ∈ fm.val.map Prod.fst
+
+omit [Lattice B] in
+theorem memKey_iff {k : A} {fm : FiniteMap A B ks} : MemKey k fm ↔ k ∈ ks := by
+  rw [MemKey, fm.property]
+
+instance {k : A} {fm : FiniteMap A B ks} [DecidableEq A] :
+    Decidable (MemKey k fm) :=
+  decidable_of_iff _ memKey_iff.symm
+
+omit [Lattice B] in
+theorem mem_key_of_mem {k : A} {v : B} {fm : FiniteMap A B ks}
+    (h : (k, v) ∈ fm) : MemKey k fm :=
+  List.mem_map_of_mem _ h
 
 section Locate
 
-variable [DecidableEq α]
+variable [DecidableEq A]
 
-/-- Recover the value stored under a present key. -/
+private def locateList (k : A) :
-def locate {k : α} {fm : FiniteMap α β ks} (h : MemKey k fm) :
+    (l : List (A × B)) → k ∈ l.map Prod.fst → {v : B // (k, v) ∈ l}
-    {v : β // (k, v) ∈ fm} :=
+  | [], h => absurd h (by simp)
-  let i : Fin ks.length := ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩
+  | p :: l', h =>
-  ⟨fm i, i, List.idxOf_get _, rfl⟩
+    if heq : p.1 = k then
+      ⟨p.2, by rw [← heq]; exact List.mem_cons_self ..⟩
+    else
+      let ⟨v, hv⟩ := locateList k l' (by
+        rcases List.mem_cons.mp h with h' | h'
+        · exact absurd h'.symm heq
+        · exact h')
+      ⟨v, List.mem_cons_of_mem _ hv⟩
+
+def locate {k : A} {fm : FiniteMap A B ks} (h : MemKey k fm) :
+    {v : B // (k, v) ∈ fm} :=
+  locateList k fm.val h
 
 end Locate
 
-variable [Lattice β]
+theorem combine_eq_right_iff : ∀ {l₁ l₂ : List (A × B)},
+    l₁.map Prod.fst = l₂.map Prod.fst →
+    (combine (· ⊔ ·) l₁ l₂ = l₂ ↔
+      List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂)
+  | [], [], _ => by simp [combine]
+  | p :: l₁, q :: l₂, h => by
+    simp only [List.map_cons, List.cons.injEq] at h
+    simp only [combine, List.zipWith_cons_cons, List.cons.injEq,
+               List.forall₂_cons, Prod.ext_iff]
+    rw [show List.zipWith (fun p q : A × B => (p.1, p.2 ⊔ q.2)) l₁ l₂
+          = combine (· ⊔ ·) l₁ l₂ from rfl,
+        combine_eq_right_iff h.2]
+    constructor
+    · rintro ⟨⟨hk, hv⟩, hrest⟩
+      exact ⟨⟨hk, sup_eq_right.mp hv⟩, hrest⟩
+    · rintro ⟨⟨hk, hv⟩, hrest⟩
+      exact ⟨⟨hk, sup_eq_right.mpr hv⟩, hrest⟩
+  | [], _ :: _, h => by simp at h
+  | _ :: _, [], h => by simp at h
 
-lemma le_of_mem_mem (hks : ks.Nodup) {fm₁ fm₂ : FiniteMap α β ks}
+theorem le_iff {fm₁ fm₂ : FiniteMap A B ks} :
-    (hle : fm₁ ≤ fm₂) {k : α} {v₁ v₂ : β}
+    fm₁ ≤ fm₂ ↔
-    (h₁ : (k, v₁) ∈ fm₁) (h₂ : (k, v₂) ∈ fm₂) : v₁ ≤ v₂ := by
+      List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) fm₁.val fm₂.val := by
-  obtain ⟨i, hi, rfl⟩ := h₁
+  rw [← sup_eq_right, ← combine_eq_right_iff (spine_eq fm₁ fm₂), Subtype.ext_iff,
-  obtain ⟨j, hj, rfl⟩ := h₂
+      sup_val]
-  have hij : i = j := hks.get_inj_iff.mp (hi.trans hj.symm)
-  subst hij
-  exact le_def.mp hle i
 
-lemma mem_sup {fm₁ fm₂ : FiniteMap α β ks} {k : α} {v : β}
+private theorem forall₂_spine : ∀ {l₁ l₂ : List (A × B)},
+    List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂ →
+    l₁.map Prod.fst = l₂.map Prod.fst
+  | _, _, List.Forall₂.nil => rfl
+  | _, _, List.Forall₂.cons hpq hrest => by
+    simp [List.map_cons, hpq.1, forall₂_spine hrest]
+
+private theorem forall₂_mem_mem {l₁ l₂ : List (A × B)}
+    (hf : List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂) :
+    (l₁.map Prod.fst).Nodup →
+    ∀ {k : A} {v₁ v₂ : B}, (k, v₁) ∈ l₁ → (k, v₂) ∈ l₂ → v₁ ≤ v₂ := by
+  induction hf with
+  | nil =>
+    intro _ k v₁ v₂ h₁ _
+    simp at h₁
+  | @cons p q l₁' l₂' hpq hrest ih =>
+    intro hnd k v₁ v₂ h₁ h₂
+    simp only [List.map_cons, List.nodup_cons] at hnd
+    have hspine := forall₂_spine hrest
+    rcases List.mem_cons.mp h₁ with heq₁ | h₁'
+    · rcases List.mem_cons.mp h₂ with heq₂ | h₂'
+      · rw [← heq₁, ← heq₂] at hpq
+        exact hpq.2
+      · exfalso
+        apply hnd.1
+        rw [show p.1 = k from (congrArg Prod.fst heq₁).symm, hspine]
+        exact List.mem_map_of_mem _ h₂'
+    · rcases List.mem_cons.mp h₂ with heq₂ | h₂'
+      · exfalso
+        apply hnd.1
+        rw [hpq.1, show q.1 = k from (congrArg Prod.fst heq₂).symm]
+        exact List.mem_map_of_mem _ h₁'
+      · exact ih hnd.2 h₁' h₂'
+
+theorem le_of_mem_mem (hks : ks.Nodup) {fm₁ fm₂ : FiniteMap A B ks}
+    (hle : fm₁ ≤ fm₂) {k : A} {v₁ v₂ : B}
+    (h₁ : (k, v₁) ∈ fm₁) (h₂ : (k, v₂) ∈ fm₂) : v₁ ≤ v₂ :=
+  forall₂_mem_mem (le_iff.mp hle) (fm₁.property.symm ▸ hks) h₁ h₂
+
+omit [Lattice B] in
+private theorem mem_combine (f : B → B → B) : ∀ {l₁ l₂ : List (A × B)} {k : A} {v : B},
+    l₁.map Prod.fst = l₂.map Prod.fst →
+    (k, v) ∈ combine f l₁ l₂ →
+    ∃ v₁ v₂, v = f v₁ v₂ ∧ (k, v₁) ∈ l₁ ∧ (k, v₂) ∈ l₂
+  | [], [], _, _, _, h => by simp [combine] at h
+  | p :: l₁, q :: l₂, k, v, hsp, h => by
+    simp only [List.map_cons, List.cons.injEq] at hsp
+    simp only [combine, List.zipWith_cons_cons] at h
+    rcases List.mem_cons.mp h with heq | h'
+    · injection heq with hk hv
+      exact ⟨p.2, q.2, hv,
+        by rw [hk]; simp,
+        by rw [hk, hsp.1]; simp⟩
+    · obtain ⟨v₁, v₂, hv, h₁, h₂⟩ := mem_combine f hsp.2 h'
+      exact ⟨v₁, v₂, hv, List.mem_cons_of_mem _ h₁, List.mem_cons_of_mem _ h₂⟩
+
+theorem mem_sup {fm₁ fm₂ : FiniteMap A B ks} {k : A} {v : B}
     (h : (k, v) ∈ fm₁ ⊔ fm₂) :
-    ∃ v₁ v₂, v = v₁ ⊔ v₂ ∧ (k, v₁) ∈ fm₁ ∧ (k, v₂) ∈ fm₂ := by
+    ∃ v₁ v₂, v = v₁ ⊔ v₂ ∧ (k, v₁) ∈ fm₁ ∧ (k, v₂) ∈ fm₂ :=
-  obtain ⟨i, hi, rfl⟩ := h
+  mem_combine _ (spine_eq fm₁ fm₂) h
-  exact ⟨fm₁ i, fm₂ i, rfl, ⟨i, hi, rfl⟩, ⟨i, hi, rfl⟩⟩
-
-lemma mem_inf {fm₁ fm₂ : FiniteMap α β ks} {k : α} {v : β}
-    (h : (k, v) ∈ fm₁ ⊓ fm₂) :
-    ∃ v₁ v₂, v = v₁ ⊓ v₂ ∧ (k, v₁) ∈ fm₁ ∧ (k, v₂) ∈ fm₂ := by
-  obtain ⟨i, hi, rfl⟩ := h
-  exact ⟨fm₁ i, fm₂ i, rfl, ⟨i, hi, rfl⟩, ⟨i, hi, rfl⟩⟩
 
 section Updating
 
-variable [DecidableEq α]
+variable [DecidableEq A]
 
-def updating (fm : FiniteMap α β ks) (ks' : List α) (g : α → β) : FiniteMap α β ks :=
+def updating (fm : FiniteMap A B ks) (ks' : List A) (g : A → B) :
-  fun i => if ks.get i ∈ ks' then g (ks.get i) else fm i
+    FiniteMap A B ks :=
+  ⟨fm.val.map (fun p => if p.1 ∈ ks' then (p.1, g p.1) else p), by
+    rw [List.map_map,
+        show (Prod.fst ∘ fun p : A × B => if p.1 ∈ ks' then (p.1, g p.1) else p)
+          = Prod.fst from funext fun p => by by_cases h : p.1 ∈ ks' <;> simp [h]]
+    exact fm.property⟩
 
-omit [Lattice β] in
+omit [Lattice B] in
-lemma eq_of_mem_updating {k : α} {v : β} {fm : FiniteMap α β ks}
+@[simp] theorem updating_val (fm : FiniteMap A B ks) (ks' : List A) (g : A → B) :
-    {ks' : List α} {g : α → β} (hk : k ∈ ks')
+    (updating fm ks' g).val
+      = fm.val.map (fun p => if p.1 ∈ ks' then (p.1, g p.1) else p) := rfl
+
+omit [Lattice B] in
+theorem memKey_updating {k : A} {fm : FiniteMap A B ks} {ks' : List A} {g : A → B} :
+    MemKey k (updating fm ks' g) ↔ MemKey k fm := by
+  rw [memKey_iff, memKey_iff]
+
+omit [Lattice B] in
+theorem eq_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks}
+    {ks' : List A} {g : A → B} (hk : k ∈ ks')
     (h : (k, v) ∈ updating fm ks' g) : v = g k := by
-  obtain ⟨i, hi, rfl⟩ := h
+  obtain ⟨p, hp, heq⟩ := List.mem_map.mp h
-  show (if ks.get i ∈ ks' then g (ks.get i) else fm i) = g k
+  by_cases hmem : p.1 ∈ ks'
-  rw [if_pos (by rw [hi]; exact hk), hi]
+  · rw [if_pos hmem] at heq
+    injection heq with h1 h2
+    rw [← h2, h1]
+  · rw [if_neg hmem] at heq
+    rw [heq] at hmem
+    exact absurd hk hmem
 
-omit [Lattice β] in
+omit [Lattice B] in
-lemma mem_of_mem_updating {k : α} {v : β} {fm : FiniteMap α β ks}
+theorem mem_updating {k : A} {fm : FiniteMap A B ks} {ks' : List A} {g : A → B}
-    {ks' : List α} {g : α → β} (hk : k ∉ ks')
+    (hk : k ∈ ks') (hmem : MemKey k fm) : (k, g k) ∈ updating fm ks' g := by
+  obtain ⟨v, hv⟩ := locate hmem
+  exact List.mem_map.mpr ⟨(k, v), hv, by simp [hk]⟩
+
+omit [Lattice B] in
+theorem mem_updating_of_not_mem {k : A} {v : B} {fm : FiniteMap A B ks}
+    {ks' : List A} {g : A → B} (hk : k ∉ ks') (h : (k, v) ∈ fm) :
+    (k, v) ∈ updating fm ks' g :=
+  List.mem_map.mpr ⟨(k, v), h, by simp [hk]⟩
+
+omit [Lattice B] in
+theorem mem_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks}
+    {ks' : List A} {g : A → B} (hk : k ∉ ks')
     (h : (k, v) ∈ updating fm ks' g) : (k, v) ∈ fm := by
-  obtain ⟨i, hi, rfl⟩ := h
+  obtain ⟨p, hp, heq⟩ := List.mem_map.mp h
-  refine ⟨i, hi, ?_⟩
+  by_cases hmem : p.1 ∈ ks'
-  show fm i = (if ks.get i ∈ ks' then g (ks.get i) else fm i)
+  · rw [if_pos hmem] at heq
-  rw [if_neg (by rw [hi]; exact hk)]
+    injection heq with h1 _
+    rw [← h1] at hk
+    exact absurd hmem hk
+  · rw [if_neg hmem] at heq
+    exact heq ▸ hp
 
-lemma updating_mono {fm₁ fm₂ : FiniteMap α β ks} {ks' : List α}
+private theorem updating_mono_list {ks' : List A} {g₁ g₂ : A → B}
-    {g₁ g₂ : α → β} (hfm : fm₁ ≤ fm₂) (hg : ∀ k, g₁ k ≤ g₂ k) :
+    (hg : ∀ k, g₁ k ≤ g₂ k) {l₁ l₂ : List (A × B)}
+    (hl : List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂) :
+    List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2)
+      (l₁.map fun p => if p.1 ∈ ks' then (p.1, g₁ p.1) else p)
+      (l₂.map fun p => if p.1 ∈ ks' then (p.1, g₂ p.1) else p) := by
+  induction hl with
+  | nil => exact List.Forall₂.nil
+  | @cons x y l₁' l₂' hpq hrest ih =>
+    simp only [List.map_cons]
+    refine List.Forall₂.cons ?_ ih
+    obtain ⟨hk, hv⟩ := hpq
+    by_cases h : x.1 ∈ ks'
+    · rw [if_pos h, if_pos (hk ▸ h)]
+      exact ⟨hk, hk ▸ hg x.1⟩
+    · rw [if_neg h, if_neg (fun hy => h (hk.symm ▸ hy))]
+      exact ⟨hk, hv⟩
+
+theorem updating_mono {fm₁ fm₂ : FiniteMap A B ks} {ks' : List A}
+    {g₁ g₂ : A → B} (hfm : fm₁ ≤ fm₂) (hg : ∀ k, g₁ k ≤ g₂ k) :
     updating fm₁ ks' g₁ ≤ updating fm₂ ks' g₂ := by
-  rw [le_def]
+  rw [le_iff] at hfm ⊢
-  intro i
+  simp only [updating_val]
-  show (if ks.get i ∈ ks' then g₁ (ks.get i) else fm₁ i)
+  exact updating_mono_list hg hfm
-     ≤ (if ks.get i ∈ ks' then g₂ (ks.get i) else fm₂ i)
-  split
-  · exact hg (ks.get i)
-  · exact le_def.mp hfm i
 
 end Updating
 
 section GeneralizedUpdate
 
-variable [DecidableEq α] {L : Type*} [Lattice L]
+variable [DecidableEq A] {L : Type*} [Lattice L]
 
-def generalizedUpdate (f : L → FiniteMap α β ks) (g : α → L → β)
+def generalizedUpdate (f : L → FiniteMap A B ks) (g : A → L → B)
-    (ks' : List α) : L → FiniteMap α β ks := fun l =>
+    (ks' : List A) (l : L) : FiniteMap A B ks :=
   (f l).updating ks' (fun k => g k l)
 
-variable {f : L → FiniteMap α β ks} {g : α → L → β} {ks' : List α}
+variable {f : L → FiniteMap A B ks} {g : A → L → B} {ks' : List A}
 
-lemma generalizedUpdate_monotone (hf : Monotone f)
+theorem generalizedUpdate_monotone (hf : Monotone f)
     (hg : ∀ k, Monotone (g k)) : Monotone (generalizedUpdate f g ks') :=
   fun _ _ hl => updating_mono (hf hl) (fun k => hg k hl)
 
-omit [Lattice β] [Lattice L] in
+omit [Lattice B] [Lattice L] in
-lemma generalizedUpdate_mem_eq {k : α} {v : β} {l : L} (hk : k ∈ ks')
+theorem generalizedUpdate_memKey {k : A} {l : L}
-    (h : (k, v) ∈ generalizedUpdate f g ks' l) : v = g k l :=
+    (h : MemKey k (f l)) : MemKey k (generalizedUpdate f g ks' l) := by
-  eq_of_mem_updating (g := fun k => g k l) hk h
+  unfold generalizedUpdate
+  exact memKey_updating.mpr h
 
-omit [Lattice β] [Lattice L] in
+omit [Lattice B] [Lattice L] in
-lemma generalizedUpdate_not_mem_backward {k : α} {v : β} {l : L} (hk : k ∉ ks')
+theorem generalizedUpdate_mem {k : A} {l : L} (hk : k ∈ ks')
-    (h : (k, v) ∈ generalizedUpdate f g ks' l) : (k, v) ∈ f l :=
+    (h : MemKey k (f l)) : (k, g k l) ∈ generalizedUpdate f g ks' l := by
-  mem_of_mem_updating hk h
+  unfold generalizedUpdate
+  exact mem_updating hk h
+
+omit [Lattice B] [Lattice L] in
+theorem generalizedUpdate_mem_eq {k : A} {v : B} {l : L} (hk : k ∈ ks')
+    (h : (k, v) ∈ generalizedUpdate f g ks' l) : v = g k l := by
+  unfold generalizedUpdate at h
+  exact eq_of_mem_updating (g := fun k => g k l) hk h
+
+omit [Lattice B] [Lattice L] in
+theorem generalizedUpdate_not_mem_forward {k : A} {v : B} {l : L} (hk : k ∉ ks')
+    (h : (k, v) ∈ f l) : (k, v) ∈ generalizedUpdate f g ks' l := by
+  unfold generalizedUpdate
+  exact mem_updating_of_not_mem hk h
+
+omit [Lattice B] [Lattice L] in
+theorem generalizedUpdate_not_mem_backward {k : A} {v : B} {l : L} (hk : k ∉ ks')
+    (h : (k, v) ∈ generalizedUpdate f g ks' l) : (k, v) ∈ f l := by
+  unfold generalizedUpdate at h
+  exact mem_of_mem_updating hk h
 
 end GeneralizedUpdate
 
 section ValuesAt
 
-variable [DecidableEq α]
+variable [DecidableEq A]
 
-/-- The value stored under `k`, if `k` is a key. -/
+private def lookup? (k : A) : List (A × B) → Option B
-private def lookup (fm : FiniteMap α β ks) (k : α) : Option β :=
+  | [] => none
-  if h : k ∈ ks then some (fm ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩) else none
+  | p :: l' => if p.1 = k then some p.2 else lookup? k l'
 
-/-- The values stored under the keys `ks'` (skipping any that are not keys). -/
+def valuesAt (fm : FiniteMap A B ks) (ks' : List A) : List B :=
-def valuesAt (fm : FiniteMap α β ks) (ks' : List α) : List β :=
+  ks'.filterMap (fun k => lookup? k fm.val)
-  ks'.filterMap fm.lookup
 
-omit [Lattice β] in
+omit [Lattice B] in
-lemma mem_valuesAt (hks : ks.Nodup) {fm : FiniteMap α β ks} {k : α} {v : β}
+private theorem lookup?_eq_some_of_mem : ∀ {l : List (A × B)},
-    {ks' : List α} (hk : k ∈ ks') (h : (k, v) ∈ fm) : v ∈ valuesAt fm ks' := by
+    (l.map Prod.fst).Nodup → ∀ {k : A} {v : B}, (k, v) ∈ l →
-  refine List.mem_filterMap.mpr ⟨k, hk, ?_⟩
+    lookup? k l = some v
-  obtain ⟨i, hi, rfl⟩ := h
+  | [], _, _, _, h => by simp at h
-  have hik : ks.get i = k := hi
+  | p :: l', hnd, k, v, h => by
-  have hmem : k ∈ ks := hik ▸ ks.get_mem i
+    simp only [List.map_cons, List.nodup_cons] at hnd
-  show (if h : k ∈ ks then
+    rcases List.mem_cons.mp h with heq | h'
-          some (fm ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩) else none) = some (fm i)
+    · rw [← heq]
-  rw [dif_pos hmem]
+      simp [lookup?]
-  have : (⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr hmem⟩ : Fin ks.length) = i :=
+    · rw [lookup?, if_neg ?_]
-    hks.get_inj_iff.mp (by rw [List.idxOf_get, hi])
+      · exact lookup?_eq_some_of_mem hnd.2 h'
-  rw [this]
+      · intro hpk
+        subst hpk
+        have := List.mem_map_of_mem Prod.fst h'
+        exact hnd.1 this
 
-private lemma lookup_rel {fm₁ fm₂ : FiniteMap α β ks} (hle : fm₁ ≤ fm₂) (k : α) :
+omit [Lattice B] in
-    Option.Rel (· ≤ ·) (fm₁.lookup k) (fm₂.lookup k) := by
+theorem mem_valuesAt (hks : ks.Nodup) {fm : FiniteMap A B ks} {k : A} {v : B}
-  show Option.Rel _
+    {ks' : List A} (hk : k ∈ ks') (h : (k, v) ∈ fm) : v ∈ valuesAt fm ks' :=
-    (if h : k ∈ ks then some (fm₁ ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩) else none)
+  List.mem_filterMap.mpr
-    (if h : k ∈ ks then some (fm₂ ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩) else none)
+    ⟨k, hk, lookup?_eq_some_of_mem (fm.property.symm ▸ hks) h⟩
-  by_cases hk : k ∈ ks
-  · rw [dif_pos hk, dif_pos hk]; exact Option.Rel.some (le_def.mp hle _)
-  · rw [dif_neg hk, dif_neg hk]; exact Option.Rel.none
 
-lemma valuesAt_le {fm₁ fm₂ : FiniteMap α β ks} (hle : fm₁ ≤ fm₂)
+private theorem lookup?_forall₂ {l₁ l₂ : List (A × B)}
-    (ks' : List α) :
+    (h : List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂) (k : A) :
+    Option.Rel (· ≤ ·) (lookup? k l₁) (lookup? k l₂) := by
+  induction h with
+  | nil => exact Option.Rel.none
+  | @cons p q l₁ l₂ hpq hrest ih =>
+    rw [lookup?, lookup?]
+    by_cases hc : q.1 = k
+    · rw [if_pos hc, if_pos (hpq.1.trans hc)]
+      exact Option.Rel.some hpq.2
+    · rw [if_neg hc, if_neg (fun hp => hc (hpq.1 ▸ hp))]
+      exact ih
+
+theorem valuesAt_le {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂)
+    (ks' : List A) :
     List.Forall₂ (· ≤ ·) (valuesAt fm₁ ks') (valuesAt fm₂ ks') := by
   induction ks' with
   | nil => exact List.Forall₂.nil
   | cons k ks'' ih =>
-    have hrel := lookup_rel hle k
+    have hrel := lookup?_forall₂ (le_iff.mp hle) k
     rw [valuesAt, valuesAt, List.filterMap_cons, List.filterMap_cons]
     revert hrel
-    generalize fm₁.lookup k = o₁
+    generalize lookup? k fm₁.val = o₁
-    generalize fm₂.lookup k = o₂
+    generalize lookup? k fm₂.val = o₂
     intro hrel
     cases hrel with
     | none => simpa [valuesAt] using ih
@@ -209,6 +427,120 @@ lemma valuesAt_le {fm₁ fm₂ : FiniteMap α β ks} (hle : fm₁ ≤ fm₂)
 
 end ValuesAt
 
+section Iso
+
+omit [Lattice B] in
+theorem val_ne_nil {k : A} {ks' : List A} (fm : FiniteMap A B (k :: ks')) :
+    fm.val ≠ [] := fun h => by
+  have hp := fm.property
+  rw [h] at hp
+  simp at hp
+
+def headVal {k : A} {ks' : List A} : FiniteMap A B (k :: ks') → B
+  | ⟨[], h⟩ => absurd h (by simp)
+  | ⟨p :: _, _⟩ => p.2
+
+def pop {k : A} {ks' : List A} : FiniteMap A B (k :: ks') → FiniteMap A B ks'
+  | ⟨[], h⟩ => absurd h (by simp)
+  | ⟨_ :: l, h⟩ =>
+    ⟨l, by simp only [List.map_cons, List.cons.injEq] at h; exact h.2⟩
+
+omit [Lattice B] in
+theorem val_eq_cons {k : A} {ks' : List A} :
+    ∀ fm : FiniteMap A B (k :: ks'), fm.val = (k, fm.headVal) :: fm.pop.val
+  | ⟨[], h⟩ => absurd h (by simp)
+  | ⟨p :: l, h⟩ => by
+    simp only [List.map_cons, List.cons.injEq] at h
+    simp [headVal, pop, ← h.1]
+
+def toIter : {ks : List A} → FiniteMap A B ks → IterProd B PUnit ks.length
+  | [], _ => PUnit.unit
+  | _ :: _, fm => (fm.headVal, toIter fm.pop)
+
+def ofIter : (ks : List A) → IterProd B PUnit ks.length → FiniteMap A B ks
+  | [], _ => ⟨[], rfl⟩
+  | k :: ks', ip =>
+    ⟨(k, ip.1) :: (ofIter ks' ip.2).val, by
+      simp [(ofIter ks' ip.2).property]⟩
+
+omit [Lattice B] in
+theorem ofIter_toIter : ∀ {ks : List A} (fm : FiniteMap A B ks),
+    ofIter ks (toIter fm) = fm
+  | [], fm => by
+    obtain ⟨val, hprop⟩ := fm
+    cases val with
+    | nil => rfl
+    | cons p l => exact absurd hprop (by simp)
+  | k :: ks', fm => Subtype.ext (by
+      show (k, fm.headVal) :: (ofIter ks' (toIter fm.pop)).val = fm.val
+      rw [ofIter_toIter fm.pop, ← val_eq_cons fm])
+
+omit [Lattice B] in
+theorem toIter_ofIter : ∀ (ks : List A) (ip : IterProd B PUnit ks.length),
+    toIter (ofIter ks ip) = ip
+  | [], _ => rfl
+  | k :: ks', ip => by
+    show (headVal (ofIter (k :: ks') ip), toIter (pop (ofIter (k :: ks') ip))) = ip
+    rw [show pop (ofIter (k :: ks') ip) = ofIter ks' ip.2 from rfl,
+        toIter_ofIter ks' ip.2]
+    rfl
+
+theorem headVal_le {k : A} {ks' : List A} {fm₁ fm₂ : FiniteMap A B (k :: ks')}
+    (h : fm₁ ≤ fm₂) : fm₁.headVal ≤ fm₂.headVal := by
+  have h' := le_iff.mp h
+  rw [val_eq_cons fm₁, val_eq_cons fm₂] at h'
+  exact (List.forall₂_cons.mp h').1.2
+
+theorem pop_le {k : A} {ks' : List A} {fm₁ fm₂ : FiniteMap A B (k :: ks')}
+    (h : fm₁ ≤ fm₂) : fm₁.pop ≤ fm₂.pop := by
+  rw [le_iff]
+  have h' := le_iff.mp h
+  rw [val_eq_cons fm₁, val_eq_cons fm₂] at h'
+  exact (List.forall₂_cons.mp h').2
+
+theorem toIter_monotone : ∀ {ks : List A},
+    Monotone (toIter : FiniteMap A B ks → IterProd B PUnit ks.length)
+  | [] => fun _ _ _ => le_refl _
+  | _ :: _ => fun _ _ h =>
+    Prod.mk_le_mk.mpr ⟨headVal_le h, toIter_monotone (pop_le h)⟩
+
+theorem ofIter_monotone : ∀ (ks : List A), Monotone (ofIter (A := A) (B := B) ks)
+  | [] => fun _ _ _ => le_refl _
+  | k :: ks' => fun ip₁ ip₂ h => by
+    rw [le_iff]
+    show List.Forall₂ _ ((k, ip₁.1) :: (ofIter ks' ip₁.2).val)
+                        ((k, ip₂.1) :: (ofIter ks' ip₂.2).val)
+    exact List.Forall₂.cons ⟨rfl, h.1⟩ (le_iff.mp (ofIter_monotone ks' h.2))
+
+def fixedHeight [FiniteHeightLattice B] (ks : List A) :
+    FiniteHeightLattice (FiniteMap A B ks) :=
+  FiniteHeightLattice.transport
+    (ofIter ks) toIter (ofIter_monotone ks) toIter_monotone
+    (toIter_ofIter ks) (fun fm => ofIter_toIter fm)
+
+instance [FiniteHeightLattice B] : FiniteHeightLattice (FiniteMap A B ks) :=
+  fixedHeight ks
+
+omit [Lattice B] in
+theorem mem_ofIter_build {b : B} : ∀ {ks : List A} {k : A} {v : B},
+    (k, v) ∈ ofIter ks (IterProd.build b PUnit.unit ks.length) → v = b
+  | [], _, _, h => by simp [ofIter, mem_def] at h
+  | k' :: ks', k, v, h => by
+    rcases List.mem_cons.mp h with heq | h'
+    · exact (Prod.ext_iff.mp heq).2
+    · exact mem_ofIter_build h'
+
+theorem bot_contains_bots [FiniteHeightLattice B] {k : A} {v : B}
+    (h : (k, v) ∈ (fixedHeight ks).bot) : v = (⊥ : B) := by
+  have hbot : (fixedHeight ks).bot
+      = ofIter ks (IterProd.build (⊥ : B) (⊥ : PUnit) ks.length) := by
+    show ofIter ks (IterProd.fixedHeight (A := B) (B := PUnit) ks.length).bot = _
+    rw [IterProd.bot_fixedHeight]
+  rw [hbot] at h
+  exact mem_ofIter_build h
+
+end Iso
+
 end FiniteMap
 
 end Spa

lean/Spa/Lattice/Finset.lean

@@ -1,38 +0,0 @@
-import Spa.Lattice
-import Mathlib.Data.Finset.Lattice.Basic
-import Mathlib.Data.Fintype.Lattice
-import Mathlib.Data.Fintype.Card
-
-/-! # Power Sets of Finite Type
-
-For a `Fintype α`, `Finset α` is the power-set lattice: `⊔` is union, `⊓` is
-intersection, `⊥ = ∅`, `⊤ = univ`. This lattice also has a finite height.
-
-The `Finset α` representation s isomorphic to `Fin α → Bool`, but far more
-efficient because it avoids building up stacks of layered closures. -/
-
-namespace Spa
-
-variable {α : Type*} [Fintype α] [DecidableEq α]
-
-omit [Fintype α] [DecidableEq α] in
-private lemma finset_card_strictMono : StrictMono (Finset.card : Finset α → ℕ) :=
-  fun _ _ h => Finset.card_lt_card h
-
-omit [DecidableEq α] in
-/-- A strictly increasing chain of finsets grows its cardinality by at least one
-    each step, and cardinality is capped by `Fintype.card α`. -/
-lemma finset_boundedChains : BoundedChains (Finset α) (Fintype.card α) := fun c => by
-  have h := LTSeries.head_add_length_le_nat (c.map Finset.card finset_card_strictMono)
-  rw [LTSeries.head_map, LTSeries.last_map, LTSeries.map_length] at h
-  have h2 : c.last.card ≤ Fintype.card α := Finset.card_le_univ _
-  omega
-
-instance instFiniteHeightFinset : FiniteHeightLattice (Finset α) where
-  toLattice := inferInstance
-  toOrderBot := inferInstance
-  toOrderTop := inferInstance
-  height := Fintype.card α
-  chains_bounded := finset_boundedChains
-
-end Spa

lean/Spa/Lattice/IterProd.lean

@@ -0,0 +1,50 @@
+import Spa.Lattice.Prod
+import Spa.Lattice.Unit
+
+namespace Spa
+
+universe u
+
+def IterProd (A B : Type u) : ℕ → Type u
+  | 0 => B
+  | k + 1 => A × IterProd A B k
+
+namespace IterProd
+
+variable {A B : Type u}
+
+instance instLattice [Lattice A] [Lattice B] :
+    ∀ k, Lattice (IterProd A B k)
+  | 0 => inferInstanceAs (Lattice B)
+  | k + 1 => @Prod.instLattice A (IterProd A B k) _ (instLattice k)
+
+instance instDecidableEq [DecidableEq A] [DecidableEq B] :
+    ∀ k, DecidableEq (IterProd A B k)
+  | 0 => inferInstanceAs (DecidableEq B)
+  | k + 1 => @instDecidableEqProd A (IterProd A B k) _ (instDecidableEq k)
+
+def build (a : A) (b : B) : (k : ℕ) → IterProd A B k
+  | 0 => b
+  | k + 1 => (a, build a b k)
+
+variable [Lattice A] [Lattice B]
+
+def fixedHeight [FiniteHeightLattice A] [FiniteHeightLattice B] :
+    ∀ k, FiniteHeightLattice (IterProd A B k)
+  | 0 => inferInstanceAs (FiniteHeightLattice B)
+  | k + 1 => @Spa.prod A (IterProd A B k) _ (instLattice k) _ (fixedHeight k)
+
+instance instFiniteHeight [FiniteHeightLattice A] [FiniteHeightLattice B] (k : ℕ) :
+    FiniteHeightLattice (IterProd A B k) := fixedHeight k
+
+theorem bot_fixedHeight [FiniteHeightLattice A] [FiniteHeightLattice B] :
+    ∀ k, (fixedHeight (A := A) (B := B) k).bot = build (⊥ : A) (⊥ : B) k
+  | 0 => rfl
+  | k + 1 => by
+    show ((⊥ : A), (fixedHeight (A := A) (B := B) k).bot)
+        = ((⊥ : A), build (⊥ : A) (⊥ : B) k)
+    rw [bot_fixedHeight k]
+
+end IterProd
+
+end Spa

lean/Spa/Lattice/Prod.lean

@@ -0,0 +1,98 @@
+import Spa.Lattice
+
+namespace Spa
+
+section Unzip
+
+variable {α β : Type*} [PartialOrder α] [PartialOrder β]
+
+theorem LTSeries.exists_unzip (c : LTSeries (α × β)) :
+    ∃ (c₁ : LTSeries α) (c₂ : LTSeries β),
+      c₁.head = c.head.1 ∧ c₁.last = c.last.1 ∧
+      c₂.head = c.head.2 ∧ c₂.last = c.last.2 ∧
+      c.length ≤ c₁.length + c₂.length := by
+  suffices H : ∀ (n : ℕ) (c : LTSeries (α × β)), c.length = n →
+      ∃ (c₁ : LTSeries α) (c₂ : LTSeries β),
+        c₁.head = c.head.1 ∧ c₁.last = c.last.1 ∧
+        c₂.head = c.head.2 ∧ c₂.last = c.last.2 ∧
+        c.length ≤ c₁.length + c₂.length from H c.length c rfl
+  intro n
+  induction n with
+  | zero =>
+    intro c hn
+    refine ⟨RelSeries.singleton _ c.head.1, RelSeries.singleton _ c.head.2,
+      rfl, ?_, rfl, ?_, by simp [hn]⟩ <;>
+    · have hlast : Fin.last c.length = 0 := by ext; simp [hn]
+      simp [RelSeries.last, RelSeries.head, hlast]
+  | succ n ih =>
+    intro c hn
+    have h0 : c.length ≠ 0 := by omega
+    obtain ⟨c₁, c₂, hh₁, hl₁, hh₂, hl₂, hlen⟩ :=
+      ih (c.tail h0) (by simp [RelSeries.tail_length, hn])
+    rw [RelSeries.last_tail] at hl₁ hl₂
+    rw [RelSeries.head_tail] at hh₁ hh₂
+    rw [RelSeries.tail_length] at hlen
+    have hstep : c.head < c 1 := by
+      have h := c.step ⟨0, by omega⟩
+      have h1 : (⟨0, by omega⟩ : Fin c.length).succ = 1 := by
+        ext; simp [Fin.val_one, Nat.mod_eq_of_lt (by omega : 1 < c.length + 1)]
+      rwa [h1] at h
+    obtain ⟨hle1, hle2⟩ := Prod.le_def.mp hstep.le
+    rcases eq_or_lt_of_le hle1 with heq1 | hlt1 <;>
+      rcases eq_or_lt_of_le hle2 with heq2 | hlt2
+    · exact absurd (Prod.ext heq1 heq2) hstep.ne
+    · refine ⟨c₁, c₂.cons c.head.2 (hh₂ ▸ hlt2),
+        hh₁.trans heq1.symm, hl₁, RelSeries.head_cons .., by
+          rw [RelSeries.last_cons]; exact hl₂, by
+          simp only [RelSeries.cons_length]; omega⟩
+    · refine ⟨c₁.cons c.head.1 (hh₁ ▸ hlt1), c₂,
+        RelSeries.head_cons .., by
+          rw [RelSeries.last_cons]; exact hl₁,
+        hh₂.trans heq2.symm, hl₂, by
+          simp only [RelSeries.cons_length]; omega⟩
+    · refine ⟨c₁.cons c.head.1 (hh₁ ▸ hlt1), c₂.cons c.head.2 (hh₂ ▸ hlt2),
+        RelSeries.head_cons .., by
+          rw [RelSeries.last_cons]; exact hl₁,
+        RelSeries.head_cons .., by
+          rw [RelSeries.last_cons]; exact hl₂, by
+          simp only [RelSeries.cons_length]; omega⟩
+
+end Unzip
+
+section FixedHeight
+
+variable {α β : Type*} [Lattice α] [Lattice β]
+
+instance prod [A : FiniteHeightLattice α] [B : FiniteHeightLattice β] :
+    FiniteHeightLattice (α × β) where
+  bot := ((⊥ : α), (⊥ : β))
+  top := ((⊤ : α), (⊤ : β))
+  height := A.height + B.height
+  longestChain :=
+    { series :=
+        RelSeries.smash
+          (A.longestChain.series.map (fun a => (a, (⊥ : β)))
+            (fun _ _ h => Prod.mk_lt_mk_iff_left.mpr h))
+          (B.longestChain.series.map (fun b => ((⊤ : α), b))
+            (fun _ _ h => Prod.mk_lt_mk_iff_right.mpr h))
+          (by simp [A.longestChain.last_series, B.longestChain.head_series])
+      head_series :=
+        (RelSeries.head_smash _).trans
+          ((LTSeries.head_map _ _ _).trans
+            (congrArg (·, (⊥ : β)) A.longestChain.head_series))
+      last_series :=
+        (RelSeries.last_smash _).trans
+          ((LTSeries.last_map _ _ _).trans
+            (congrArg ((⊤ : α), ·) B.longestChain.last_series))
+      length_series := by
+        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₁
+    have h₂ := B.chains_bounded c₂
+    omega
+
+end FixedHeight
+
+end Spa

lean/Spa/Lattice/Tuple.lean

@@ -1,128 +0,0 @@
-import Spa.Lattice
-import Mathlib.Data.Fin.Tuple.Basic
-import Mathlib.Algebra.Order.BigOperators.Group.Finset
-
-/-!
-
-# Finite Tuple Lattices
-
-This file provides a proof that, in addition to being a lattice, the function
-space `Fin n → β` is itself a `Spa.FiniteHeightLattice` if the element type
-`β` is a lattice.
-
-Finite tuple lattices are the workhorse behind `FiniteMap`, whose carrier is
-`Fin ks.length → β`.
-
-The proof proceeds by "unzipping" a chain (`LTSeries`):
-
-$$
-(a_1, b_1, c_1) < \ldots < (a_1, b_1, c_o) < \ldots < (a_1, b_m, c_o) <
-  \ldots < (a_n, b_m, c_o)
-$$
-
-In which, at each step, at least one of the components must have increased
-(otherwise, the chain is not striclty increasing), into `n` chains
-(`LTSeries`).
-
-$$
-\begin{aligned}
-a_1 < \ldots < a_n \\
-b_1 < \ldots < b_m \
-c_1 < \ldots < c_o \
-\end{aligned}
-$$
-
-Because at least one of the two "unzipped" chains grows with each element of
-the product chain, the full chain length can't exceed the sum of the
-components. By the definition of finite height, these two chains are bounded,
-and therefore, the product chain is bounded too. -/
-
-namespace Spa
-
-namespace Tuple
-
-variable {β : Type*}
-
-section Unzip
-
-variable [PartialOrder β]
-
-open Classical in -- chain bounds are in Prop, so classical helps here.
-/-- The generalized unzip: any chain in `Fin n → β` decomposes into a family of
-    per-tuple-coordinate chains in `β`, agreeing with the original at each end, whose
-    lengths sum to an upper bound on the original chain's length. -/
-lemma exists_unzip {n : ℕ} (c : LTSeries (Fin n → β)) :
-    ∃ cs : Fin n → LTSeries β,
-      (∀ i, (cs i).head = c.head i) ∧ (∀ i, (cs i).last = c.last i) ∧
-      c.length ≤ ∑ i, (cs i).length := by
-  suffices H : ∀ (m : ℕ) (c : LTSeries (Fin n → β)), c.length = m →
-      ∃ cs : Fin n → LTSeries β,
-        (∀ i, (cs i).head = c.head i) ∧ (∀ i, (cs i).last = c.last i) ∧
-        c.length ≤ ∑ i, (cs i).length from H c.length c rfl
-  intro m
-  induction m with
-  | zero =>
-    intro c hn
-    have hlast : (Fin.last c.length) = 0 := by ext; simp [hn]
-    have hhl : c.last = c.head := by rw [RelSeries.last, RelSeries.head, hlast]
-    refine ⟨fun i => RelSeries.singleton _ (c.head i), fun i => ?_, fun i => ?_, ?_⟩
-    · exact RelSeries.head_singleton _
-    · rw [RelSeries.last_singleton, hhl]
-    · simp [hn, RelSeries.singleton]
-  | succ m ih =>
-    intro c hn
-    have h0 : c.length ≠ 0 := by omega
-    haveI : NeZero c.length := ⟨h0⟩
-    obtain ⟨cs', hh', hl', hlen'⟩ := ih (c.tail h0) (by rw [RelSeries.tail_length]; omega)
-    have hstep : c.head < c 1 := c.strictMono Fin.one_pos'
-    obtain ⟨hle, j, hjlt⟩ := Pi.lt_def.mp hstep
-    have hh'1 : ∀ i, (cs' i).head = c 1 i := fun i => by rw [hh' i, RelSeries.head_tail]
-    refine ⟨fun i =>
-        if hlt : c.head i < c 1 i then
-          (cs' i).cons (c.head i) (by rw [hh'1 i]; exact hlt)
-        else cs' i,
-      fun i => ?_, fun i => ?_, ?_⟩
-    · by_cases hlt : c.head i < c 1 i
-      · simp only [dif_pos hlt, RelSeries.head_cons]
-      · simp only [dif_neg hlt]
-        rw [hh'1 i]
-        exact ((lt_or_eq_of_le (hle i)).resolve_left hlt).symm
-    · by_cases hlt : c.head i < c 1 i
-      · simp only [dif_pos hlt, RelSeries.last_cons, hl' i, RelSeries.last_tail]
-      · simp only [dif_neg hlt, hl' i, RelSeries.last_tail]
-    · calc c.length
-          = (c.tail h0).length + 1 := by rw [RelSeries.tail_length]; omega
-        _ ≤ (∑ i, (cs' i).length) + 1 := Nat.add_le_add_right hlen' 1
-        _ ≤ ∑ i, (if hlt : c.head i < c 1 i then
-              (cs' i).cons (c.head i) (by rw [hh'1 i]; exact hlt) else cs' i).length :=
-          Nat.succ_le_of_lt (Finset.sum_lt_sum (fun i _ => by
-              split
-              · rw [RelSeries.cons_length]; omega
-              · exact le_rfl)
-            ⟨j, Finset.mem_univ j, by rw [dif_pos hjlt, RelSeries.cons_length]; omega⟩)
-
-end Unzip
-
-section FiniteHeight
-
-variable [FiniteHeightLattice β]
-
-instance instFiniteHeight {n : ℕ} : FiniteHeightLattice (Fin n → β) where
-  toLattice := inferInstance
-  toOrderBot := inferInstance
-  toOrderTop := inferInstance
-  height := n * FiniteHeightLattice.height (α := β)
-  chains_bounded := fun c => by
-    obtain ⟨cs, _, _, hbound⟩ := exists_unzip c
-    refine hbound.trans ?_
-    calc ∑ i, (cs i).length
-        ≤ ∑ _i : Fin n, FiniteHeightLattice.height (α := β) :=
-          Finset.sum_le_sum (fun i _ => FiniteHeightLattice.chains_bounded (cs i))
-      _ = n * FiniteHeightLattice.height (α := β) := by
-          simp [Finset.sum_const, Finset.card_univ, Fintype.card_fin]
-
-end FiniteHeight
-
-end Tuple
-
-end Spa

lean/Spa/Lattice/Unit.lean

@@ -1,14 +1,18 @@
 import Spa.Lattice
 
-/-!
-
-# Unit Lattice
-
-This file provides a proof that in addition to being a lattice,
-`PUnit` is a `Spa.FiniteHeightLattice`. This is a fairly trivial result. -/
-
 namespace Spa
 
-instance : FiniteHeightLattice PUnit := FiniteHeightLattice.ofUnique PUnit
+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 _ _)
+
+instance : FiniteHeightLattice PUnit where
+  bot := PUnit.unit
+  top := PUnit.unit
+  height := 0
+  longestChain := { series := RelSeries.singleton _ PUnit.unit, head_series := refl _, last_series := refl _, length_series := refl _ }
+  chains_bounded := boundedChains_of_subsingleton PUnit 0
 
 end Spa

lean/Spa/Showable.lean

@@ -30,8 +30,7 @@ instance {α : Type*} [Showable α] : Showable (AboveBelow α) :=
 instance {α β : Type*} {ks : List α} [Showable α] [Showable β] :
     Showable (FiniteMap α β ks) :=
   ⟨fun fm =>
-    "{" ++ (FiniteMap.toList fm).foldr
+    "{" ++ fm.val.foldr (fun p rest => show' p.1 ++ " ↦ " ++ show' p.2 ++ ", " ++ rest) ""
-        (fun p rest => show' p.1 ++ " ↦ " ++ show' p.2 ++ ", " ++ rest) ""
         ++ "}"⟩
 
 end Spa

lean/Spa/Transformation/Licm.lean

@@ -1,102 +0,0 @@
-import Spa.Analysis.Reaching
-import Spa.Language.Tagged.Graphs
-
-/-!
-# Finding loop-invariant assignments (LICM groundwork)
-
-This wires the **reaching-definitions** analysis (`Spa/Analysis/Reaching.lean`)
-to the **tagged AST** to *find* — not yet move — assignments inside a `while`
-loop whose right-hand side depends only on definitions made *outside* the loop.
-These are the candidates a later LICM pass could hoist.
-
-The pipeline, for each assignment immediately enclosed by a loop:
-
-1. locate its CFG state via the tagged-graph bridge (`Program.stateOfNodeId`);
-2. read the reaching definitions at the assignment's *entry*
-   (`joinForKey s result` — the join over predecessors, i.e. before the
-   assignment itself runs);
-3. union the definition sets of the RHS variables;
-4. map each definition site back to its `RawId` (`Program.nodeIdOf`) and check
-   it is **not** inside the loop body (structural `subtreeIds` membership).
-
-If every reaching definition of every RHS variable lies outside the loop, the
-assignment is reported as loop-invariant.  This is the first-order check ("all
-reaching definitions outside the loop"); transitive/iterated invariance and the
-actual hoisting are out of scope here.
--/
-
-namespace Spa
-
-namespace LicmTransformation
-
-open Forward
-
-/-- An assignment found inside a loop, paired with the data needed to test its
-invariance against that (immediately enclosing) loop. -/
-structure Candidate (prog : Program) where
-  /-- The enclosing `whileLoop`'s tag (for reporting). -/
-  loopId : prog.NodeId
-  /-- Every node id inside the loop body (the "is-child-of-loop" set). -/
-  bodyIds : List prog.NodeId
-  /-- The assignment `BasicStmt`'s tag — what labels its CFG node. -/
-  assignId : prog.NodeId
-  /-- The variables read by the assignment's RHS. -/
-  rhsVars : List String
-
-/-- Collect every assignment together with its *immediately enclosing* loop.
-`enclosing` carries the current loop's tag and body id-set, or `none` outside any
-loop (in which case assignments are skipped — only in-loop assignments are
-candidates). -/
-def collectCandidates (prog : Program) (enc : Option (prog.NodeId × List prog.NodeId)) :
-    Stmt.Tagged prog.NodeId → List (Candidate prog)
-  | .basic _ bs =>
-      match bs, enc with
-      | .assign t _ e, some (loopId, bodyIds) =>
-          [{ loopId := loopId, bodyIds := bodyIds, assignId := t,
-             rhsVars := e.erase.vars.sort (· ≤ ·) }]
-      | _, _ => []
-  | .andThen _ a b => collectCandidates prog enc a ++ collectCandidates prog enc b
-  | .ifElse _ _ a b => collectCandidates prog enc a ++ collectCandidates prog enc b
-  | .whileLoop loopT _ body =>
-      collectCandidates prog (some (loopT, body.subtreeIds)) body
-
-/-- Read the definition set assigned to variable `k`, or `⊥` if absent. -/
-def lookupDef (prog : Program) (vs : VariableValues (DefSet prog) prog)
-    (k : String) : DefSet prog :=
-  if h : FiniteMap.MemKey k vs then (FiniteMap.locate h).1 else ⊥
-
-/-- The AST node ids marked as definition sites in a `DefSet`. With the
-`Finset`-of-AST-ids lattice these are just the elements of the set. -/
-def defSites (prog : Program) (d : DefSet prog) : List prog.NodeId :=
-  (List.finRange prog.size).filter (fun i => decide (i ∈ d))
-
-/-- Is the candidate assignment loop-invariant: do all reaching definitions of
-its RHS variables lie outside the loop body? Reaching sets are now keyed by AST
-node id, so we compare against the loop-body ids directly (embedding the raw
-body ids into `p.NodeId`). -/
-def isInvariant (prog : Program) (c : Candidate prog) : Bool :=
-  match prog.stateOfNodeId c.assignId with
-  | none => false
-  | some s =>
-      let entry := joinForKey s (result (DefSet prog) prog)
-      let combined : DefSet prog :=
-        c.rhsVars.foldl (fun acc k => acc ⊔ lookupDef prog entry k) ⊥
-      (defSites prog combined).all (fun nid => ! decide (nid ∈ c.bodyIds))
-
-/-- The loop-invariant assignments of `prog`, as `(loopId, assignId)` pairs. -/
-def licmCandidates (prog : Program) : List (prog.NodeId × prog.NodeId) :=
-  (collectCandidates prog none prog.taggedFin).filterMap (fun c =>
-    if isInvariant prog c then some (c.loopId, c.assignId) else none)
-
-/-- A human-readable report of the loop-invariant assignments. -/
-def output (prog : Program) : String :=
-  match licmCandidates prog with
-  | [] => "no loop-invariant assignments found"
-  | cands =>
-      "loop-invariant assignments (loop ↦ assignment):\n" ++
-        String.intercalate "\n"
-          (cands.map (fun p => s!"  loop #{p.1.val}: assignment #{p.2.val}"))
-
-end LicmTransformation
-
-end Spa