Make FiniteHeightLattice extend Lattice and derive Top/Bot

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

lean/Spa/Analysis/Forward.lean

@@ -7,7 +7,7 @@ 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 :=
@@ -33,8 +33,6 @@ 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)
 
@@ -58,7 +56,7 @@ lemma joinForKey_initialState :
 
 variable [I : LatticeInterpretation L] [V : ValidStmtEvaluator L prog]
 
-omit [FiniteHeightLattice L] [DecidableEq L] in
+omit [DecidableEq L] in
 lemma eval_fold_valid {s : prog.State} {bss : List BasicStmt}
     {vs : VariableValues L prog} {ρ₁ ρ₂ : Env}
     (hbss : EvalBasicStmts ρ₁ bss ρ₂) (hvs : ⟦ vs ⟧ ρ₁) :
@@ -67,7 +65,7 @@ lemma 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
+omit [DecidableEq L] in
 lemma updateVariablesForState_matches {s : prog.State}
     {sv : StateVariables L prog} {ρ₁ ρ₂ : Env}
     (hbss : EvalBasicStmts ρ₁ (prog.code s) ρ₂)
@@ -75,7 +73,7 @@ lemma updateVariablesForState_matches {s : prog.State}
     ⟦ updateVariablesForState s sv ⟧ ρ₂ :=
   eval_fold_valid hbss hvs
 
-omit [FiniteHeightLattice L] [DecidableEq L] in
+omit [DecidableEq L] in
 lemma updateAll_matches {s : prog.State} {sv : StateVariables L prog}
     {ρ₁ ρ₂ : Env} (hbss : EvalBasicStmts ρ₁ (prog.code s) ρ₂)
     (hvs : ⟦ variablesAt s sv ⟧ ρ₁) :

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⟩
@@ -39,7 +39,8 @@ lemma doStep_le (f : α → α) (hf : Monotone f)
     ∀ (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/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 ⊥
+  toLattice := inferInstance
-  top := f ⊤
-  height := I.height
   longestChain :=
-    { series :=
+    I.longestChain.map f (hf.strictMono_of_injective hgf.injective)
-        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 }
   chains_bounded := fun c =>
     I.chains_bounded (c.map g (hg.strictMono_of_injective hfg.injective))
 

lean/Spa/Lattice.lean

@@ -67,34 +67,44 @@ end Folds
 def BoundedChains (α : Type*) [Preorder α] (n : ℕ) : Prop :=
   ∀ c : LTSeries α, c.length ≤ n
 
-/-- Wrapper over `LTSeries` that exposes its beginning and end points, as well as its length, as part of the type. -/
-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*) [Lattice α] extends Bot α, Top α where
+class FiniteHeightLattice (α : Type*) extends Lattice α where
-  height : ℕ
+  longestChain : LTSeries α
-  longestChain : PointedLTSeries α ⊥ ⊤ height
+  chains_bounded : BoundedChains α longestChain.length
-  chains_bounded : BoundedChains α height
+
+-- a < ... < z
+-- ----------- length <= height
 
 namespace FiniteHeightLattice
 
-variable (α : Type*) [Lattice α] [FiniteHeightLattice α]
+def height (α : Type*) [FiniteHeightLattice α] : ℕ :=
+  (longestChain (α := α)).length
+
+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 < (longestChain (α := α)).head :=
-    have hlt : ⊥ ⊓ a < lc.series.head := by
+      lt_of_le_of_ne inf_le_left heq
-      rw [lc.head_series]
+    have hbound := chains_bounded ((longestChain (α := α)).cons (⊥ ⊓ a) hlt)
-      exact lt_of_le_of_ne inf_le_left heq
+    rw [RelSeries.cons_length] at hbound
-    have hbound := FiniteHeightLattice.chains_bounded (lc.series.cons (⊥ ⊓ a) hlt)
+    omega
-    rw [RelSeries.cons_length, lc.length_series] at hbound
+
+/-- 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

@@ -223,17 +223,11 @@ lemma boundedChains : BoundedChains (AboveBelow α) 2 := fun c => by
   omega
 
 instance [Inhabited α] : FiniteHeightLattice (AboveBelow α) where
-  bot := bot
+  toLattice := inferInstance
-  top := top
-  height := 2
   longestChain :=
-    { series :=
     ((RelSeries.singleton _ bot).snoc (mk default)
         (by rw [RelSeries.last_singleton]; exact bot_lt_mk default)).snoc top
       (by rw [RelSeries.last_snoc]; exact mk_lt_top default)
-      head_series := by simp
-      last_series := by simp
-      length_series := by simp [RelSeries.snoc, RelSeries.append] }
   chains_bounded := boundedChains
 
 end AboveBelow

lean/Spa/Lattice/Bool.lean

@@ -28,13 +28,9 @@ lemma boundedChains : BoundedChains Bool 1 := fun c => by
   omega
 
 instance : FiniteHeightLattice Bool where
-  height := 1
+  toLattice := inferInstance
-  longestChain :=
+  longestChain := (RelSeries.singleton _ (⊥ : Bool)).snoc (⊤ : Bool)
-    { series := (RelSeries.singleton _ (⊥ : Bool)).snoc (⊤ : Bool)
     (by rw [RelSeries.last_singleton]; exact bot_lt_top)
-      head_series := by simp
-      last_series := by simp
-      length_series := by simp [RelSeries.snoc, RelSeries.append] }
   chains_bounded := boundedChains
 
 end Bool

