Make FiniteHeightLattice extend Lattice and derive Top/Bot

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

lean/Spa.lean

@@ -6,6 +6,7 @@ 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

lean/Spa/Analysis/Constant.lean

@@ -27,13 +27,13 @@ def minus : ConstLattice → ConstLattice → ConstLattice
   | _, top => top
   | mk z₁, mk z₂ => mk (z₁ - z₂)
 
-theorem plus_mono₂ : Monotone₂ plus :=
+lemma plus_mono₂ : Monotone₂ plus :=
   AboveBelow.monotone₂_of_strict plus
     (fun y => by cases y <;> rfl) (fun x => by cases x <;> rfl)
     (fun y hy => by cases y <;> first | exact absurd rfl hy | rfl)
     (fun x hx => by cases x <;> first | exact absurd rfl hx | rfl)
 
-theorem minus_mono₂ : Monotone₂ minus :=
+lemma minus_mono₂ : Monotone₂ minus :=
   AboveBelow.monotone₂_of_strict minus
     (fun y => by cases y <;> rfl) (fun x => by cases x <;> rfl)
     (fun y hy => by cases y <;> first | exact absurd rfl hy | rfl)
@@ -44,7 +44,7 @@ def interpConst : ConstLattice → Value → Prop
   | .top, _ => True
   | .mk z, v => v = .int z
 
-theorem interpConst_mk_disjoint {z₁ z₂ : ℤ} (hne : z₁ ≠ z₂) {v : Value} :
+lemma 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₂
@@ -65,7 +65,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
 
-theorem eval_mono (e : Expr) : Monotone (eval prog e) := by
+lemma eval_mono (e : Expr) : Monotone (eval prog e) := by
   induction e with
   | add e₁ e₂ ih₁ ih₂ =>
     intro vs₁ vs₂ h
@@ -77,12 +77,12 @@ theorem 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),
-          dif_pos (FiniteMap.memKey_iff.mpr hk)]
+    · rw [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)),
-          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))]
   | num n =>
     intro vs₁ vs₂ _
     exact le_refl _
@@ -93,7 +93,7 @@ instance exprEvaluator : ExprEvaluator ConstLattice prog :=
 def output : String :=
   show' (result ConstLattice prog)
 
-theorem plus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ}
+lemma 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₁
@@ -110,7 +110,7 @@ theorem plus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ}
       show Value.int (z₁ + z₂) = Value.int (c₁ + c₂)
       rw [hz₁, hz₂]
 
-theorem minus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ}
+lemma 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₁

lean/Spa/Analysis/Forward.lean

@@ -7,13 +7,13 @@ 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 :=
   (prog.code s).foldl (fun vs bs => E.eval s bs vs) (variablesAt s sv)
 
-theorem updateVariablesForState_mono (s : prog.State) :
+lemma updateVariablesForState_mono (s : prog.State) :
     Monotone (updateVariablesForState (L := L) s) := fun _ _ hle =>
   foldl_mono' (prog.code s) _ (E.eval_mono s ·) (variablesAt_le hle s)
 
@@ -21,24 +21,22 @@ def updateAll (sv : StateVariables L prog) : StateVariables L prog :=
   FiniteMap.generalizedUpdate id updateVariablesForState
     prog.states sv
 
-theorem updateAll_mono : Monotone (updateAll (L := L) (prog := prog)) :=
+lemma updateAll_mono : Monotone (updateAll (L := L) (prog := prog)) :=
   FiniteMap.generalizedUpdate_monotone monotone_id updateVariablesForState_mono
 
-theorem updateAll_mem_eq {s : prog.State} {vs : VariableValues L prog}
+lemma 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
 
-theorem variablesAt_updateAll (s : prog.State) (sv : StateVariables L prog) :
+lemma 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)
 
-theorem analyze_mono : Monotone (analyze (L := L) (prog := prog)) := fun _ _ hle =>
+lemma analyze_mono : Monotone (analyze (L := L) (prog := prog)) := fun _ _ hle =>
   updateAll_mono (joinAll_mono hle)
 
 variable [DecidableEq L]
@@ -48,18 +46,18 @@ def result : StateVariables L prog :=
   Fixedpoint.aFix analyze analyze_mono
 
 variable (L prog) in
-theorem result_eq : result L prog = analyze (result L prog) :=
+lemma result_eq : result L prog = analyze (result L prog) :=
   Fixedpoint.aFix_eq analyze analyze_mono
 
-theorem joinForKey_initialState :
+lemma joinForKey_initialState :
     joinForKey prog.initialState (result L prog) = botV L prog := by
   rw [joinForKey, prog.incoming_initialState_eq_nil]
   rfl
 
 variable [I : LatticeInterpretation L] [V : ValidStmtEvaluator L prog]
 
-omit [FiniteHeightLattice L] [DecidableEq L] in
-theorem eval_fold_valid {s : prog.State} {bss : List BasicStmt}
+omit [DecidableEq L] in
+lemma eval_fold_valid {s : prog.State} {bss : List BasicStmt}
     {vs : VariableValues L prog} {ρ₁ ρ₂ : Env}
     (hbss : EvalBasicStmts ρ₁ bss ρ₂) (hvs : ⟦ vs ⟧ ρ₁) :
     ⟦ bss.foldl (fun vs bs => E.eval s bs vs) vs ⟧ ρ₂ := by
@@ -67,23 +65,23 @@ theorem eval_fold_valid {s : prog.State} {bss : List BasicStmt}
   | nil => exact hvs
   | cons hbs _ ih => exact ih (ValidStmtEvaluator.valid hbs hvs)
 
-omit [FiniteHeightLattice L] [DecidableEq L] in
-theorem updateVariablesForState_matches {s : prog.State}
+omit [DecidableEq L] in
+lemma 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 [FiniteHeightLattice L] [DecidableEq L] in
-theorem updateAll_matches {s : prog.State} {sv : StateVariables L prog}
+omit [DecidableEq L] in
+lemma updateAll_matches {s : prog.State} {sv : StateVariables L prog}
     {ρ₁ ρ₂ : Env} (hbss : EvalBasicStmts ρ₁ (prog.code s) ρ₂)
     (hvs : ⟦ variablesAt s sv ⟧ ρ₁) :
     ⟦ variablesAt s (updateAll sv) ⟧ ρ₂ := by
   rw [variablesAt_updateAll]
   exact updateVariablesForState_matches hbss hvs
 
-theorem stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env}
+lemma stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env}
     (hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁)
     (hbss : EvalBasicStmts ρ₁ (prog.code s₁) ρ₂) :
     ⟦ variablesAt s₁ (result L prog) ⟧ ρ₂ := by
@@ -92,9 +90,9 @@ theorem stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env}
   rw [variablesAt_joinAll]
   exact hjoin
 
-theorem walkTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
+lemma walkTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
     (hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁)
-    (tr : Trace prog.graph s₁ s₂ ρ₁ ρ₂) :
+    (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) :
     ⟦ variablesAt s₂ (result L prog) ⟧ ρ₂ := by
   induction tr with
   | single hbss => exact stepTrace hjoin hbss
@@ -108,7 +106,7 @@ theorem walkTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
     exact ih (interp_foldr hstep hmem)
 
 omit V in
-theorem interp_joinForKey_initialState :
+lemma interp_joinForKey_initialState :
     ⟦ joinForKey prog.initialState (result L prog) ⟧ [] := by
   rw [joinForKey_initialState]
   exact interp_botV_nil

lean/Spa/Analysis/Forward/Adapters.lean

@@ -10,24 +10,24 @@ def updateVariablesFromExpression (k : String) (e : Expr)
     (vs : VariableValues L prog) : VariableValues L prog :=
   FiniteMap.generalizedUpdate id (fun _ vs => E.eval e vs) [k] vs
 
-theorem updateVariablesFromExpression_mono (k : String) (e : Expr) :
+lemma 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 evalB (_ : prog.State) (bs : BasicStmt)
+def evalBasicStmt (_ : prog.State) (bs : BasicStmt)
     (vs : VariableValues L prog) : VariableValues L prog :=
   match bs with
   | .assign k e => updateVariablesFromExpression k e vs
   | .noop => vs
 
-theorem evalB_mono (s : prog.State) (bs : BasicStmt) :
-    Monotone (evalB (L := L) (prog := prog) s bs) := by
+lemma evalBasicStmt_mono (s : prog.State) (bs : BasicStmt) :
+    Monotone (evalBasicStmt (L := L) (prog := prog) s bs) := by
   cases bs with
   | assign k e => exact updateVariablesFromExpression_mono k e
   | noop => exact monotone_id
 
 instance ExprEvaluator.toStmtEvaluator : StmtEvaluator L prog :=
-  ⟨evalB, evalB_mono⟩
+  ⟨evalBasicStmt, evalBasicStmt_mono⟩
 
 instance ExprEvaluator.toStmtEvaluator_valid [LatticeInterpretation L]
     [ValidExprEvaluator L prog] : ValidStmtEvaluator L prog := by

lean/Spa/Analysis/Forward/Lattices.lean

