DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Lean: inline BoundedChains.no_longer into FixedHeight.bot_le

Browse Source 
The lemma had a single caller. Inline it as `chains_bounded` applied to the
over-long chain, rewriting its length to `height + 1 ≤ height` and closing with
`omega`, and drop the standalone theorem.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This commit is contained in:
Danila Fedorin
2026-06-22 18:46:58 -05:00
parent 2ee32580a2
commit 8c37a4c049
1 changed files with 3 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files

10
lean/Spa/Lattice.lean
View File

@@ -56,10 +56,6 @@ structure PointedLTSeries (α : Type*) (f t : α)(n : ℕ) [Preorder α] where
last_series : series.last = t last_series : series.last = t
length_series : series.length = n length_series : series.length = n
theorem BoundedChains.no_longer {α : Type*} [Preorder α] {n : ℕ}
(h : BoundedChains α n) (c : LTSeries α) : c.length ≠ n + 1 :=
fun hc => absurd (h c) (by omega)
class FiniteHeightLattice (α : Type*) [Lattice α] extends Bot α, Top α where class FiniteHeightLattice (α : Type*) [Lattice α] extends Bot α, Top α where
height : ℕ height : ℕ
longest_chain : PointedLTSeries α ⊥ ⊤ height longest_chain : PointedLTSeries α ⊥ ⊤ height
@@ -78,9 +74,9 @@ theorem bot_le [FiniteHeightLattice α] : ∀ (a : α), ⊥ ≤ a := by
have hlt : ⊥ ⊓ a < lc.series.head := by have hlt : ⊥ ⊓ a < lc.series.head := by
rw [lc.head_series] rw [lc.head_series]
exact lt_of_le_of_ne inf_le_left heq exact lt_of_le_of_ne inf_le_left heq
exact FiniteHeightLattice.chains_bounded.no_longer have hbound := FiniteHeightLattice.chains_bounded (lc.series.cons (⊥ ⊓ a) hlt)
(lc.series.cons (⊥ ⊓ a) hlt) rw [RelSeries.cons_length, lc.length_series] at hbound
(by simp [RelSeries.cons_length, lc.length_series]) omega
end FixedHeight end FixedHeight