43 lines
1.3 KiB
Lean4
43 lines
1.3 KiB
Lean4
|
import Spa.Lattice
|
|||
|
|
import Mathlib.Order.BooleanAlgebra
|
|||
|
|
|
|||
|
|
namespace Spa
|
|||
|
|
|
|||
|
|
/-! ### `Bool` as a finite-height lattice
|
|||
|
|
|
|||
|
|
`Bool` is the two-element lattice `false ≤ true` (with `⊥ = false`, `⊤ = true`).
|
|||
|
|
It is the building block of the "power set" lattice `FiniteMap A Bool ks`, used by
|
|||
|
|
the reaching-definitions analysis to represent sets of definition sites. -/
|
|||
|
|
|
|||
|
|
namespace Bool
|
|||
|
|
|
|||
|
|
/-- Rank of a boolean: `false ↦ 0`, `true ↦ 1`. Used to bound chains, mirroring
|
|||
|
|
`AboveBelow.rank`. -/
|
|||
|
|
def rank : Bool → ℕ
|
|||
|
|
| false => 0
|
|||
|
|
| true => 1
|
|||
|
|
|
|||
|
|
theorem rank_strictMono : StrictMono rank := by
|
|||
|
|
intro a b hab
|
|||
|
|
cases a <;> cases b <;> revert hab <;> decide
|
|||
|
|
|
|||
|
|
theorem boundedChains : BoundedChains Bool 1 := 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 ≤ 1 := by cases c.last <;> simp [rank]
|
|||
|
|
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] }
|
|||
|
|
chains_bounded := boundedChains
|
|||
|
|
|
|||
|
|
end Bool
|
|||
|
|
|
|||
|
|
end Spa
|