From 4c337afa9cbecbbee643fc85ec65d5df28d3d70f Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Tue, 9 Jun 2026 18:48:02 -0700 Subject: [PATCH] Lean migration: Phase 3 (Unit, Prod, AboveBelow lattices) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Spa.Lattice.Unit: PUnit fixed height 0 (lattice lifted from mathlib) - Spa.Lattice.Prod: chain unzip + FixedHeight (h1+h2) on products (componentwise lattice lifted from mathlib's Prod.instLattice) - Spa.Lattice.AboveBelow: flat lattice via Lattice.mk' (mirrors the Agda semilattices+absorption construction), boundedness via rank into Nat, Plain x ↦ plainFixedHeight x, height 2 Co-Authored-By: Claude Fable 5 --- lean/Spa.lean | 3 + lean/Spa/Lattice/AboveBelow.lean | 199 +++++++++++++++++++++++++++++++ lean/Spa/Lattice/Prod.lean | 113 ++++++++++++++++++ lean/Spa/Lattice/Unit.lean | 32 +++++ 4 files changed, 347 insertions(+) create mode 100644 lean/Spa/Lattice/AboveBelow.lean create mode 100644 lean/Spa/Lattice/Prod.lean create mode 100644 lean/Spa/Lattice/Unit.lean diff --git a/lean/Spa.lean b/lean/Spa.lean index 2768b75..a980c3d 100644 --- a/lean/Spa.lean +++ b/lean/Spa.lean @@ -1,3 +1,6 @@ import Spa.Lattice import Spa.Fixedpoint import Spa.Isomorphism +import Spa.Lattice.Unit +import Spa.Lattice.Prod +import Spa.Lattice.AboveBelow diff --git a/lean/Spa/Lattice/AboveBelow.lean b/lean/Spa/Lattice/AboveBelow.lean new file mode 100644 index 0000000..06937b9 --- /dev/null +++ b/lean/Spa/Lattice/AboveBelow.lean @@ -0,0 +1,199 @@ +/- +Port of `Lattice/AboveBelow.agda`: the flat lattice obtained by adjoining a +top and bottom element to an (unordered, decidable-equality) type. + +With propositional equality the `_≈_` data type and its equivalence/decidability +proofs disappear (`deriving DecidableEq`). The lattice itself cannot be lifted: +mathlib has no "flat lattice on a discrete type". The `Lattice` instance is +built with `Lattice.mk'`, which — exactly like the Agda module — consumes the +two semilattices (comm/assoc, idempotence derived) plus the absorption laws, +and defines `a ≤ b ↔ a ⊔ b = b` (Agda's `_≼_`). + +The Agda module's `Plain x` submodule (the witness `x` seeds the longest chain +`⊥ ≺ [x] ≺ ⊤`) becomes `plainFixedHeight x`; the boundedness proof `isLongest` +is restated through a rank function since chains are mathlib `LTSeries` rather +than a pattern-matchable inductive (the `¬-Chain-⊤`-style case analysis lives +in `rank_strictMono`). +-/ +import Spa.Lattice + +namespace Spa + +/-- Agda: `AboveBelow` with constructors `⊥`, `⊤`, `[_]`. -/ +inductive AboveBelow (α : Type*) where + | bot + | top + | mk (x : α) + deriving DecidableEq + +namespace AboveBelow + +/-- Agda: the `Showable` instance. -/ +instance {α : Type*} [ToString α] : ToString (AboveBelow α) where + toString + | bot => "⊥" + | top => "⊤" + | mk x => toString x + +variable {α : Type*} [DecidableEq α] + +instance : Max (AboveBelow α) where + max + | bot, x => x + | top, _ => top + | mk x, mk y => if x = y then mk x else top + | mk x, bot => mk x + | mk _, top => top + +instance : Min (AboveBelow α) where + min + | bot, _ => bot + | top, x => x + | mk x, mk y => if x = y then mk x else bot + | mk _, bot => bot + | mk x, top => mk x + +/-! Agda: `⊥⊔x≡x`, `⊤⊔x≡⊤`, `x⊔⊥≡x`, `x⊔⊤≡⊤`, and the `[x]⊔[y]` reductions +(`x≈y⇒[x]⊔[y]≡[x]` / `x̷≈y⇒[x]⊔[y]≡⊤` are the two branches of `mk_sup_mk`). -/ + +@[simp] theorem bot_sup (x : AboveBelow α) : bot ⊔ x = x := rfl +@[simp] theorem top_sup (x : AboveBelow α) : top ⊔ x = top := rfl +@[simp] theorem sup_bot (x : AboveBelow α) : x ⊔ bot = x := by cases x <;> rfl +@[simp] theorem sup_top (x : AboveBelow α) : x ⊔ top = top := by cases x <;> rfl +@[simp] theorem mk_sup_mk (x y : α) : + (mk x ⊔ mk y : AboveBelow α) = if x = y then mk x else top := rfl + +@[simp] theorem bot_inf (x : AboveBelow α) : bot ⊓ x = bot := rfl +@[simp] theorem top_inf (x : AboveBelow α) : top ⊓ x = x := rfl +@[simp] theorem inf_bot (x : AboveBelow α) : x ⊓ bot = bot := by cases x <;> rfl +@[simp] theorem inf_top (x : AboveBelow α) : x ⊓ top = x := by cases x <;> rfl +@[simp] theorem mk_inf_mk (x y : α) : + (mk x ⊓ mk y : AboveBelow α) = if x = y then mk x else bot := rfl + +/-- Agda: `⊔-comm`. -/ +protected theorem sup_comm (a b : AboveBelow α) : a ⊔ b = b ⊔ a := by + rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> simp only + [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk] + split_ifs with h₁ h₂ h₂ <;> simp_all + +/-- Agda: `⊔-assoc`. -/ +protected theorem sup_assoc (a b c : AboveBelow α) : a ⊔ b ⊔ c = a ⊔ (b ⊔ c) := by + rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> rcases c with _ | _ | z <;> + simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk] + split_ifs <;> simp_all + +/-- Agda: `⊓-comm`. -/ +protected theorem inf_comm (a b : AboveBelow α) : a ⊓ b = b ⊓ a := by + rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> simp only + [bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk] + split_ifs with h₁ h₂ h₂ <;> simp_all + +/-- Agda: `⊓-assoc`. -/ +protected theorem inf_assoc (a b c : AboveBelow α) : a ⊓ b ⊓ c = a ⊓ (b ⊓ c) := by + rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> rcases c with _ | _ | z <;> + simp only [bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk] + split_ifs <;> simp_all + +/-- Agda: `absorb-⊔-⊓`. -/ +protected theorem sup_inf_self (a b : AboveBelow α) : a ⊔ a ⊓ b = a := by + rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> + simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk, + bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk] <;> + try (split_ifs <;> simp_all) + +/-- Agda: `absorb-⊓-⊔`. -/ +protected theorem inf_sup_self (a b : AboveBelow α) : a ⊓ (a ⊔ b) = a := by + rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> + simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk, + bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk] <;> + try (split_ifs <;> simp_all) + +/-- Agda: `isLattice` (via the two semilattices + absorption, like the Agda +record; `Lattice.mk'` derives idempotence and sets `a ≤ b ↔ a ⊔ b = b`). -/ +instance : Lattice (AboveBelow α) := + Lattice.mk' AboveBelow.sup_comm AboveBelow.sup_assoc + AboveBelow.inf_comm AboveBelow.inf_assoc + AboveBelow.sup_inf_self AboveBelow.inf_sup_self + +theorem le_iff {a b : AboveBelow α} : a ≤ b ↔ a ⊔ b = b := sup_eq_right.symm + +/-- Agda: `⊥≺[x]` (the `≤` part; `⊥` is least). -/ +theorem bot_le' (a : AboveBelow α) : (bot : AboveBelow α) ≤ a := + le_iff.mpr (bot_sup a) + +/-- Agda: `[x]≺⊤` (the `≤` part; `⊤` is greatest). -/ +theorem le_top' (a : AboveBelow α) : a ≤ (top : AboveBelow α) := + le_iff.mpr (sup_top a) + +theorem bot_lt_mk (x : α) : (bot : AboveBelow α) < mk x := + lt_of_le_of_ne (bot_le' _) (by simp) + +theorem mk_lt_top (x : α) : (mk x : AboveBelow α) < top := + lt_of_le_of_ne (le_top' _) (by simp) + +theorem bot_lt_top : (bot : AboveBelow α) < top := + lt_of_le_of_ne (bot_le' _) (by simp) + +/-- Rank of an element: `⊥ ↦ 0`, `[x] ↦ 1`, `⊤ ↦ 2`. Used to bound chains +(Agda's `isLongest` / `x≺[y]⇒x≡⊥` / `[x]≺y⇒y≡⊤` case analysis lives here). -/ +def rank : AboveBelow α → ℕ + | bot => 0 + | mk _ => 1 + | top => 2 + +/-- Agda: the impossibility of `[x] ≺ [y]` (combines `x≺[y]⇒x≡⊥` and +`[x]≺y⇒y≡⊤`: the flat middle layer is an antichain). -/ +theorem not_mk_lt_mk (x y : α) : ¬(mk x : AboveBelow α) < mk y := by + intro h + obtain ⟨hle, hne⟩ := lt_iff_le_and_ne.mp h + have hsup := le_iff.mp hle + rw [mk_sup_mk] at hsup + by_cases hxy : x = y + · rw [if_pos hxy] at hsup + exact hne hsup + · rw [if_neg hxy] at hsup + exact absurd hsup (by simp) + +theorem rank_strictMono : StrictMono (rank : AboveBelow α → ℕ) := by + intro a b hab + rcases a with _ | _ | x <;> rcases b with _ | _ | y + · exact absurd hab (lt_irrefl _) + · simp [rank] + · simp [rank] + · exact absurd hab (bot_le' _).not_lt + · exact absurd hab (lt_irrefl _) + · exact absurd hab (le_top' _).not_lt + · exact absurd hab (bot_le' _).not_lt + · simp [rank] + · exact absurd hab (not_mk_lt_mk x y) + +/-- Agda: `isLongest` — no chain is longer than 2. -/ +theorem boundedChains : BoundedChains (AboveBelow α) 2 := fun c => by + have h := LTSeries.head_add_length_le_nat (c.map rank rank_strictMono) + rw [LTSeries.head_map, LTSeries.last_map, LTSeries.map_length] at h + have h2 : rank c.last ≤ 2 := by cases c.last <;> simp [rank] + omega + +/-- Agda: `Plain.longestChain` and `Plain.fixedHeight` — the witness `x` +seeds the chain `⊥ ≺ [x] ≺ ⊤` of length 2. -/ +def plainFixedHeight (x : α) : FixedHeight (AboveBelow α) 2 where + bot := bot + top := top + longestChain := + ((RelSeries.singleton _ bot).snoc (mk x) + (by rw [RelSeries.last_singleton]; exact bot_lt_mk x)).snoc top + (by rw [RelSeries.last_snoc]; exact mk_lt_top x) + head_longestChain := by simp + last_longestChain := by simp + length_longestChain := by simp [RelSeries.snoc, RelSeries.append] + bounded := boundedChains + +/-- Agda: `Plain.isFiniteHeightLattice` / `Plain.finiteHeightLattice` +(`default` plays the role of the Agda module parameter `x`). -/ +instance [Inhabited α] : FiniteHeightLattice (AboveBelow α) where + height := 2 + fixedHeight := plainFixedHeight default + +end AboveBelow + +end Spa diff --git a/lean/Spa/Lattice/Prod.lean b/lean/Spa/Lattice/Prod.lean new file mode 100644 index 0000000..240dabd --- /dev/null +++ b/lean/Spa/Lattice/Prod.lean @@ -0,0 +1,113 @@ +/- +Port of `Lattice/Prod.agda`. + +The component-wise lattice structure on `α × β` is lifted into mathlib +(`Prod.instLattice`), as is decidability of equality. What remains custom is +the fixed-height content: + + unzip ↦ LTSeries.exists_unzip + a,∙-Monotonic/∙,b-Monotonic ↦ Prod.mk_lt_mk_iff_right/left (strict mono of + the two injections, used to map the chains) + fixedHeight (h₁ + h₂) ↦ FixedHeight.prod + isFiniteHeightLattice ↦ instance FiniteHeightLattice (α × β) +-/ +import Spa.Lattice + +namespace Spa + +section Unzip + +variable {α β : Type*} [PartialOrder α] [PartialOrder β] + +/-- Agda: `unzip` — a chain in the product splits into chains of the +components whose lengths sum to at least the original length. -/ +theorem 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 + 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 := by + have h := c.step ⟨0, by omega⟩ + have h1 : (⟨0, by omega⟩ : Fin c.length).succ = 1 := by + ext; simp [Fin.val_one, Nat.mod_eq_of_lt (by omega : 1 < c.length + 1)] + rwa [h1] at h + 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*} [Lattice α] [Lattice β] + +/-- Agda: `Lattice/Prod.agda`'s `fixedHeight` — the product of lattices of +heights `h₁` and `h₂` has height `h₁ + h₂`. The longest chain climbs the first +component (at `⊥₂`), then the second component (at `⊤₁`). -/ +def FixedHeight.prod {h₁ h₂ : ℕ} (fhA : FixedHeight α h₁) (fhB : FixedHeight β h₂) : + FixedHeight (α × β) (h₁ + h₂) where + bot := (fhA.bot, fhB.bot) + top := (fhA.top, fhB.top) + longestChain := + RelSeries.smash + (fhA.longestChain.map (fun a => (a, fhB.bot)) + (fun _ _ h => Prod.mk_lt_mk_iff_left.mpr h)) + (fhB.longestChain.map (fun b => (fhA.top, b)) + (fun _ _ h => Prod.mk_lt_mk_iff_right.mpr h)) + (by simp [fhA.last_longestChain, fhB.head_longestChain]) + head_longestChain := by simp [fhA.head_longestChain] + last_longestChain := by simp [fhB.last_longestChain] + length_longestChain := by + simp [fhA.length_longestChain, fhB.length_longestChain] + bounded := fun c => by + obtain ⟨c₁, c₂, -, -, -, -, hlen⟩ := LTSeries.exists_unzip c + have h₁ := fhA.bounded c₁ + have h₂ := fhB.bounded c₂ + omega + +/-- Agda: `Lattice/Prod.agda`'s `isFiniteHeightLattice`/`finiteHeightLattice`. -/ +instance [IA : FiniteHeightLattice α] [IB : FiniteHeightLattice β] : + FiniteHeightLattice (α × β) where + height := IA.height + IB.height + fixedHeight := IA.fixedHeight.prod IB.fixedHeight + +end FixedHeight + +end Spa diff --git a/lean/Spa/Lattice/Unit.lean b/lean/Spa/Lattice/Unit.lean new file mode 100644 index 0000000..3e7cc22 --- /dev/null +++ b/lean/Spa/Lattice/Unit.lean @@ -0,0 +1,32 @@ +/- +Port of `Lattice/Unit.agda`. + +The lattice structure itself (`_⊔_`, `_⊓_`, all semilattice/lattice laws) is +lifted into mathlib: `PUnit.instLinearOrder` provides `Lattice PUnit`. +What remains is the fixed-height structure: the unit lattice has height 0. +-/ +import Spa.Lattice + +namespace Spa + +/-- Chains in a subsingleton order are bounded by any `n` (Agda: the `bounded` +field of `Lattice/Unit.agda`'s `fixedHeight`, generalized). -/ +theorem 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 _ _) + +/-- Agda: `Lattice/Unit.agda`'s `fixedHeight`/`isFiniteHeightLattice`. -/ +instance : FiniteHeightLattice PUnit where + height := 0 + fixedHeight := + { bot := PUnit.unit + top := PUnit.unit + longestChain := RelSeries.singleton _ PUnit.unit + head_longestChain := rfl + last_longestChain := rfl + length_longestChain := rfl + bounded := boundedChains_of_subsingleton PUnit 0 } + +end Spa