@@ -18,20 +18,20 @@ def botV [FiniteHeightLattice L] : VariableValues L prog :=
 variable {L prog}
 
 omit [Lattice L] in
-theorem states_memKey (s : prog.State) (sv : StateVariables L prog) :
+lemma 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
-theorem variablesAt_mem (s : prog.State) (sv : StateVariables L prog) :
+lemma variablesAt_mem (s : prog.State) (sv : StateVariables L prog) :
     (s, variablesAt s sv) ∈ sv :=
   (FiniteMap.locate (states_memKey s sv)).2
 
-theorem variablesAt_le {sv₁ sv₂ : StateVariables L prog} (hle : sv₁ ≤ sv₂)
+lemma 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 +42,7 @@ def joinForKey (k : prog.State) (sv : StateVariables L prog) :
     VariableValues L prog :=
   (sv.valuesAt (prog.incoming k)).foldr (· ⊔ ·) (botV L prog)
 
-theorem joinForKey_mono (k : prog.State) :
+lemma 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,15 +52,15 @@ theorem joinForKey_mono (k : prog.State) :
 def joinAll (sv : StateVariables L prog) : StateVariables L prog :=
   FiniteMap.generalizedUpdate id joinForKey prog.states sv
 
-theorem joinAll_mono : Monotone (joinAll (L := L) (prog := prog)) :=
+lemma joinAll_mono : Monotone (joinAll (L := L) (prog := prog)) :=
   FiniteMap.generalizedUpdate_monotone monotone_id joinForKey_mono
 
-theorem joinAll_mem_eq {s : prog.State} {vs : VariableValues L prog}
+lemma 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
 
-theorem variablesAt_joinAll (s : prog.State) (sv : StateVariables L prog) :
+lemma variablesAt_joinAll (s : prog.State) (sv : StateVariables L prog) :
     variablesAt s (joinAll sv) = joinForKey s sv :=
   joinAll_mem_eq (variablesAt_mem s (joinAll sv))
 
@@ -74,12 +74,12 @@ instance : Interp (VariableValues L prog) (Env → Prop) where
     ∀ (k : String) (l : L), (k, l) ∈ vs →
       ∀ (v : Value), Env.Mem (k, v) ρ → I.interp l v
 
-theorem interp_botV_nil : ⟦ botV L prog ⟧ [] := by
+lemma interp_botV_nil : ⟦ botV L prog ⟧ [] := by
   intro k l _ v hmem
   cases hmem
 
 omit [FiniteHeightLattice L] in
-theorem interp_sup {vs₁ vs₂ : VariableValues L prog} {ρ : Env}
+lemma interp_sup {vs₁ vs₂ : VariableValues L prog} {ρ : Env}
     (h : ⟦ vs₁⟧ ρ ∨ ⟦ vs₂ ⟧ ρ) : ⟦ vs₁ ⊔ vs₂ ⟧ ρ := by
   intro k l hmem v hv
   obtain ⟨l₁, l₂, rfl, h₁, h₂⟩ := FiniteMap.mem_sup hmem
@@ -87,7 +87,7 @@ theorem interp_sup {vs₁ vs₂ : VariableValues L prog} {ρ : Env}
   · 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}
+lemma interp_foldr {vs : VariableValues L prog}
     {vss : List (VariableValues L prog)} {ρ : Env}
     (hvs : ⟦ vs ⟧ ρ) (hmem : vs ∈ vss) :
     ⟦ vss.foldr (· ⊔ ·) (botV L prog) ⟧ ρ := by

lean/Spa/Analysis/Reaching.lean

@@ -0,0 +1,41 @@
+import Spa.Analysis.Forward
+import Spa.Lattice.Bool
+import Spa.Showable
+
+namespace Spa
+
+open Forward
+
+instance : Showable Bool := ⟨fun b => if b then "true" else "false"⟩
+
+abbrev DefSet (prog : Program) : Type := FiniteMap prog.State Bool prog.states
+
+namespace ReachingAnalysis
+
+variable (prog : Program)
+
+def genSet (s : prog.State) : DefSet prog :=
+  FiniteMap.updating (⊥ : DefSet prog) [s] (fun _ => true)
+
+def eval (s : prog.State) :
+    BasicStmt → VariableValues (DefSet prog) prog → VariableValues (DefSet prog) prog
+  | .assign k _, vs =>
+    FiniteMap.generalizedUpdate id (fun _ _ => genSet prog s) [k] vs
+  | .noop, vs => vs
+
+lemma eval_mono (s : prog.State) (bs : BasicStmt) :
+    Monotone (eval prog s bs) := by
+  cases bs with
+  | assign k e =>
+    exact FiniteMap.generalizedUpdate_monotone monotone_id (fun _ => monotone_const)
+  | noop => exact monotone_id
+
+instance stmtEvaluator : StmtEvaluator (DefSet prog) prog :=
+  ⟨eval prog, eval_mono prog⟩
+
+def output : String :=
+  show' (result (DefSet prog) prog)
+
+end ReachingAnalysis
+
+end Spa

lean/Spa/Analysis/Sign.lean

@@ -55,7 +55,7 @@ def minus : SignLattice → SignLattice → SignLattice
   | mk .zero, mk .minus => mk .plus
   | mk .zero, mk .zero => mk .zero
 
-theorem plus_mono₂ : Monotone₂ plus :=
+lemma plus_mono₂ : Monotone₂ plus :=
   AboveBelow.monotone₂_of_strict plus
     (fun y => by cases y <;> rfl)
     (fun x => by rcases x with _ | _ | s <;> first | rfl | (cases s <;> rfl))
@@ -64,7 +64,7 @@ theorem plus_mono₂ : Monotone₂ plus :=
       rcases x with _ | _ | s <;>
         first | exact absurd rfl hx | rfl | (cases s <;> rfl))
 
-theorem minus_mono₂ : Monotone₂ minus :=
+lemma minus_mono₂ : Monotone₂ minus :=
   AboveBelow.monotone₂_of_strict minus
     (fun y => by cases y <;> rfl)
     (fun x => by rcases x with _ | _ | s <;> first | rfl | (cases s <;> rfl))
@@ -80,7 +80,7 @@ def interpSign : SignLattice → Value → Prop
   | .mk .zero, v => v = .int 0
   | .mk .minus, v => ∃ n : ℕ, v = .int (-(n + 1))
 
-theorem interpSign_mk_disjoint {s₁ s₂ : Sign} (hne : s₁ ≠ s₂) {v : Value} :
+lemma 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
@@ -125,7 +125,7 @@ def eval : Expr → VariableValues SignLattice prog → SignLattice
   | .num 0, _ => .mk .zero
   | .num (_ + 1), _ => .mk .plus
 
-theorem eval_mono (e : Expr) : Monotone (eval prog e) := by
+lemma eval_mono (e : Expr) : Monotone (eval prog e) := by
   induction e with
   | add e₁ e₂ ih₁ ih₂ =>
     intro vs₁ vs₂ h
@@ -137,12 +137,12 @@ theorem 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),
-          dif_pos (FiniteMap.memKey_iff.mpr hk)]
+    · rw [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)),
-          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))]
   | num n =>
     intro vs₁ vs₂ _
     cases n <;> exact le_refl _
@@ -154,18 +154,18 @@ def output : String :=
   show' (result SignLattice prog)
 
 /-- A nonneg-shifted interpretation `∃ n : ℕ, z = n + 1` just means `z` is positive. -/
-private theorem int_pos_iff (z : ℤ) : (∃ n : ℕ, z = (n : ℤ) + 1) ↔ 0 < z := by
+private lemma int_pos_iff (z : ℤ) : (∃ n : ℕ, z = (n : ℤ) + 1) ↔ 0 < z := by
   constructor
   · rintro ⟨n, rfl⟩; omega
   · intro h; exact ⟨(z - 1).toNat, by omega⟩
 
 /-- Dually, `∃ n : ℕ, z = -(n + 1)` just means `z` is negative. -/
-private theorem int_neg_iff (z : ℤ) : (∃ n : ℕ, z = -((n : ℤ) + 1)) ↔ z < 0 := by
+private lemma int_neg_iff (z : ℤ) : (∃ n : ℕ, z = -((n : ℤ) + 1)) ↔ z < 0 := by
   constructor
   · rintro ⟨n, rfl⟩; omega
   · intro h; exact ⟨(-z - 1).toNat, by omega⟩
 
-theorem plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
+lemma 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₂ <;>
@@ -174,7 +174,7 @@ theorem plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
       at h₁ h₂ ⊢ <;>
     omega
 
-theorem minus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
+lemma 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₂ <;>

lean/Spa/Analysis/Utils.lean

@@ -2,7 +2,7 @@ import Spa.Lattice
 
 namespace Spa
 
-theorem eval_combine₂ {O : Type*} [Preorder O] {combine : O → O → O}
+lemma 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

@@ -6,13 +6,13 @@ namespace Fixedpoint
 
 open FiniteHeightLattice (height)
 
