From cbad43efdc8ee735b068119dc04cf765ff95f9d1 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 25 Jun 2026 18:42:28 -0500 Subject: [PATCH] Make FiniteHeightLattice extend Lattice and derive Top/Bot Co-Authored-By: Claude Opus 4.8 --- lean/Spa/Analysis/Forward.lean | 10 +++---- lean/Spa/Fixedpoint.lean | 7 ++--- lean/Spa/Isomorphism.lean | 12 +++------ lean/Spa/Lattice.lean | 46 +++++++++++++++++++------------- lean/Spa/Lattice/AboveBelow.lean | 14 +++------- lean/Spa/Lattice/Bool.lean | 10 +++---- lean/Spa/Lattice/FiniteMap.lean | 2 +- lean/Spa/Lattice/IterProd.lean | 17 +----------- lean/Spa/Lattice/Prod.lean | 31 +++++++-------------- lean/Spa/Lattice/Tuple.lean | 4 +-- lean/Spa/Lattice/Unit.lean | 10 ++----- 11 files changed, 61 insertions(+), 102 deletions(-) diff --git a/lean/Spa/Analysis/Forward.lean b/lean/Spa/Analysis/Forward.lean index 726ad2d..497226a 100644 --- a/lean/Spa/Analysis/Forward.lean +++ b/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 ⟧ ρ₁) : diff --git a/lean/Spa/Fixedpoint.lean b/lean/Spa/Fixedpoint.lean index 8dc04ef..6666277 100644 --- a/lean/Spa/Fixedpoint.lean +++ b/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 diff --git a/lean/Spa/Isomorphism.lean b/lean/Spa/Isomorphism.lean index d05b0cd..dd5e0e6 100644 --- a/lean/Spa/Isomorphism.lean +++ b/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)) diff --git a/lean/Spa/Lattice.lean b/lean/Spa/Lattice.lean index 34cf3d7..39e96d3 100644 --- a/lean/Spa/Lattice.lean +++ b/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 - height : ℕ - longestChain : PointedLTSeries α ⊥ ⊤ height - chains_bounded : BoundedChains α height +class FiniteHeightLattice (α : Type*) extends Lattice α where + longestChain : LTSeries α + chains_bounded : BoundedChains α longestChain.length + +-- 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 < 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 diff --git a/lean/Spa/Lattice/AboveBelow.lean b/lean/Spa/Lattice/AboveBelow.lean index 05bd6fe..d25b777 100644 --- a/lean/Spa/Lattice/AboveBelow.lean +++ b/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 - 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 diff --git a/lean/Spa/Lattice/Bool.lean b/lean/Spa/Lattice/Bool.lean index 4f93174..390a0c8 100644 --- a/lean/Spa/Lattice/Bool.lean +++ b/lean/Spa/Lattice/Bool.lean @@ -28,13 +28,9 @@ lemma boundedChains : BoundedChains Bool 1 := fun c => by omega instance : FiniteHeightLattice Bool where - height := 1 - longestChain := - { 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] } + toLattice := inferInstance + longestChain := (RelSeries.singleton _ (⊥ : Bool)).snoc (⊤ : Bool) + (by rw [RelSeries.last_singleton]; exact bot_lt_top) chains_bounded := boundedChains end Bool diff --git a/lean/Spa/Lattice/FiniteMap.lean b/lean/Spa/Lattice/FiniteMap.lean index 24a1927..4f3ee6c 100644 --- a/lean/Spa/Lattice/FiniteMap.lean +++ b/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) := diff --git a/lean/Spa/Lattice/IterProd.lean b/lean/Spa/Lattice/IterProd.lean index d910735..27d7752 100644 --- a/lean/Spa/Lattice/IterProd.lean +++ b/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 diff --git a/lean/Spa/Lattice/Prod.lean b/lean/Spa/Lattice/Prod.lean index a53a51b..ca382fd 100644 --- a/lean/Spa/Lattice/Prod.lean +++ b/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 := ((⊥ : α), (⊥ : β)) - 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 diff --git a/lean/Spa/Lattice/Tuple.lean b/lean/Spa/Lattice/Tuple.lean index ed37caa..ec2b3f6 100644 --- a/lean/Spa/Lattice/Tuple.lean +++ b/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 diff --git a/lean/Spa/Lattice/Unit.lean b/lean/Spa/Lattice/Unit.lean index 4a3c537..f63c415 100644 --- a/lean/Spa/Lattice/Unit.lean +++ b/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 - top := PUnit.unit - height := 0 - longestChain := - { series := RelSeries.singleton _ PUnit.unit - head_series := rfl - last_series := rfl - length_series := rfl } + toLattice := inferInstance + longestChain := RelSeries.singleton _ PUnit.unit chains_bounded := boundedChains_of_subsingleton PUnit 0 end Spa