Use a direct N-way unzip instead of induction over product size

This makes a finite-height proof for any `Fin n -> a` lattice
immediate, and precludes the need for IterProd and Prod altogether.

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

lean/Spa.lean

@@ -1,10 +1,7 @@
 import Spa.Lattice
 import Spa.Fixedpoint
-import Spa.Isomorphism
 import Spa.Lattice.Unit
-import Spa.Lattice.Prod
 import Spa.Lattice.AboveBelow
-import Spa.Lattice.IterProd
 import Spa.Lattice.FiniteMap
 import Spa.Lattice.Bool
 import Spa.Language.Base

lean/Spa/Isomorphism.lean

@@ -1,16 +0,0 @@
-import Spa.Lattice
-
-namespace Spa
-
-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
-  toLattice := inferInstance
-  longestChain :=
-    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))
-
-end Spa

lean/Spa/Language/Semantics.lean

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

lean/Spa/Lattice.lean

@@ -67,6 +67,14 @@ end Folds
 def BoundedChains (α : Type*) [Preorder α] (n : ℕ) : Prop :=
   ∀ c : LTSeries α, c.length ≤ n
 
+/-- Since a singleton type's preorder has no nonempty `<` chains,
+    they are vacuously bounded by any minimum height. -/
+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 _ _)
+
 /-- 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 α
@@ -107,6 +115,32 @@ lemma le_top (a : α) : a ≤ (⊤ : α) := by
     rw [RelSeries.snoc_length] at hbound
     omega
 
+/-- This is something like a lemma about isomorphic types having the same height.
+    Given a finite-height lattice `α`, lattice `β`, and a `Monotone` bijection
+    between the two, we can show that lattice `β` also has a finite height.
+
+    The proof is fairly trivial: the longest chain in `α` can be transported
+    to be a longest chain in `β` (by monotonicity), establishing a height witness.
+    At the same time, any chain in `β` can be transported to a chain in `α`,
+    and must be bounded by the same height by `FiniteHeightLattice.chains_bounded`. -/
+def transport {α β : Type*} [Lattice β]
+    [I : FiniteHeightLattice α] (f : α → β) (g : β → α)
+    (hf : Monotone f) (hg : Monotone g)
+    (hgf : Function.LeftInverse g f) (hfg : Function.LeftInverse f g) :
+    FiniteHeightLattice β where
+  toLattice := inferInstance
+  longestChain :=
+    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))
+
+/-- A `Unique` lattice trivially has finite height: its only chain is the singleton
+    `[default]`, and there are no nontrivial `<` chains in a subsingleton. -/
+def ofUnique (α : Type*) [Lattice α] [Unique α] : FiniteHeightLattice α where
+  toLattice := inferInstance
+  longestChain := RelSeries.singleton _ default
+  chains_bounded := boundedChains_of_subsingleton α 0
+
 end FiniteHeightLattice
 
 end Spa

lean/Spa/Lattice/IterProd.lean

@@ -1,35 +0,0 @@
-import Spa.Lattice.Prod
-import Spa.Lattice.Unit
-
-namespace Spa
-
-universe u
-
-def IterProd (A B : Type u) : ℕ → Type u
-  | 0 => B
-  | k + 1 => A × IterProd A B k
-
-namespace IterProd
-
-variable {A B : Type u}
-
-instance decidableEq [DecidableEq A] [DecidableEq B] :
-    ∀ k, DecidableEq (IterProd A B k)
-  | 0 => inferInstanceAs (DecidableEq B)
-  | 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)
-
-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) _ (fixedHeight k)
-
-instance finiteHeight [FiniteHeightLattice A] [FiniteHeightLattice B] (k : ℕ) :
-    FiniteHeightLattice (IterProd A B k) := fixedHeight k
-
-end IterProd
-
-end Spa

lean/Spa/Lattice/Prod.lean