-variable {α : Type*} [Lattice α] [DecidableEq α] [FiniteHeightLattice α]
+variable {α : Type*} [DecidableEq α] [FiniteHeightLattice α]
 
 def doStep (f : α → α) (hf : Monotone f) :
     ∀ (g : ℕ) (c : LTSeries α), c.length + g = height (α := α) + 1 →
       c.last ≤ f c.last → {a : α // a = f a}
   | 0, c, hlen, _ =>
-    absurd (FiniteHeightLattice.chains_bounded c) (by omega)
+    absurd (FiniteHeightLattice.chains_bounded c) (by simp only [height] at hlen; omega)
   | g + 1, c, hlen, hle =>
     if heq : c.last = f c.last then
       ⟨c.last, heq⟩
@@ -34,12 +34,13 @@ theorem aFix_eq (f : α → α) (hf : Monotone f) :
     aFix f hf = f (aFix f hf) :=
   (fix f hf).2
 
-theorem doStep_le (f : α → α) (hf : Monotone f)
+lemma doStep_le (f : α → α) (hf : Monotone f)
     {b : α} (hb : b = f b) :
     ∀ (g : ℕ) (c : LTSeries α) (hlen : c.length + g = height (α := α) + 1)
       (hle : c.last ≤ f c.last), c.last ≤ b →
       (doStep f hf g c hlen hle : α) ≤ b
-  | 0, c, hlen, _ => fun _ => absurd (FiniteHeightLattice.chains_bounded c) (by omega)
+  | 0, c, hlen, _ => fun _ =>
+    absurd (FiniteHeightLattice.chains_bounded c) (by simp only [height] at hlen; omega)
   | g + 1, c, hlen, hle => fun hcb => by
     rw [doStep]
     split

lean/Spa/Interp.lean

@@ -1,7 +1,17 @@
 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

@@ -2,20 +2,14 @@ import Spa.Lattice
 
 namespace Spa
 
-def FiniteHeightLattice.transport {α β : Type*} [Lattice α] [Lattice β]
+def FiniteHeightLattice.transport {α β : Type*} [Lattice β]
     [I : FiniteHeightLattice α] (f : α → β) (g : β → α)
     (hf : Monotone f) (hg : Monotone g)
     (hgf : Function.LeftInverse g f) (hfg : Function.LeftInverse f g) :
     FiniteHeightLattice β where
-  bot := f ⊥
-  top := f ⊤
-  height := I.height
+  toLattice := inferInstance
   longestChain :=
-    { series :=
-        I.longestChain.series.map f (hf.strictMono_of_injective hgf.injective)
-      head_series := congrArg f I.longestChain.head_series
-      last_series := congrArg f I.longestChain.last_series
-      length_series := I.longestChain.length_series }
+    I.longestChain.map f (hf.strictMono_of_injective hgf.injective)
   chains_bounded := fun c =>
     I.chains_bounded (c.map g (hg.strictMono_of_injective hfg.injective))
 

lean/Spa/Language.lean

@@ -15,17 +15,17 @@ namespace Program
 
 variable (p : Program)
 
-def graph : Graph := Graph.wrap (buildCfg p.rootStmt)
+def cfg : Graph := Graph.wrap p.rootStmt.cfg
 
-abbrev State : Type := p.graph.Index
+abbrev State : Type := p.cfg.Index
 
-def initialState : p.State := (buildCfg p.rootStmt).wrapInput
+def initialState : p.State := p.rootStmt.cfg.wrapInput
 
-def finalState : p.State := (buildCfg p.rootStmt).wrapOutput
+def finalState : p.State := p.rootStmt.cfg.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)
+    Trace p.cfg p.initialState p.finalState [] ρ := by
+  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₂
@@ -33,25 +33,25 @@ theorem trace {ρ : Env} (h : EvalStmt [] p.rootStmt ρ) :
 
 def vars : List String := p.rootStmt.vars.sort (· ≤ ·)
 
-theorem vars_nodup : p.vars.Nodup := Finset.sort_nodup _ _
+lemma vars_nodup : p.vars.Nodup := Finset.sort_nodup _ _
 
-def states : List p.State := p.graph.indices
+def states : List p.State := p.cfg.indices
 
-theorem states_complete (s : p.State) : s ∈ p.states := p.graph.mem_indices s
+lemma states_complete (s : p.State) : s ∈ p.states := p.cfg.mem_indices s
 
-theorem states_nodup : p.states.Nodup := p.graph.nodup_indices
+lemma states_nodup : p.states.Nodup := p.cfg.nodup_indices
 
-def code (st : p.State) : List BasicStmt := p.graph.nodes st
+def code (st : p.State) : List BasicStmt := p.cfg.nodes st
 
-def incoming (s : p.State) : List p.State := p.graph.predecessors s
+def incoming (s : p.State) : List p.State := p.cfg.predecessors s
 
-theorem incoming_initialState_eq_nil : p.incoming p.initialState = [] :=
-  Graph.wrap_predecessors_eq_nil (buildCfg p.rootStmt) p.initialState
+lemma incoming_initialState_eq_nil : p.incoming p.initialState = [] :=
+  Graph.wrap_predecessors_eq_nil p.rootStmt.cfg 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
+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
 
 end Program
 

lean/Spa/Language/Base.lean

@@ -1,7 +1,19 @@
 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)
@@ -9,11 +21,15 @@ 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)
@@ -21,34 +37,23 @@ inductive Stmt where
   | whileLoop (e : Expr) (s : Stmt)
   deriving DecidableEq
 
-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)
-
+/-- Variables mentioned in this expression. -/
 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,45 +3,104 @@ 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.
+
+-/
+
+/-- 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
 
-structure Graph where
+/-- Graph with general (`α`-labeled) nodes. By using a tuple `Fin size → α`
+    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 → List BasicStmt
+  nodes : Fin size → α
   edges : List (Fin size × Fin size)
   inputs : List (Fin size)
   outputs : List (Fin size)
 
-namespace Graph
+namespace GGraph
 
-abbrev Index (g : Graph) : Type := Fin g.size
+variable {α β : Type}
 
-abbrev Edge (g : Graph) : Type := g.Index × g.Index
+/-- An index (node) in the CFG. -/
+abbrev Index (g : GGraph α) : Type := Fin g.size
 
-def comp (g₁ g₂ : Graph) : Graph where
+/-- An edge in the CFG. -/
+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 " ∙ " => Graph.comp
+@[inherit_doc] scoped infixr:70 " ∙ " => GGraph.overlay
 
-def link (g₁ g₂ : Graph) : Graph where
+/-- Sequence two CFGs: create a combined graph whose nodes and edges come
+    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 ++
@@ -49,74 +108,140 @@ def link (g₁ g₂ : Graph) : Graph where
   inputs := g₁.inputs.finCastAdd g₂.size
   outputs := g₂.outputs.finNatAdd g₁.size
 
-@[inherit_doc] scoped infixr:70 " ⤳ " => Graph.link
+@[inherit_doc] scoped infixr:70 " ⤳ " => GGraph.sequence
 
-/-- The entry node of a `loop` graph. -/
-def loopIn (g : Graph) : Fin (2 + g.size) := (0 : Fin 2).castAdd g.size
+/-- When a graph `g` is wrapped in a `loop`, the index / node corresponding
+    to the input of the new loop. -/
+def loopIn (g : GGraph α) : Fin (2 + g.size) := (0 : Fin 2).castAdd g.size
 
-/-- The exit node of a `loop` graph. -/
-def loopOut (g : Graph) : Fin (2 + g.size) := (1 : Fin 2).castAdd g.size
+/-- When a graph `g` is wrapped in a `loop`, the index / node corresponding
+    to the output of the new loop. -/
+def loopOut (g : GGraph α) : Fin (2 + g.size) := (1 : Fin 2).castAdd g.size
 
-def loop (g : Graph) : Graph where
+/-- Creates a zero-or-more loop loop in the CFG: connects all the output
+    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 (List β)) : GGraph (List β) where
   size := 2 + g.size
   nodes := Fin.append (fun _ : Fin 2 => []) g.nodes
   edges := g.edges.finNatAddProd 2 ++
-    (g.inputs.finNatAdd 2).map (g.loopIn, ·) ++
-    (g.outputs.finNatAdd 2).map (·, g.loopOut) ++
+    ((g.loopIn, ·) <$> g.inputs.finNatAdd 2)  ++
+    ((·, g.loopOut) <$> g.outputs.finNatAdd 2) ++
     [(g.loopOut, g.loopIn), (g.loopIn, g.loopOut)]
   inputs := [g.loopIn]
   outputs := [g.loopOut]
 
-@[simp] theorem loop_inputs (g : Graph) : (loop g).inputs = [g.loopIn] := rfl
+@[simp] lemma loop_inputs (g : GGraph (List β)) : (loop g).inputs = [g.loopIn] := rfl
 
-@[simp] theorem loop_outputs (g : Graph) : (loop g).outputs = [g.loopOut] := rfl
+@[simp] lemma loop_outputs (g : GGraph (List β)) : (loop g).outputs = [g.loopOut] := rfl
 
-def skipto (g₁ g₂ : Graph) : Graph 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
+/-- Creates a single-node graph whose node contains the given value. -/
+def singleton (a : α) : GGraph α where
   size := 1
