121 lines
4.2 KiB
Lean4
121 lines
4.2 KiB
Lean4
import Spa.Lattice
|
||
|
||
/-!
|
||
|
||
# Product Lattice
|
||
|
||
This file provides a proof that, in addition to being a lattice,
|
||
the product of two types $\alpha \times \beta$ forms a `Spa.FiniteHeightLattice`
|
||
if both $\alpha$ and $\beta$ have a finite height.
|
||
|
||
The proof proceeds by "unzipping" a chain:
|
||
|
||
$$
|
||
(a_1, b_1) < (a_1, b_2) < \ldots < (a_n, b_m)
|
||
$$
|
||
|
||
In which, at each step, either an $\alpha$ or $\beta$ element
|
||
might ratchet up, into two chains:
|
||
|
||
$$
|
||
\begin{aligned}
|
||
a_1 < \ldots < a_n \\
|
||
b_1 < \ldots < b_m
|
||
\end{aligned}
|
||
$$
|
||
|
||
Because at least one of the two "unzipped" chains grows with
|
||
each element of the product chain, the full chain length
|
||
can't exceed the sum of the two components. By the definition
|
||
of finite height, these two chains are bounded, and therefore,
|
||
the product chain is bounded too.
|
||
|
||
-/
|
||
|
||
namespace Spa
|
||
|
||
section Unzip
|
||
|
||
variable {α β : Type*} [PartialOrder α] [PartialOrder β]
|
||
|
||
/-- The unzipping lemma: any chain (`LTSeries`) of product
|
||
elements can be decomposed into chains of components,
|
||
whose lengths bound the chain. -/
|
||
lemma 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
|
||
haveI : NeZero c.length := ⟨h0⟩
|
||
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 := c.strictMono Fin.one_pos'
|
||
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*}
|
||
|
||
/-- The longest possible chain is one in which only one of the components grows
|
||
at a time, making the maximum height of $\alpha \times \beta$ be
|
||
$\text{height}_\alpha + \text{height}_\beta$. -/
|
||
instance prod [A : FiniteHeightLattice α] [B : FiniteHeightLattice β] :
|
||
FiniteHeightLattice (α × β) where
|
||
toLattice := inferInstance
|
||
longestChain :=
|
||
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
|
||
|
||
end Spa
|