@@ -1,82 +0,0 @@
-import Spa.Lattice
-
-namespace Spa
-
-section Unzip
-
-variable {α β : Type*} [PartialOrder α] [PartialOrder β]
-
-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 ∧
-      c.length ≤ c₁.length + c₂.length := by
-  suffices H : ∀ (n : ℕ) (c : LTSeries (α × β)), c.length = n →
-      ∃ (c₁ : LTSeries α) (c₂ : LTSeries β),
-        c₁.head = c.head.1 ∧ c₁.last = c.last.1 ∧
-        c₂.head = c.head.2 ∧ c₂.last = c.last.2 ∧
-        c.length ≤ c₁.length + c₂.length from H c.length c rfl
-  intro n
-  induction n with
-  | zero =>
-    intro c hn
-    refine ⟨RelSeries.singleton _ c.head.1, RelSeries.singleton _ c.head.2,
-      rfl, ?_, rfl, ?_, by simp [hn]⟩ <;>
-    · have hlast : Fin.last c.length = 0 := by ext; simp [hn]
-      simp [RelSeries.last, RelSeries.head, hlast]
-  | succ n ih =>
-    intro c hn
-    have h0 : c.length ≠ 0 := by omega
-    haveI : NeZero c.length := ⟨h0⟩
-    obtain ⟨c₁, c₂, hh₁, hl₁, hh₂, hl₂, hlen⟩ :=
-      ih (c.tail h0) (by simp [RelSeries.tail_length, hn])
-    rw [RelSeries.last_tail] at hl₁ hl₂
-    rw [RelSeries.head_tail] at hh₁ hh₂
-    rw [RelSeries.tail_length] at hlen
-    have hstep : c.head < c 1 := c.strictMono Fin.one_pos'
-    obtain ⟨hle1, hle2⟩ := Prod.le_def.mp hstep.le
-    rcases eq_or_lt_of_le hle1 with heq1 | hlt1 <;>
-      rcases eq_or_lt_of_le hle2 with heq2 | hlt2
-    · exact absurd (Prod.ext heq1 heq2) hstep.ne
-    · refine ⟨c₁, c₂.cons c.head.2 (hh₂ ▸ hlt2),
-        hh₁.trans heq1.symm, hl₁, RelSeries.head_cons .., by
-          rw [RelSeries.last_cons]; exact hl₂, by
-          simp only [RelSeries.cons_length]; omega⟩
-    · refine ⟨c₁.cons c.head.1 (hh₁ ▸ hlt1), c₂,
-        RelSeries.head_cons .., by
-          rw [RelSeries.last_cons]; exact hl₁,
-        hh₂.trans heq2.symm, hl₂, by
-          simp only [RelSeries.cons_length]; omega⟩
-    · refine ⟨c₁.cons c.head.1 (hh₁ ▸ hlt1), c₂.cons c.head.2 (hh₂ ▸ hlt2),
-        RelSeries.head_cons .., by
-          rw [RelSeries.last_cons]; exact hl₁,
-        RelSeries.head_cons .., by
-          rw [RelSeries.last_cons]; exact hl₂, by
-          simp only [RelSeries.cons_length]; omega⟩
-
-end Unzip
-
-section FixedHeight
-
-variable {α β : Type*}
-
-instance prod [A : FiniteHeightLattice α] [B : FiniteHeightLattice β] :
-    FiniteHeightLattice (α × β) where
-  toLattice := inferInstance
-  longestChain :=
-    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
-
-end Spa

lean/Spa/Lattice/Tuple.lean

@@ -1,64 +1,171 @@
-import Spa.Lattice.IterProd
+import Spa.Lattice
-import Spa.Isomorphism
+import Mathlib.Data.Fin.Tuple.Basic
+import Mathlib.Algebra.Order.BigOperators.Group.Finset
+
+/-!
+
+# Finite Tuple Lattices
+
+This file provides a proof that, in addition to being a lattice, the function
+space `Fin n → β` is itself a `Spa.FiniteHeightLattice` if the element type
+`β` is a lattice.
+
+Finite tuple lattices are the workhorse behind `FiniteMap`, whose carrier is
+`Fin ks.length → β`.
+
+The proof proceeds by "unzipping" a chain (`LTSeries`):
+
+$$
+(a_1, b_1, c_1) < \ldots < (a_1, b_1, c_o) < \ldots < (a_1, b_m, c_o) <
+  \ldots < (a_n, b_m, c_o)
+$$
+
+In which, at each step, at least one of the components must have increased
+(otherwise, the chain is not striclty increasing), into `n` chains
+(`LTSeries`).
+
+$$
+\begin{aligned}
+a_1 < \ldots < a_n \\
+b_1 < \ldots < b_m \
+c_1 < \ldots < c_o \
+\end{aligned}
+$$
+
+Because at least one of the two "unzipped" chains grows with each element of
+the product chain, the full chain length can't exceed the sum of the
+components. By the definition of finite height, these two chains are bounded,
+and therefore, the product chain is bounded too. -/
 
 namespace Spa
 
 namespace Tuple
 
-universe u
+variable {β : Type*}
 
-variable {B : Type u}
+section Unzip
 
-private def iterOfFun : {n : ℕ} → (Fin n → B) → IterProd B PUnit n
+variable [PartialOrder β]
-  | 0, _ => PUnit.unit
-  | _ + 1, f => (f 0, iterOfFun (Fin.tail f))
 