-  nodes := fun _ => bss
+  nodes := fun _ => a
   edges := []
   inputs := [0]
   outputs := [0]
 
-def wrap (g : Graph) : Graph :=
+/-- Creates a new graph with a single input and single output node. Useful to ensure there's
+    a single point of entry and single point of exit. -/
+def wrap (g : GGraph (List β)) : GGraph (List β) :=
   singleton [] ⤳ g ⤳ singleton []
 
-variable (g : Graph)
+@[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 (List β)) :
+    (List.map h) <$> (loop g) = loop (List.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 (List β)) :
+    (List.map h) <$> wrap g = wrap (List.map h <$> g) := by
+  simp [GGraph.wrap, GGraph.map_sequence, GGraph.map_singleton]
+
+variable (g : GGraph α)
+
+/-- All the nodes in the graph. -/
 def indices : List g.Index := List.finRange g.size
 
-theorem mem_indices (idx : g.Index) : idx ∈ g.indices :=
+/-- All of the graph's indices are listed in `indices`. -/
+lemma mem_indices (idx : g.Index) : idx ∈ g.indices :=
   List.mem_finRange idx
 
-theorem nodup_indices : g.indices.Nodup :=
+/-- `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)
 
-theorem mem_predecessors_of_edge {idx₁ idx₂ : g.Index}
+/-- 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⟩
 
-theorem edge_of_mem_predecessors {idx₁ idx₂ : g.Index}
+/-- 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 blocks in their nodes, and nothing else. -/
+abbrev Graph : Type := GGraph (List BasicStmt)
+
+namespace Graph
+
+export GGraph (overlay sequence loop singleton wrap loop_inputs loop_outputs)
+
+@[inherit_doc] scoped infixr:70 " ∙ " => GGraph.overlay
+@[inherit_doc] scoped infixr:70 " ⤳ " => GGraph.sequence
+
 end Graph
 
 open Graph in
-def buildCfg : Stmt → Graph
-  | .basic bs => Graph.singleton [bs]
-  | .andThen s₁ s₂ => buildCfg s₁ ⤳ buildCfg s₂
-  | .ifElse _ s₁ s₂ => buildCfg s₁ ∙ buildCfg s₂
-  | .whileLoop _ s => Graph.loop (buildCfg s)
+def Stmt.cfg : Stmt → Graph
+  -- A basic statement goes into a single basic block
+  | .basic bs => singleton [bs]
+  -- Sequencing of statements corresponds naturally to CFG sequencing
+  | .andThen s₁ s₂ => s₁.cfg ⤳  s₂.cfg
+  -- An if can execute either one branch or the other; overlap them.
+  -- Subsequent sequencing (etc.) will end up creating the forks and joins.
+  | .ifElse _ s₁ s₂ => s₁.cfg ∙ s₂.cfg
+  -- The `loop` construct was developed specifically for zero-or-more loops like this.
+  | .whileLoop _ s => loop s.cfg
 
 end Spa

lean/Spa/Language/Properties.lean

@@ -4,7 +4,7 @@ namespace Spa
 
 open Graph
 
-theorem Fin.castAdd_ne_natAdd {n m : ℕ} (i : Fin n) (j : Fin m) :
+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
@@ -17,7 +17,7 @@ section Embeddings
 
 variable {g₁ g₂ : Graph} {ρ₁ ρ₂ : Env}
 
-theorem Trace.comp_left {idx₁ idx₂ : g₁.Index}
+lemma Trace.overlay_left {idx₁ idx₂ : g₁.Index}
     (tr : Trace g₁ idx₁ idx₂ ρ₁ ρ₂) :
     Trace (g₁ ∙ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by
   induction tr with
@@ -29,7 +29,7 @@ theorem Trace.comp_left {idx₁ idx₂ : g₁.Index}
     · rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_left]
     · exact List.mem_append_left _ (List.mem_map_of_mem _ he)
 
-theorem Trace.comp_right {idx₁ idx₂ : g₂.Index}
+lemma Trace.overlay_right {idx₁ idx₂ : g₂.Index}
     (tr : Trace g₂ idx₁ idx₂ ρ₁ ρ₂) :
     Trace (g₁ ∙ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ := by
   induction tr with
@@ -41,7 +41,7 @@ theorem Trace.comp_right {idx₁ idx₂ : g₂.Index}
     · rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_right]
     · exact List.mem_append_right _ (List.mem_map_of_mem _ he)
 
-theorem Trace.link_left {idx₁ idx₂ : g₁.Index}
+lemma Trace.sequence_left {idx₁ idx₂ : g₁.Index}
     (tr : Trace g₁ idx₁ idx₂ ρ₁ ρ₂) :
     Trace (g₁ ⤳ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by
   induction tr with
@@ -53,7 +53,7 @@ theorem Trace.link_left {idx₁ idx₂ : g₁.Index}
     · rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_left]
     · exact List.mem_append_left _ (List.mem_append_left _ (List.mem_map_of_mem _ he))
 
-theorem Trace.link_right {idx₁ idx₂ : g₂.Index}
+lemma Trace.sequence_right {idx₁ idx₂ : g₂.Index}
     (tr : Trace g₂ idx₁ idx₂ ρ₁ ρ₂) :
     Trace (g₁ ⤳ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ := by
   induction tr with
@@ -66,27 +66,27 @@ theorem Trace.link_right {idx₁ idx₂ : g₂.Index}
     · exact List.mem_append_left _
         (List.mem_append_right _ (List.mem_map_of_mem _ he))
 
-theorem EndToEndTrace.comp_left (etr : EndToEndTrace g₁ ρ₁ ρ₂) :
+lemma 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.comp_left⟩
+         tr.overlay_left⟩
 
-theorem EndToEndTrace.comp_right (etr : EndToEndTrace g₂ ρ₁ ρ₂) :
+lemma 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.comp_right⟩
+         tr.overlay_right⟩
 
-theorem EndToEndTrace.concat {ρ₃ : Env} (etr₁ : EndToEndTrace g₁ ρ₁ ρ₂)
+lemma 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₂,
-          Trace.concat tr₁.link_left ?_ tr₂.link_right⟩
+          Trace.concat tr₁.sequence_left ?_ tr₂.sequence_right⟩
   exact List.mem_append_right _
     (List.mem_product.mpr ⟨List.mem_map_of_mem _ h₂, List.mem_map_of_mem _ k₁⟩)
 
@@ -98,7 +98,7 @@ section Loop
 
 variable {g : Graph} {ρ₁ ρ₂ ρ₃ : Env}
 
-theorem Trace.loop {idx₁ idx₂ : g.Index} (tr : Trace g idx₁ idx₂ ρ₁ ρ₂) :
+lemma Trace.loop {idx₁ idx₂ : g.Index} (tr : Trace g idx₁ idx₂ ρ₁ ρ₂) :
     Trace (Graph.loop g) (idx₁.natAdd 2) (idx₂.natAdd 2) ρ₁ ρ₂ := by
   induction tr with
   | single hbs =>
@@ -112,15 +112,15 @@ theorem Trace.loop {idx₁ idx₂ : g.Index} (tr : Trace g idx₁ idx₂ ρ₁
     · exact List.mem_append_left _ (List.mem_append_left _
         (List.mem_append_left _ (List.mem_map_of_mem _ he)))
 
-private theorem loop_nodes_at_in :
+private lemma loop_nodes_at_in :
     (Graph.loop g).nodes g.loopIn = [] :=
   Fin.append_left (fun _ : Fin 2 => []) g.nodes 0
 
-private theorem loop_nodes_at_out :
+private lemma loop_nodes_at_out :
     (Graph.loop g).nodes g.loopOut = [] :=
   Fin.append_left (fun _ : Fin 2 => []) g.nodes 1
 
-theorem EndToEndTrace.loop (etr : EndToEndTrace g ρ₁ ρ₂) :
+lemma 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
@@ -135,12 +135,12 @@ theorem EndToEndTrace.loop (etr : EndToEndTrace g ρ₁ ρ₂) :
   exact Trace.concat (Trace.single (loop_nodes_at_in ▸ EvalBasicStmts.nil)) hin
     (Trace.concat tr.loop hout (Trace.single (loop_nodes_at_out ▸ EvalBasicStmts.nil)))
 
-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 _ _
 
-theorem EndToEndTrace.loop_concat (etr₁ : EndToEndTrace (Graph.loop g) ρ₁ ρ₂)
+lemma 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,7 +150,7 @@ theorem EndToEndTrace.loop_concat (etr₁ : EndToEndTrace (Graph.loop g) ρ₁
   exact ⟨g.loopIn, List.mem_singleton_self _, g.loopOut, List.mem_singleton_self _,
     Trace.concat tr₁ loop_edge_out_in tr₂⟩
 
-theorem EndToEndTrace.loop_empty {ρ : Env} : EndToEndTrace (Graph.loop g) ρ ρ := by
+lemma 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 _,
@@ -161,30 +161,30 @@ end Loop
 
 /-! ### Singletons, wrap, and the main result -/
 
-theorem EndToEndTrace.singleton {bss : List BasicStmt} {ρ₁ ρ₂ : Env}
+lemma 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⟩
 
-theorem EndToEndTrace.singleton_nil (ρ : Env) :
+lemma EndToEndTrace.singleton_nil (ρ : Env) :
     EndToEndTrace (Graph.singleton []) ρ ρ :=
   EndToEndTrace.singleton EvalBasicStmts.nil
 
-theorem EndToEndTrace.wrap {g : Graph} {ρ₁ ρ₂ : Env}
+lemma EndToEndTrace.wrap {g : Graph} {ρ₁ ρ₂ : Env}
     (etr : EndToEndTrace g ρ₁ ρ₂) : EndToEndTrace (Graph.wrap g) ρ₁ ρ₂ :=
   (EndToEndTrace.singleton_nil ρ₁).concat (etr.concat (EndToEndTrace.singleton_nil ρ₂))
 
-theorem buildCfg_sufficient {s : Stmt} {ρ₁ ρ₂ : Env}
-    (h : EvalStmt ρ₁ s ρ₂) : EndToEndTrace (buildCfg s) ρ₁ ρ₂ := by
+theorem Stmt.cfg_sufficient {s : Stmt} {ρ₁ ρ₂ : Env}
+    (h : EvalStmt ρ₁ s ρ₂) : EndToEndTrace s.cfg ρ₁ ρ₂ := by
   induction h with
   | basic ρ₁ ρ₂ bs 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.comp_left
+    exact ih.overlay_left
   | ifFalse ρ₁ ρ₂ e s₁ s₂ _ _ ih =>
-    exact ih.comp_right
+    exact ih.overlay_right
   | whileTrue ρ₁ ρ₂ ρ₃ e z s _ _ _ _ ih₁ ih₂ =>
     exact (ih₁.loop).loop_concat ih₂
   | whileFalse ρ e s _ =>
@@ -198,13 +198,13 @@ def Graph.wrapInput (g : Graph) : (Graph.wrap g).Index :=
 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) :
+lemma Graph.wrap_inputs (g : Graph) :
     (Graph.wrap g).inputs = [g.wrapInput] := rfl
 
-theorem Graph.wrap_outputs (g : Graph) :
+lemma Graph.wrap_outputs (g : Graph) :
     (Graph.wrap g).outputs = [g.wrapOutput] := rfl
 
-private theorem not_mem_edges_castAdd_link {g₂ : Graph} (i : Fin 1)
+private lemma not_mem_edges_castAdd_sequence {g₂ : Graph} (i : Fin 1)
     (idx : (Graph.singleton [] ⤳ g₂).Index) :
     ((idx, i.castAdd g₂.size) : (Graph.singleton [] ⤳ g₂).Edge)
       ∉ (Graph.singleton [] ⤳ g₂).edges := by
@@ -221,13 +221,13 @@ private theorem not_mem_edges_castAdd_link {g₂ : Graph} (i : Fin 1)
     obtain ⟨j, -, heq⟩ := List.mem_map.mp hb
     exact Fin.castAdd_ne_natAdd i j heq.symm
 
-theorem Graph.wrap_predecessors_eq_nil (g : Graph) (idx : (Graph.wrap g).Index)
+lemma 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]
+  rw [GGraph.predecessors, List.filter_eq_nil_iff]
   intro idx' _
-  simpa using not_mem_edges_castAdd_link (g₂ := g ⤳ Graph.singleton []) 0 idx'
+  simpa using not_mem_edges_castAdd_sequence (g₂ := g ⤳ Graph.singleton []) 0 idx'
 
 end Spa

lean/Spa/Language/Traces.lean

@@ -10,7 +10,7 @@ inductive Trace (g : Graph) : g.Index → g.Index → Env → Env → Prop
       EvalBasicStmts ρ₁ (g.nodes idx₁) ρ₂ → (idx₁, idx₂) ∈ g.edges →
       Trace g idx₂ idx₃ ρ₂ ρ₃ → Trace g idx₁ idx₃ ρ₁ ρ₃
 
-theorem Trace.concat {g : Graph} {idx₁ idx₂ idx₃ idx₄ : g.Index}
+lemma 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₄ ρ₁ ρ₃ := by

lean/Spa/Lattice.lean

@@ -1,8 +1,20 @@
 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 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 ·))
@@ -11,18 +23,20 @@ section Folds
 
 variable {α β : Type*} [Preorder α] [Preorder β]
 
-theorem foldr_mono {l₁ l₂ : List α} (f : α → β → β) {b₁ b₂ : β}
+/-- (right) folds are monotonic in both their arguments if the underlying accumulator function is. -/
+lemma foldr_mono {l₁ l₂ : List α} (f : α → β → β) {b₁ b₂ : β}
     (hl : List.Forall₂ (· ≤ ·) l₁ l₂) (hb : b₁ ≤ b₂)
-    (hf₁ : ∀ b, Monotone fun a => f a b) (hf₂ : ∀ a, Monotone (f a)) :
+    (hf₁ : ∀ b, Monotone (f · 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)
 
-theorem foldl_mono {l₁ l₂ : List α} (f : β → α → β) {b₁ b₂ : β}
+/-- (left) folds are monotinic in both their arguments if the underlying accumulator function is. -/
+lemma foldl_mono {l₁ l₂ : List α} (f : β → α → β) {b₁ b₂ : β}
     (hl : List.Forall₂ (· ≤ ·) l₁ l₂) (hb : b₁ ≤ b₂)
-    (hf₁ : ∀ a, Monotone fun b => f b a) (hf₂ : ∀ b, Monotone (f b)) :
+    (hf₁ : ∀ a, Monotone (f · a)) (hf₂ : ∀ b, Monotone (f b ·)) :
     l₁.foldl f b₁ ≤ l₂.foldl f b₂ := by
   induction hl generalizing b₁ b₂ with
   | nil => exact hb
@@ -30,15 +44,17 @@ theorem foldl_mono {l₁ l₂ : List α} (f : β → α → β) {b₁ b₂ : β}
     exact ih (le_trans (hf₁ _ hb) (hf₂ _ hxy))
 
 omit [Preorder α] in
-theorem foldr_mono' (l : List α) (f : α → β → β)
-    (hf : ∀ a, Monotone (f a ·)) : Monotone fun b => l.foldr f b := by
+/-- (right) folds on a particular list are monotonic if the underlying accumulator is monotonic in its accumulator argument. -/
+lemma foldr_mono' (l : List α) (f : α → β → β)
+    (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
-theorem foldl_mono' (l : List α) (f : β → α → β)
+/-- (left) folds on a particular list are monotonic if the underlying accumulator is monotonic in its accumulator argument. -/
+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
@@ -47,34 +63,48 @@ theorem foldl_mono' (l : List α) (f : β → α → β)
 
 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
 
-structure PointedLTSeries (α : Type*) (f t : α)(n : ℕ) [Preorder α] where
-  series : LTSeries α
-  head_series : series.head = f
-  last_series : series.last = t
-  length_series : series.length = n
+/-- A finite height lattice is a lattice in which all chains $a < \ldots < z$ have a maximum height `height`. -/
+class FiniteHeightLattice (α : Type*) extends Lattice α where
+  longestChain : LTSeries α
+  chains_bounded : BoundedChains α longestChain.length
 
-class FiniteHeightLattice (α : Type*) [Lattice α] extends Bot α, Top α where
-  height : ℕ
-  longestChain : PointedLTSeries α ⊥ ⊤ height
-  chains_bounded : BoundedChains α height
+-- a < ... < z
+-- ----------- length <= height
 
 namespace FiniteHeightLattice
 
-variable (α : Type*) [Lattice α] [FiniteHeightLattice α]
+def height (α : Type*) [FiniteHeightLattice α] : ℕ :=
+  (longestChain (α := α)).length
 
-theorem bot_le (a : α) : (⊥ : α) ≤ a := by
+variable (α : Type*) [FiniteHeightLattice α]
+
+instance (priority := 100) : Bot α := ⟨(longestChain (α := α)).head⟩
+instance (priority := 100) : Top α := ⟨(longestChain (α := α)).last⟩
+
+/-- The bottom element `⊥` of a finite height lattice is _actually_ the least element. -/
+lemma bot_le (a : α) : (⊥ : α) ≤ a := by
   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
+    have hlt : ⊥ ⊓ a < (longestChain (α := α)).head :=
+      lt_of_le_of_ne inf_le_left heq
+    have hbound := chains_bounded ((longestChain (α := α)).cons (⊥ ⊓ a) hlt)
+    rw [RelSeries.cons_length] at hbound
+    omega
+
+/-- The top element `⊤` of a finite height lattice is _actually_ the greatest element. -/
+lemma le_top (a : α) : a ≤ (⊤ : α) := by
+  by_cases heq : a ⊔ ⊤ = ⊤
+  · exact sup_eq_right.mp heq
+  · exfalso
+    have hlt : (longestChain (α := α)).last < a ⊔ ⊤ :=
+      lt_of_le_of_ne le_sup_right (Ne.symm heq)
+    have hbound := chains_bounded ((longestChain (α := α)).snoc (a ⊔ ⊤) hlt)
+    rw [RelSeries.snoc_length] at hbound
     omega
 
 end FiniteHeightLattice

lean/Spa/Lattice/AboveBelow.lean

@@ -34,47 +34,47 @@ instance : Min (AboveBelow α) where
     | mk _, bot => bot
     | mk x, top => mk x
 
-@[simp] theorem bot_sup (x : AboveBelow α) : bot ⊔ x = x := rfl
-@[simp] theorem top_sup (x : AboveBelow α) : top ⊔ x = top := rfl
-@[simp] theorem sup_bot (x : AboveBelow α) : x ⊔ bot = x := by cases x <;> rfl
-@[simp] theorem sup_top (x : AboveBelow α) : x ⊔ top = top := by cases x <;> rfl
-@[simp] theorem mk_sup_mk (x y : α) :
+@[simp] lemma bot_sup (x : AboveBelow α) : bot ⊔ x = x := rfl
+@[simp] lemma top_sup (x : AboveBelow α) : top ⊔ x = top := rfl
+@[simp] lemma 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] lemma mk_sup_mk (x y : α) :
     (mk x ⊔ mk y : AboveBelow α) = if x = y then mk x else top := rfl
 
-@[simp] theorem bot_inf (x : AboveBelow α) : bot ⊓ x = bot := rfl
-@[simp] theorem top_inf (x : AboveBelow α) : top ⊓ x = x := rfl
-@[simp] theorem inf_bot (x : AboveBelow α) : x ⊓ bot = bot := by cases x <;> rfl
-@[simp] theorem inf_top (x : AboveBelow α) : x ⊓ top = x := by cases x <;> rfl
-@[simp] theorem mk_inf_mk (x y : α) :
+@[simp] lemma bot_inf (x : AboveBelow α) : bot ⊓ x = bot := rfl
+@[simp] lemma top_inf (x : AboveBelow α) : top ⊓ x = x := rfl
+@[simp] lemma 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] lemma mk_inf_mk (x y : α) :
     (mk x ⊓ mk y : AboveBelow α) = if x = y then mk x else bot := rfl
 
-protected theorem sup_comm (a b : AboveBelow α) : a ⊔ b = b ⊔ a := by
+protected lemma sup_comm (a b : AboveBelow α) : a ⊔ b = b ⊔ a := by
   rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> simp only
     [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk]
   split_ifs with h₁ h₂ h₂ <;> simp_all
 
-protected theorem sup_assoc (a b c : AboveBelow α) : a ⊔ b ⊔ c = a ⊔ (b ⊔ c) := by
+protected lemma 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
+protected lemma 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
+protected lemma 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
+protected lemma 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
+protected lemma 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] <;>
@@ -85,24 +85,24 @@ instance : Lattice (AboveBelow α) :=
     AboveBelow.inf_comm AboveBelow.inf_assoc
     AboveBelow.sup_inf_self AboveBelow.inf_sup_self
 
-theorem le_iff {a b : AboveBelow α} : a ≤ b ↔ a ⊔ b = b := sup_eq_right.symm
+lemma le_iff {a b : AboveBelow α} : a ≤ b ↔ a ⊔ b = b := sup_eq_right.symm
 
-theorem bot_le' (a : AboveBelow α) : (bot : AboveBelow α) ≤ a :=
+lemma bot_le' (a : AboveBelow α) : (bot : AboveBelow α) ≤ a :=
   le_iff.mpr (bot_sup a)
 
-theorem le_top' (a : AboveBelow α) : a ≤ (top : AboveBelow α) :=
+lemma le_top' (a : AboveBelow α) : a ≤ (top : AboveBelow α) :=
   le_iff.mpr (sup_top a)
 
-theorem bot_lt_mk (x : α) : (bot : AboveBelow α) < mk x :=
+lemma bot_lt_mk (x : α) : (bot : AboveBelow α) < mk x :=
   lt_of_le_of_ne (bot_le' _) (by simp)
 
-theorem mk_lt_top (x : α) : (mk x : AboveBelow α) < top :=
+lemma mk_lt_top (x : α) : (mk x : AboveBelow α) < top :=
   lt_of_le_of_ne (le_top' _) (by simp)
 
-theorem bot_lt_top : (bot : AboveBelow α) < top :=
+lemma bot_lt_top : (bot : AboveBelow α) < top :=
   lt_of_le_of_ne (bot_le' _) (by simp)
 
-theorem le_cases {a b : AboveBelow α} (h : a ≤ b) :
+lemma le_cases {a b : AboveBelow α} (h : a ≤ b) :
     a = bot ∨ b = top ∨ a = b := by
   have hsup := le_iff.mp h
   rcases a with _ | _ | x <;> rcases b with _ | _ | y
@@ -125,7 +125,7 @@ theorem le_cases {a b : AboveBelow α} (h : a ≤ b) :
 monotone in both arguments — regardless of its values on plain elements.
 `Analysis/Sign.agda` and `Analysis/Constant.agda` postulated exactly these
 monotonicity facts for their `plus`/`minus`, all of which have this shape. -/
-theorem monotone₂_of_strict {β γ : Type*} [DecidableEq β] [DecidableEq γ]
+lemma 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)
@@ -154,7 +154,7 @@ section Interp
 
 variable {V : Type*} {P : AboveBelow α → V → Prop}
 
-theorem interp_sup_of (hbot : ∀ v, ¬P bot v) (htop : ∀ v, P top v)
+lemma interp_sup_of (hbot : ∀ v, ¬P bot v) (htop : ∀ v, P top v)
     {s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∨ P s₂ v) : P (s₁ ⊔ s₂) v := by
   rcases s₁ with _ | _ | x
   · rw [bot_sup]; exact h.resolve_left (hbot v)
@@ -167,7 +167,7 @@ theorem interp_sup_of (hbot : ∀ v, ¬P bot v) (htop : ∀ v, P top v)
       · next heq => subst heq; exact h.elim id id
       · exact htop v
 
-theorem interp_inf_of
+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
@@ -192,7 +192,7 @@ def rank : AboveBelow α → ℕ
 
 /-- Agda: the impossibility of `[x] ≺ [y]` (combines `x≺[y]⇒x≡⊥` and
 `[x]≺y⇒y≡⊤`: the flat middle layer is an antichain). -/
-theorem not_mk_lt_mk (x y : α) : ¬(mk x : AboveBelow α) < mk y := by
+lemma not_mk_lt_mk (x y : α) : ¬(mk x : AboveBelow α) < mk y := by
   intro h
   obtain ⟨hle, hne⟩ := lt_iff_le_and_ne.mp h
   have hsup := le_iff.mp hle
@@ -203,7 +203,7 @@ theorem not_mk_lt_mk (x y : α) : ¬(mk x : AboveBelow α) < mk y := by
   · rw [if_neg hxy] at hsup
     exact absurd hsup (by simp)
 
-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
   · exact absurd hab (lt_irrefl _)
@@ -216,24 +216,18 @@ theorem rank_strictMono : StrictMono (rank : AboveBelow α → ℕ) := by
   · simp [rank]
   · exact absurd hab (not_mk_lt_mk x y)
 
-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
-  bot := bot
-  top := top
-  height := 2
+  toLattice := inferInstance
   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] }
+    ((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)
   chains_bounded := boundedChains
 
 end AboveBelow

lean/Spa/Lattice/Bool.lean

@@ -0,0 +1,38 @@
+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
+  longestChain := (RelSeries.singleton _ (⊥ : Bool)).snoc (⊤ : Bool)
+    (by rw [RelSeries.last_singleton]; exact bot_lt_top)
+  chains_bounded := boundedChains
+
+end Bool
+
+end Spa

lean/Spa/Lattice/FiniteMap.lean

@@ -1,318 +1,111 @@
-import Spa.Lattice.IterProd
-import Spa.Isomorphism
+import Spa.Lattice.Tuple
+import Mathlib.Data.List.Nodup
 
 namespace Spa
 
-def FiniteMap (A B : Type*) (ks : List A) : Type _ :=
-  { l : List (A × B) // l.map Prod.fst = ks }
+def FiniteMap (A B : Type*) (ks : List A) : Type _ := Fin ks.length → B
 
 namespace FiniteMap
 
 variable {A B : Type*} {ks : List A}
 
-instance [DecidableEq A] [DecidableEq B] : DecidableEq (FiniteMap A B ks) :=
-  fun a b => decidable_of_iff (a.val = b.val) Subtype.ext_iff.symm
+instance [Lattice B] : Lattice (FiniteMap A B ks) :=
+  inferInstanceAs (Lattice (Fin ks.length → B))
 
-theorem spine_eq (fm₁ fm₂ : FiniteMap A B ks) :
-    fm₁.val.map Prod.fst = fm₂.val.map Prod.fst :=
-  fm₁.property.trans fm₂.property.symm
+instance [FiniteHeightLattice B] : FiniteHeightLattice (FiniteMap A B ks) :=
+  inferInstanceAs (FiniteHeightLattice (Fin ks.length → B))
 
-def combine (f : B → B → B) (l₁ l₂ : List (A × B)) : List (A × B) :=
-  List.zipWith (fun p q => (p.1, f p.2 q.2)) l₁ l₂
-
-theorem combine_spine (f : B → B → B) : ∀ {l₁ l₂ : List (A × B)},
-    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
-
-theorem combine_comm (f : B → B → B) (hf : ∀ a b, f a b = f b a) :
-    ∀ {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
-
-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
-
-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
-
-variable [Lattice B]
-
-instance : Max (FiniteMap A B ks) where
-  max fm₁ fm₂ :=
-    ⟨combine (· ⊔ ·) fm₁.val fm₂.val,
-     (combine_spine _ (spine_eq fm₁ fm₂)).trans fm₁.property⟩
-
-instance : Min (FiniteMap A B ks) where
-  min fm₁ fm₂ :=
-    ⟨combine (· ⊓ ·) fm₁.val fm₂.val,
-     (combine_spine _ (spine_eq fm₁ fm₂)).trans fm₁.property⟩
-
-@[simp] theorem sup_val (fm₁ fm₂ : FiniteMap A B ks) :
-    (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 [DecidableEq B] : DecidableEq (FiniteMap A B ks) :=
+  inferInstanceAs (DecidableEq (Fin ks.length → B))
 
 instance : Membership (A × B) (FiniteMap A B ks) :=
-  ⟨fun fm p => p ∈ fm.val⟩
+  ⟨fun fm p => ∃ i : Fin ks.length, ks.get i = p.1 ∧ fm i = p.2⟩
 
-omit [Lattice B] in
-theorem mem_def {p : A × B} {fm : FiniteMap A B ks} : p ∈ fm ↔ p ∈ fm.val :=
-  Iff.rfl
+lemma mem_iff {fm : FiniteMap A B ks} {p : A × B} :
+    p ∈ fm ↔ ∃ i : Fin ks.length, ks.get i = p.1 ∧ fm i = p.2 := Iff.rfl
 
-def MemKey (k : A) (fm : FiniteMap A B ks) : Prop :=
-  k ∈ fm.val.map Prod.fst
+def MemKey (k : A) (_fm : FiniteMap A B ks) : Prop := k ∈ ks
 
-omit [Lattice B] in
-theorem memKey_iff {k : A} {fm : FiniteMap A B ks} : MemKey k fm ↔ k ∈ ks := by
-  rw [MemKey, fm.property]
+lemma MemKey_iff {k : A} {fm : FiniteMap A B ks} : MemKey k fm ↔ k ∈ ks := Iff.rfl
 
-instance {k : A} {fm : FiniteMap A B ks} [DecidableEq A] :
-    Decidable (MemKey k fm) :=
-  decidable_of_iff _ memKey_iff.symm
+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
+lemma mem_key_of_mem {k : A} {v : B} {fm : FiniteMap A B ks}
+    (h : (k, v) ∈ fm) : MemKey k fm := by
+  obtain ⟨i, hi, _⟩ := h
+  have hik : ks.get i = k := hi
+  exact hik ▸ ks.get_mem i
+
+def toList (fm : FiniteMap A B ks) : List (A × B) :=
+  (List.finRange ks.length).map fun i => (ks.get i, fm i)
+
+lemma le_def [Lattice B] {fm₁ fm₂ : FiniteMap A B ks} :
+    fm₁ ≤ fm₂ ↔ ∀ i, fm₁ i ≤ fm₂ i := Iff.rfl
 
 section Locate
 
 variable [DecidableEq A]
 
-private def locateList (k : A) :
-    (l : List (A × B)) → k ∈ l.map Prod.fst → {v : B // (k, v) ∈ l}
-  | [], h => absurd h (by simp)
-  | p :: l', h =>
-    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⟩
-
+/-- Recover the value stored under a present key. -/
 def locate {k : A} {fm : FiniteMap A B ks} (h : MemKey k fm) :
     {v : B // (k, v) ∈ fm} :=
-  locateList k fm.val h
+  let i : Fin ks.length := ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩
+  ⟨fm i, i, List.idxOf_get _, rfl⟩
 
 end Locate
 
-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
+variable [Lattice B]
 
-theorem le_iff {fm₁ fm₂ : FiniteMap A B ks} :
-    fm₁ ≤ fm₂ ↔
-      List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) fm₁.val fm₂.val := by
-  rw [← sup_eq_right, ← combine_eq_right_iff (spine_eq fm₁ fm₂), Subtype.ext_iff,
-      sup_val]
-
-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}
+lemma 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₂
+    (h₁ : (k, v₁) ∈ fm₁) (h₂ : (k, v₂) ∈ fm₂) : v₁ ≤ v₂ := by
+  obtain ⟨i, hi, rfl⟩ := h₁
+  obtain ⟨j, hj, rfl⟩ := h₂
+  have hij : i = j := hks.get_inj_iff.mp (hi.trans hj.symm)
+  subst hij
+  exact le_def.mp hle i
 
-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}
+lemma 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₂ :=
-  mem_combine _ (spine_eq fm₁ fm₂) h
+    ∃ 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 A]
 
-def updating (fm : FiniteMap A B ks) (ks' : List A) (g : A → B) :
-    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⟩
+def updating (fm : FiniteMap A B ks) (ks' : List A) (g : A → B) : FiniteMap A B ks :=
+  fun i => if ks.get i ∈ ks' then g (ks.get i) else fm i
 
 omit [Lattice B] in
-@[simp] theorem updating_val (fm : FiniteMap A B ks) (ks' : List A) (g : A → B) :
-    (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}
+lemma 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 ⟨p, hp, heq⟩ := List.mem_map.mp h
-  by_cases hmem : p.1 ∈ ks'
-  · 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
+  obtain ⟨i, hi, rfl⟩ := h
+  show (if ks.get i ∈ ks' then g (ks.get i) else fm i) = g k
+  rw [if_pos (by rw [hi]; exact hk), hi]
 
 omit [Lattice B] in
-theorem mem_updating {k : A} {fm : FiniteMap A B ks} {ks' : List A} {g : A → B}
-    (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}
+lemma 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 ⟨p, hp, heq⟩ := List.mem_map.mp h
-  by_cases hmem : p.1 ∈ ks'
-  · rw [if_pos hmem] at heq
-    injection heq with h1 _
-    rw [← h1] at hk
-    exact absurd hmem hk
-  · rw [if_neg hmem] at heq
-    exact heq ▸ hp
+  obtain ⟨i, hi, rfl⟩ := h
+  refine ⟨i, hi, ?_⟩
+  show fm i = (if ks.get i ∈ ks' then g (ks.get i) else fm i)
+  rw [if_neg (by rw [hi]; exact hk)]
 
-private theorem updating_mono_list {ks' : List A} {g₁ g₂ : A → B}
-    (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}
+lemma 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_iff] at hfm ⊢
-  simp only [updating_val]
-  exact updating_mono_list hg hfm
+  rw [le_def]
+  intro i
+  show (if ks.get i ∈ ks' then g₁ (ks.get i) else fm₁ i)
+     ≤ (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
 
@@ -321,44 +114,24 @@ section GeneralizedUpdate
 variable [DecidableEq A] {L : Type*} [Lattice L]
 
 def generalizedUpdate (f : L → FiniteMap A B ks) (g : A → L → B)
-    (ks' : List A) (l : L) : FiniteMap A B ks :=
+    (ks' : List A) : L → FiniteMap A B ks := fun l =>
   (f l).updating ks' (fun k => g k l)
 
 variable {f : L → FiniteMap A B ks} {g : A → L → B} {ks' : List A}
 
-theorem generalizedUpdate_monotone (hf : Monotone f)
+lemma 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 B] [Lattice L] in
-theorem generalizedUpdate_memKey {k : A} {l : L}
-    (h : MemKey k (f l)) : MemKey k (generalizedUpdate f g ks' l) := by
-  unfold generalizedUpdate
-  exact memKey_updating.mpr h
+lemma generalizedUpdate_mem_eq {k : A} {v : B} {l : L} (hk : k ∈ ks')
+    (h : (k, v) ∈ generalizedUpdate f g ks' l) : v = g k l :=
+  eq_of_mem_updating (g := fun k => g k l) hk h
 
 omit [Lattice B] [Lattice L] in
-theorem generalizedUpdate_mem {k : A} {l : L} (hk : k ∈ ks')
-    (h : MemKey k (f l)) : (k, g k l) ∈ generalizedUpdate f g ks' l := by
-  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
+lemma 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 :=
+  mem_of_mem_updating hk h
 
 end GeneralizedUpdate
 
@@ -366,60 +139,48 @@ section ValuesAt
 
 variable [DecidableEq A]
 
-private def lookup? (k : A) : List (A × B) → Option B
-  | [] => none
-  | p :: l' => if p.1 = k then some p.2 else lookup? k l'
+/-- The value stored under `k`, if `k` is a key. -/
+private def lookup (fm : FiniteMap A B ks) (k : A) : Option B :=
+  if h : k ∈ ks then some (fm ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩) else none
 
+/-- 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 :=
-  ks'.filterMap (fun k => lookup? k fm.val)
+  ks'.filterMap fm.lookup
 
 omit [Lattice B] in
-private theorem lookup?_eq_some_of_mem : ∀ {l : List (A × B)},
-    (l.map Prod.fst).Nodup → ∀ {k : A} {v : B}, (k, v) ∈ l →
-    lookup? k l = some v
-  | [], _, _, _, h => by simp at h
-  | p :: l', hnd, k, v, h => by
-    simp only [List.map_cons, List.nodup_cons] at hnd
-    rcases List.mem_cons.mp h with heq | h'
-    · rw [← heq]
-      simp [lookup?]
-    · rw [lookup?, if_neg ?_]
-      · exact lookup?_eq_some_of_mem hnd.2 h'
-      · intro hpk
-        subst hpk
-        have := List.mem_map_of_mem Prod.fst h'
-        exact hnd.1 this
+lemma mem_valuesAt (hks : ks.Nodup) {fm : FiniteMap A B ks} {k : A} {v : B}
+    {ks' : List A} (hk : k ∈ ks') (h : (k, v) ∈ fm) : v ∈ valuesAt fm ks' := by
+  refine List.mem_filterMap.mpr ⟨k, hk, ?_⟩
+  obtain ⟨i, hi, rfl⟩ := h
+  have hik : ks.get i = k := hi
+  have hmem : k ∈ ks := hik ▸ ks.get_mem i
+  show (if h : k ∈ ks then
+          some (fm ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩) else none) = some (fm i)
+  rw [dif_pos hmem]
+  have : (⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr hmem⟩ : Fin ks.length) = i :=
+    hks.get_inj_iff.mp (by rw [List.idxOf_get, hi])
+  rw [this]
 
-omit [Lattice B] in
-theorem mem_valuesAt (hks : ks.Nodup) {fm : FiniteMap A B ks} {k : A} {v : B}
-    {ks' : List A} (hk : k ∈ ks') (h : (k, v) ∈ fm) : v ∈ valuesAt fm ks' :=
-  List.mem_filterMap.mpr
-    ⟨k, hk, lookup?_eq_some_of_mem (fm.property.symm ▸ hks) h⟩
+private lemma lookup_rel {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂) (k : A) :
+    Option.Rel (· ≤ ·) (fm₁.lookup k) (fm₂.lookup k) := by
+  show Option.Rel _
+    (if h : k ∈ ks then some (fm₁ ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩) else none)
+    (if h : k ∈ ks then some (fm₂ ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩) else none)
+  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
 
-private theorem lookup?_forall₂ {l₁ l₂ : List (A × B)}
-    (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₂)
+lemma 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?_forall₂ (le_iff.mp hle) k
+    have hrel := lookup_rel hle k
     rw [valuesAt, valuesAt, List.filterMap_cons, List.filterMap_cons]
     revert hrel
-    generalize lookup? k fm₁.val = o₁
-    generalize lookup? k fm₂.val = o₂
+    generalize fm₁.lookup k = o₁
+    generalize fm₂.lookup k = o₂
     intro hrel
     cases hrel with
     | none => simpa [valuesAt] using ih
@@ -427,120 +188,6 @@ theorem valuesAt_le {fm₁ fm₂ : FiniteMap A B 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) ofIter_toIter
-
-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/IterProd.lean

@@ -13,38 +13,23 @@ 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] :
+instance decidableEq [DecidableEq A] [DecidableEq B] :
     ∀ k, DecidableEq (IterProd A B k)
   | 0 => inferInstanceAs (DecidableEq B)
-  | k + 1 => @instDecidableEqProd A (IterProd A B k) _ (instDecidableEq k)
+  | k + 1 => @instDecidableEqProd A (IterProd A B k) _ (decidableEq 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)
+  | k + 1 => @Spa.prod A (IterProd A B k) _ (fixedHeight k)
 
-instance instFiniteHeight [FiniteHeightLattice A] [FiniteHeightLattice B] (k : ℕ) :
+instance finiteHeight [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

@@ -6,7 +6,7 @@ section Unzip
 
 variable {α β : Type*} [PartialOrder α] [PartialOrder β]
 
-theorem LTSeries.exists_unzip (c : LTSeries (α × β)) :
+lemma 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 ∧
@@ -58,36 +58,23 @@ end Unzip
 
 section FixedHeight
 
-variable {α β : Type*} [Lattice α] [Lattice β]
+variable {α β : Type*}
 
 instance prod [A : FiniteHeightLattice α] [B : FiniteHeightLattice β] :
     FiniteHeightLattice (α × β) where
-  bot := ((⊥ : α), (⊥ : β))
-  top := ((⊤ : α), (⊤ : β))
-  height := A.height + B.height
+  toLattice := inferInstance
   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] }
+    RelSeries.smash
+      (A.longestChain.map (fun a => (a, (⊥ : β)))
+        (fun _ _ h => Prod.mk_lt_mk_iff_left.mpr h))
+      (B.longestChain.map (fun b => ((⊤ : α), b))
+        (fun _ _ h => Prod.mk_lt_mk_iff_right.mpr h))
+      rfl
   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₂
+    show c.length ≤ A.longestChain.length + B.longestChain.length
     omega
 
 end FixedHeight

lean/Spa/Lattice/Tuple.lean

@@ -0,0 +1,65 @@
+import Spa.Lattice.IterProd
+import Spa.Isomorphism
+
+namespace Spa
+
+namespace Tuple
+
+universe u
+
+variable {B : Type u}
+
+private def iterOfFun : {n : ℕ} → (Fin n → B) → IterProd B PUnit n
+  | 0, _ => PUnit.unit
+  | _ + 1, f => (f 0, iterOfFun (Fin.tail f))
+
+private def funOfIter : {n : ℕ} → IterProd B PUnit n → (Fin n → B)
+  | 0, _ => Fin.elim0
+  | _ + 1, ip => Fin.cons ip.1 (funOfIter ip.2)
+
+private lemma funOfIter_iterOfFun : ∀ {n : ℕ} (f : Fin n → B),
+    funOfIter (iterOfFun f) = f
+  | 0, _ => funext fun i => i.elim0
+  | _ + 1, f => by
+    show Fin.cons (f 0) (funOfIter (iterOfFun (Fin.tail f))) = f
+    rw [funOfIter_iterOfFun (Fin.tail f), Fin.cons_self_tail]
+
+private lemma iterOfFun_funOfIter : ∀ {n : ℕ} (ip : IterProd B PUnit n),
+    iterOfFun (funOfIter ip) = ip
+  | 0, PUnit.unit => rfl
+  | _ + 1, ip => by
+    show (funOfIter ip 0, iterOfFun (Fin.tail (funOfIter ip))) = ip
+    rw [show funOfIter ip = Fin.cons ip.1 (funOfIter ip.2) from rfl]
+    simp [Fin.cons_zero, Fin.tail_cons, iterOfFun_funOfIter ip.2]
+
+variable [FiniteHeightLattice B]
+
+private lemma funOfIter_mono {n : ℕ} :
+    Monotone (funOfIter : IterProd B PUnit n → (Fin n → B)) := by
+  induction n with
+  | zero => intro _ _ _ i; exact i.elim0
+  | succ n ih =>
+    intro ip₁ ip₂ h i
+    obtain ⟨h1, h2⟩ := Prod.le_def.mp h
+    rw [show funOfIter ip₁ = Fin.cons ip₁.1 (funOfIter ip₁.2) from rfl,
+        show funOfIter ip₂ = Fin.cons ip₂.1 (funOfIter ip₂.2) from rfl]
+    induction i using Fin.cases with
+    | zero => rw [Fin.cons_zero, Fin.cons_zero]; exact h1
+    | succ j => rw [Fin.cons_succ, Fin.cons_succ]; exact ih h2 j
+
+private lemma iterOfFun_mono {n : ℕ} :
+    Monotone (iterOfFun : (Fin n → B) → IterProd B PUnit n) := by
+  induction n with
+  | zero => intro f g _; exact le_of_eq rfl
+  | succ n ih =>
+    intro f g h
+    exact Prod.le_def.mpr ⟨h 0, ih fun i => h i.succ⟩
+
+instance instFiniteHeight {n : ℕ} :
+    FiniteHeightLattice (Fin n → B) :=
+  FiniteHeightLattice.transport funOfIter iterOfFun
+    funOfIter_mono iterOfFun_mono iterOfFun_funOfIter funOfIter_iterOfFun
+
+end Tuple
+
+end Spa

lean/Spa/Lattice/Unit.lean

@@ -2,17 +2,15 @@ import Spa.Lattice
 
 namespace Spa
 
-theorem boundedChains_of_subsingleton (α : Type*) [Preorder α] [Subsingleton α]
+lemma 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 _ }
+  toLattice := inferInstance
+  longestChain := RelSeries.singleton _ PUnit.unit
   chains_bounded := boundedChains_of_subsingleton PUnit 0
 
 end Spa

lean/Spa/Showable.lean

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