lean/Spa/Lattice/FiniteMap.lean

@@ -12,7 +12,7 @@ variable {A B : Type*} {ks : List A}
 instance [Lattice B] : Lattice (FiniteMap A B ks) :=
   inferInstanceAs (Lattice (Fin ks.length → B))
 
-instance [Lattice B] [FiniteHeightLattice B] : FiniteHeightLattice (FiniteMap A B ks) :=
+instance [FiniteHeightLattice B] : FiniteHeightLattice (FiniteMap A B ks) :=
   inferInstanceAs (FiniteHeightLattice (Fin ks.length → B))
 
 instance [DecidableEq B] : DecidableEq (FiniteMap A B ks) :=

lean/Spa/Lattice/IterProd.lean

@@ -13,11 +13,6 @@ namespace IterProd
 
 variable {A B : Type u}
 
-instance lattice [Lattice A] [Lattice B] :
-    ∀ k, Lattice (IterProd A B k)
-  | 0 => inferInstanceAs (Lattice B)
-  | k + 1 => @Prod.instLattice A (IterProd A B k) _ (lattice k)
-
 instance decidableEq [DecidableEq A] [DecidableEq B] :
     ∀ k, DecidableEq (IterProd A B k)
   | 0 => inferInstanceAs (DecidableEq B)
@@ -27,24 +22,14 @@ 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) _ (lattice k) _ (fixedHeight k)
+  | 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
 
-lemma 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

@@ -58,36 +58,23 @@ end Unzip
 
 section FixedHeight
 
-variable {α β : Type*} [Lattice α] [Lattice β]
+variable {α β : Type*}
 
 instance prod [A : FiniteHeightLattice α] [B : FiniteHeightLattice β] :
     FiniteHeightLattice (α × β) where
-  bot := ((⊥ : α), (⊥ : β))
+  toLattice := inferInstance
-  top := ((⊤ : α), (⊤ : β))
-  height := A.height + B.height
   longestChain :=
-    { series :=
     RelSeries.smash
-          (A.longestChain.series.map (fun a => (a, (⊥ : β)))
+      (A.longestChain.map (fun a => (a, (⊥ : β)))
         (fun _ _ h => Prod.mk_lt_mk_iff_left.mpr h))
-          (B.longestChain.series.map (fun b => ((⊤ : α), b))
+      (B.longestChain.map (fun b => ((⊤ : α), b))
         (fun _ _ h => Prod.mk_lt_mk_iff_right.mpr h))
-          (by simp [A.longestChain.last_series, B.longestChain.head_series])
+      rfl
-      head_series :=
-        (RelSeries.head_smash _).trans
-          ((LTSeries.head_map _ _ _).trans
-            (congrArg (·, (⊥ : β)) A.longestChain.head_series))
-      last_series :=
-        (RelSeries.last_smash _).trans
-          ((LTSeries.last_map _ _ _).trans
-            (congrArg ((⊤ : α), ·) B.longestChain.last_series))
-      length_series := by
-        show A.longestChain.series.length + B.longestChain.series.length = _
-        rw [A.longestChain.length_series, B.longestChain.length_series] }
   chains_bounded := fun c => by
     obtain ⟨c₁, c₂, -, -, -, -, hlen⟩ := LTSeries.exists_unzip c
     have h₁ := A.chains_bounded c₁
     have h₂ := B.chains_bounded c₂
+    show c.length ≤ A.longestChain.length + B.longestChain.length
     omega
 
 end FixedHeight

lean/Spa/Lattice/Tuple.lean

@@ -32,7 +32,7 @@ private lemma iterOfFun_funOfIter : ∀ {n : ℕ} (ip : IterProd B PUnit n),
     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 [Lattice B]
+variable [FiniteHeightLattice B]
 
 private lemma funOfIter_mono {n : ℕ} :
     Monotone (funOfIter : IterProd B PUnit n → (Fin n → B)) := by
@@ -55,7 +55,7 @@ private lemma iterOfFun_mono {n : ℕ} :
     intro f g h
     exact Prod.le_def.mpr ⟨h 0, ih fun i => h i.succ⟩
 
-instance instFiniteHeight {n : ℕ} [FiniteHeightLattice B] :
+instance instFiniteHeight {n : ℕ} :
     FiniteHeightLattice (Fin n → B) :=
   FiniteHeightLattice.transport funOfIter iterOfFun
     funOfIter_mono iterOfFun_mono iterOfFun_funOfIter funOfIter_iterOfFun

lean/Spa/Lattice/Unit.lean

@@ -9,14 +9,8 @@ lemma boundedChains_of_subsingleton (α : Type*) [Preorder α] [Subsingleton α]
   exact (c.step ⟨0, by omega⟩).ne (Subsingleton.elim _ _)
 
 instance : FiniteHeightLattice PUnit where
-  bot := PUnit.unit
+  toLattice := inferInstance
-  top := PUnit.unit
+  longestChain := RelSeries.singleton _ PUnit.unit
-  height := 0
-  longestChain :=
-    { series := RelSeries.singleton _ PUnit.unit
-      head_series := rfl
-      last_series := rfl
-      length_series := rfl }
   chains_bounded := boundedChains_of_subsingleton PUnit 0
 
 end Spa