-private def funOfIter : {n : ℕ} → IterProd B PUnit n → (Fin n → B)
+open Classical in -- chain bounds are in Prop, so classical helps here.
-  | 0, _ => Fin.elim0
+/-- The generalized unzip: any chain in `Fin n → β` decomposes into a family of
-  | _ + 1, ip => Fin.cons ip.1 (funOfIter ip.2)
+    per-tuple-coordinate chains in `β`, agreeing with the original at each end, whose
+    lengths sum to an upper bound on the original chain's length. -/
+lemma exists_unzip {n : ℕ} (c : LTSeries (Fin n → β)) :
+    ∃ cs : Fin n → LTSeries β,
+      (∀ i, (cs i).head = c.head i) ∧ (∀ i, (cs i).last = c.last i) ∧
+      c.length ≤ ∑ i, (cs i).length := by
+  suffices H : ∀ (m : ℕ) (c : LTSeries (Fin n → β)), c.length = m →
+      ∃ cs : Fin n → LTSeries β,
+        (∀ i, (cs i).head = c.head i) ∧ (∀ i, (cs i).last = c.last i) ∧
+        c.length ≤ ∑ i, (cs i).length from H c.length c rfl
+  intro m
+  induction m with
+  | zero =>
+    intro c hn
+    have hlast : (Fin.last c.length) = 0 := by ext; simp [hn]
+    have hhl : c.last = c.head := by rw [RelSeries.last, RelSeries.head, hlast]
+    refine ⟨fun i => RelSeries.singleton _ (c.head i), fun i => ?_, fun i => ?_, ?_⟩
+    · exact RelSeries.head_singleton _
+    · rw [RelSeries.last_singleton, hhl]
+    · simp [hn, RelSeries.singleton]
+  | succ m ih =>
+    intro c hn
+    have h0 : c.length ≠ 0 := by omega
+    haveI : NeZero c.length := ⟨h0⟩
+    obtain ⟨cs', hh', hl', hlen'⟩ := ih (c.tail h0) (by rw [RelSeries.tail_length]; omega)
+    have hstep : c.head < c 1 := c.strictMono Fin.one_pos'
+    obtain ⟨hle, j, hjlt⟩ := Pi.lt_def.mp hstep
+    have hh'1 : ∀ i, (cs' i).head = c 1 i := fun i => by rw [hh' i, RelSeries.head_tail]
+    refine ⟨fun i =>
+        if hlt : c.head i < c 1 i then
+          (cs' i).cons (c.head i) (by rw [hh'1 i]; exact hlt)
+        else cs' i,
+      fun i => ?_, fun i => ?_, ?_⟩
+    · by_cases hlt : c.head i < c 1 i
+      · simp only [dif_pos hlt, RelSeries.head_cons]
+      · simp only [dif_neg hlt]
+        rw [hh'1 i]
+        exact ((lt_or_eq_of_le (hle i)).resolve_left hlt).symm
+    · by_cases hlt : c.head i < c 1 i
+      · simp only [dif_pos hlt, RelSeries.last_cons, hl' i, RelSeries.last_tail]
+      · simp only [dif_neg hlt, hl' i, RelSeries.last_tail]
+    · calc c.length
+          = (c.tail h0).length + 1 := by rw [RelSeries.tail_length]; omega
+        _ ≤ (∑ i, (cs' i).length) + 1 := Nat.add_le_add_right hlen' 1
+        _ ≤ ∑ i, (if hlt : c.head i < c 1 i then
+              (cs' i).cons (c.head i) (by rw [hh'1 i]; exact hlt) else cs' i).length :=
+          Nat.succ_le_of_lt (Finset.sum_lt_sum (fun i _ => by
+              split
+              · rw [RelSeries.cons_length]; omega
+              · exact le_rfl)
+            ⟨j, Finset.mem_univ j, by rw [dif_pos hjlt, RelSeries.cons_length]; omega⟩)
 
-private lemma funOfIter_iterOfFun : ∀ {n : ℕ} (f : Fin n → B),
+end Unzip
-    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),
+section FiniteHeight
-    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]
+variable [FiniteHeightLattice β]
 
-private lemma funOfIter_mono {n : ℕ} :
+private lemma consBot_strictMono {n : ℕ} :
-    Monotone (funOfIter : IterProd B PUnit n → (Fin n → B)) := by
+    StrictMono (fun b : β => (Fin.cons b (⊥ : Fin n → β) : Fin (n + 1) → β)) := by
-  induction n with
+  intro a b hab
-  | zero => intro _ _ _ i; exact i.elim0
+  refine lt_iff_le_and_ne.mpr ⟨?_, ?_⟩
-  | succ n ih =>
+  · refine Pi.le_def.mpr (fun i => Fin.cases ?_ (fun j => ?_) i)
-    intro ip₁ ip₂ h i
+    · simpa using hab.le
-    obtain ⟨h1, h2⟩ := Prod.le_def.mp h
+    · simp
-    rw [show funOfIter ip₁ = Fin.cons ip₁.1 (funOfIter ip₁.2) from rfl,
+  · exact fun h => hab.ne (by simpa using congrFun h 0)
-        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 : ℕ} :
+private lemma consTop_strictMono {n : ℕ} :
-    Monotone (iterOfFun : (Fin n → B) → IterProd B PUnit n) := by
+    StrictMono (fun f : Fin n → β => (Fin.cons (⊤ : β) f : Fin (n + 1) → β)) := by
-  induction n with
+  intro f g hfg
-  | zero => intro f g _; exact le_of_eq rfl
+  refine lt_iff_le_and_ne.mpr ⟨?_, ?_⟩
-  | succ n ih =>
+  · refine Pi.le_def.mpr (fun i => Fin.cases ?_ (fun j => ?_) i)
-    intro f g h
+    · simp
-    exact Prod.le_def.mpr ⟨h 0, ih fun i => h i.succ⟩
+    · simpa using Pi.le_def.mp hfg.le j
+  · intro h
+    apply hfg.ne
+    funext j
+    simpa using congrFun h j.succ
 
-instance instFiniteHeight {n : ℕ} :
+/-- The maximal chain in `Fin n → β`: walk the first tuple element from `⊥` to `⊤`
-    FiniteHeightLattice (Fin n → B) :=
+    through `β`'s longest chain, then do that with the second element, and so on. -/
-  FiniteHeightLattice.transport funOfIter iterOfFun
+private def stdChain : (n : ℕ) →
-    funOfIter_mono iterOfFun_mono iterOfFun_funOfIter funOfIter_iterOfFun
+    { s : LTSeries (Fin n → β) //
+        s.head = (⊥ : Fin n → β) ∧
+        s.length = n * (FiniteHeightLattice.longestChain (α := β)).length }
+  | 0 => ⟨RelSeries.singleton _ ⊥, by rw [RelSeries.head_singleton], by simp⟩
+  | n + 1 =>
+      let prev := stdChain n
+      ⟨RelSeries.smash
+          ((FiniteHeightLattice.longestChain (α := β)).map
+            (fun b => (Fin.cons b (⊥ : Fin n → β) : Fin (n + 1) → β)) consBot_strictMono)
+          (prev.1.map (fun f => (Fin.cons (⊤ : β) f : Fin (n + 1) → β)) consTop_strictMono)
+          (by rw [LTSeries.last_map, LTSeries.head_map, prev.2.1]; rfl),
+        by
+          simp only [RelSeries.head_smash, LTSeries.head_map]
+          rw [show (FiniteHeightLattice.longestChain (α := β)).head = (⊥ : β) from rfl]
+          funext i
+          refine Fin.cases ?_ (fun j => ?_) i <;> simp [Pi.bot_apply],
+        by
+          show (FiniteHeightLattice.longestChain (α := β)).length + prev.1.length
+              = (n + 1) * (FiniteHeightLattice.longestChain (α := β)).length
+          rw [prev.2.2, Nat.succ_mul]; exact Nat.add_comm _ _⟩
+
+instance instFiniteHeight {n : ℕ} : FiniteHeightLattice (Fin n → β) where
+  toLattice := inferInstance
+  longestChain := (stdChain n).1
+  chains_bounded := fun c => by
+    obtain ⟨cs, _, _, hbound⟩ := exists_unzip c
+    refine hbound.trans ?_
+    rw [(stdChain n).2.2]
+    calc ∑ i, (cs i).length
+        ≤ ∑ _i : Fin n, (FiniteHeightLattice.longestChain (α := β)).length :=
+          Finset.sum_le_sum (fun i _ => FiniteHeightLattice.chains_bounded (cs i))
+      _ = n * (FiniteHeightLattice.longestChain (α := β)).length := by
+          simp [Finset.sum_const, Finset.card_univ, Fintype.card_fin]
+
+end FiniteHeight
 
 end Tuple
 

lean/Spa/Lattice/Unit.lean

@@ -1,16 +1,14 @@
 import Spa.Lattice
 
+/-!
+
+# Unit Lattice
+
+This file provides a proof that in addition to being a lattice,
+`PUnit` is a `Spa.FiniteHeightLattice`. This is a fairly trivial result. -/
+
 namespace Spa
 
-lemma boundedChains_of_subsingleton (α : Type*) [Preorder α] [Subsingleton α]
+instance : FiniteHeightLattice PUnit := FiniteHeightLattice.ofUnique PUnit
-    (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
-  toLattice := inferInstance
-  longestChain := RelSeries.singleton _ PUnit.unit
-  chains_bounded := boundedChains_of_subsingleton PUnit 0
 
 end Spa