Remove maximal chain witness from FiniteHeightLattice

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

lean/Spa/Fixedpoint.lean

@@ -12,7 +12,7 @@ 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 simp only [height] at hlen; omega)
+    absurd (FiniteHeightLattice.chains_bounded c) (by omega)
   | g + 1, c, hlen, hle =>
     if heq : c.last = f c.last then
       ⟨c.last, heq⟩
@@ -39,7 +39,7 @@ lemma doStep_le (f : α → α) (hf : Monotone f)
       (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 simp only [height] at hlen; omega)
+    absurd (FiniteHeightLattice.chains_bounded c) (by omega)
   | g + 1, c, hlen, hle => fun hcb => by
     rw [doStep]
     split

lean/Spa/Lattice.lean

@@ -77,45 +77,24 @@ lemma boundedChains_of_subsingleton (α : Type*) [Preorder α] [Subsingleton α]
 
 /-- A finite height lattice is a lattice in which all chains $a < \ldots < z$ have a maximum height `height`. -/
 class FiniteHeightLattice (α : Type*) extends Lattice α, OrderBot α, OrderTop α where
-  longestChain : LTSeries α
-  chains_bounded : BoundedChains α longestChain.length
+  height : ℕ
+  chains_bounded : BoundedChains α height
 
 -- a < ... < z
 -- ----------- length <= height
 
 namespace FiniteHeightLattice
 
-def height (α : Type*) [FiniteHeightLattice α] : ℕ :=
-  (longestChain (α := α)).length
-
-variable (α : Type*) [FiniteHeightLattice α]
-
-/-- Any maximum-length chain in a bounded finite-height lattice starts at `⊥`. -/
-lemma longestChain_head : (longestChain (α := α)).head = ⊥ := by
-  by_contra hne
-  have hbound := chains_bounded ((longestChain (α := α)).cons ⊥ (bot_lt_iff_ne_bot.mpr hne))
-  rw [RelSeries.cons_length] at hbound
-  omega
-
-/-- Any maximum-length chain in a bounded finite-height lattice ends at `⊤`. -/
-lemma longestChain_last : (longestChain (α := α)).last = ⊤ := by
-  by_contra hne
-  have hbound := chains_bounded ((longestChain (α := α)).snoc ⊤ (lt_top_iff_ne_top.mpr hne))
-  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 `α`,
+    The proof is fairly trivial: 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) :
+    (hfg : Function.LeftInverse f g) :
     FiniteHeightLattice β where
   toLattice := inferInstance
   toOrderBot := {
@@ -128,8 +107,7 @@ def transport {α β : Type*} [Lattice β]
     le_top := fun b => by
       rw [← hfg b]
       exact hf (_root_.le_top : g b ≤ (⊤ : α)) }
-  longestChain :=
-    I.longestChain.map f (hf.strictMono_of_injective hgf.injective)
+  height := I.height
   chains_bounded := fun c =>
     I.chains_bounded (c.map g (hg.strictMono_of_injective hfg.injective))
 
@@ -144,7 +122,7 @@ def ofUnique (α : Type*) [Lattice α] [Unique α] :
   toOrderTop := {
     top := default
     le_top := fun _ => le_of_eq (Subsingleton.elim _ _) }
-  longestChain := RelSeries.singleton _ default
+  height := 0
   chains_bounded := boundedChains_of_subsingleton α 0
 
 end FiniteHeightLattice

lean/Spa/Lattice/AboveBelow.lean

@@ -234,10 +234,7 @@ instance [Inhabited α] : FiniteHeightLattice (AboveBelow α) where
   toLattice := inferInstance
   toOrderBot := inferInstance
   toOrderTop := inferInstance
-  longestChain :=
-    ((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)
+  height := 2
   chains_bounded := boundedChains
 
 end AboveBelow

lean/Spa/Lattice/Bool.lean

@@ -31,8 +31,7 @@ instance : FiniteHeightLattice Bool where
   toLattice := inferInstance
   toOrderBot := inferInstance
   toOrderTop := inferInstance
-  longestChain := (RelSeries.singleton _ (⊥ : Bool)).snoc (⊤ : Bool)
-    (by rw [RelSeries.last_singleton]; exact bot_lt_top)
+  height := 1
   chains_bounded := boundedChains
 
 end Bool

lean/Spa/Lattice/Tuple.lean

@@ -107,66 +107,18 @@ section FiniteHeight
 
 variable [FiniteHeightLattice β]
 
-private lemma consBot_strictMono {n : ℕ} :
-    StrictMono (fun b : β => (Fin.cons b (⊥ : Fin n → β) : Fin (n + 1) → β)) := by
-  intro a b hab
-  refine lt_iff_le_and_ne.mpr ⟨?_, ?_⟩
-  · refine Pi.le_def.mpr (fun i => Fin.cases ?_ (fun j => ?_) i)
-    · simpa using hab.le
-    · simp
-  · exact fun h => hab.ne (by simpa using congrFun h 0)
-
-private lemma consTop_strictMono {n : ℕ} :
-    StrictMono (fun f : Fin n → β => (Fin.cons (⊤ : β) f : Fin (n + 1) → β)) := by
-  intro f g hfg
-  refine lt_iff_le_and_ne.mpr ⟨?_, ?_⟩
-  · refine Pi.le_def.mpr (fun i => Fin.cases ?_ (fun j => ?_) i)
-    · simp
-    · simpa using Pi.le_def.mp hfg.le j
-  · intro h
-    apply hfg.ne
-    funext j
-    simpa using congrFun h j.succ
-
-/-- The maximal chain in `Fin n → β`: walk the first tuple element from `⊥` to `⊤`
-    through `β`'s longest chain, then do that with the second element, and so on. -/
-private def stdChain : (n : ℕ) →
-    { 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,
-              FiniteHeightLattice.longestChain_last, prev.2.1]),
-        by
-          simp only [RelSeries.head_smash, LTSeries.head_map]
-          rw [FiniteHeightLattice.longestChain_head]
-          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
   toOrderBot := inferInstance
   toOrderTop := inferInstance
-  longestChain := (stdChain n).1
+  height := n * FiniteHeightLattice.height (α := β)
   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 :=
+        ≤ ∑ _i : Fin n, FiniteHeightLattice.height (α := β) :=
           Finset.sum_le_sum (fun i _ => FiniteHeightLattice.chains_bounded (cs i))
-      _ = n * (FiniteHeightLattice.longestChain (α := β)).length := by
+      _ = n * FiniteHeightLattice.height (α := β) := by
           simp [Finset.sum_const, Finset.card_univ, Fintype.card_fin]
 
 end FiniteHeight