Examples.Classical.Lattices.L7¶
Worked example — the seven-element lattice L7¶
This is the Examples.Classical.Lattices.L7 module of the Agda Universal Algebra Library.
L7 is a seven-element lattice of interest in the Finite Lattice Representation
Problem (FLRP): it is, to our knowledge, the smallest lattice for which no
representation as the congruence lattice of a finite algebra is known. (This is a
question of the FLRP and must not be conflated with the separate
algebraic-complexity / CSP line of work — see CLAUDE.md.)
Its shape is as follows. Six of its elements form a 2 × 3 grid — the product of a
two-chain and a three-chain — with bottom ⊥ = (0,0), top ⊤ = (1,2), two atoms
(0,1) and (1,0), and two coatoms (0,2) and (1,1). The seventh element x
sits beside the grid with ⊥ < x < ⊤ and is incomparable to every nontrivial grid
element; consequently x is the unique element that is both an atom and a coatom.
Because x together with the chain (1,0) < (1,1) forms a pentagon N5, L7 is
not distributive, so it is a genuine Lattice example rather than a
DistributiveLattice one.
We label the carrier Fin 7 by ⊥ = 0, (1,0) = 1, (0,1) = 2, x = 3,
(1,1) = 4, (0,2) = 5, ⊤ = 6, giving the Hasse diagram
⊤ = 6
/ | \
(0,2)=5 (1,1)=4 \
| / \ \
| / \ \
(0,1)=2 (1,0)=1 x = 3
\ / |
\ / |
⊥ = 0 ───────────┘
As in the Heyting chain and the
finite-group examples, meet and join are given by
Cayley tables and every law is discharged by decision over the finite carrier — a
wrong table entry would make some decision compute to no and break compilation.
The Cayley tables¶
The pattern 6F (= suc 5F, from Data.Fin.Patterns) is the top element. Meet is
the greatest lower bound, join the least upper bound, read off the diagram above.
∧ |
0 | 1 | 2 | 3 | 4 | 5 | 6 | ∨ |
0 | 1 | 2 | 3 | 4 | 5 | 6 | |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 2 | 3 | 4 | 5 | 6 | |
| 1 | 0 | 1 | 0 | 0 | 1 | 0 | 1 | 1 | 1 | 1 | 4 | 6 | 4 | 6 | 6 | |
| 2 | 0 | 0 | 2 | 0 | 2 | 2 | 2 | 2 | 2 | 4 | 2 | 6 | 4 | 5 | 6 | |
| 3 | 0 | 0 | 0 | 3 | 0 | 0 | 3 | 3 | 3 | 6 | 6 | 3 | 6 | 6 | 6 | |
| 4 | 0 | 1 | 2 | 0 | 4 | 2 | 4 | 4 | 4 | 4 | 4 | 6 | 4 | 6 | 6 | |
| 5 | 0 | 0 | 2 | 0 | 2 | 5 | 5 | 5 | 5 | 6 | 5 | 6 | 6 | 5 | 6 | |
| 6 | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 6 | 6 | 6 | 6 | 6 | 6 | 6 | 6 |
∧-table : Table 7 ∧-table = (0F ∷ 0F ∷ 0F ∷ 0F ∷ 0F ∷ 0F ∷ 0F ∷ []) ∷ (0F ∷ 1F ∷ 0F ∷ 0F ∷ 1F ∷ 0F ∷ 1F ∷ []) ∷ (0F ∷ 0F ∷ 2F ∷ 0F ∷ 2F ∷ 2F ∷ 2F ∷ []) ∷ (0F ∷ 0F ∷ 0F ∷ 3F ∷ 0F ∷ 0F ∷ 3F ∷ []) ∷ (0F ∷ 1F ∷ 2F ∷ 0F ∷ 4F ∷ 2F ∷ 4F ∷ []) ∷ (0F ∷ 0F ∷ 2F ∷ 0F ∷ 2F ∷ 5F ∷ 5F ∷ []) ∷ (0F ∷ 1F ∷ 2F ∷ 3F ∷ 4F ∷ 5F ∷ 6F ∷ []) ∷ [] ∨-table : Table 7 ∨-table = (0F ∷ 1F ∷ 2F ∷ 3F ∷ 4F ∷ 5F ∷ 6F ∷ []) ∷ (1F ∷ 1F ∷ 4F ∷ 6F ∷ 4F ∷ 6F ∷ 6F ∷ []) ∷ (2F ∷ 4F ∷ 2F ∷ 6F ∷ 4F ∷ 5F ∷ 6F ∷ []) ∷ (3F ∷ 6F ∷ 6F ∷ 3F ∷ 6F ∷ 6F ∷ 6F ∷ []) ∷ (4F ∷ 4F ∷ 4F ∷ 6F ∷ 4F ∷ 6F ∷ 6F ∷ []) ∷ (5F ∷ 6F ∷ 5F ∷ 6F ∷ 6F ∷ 5F ∷ 6F ∷ []) ∷ (6F ∷ 6F ∷ 6F ∷ 6F ∷ 6F ∷ 6F ∷ 6F ∷ []) ∷ [] infixr 7 _∧_ infixr 6 _∨_ _∧_ _∨_ : Fin 7 → Fin 7 → Fin 7 _∧_ = ⟦ ∧-table ⟧ _∨_ = ⟦ ∨-table ⟧
L7 as a lattice¶
The decidable law-checkers all come from Overture.Operations.Properties:
associativity, commutativity, and idempotency of each operation, plus the two
absorption laws (Absorbsˡ?, Absorbsʳ?).
L7-lattice : Lattice L7-lattice = eqsToLattice (Fin 7) _∧_ _∨_ (from-yes (Associative? _∧_)) (from-yes (Commutative? _∧_)) (from-yes (Idempotent? _∧_)) (from-yes (Associative? _∨_)) (from-yes (Commutative? _∨_)) (from-yes (Idempotent? _∨_)) (from-yes (Absorbsˡ? _∧_ _∨_)) (from-yes (Absorbsʳ? _∧_ _∨_))
L7 is not distributive¶
The pentagon N5 on {⊥, (1,0), (1,1), x, ⊤} witnesses the failure of
distributivity: (1,0) < (1,1), while x is incomparable to both and joins each to
⊤ and meets each to ⊥. All five facts hold by refl.
n5-chain-l7 : (1F ∧ 4F) ≡ 1F -- (1,0) ≤ (1,1) n5-chain-l7 = refl n5-x∨lo-l7 : (3F ∨ 1F) ≡ 6F -- x ∨ (1,0) = ⊤ n5-x∨lo-l7 = refl n5-x∨hi-l7 : (3F ∨ 4F) ≡ 6F -- x ∨ (1,1) = ⊤ n5-x∨hi-l7 = refl n5-x∧lo-l7 : (3F ∧ 1F) ≡ 0F -- x ∧ (1,0) = ⊥ n5-x∧lo-l7 = refl n5-x∧hi-l7 : (3F ∧ 4F) ≡ 0F -- x ∧ (1,1) = ⊥ n5-x∧hi-l7 = refl -- Distributivity fails at (a,b,c) = ((1,1), (1,0), x): -- (1,1) ∧ ((1,0) ∨ x) = (1,1) ∧ ⊤ = (1,1), but -- ((1,1) ∧ (1,0)) ∨ ((1,1) ∧ x) = (1,0) ∨ ⊥ = (1,0). L7-not-distributive-l7 : (4F ∧ (1F ∨ 3F)) ≢ ((4F ∧ 1F) ∨ (4F ∧ 3F)) L7-not-distributive-l7 ()
x is the unique atom-coatom¶
With the meet order a ≤ b := a ∧ b ≡ a, an atom is a non-bottom element with
nothing strictly below it, and dually for a coatom. The order, the atom/coatom
predicates, and their deciders come from Classical.Properties.Lattice.FiniteOrder
(instantiated at _∧_, with bottom 0 and top 6). The atoms of L7 are
{(1,0), (0,1), x} and the coatoms are {x, (1,1), (0,2)}, so x is the unique
element that is both; this is decided over the finite carrier.
open FiniteOrder _∧_ open Bounded 0F 6F x-atom-l7 : atom 3F x-atom-l7 = from-yes (atom? 3F) x-coatom-l7 : coatom 3F x-coatom-l7 = from-yes (coatom? 3F) unique-atom-coatom-l7 : ∀ a → atom a → coatom a → a ≡ 3F unique-atom-coatom-l7 = from-yes (all? (λ a → (atom? a) →-dec ((coatom? a) →-dec (a ≟ 3F))))
Acceptance checks¶
The Lattice-Op accessors interpret to the tabulated meet and join on the nose, and
the bundle bridge round-trips; both discharged by refl.
open Polymorphic.Lattice-Op L7-lattice renaming ( _∧_ to _∙∧_ ; _∨_ to _∙∨_ ) ∙∧-is-∧-l7 : ∀ (a b : Fin 7) → a ∙∧ b ≡ a ∧ b ∙∧-is-∧-l7 a b = refl ∙∨-is-∨-l7 : ∀ (a b : Fin 7) → a ∙∨ b ≡ a ∨ b ∙∨-is-∨-l7 a b = refl open Polymorphic.Lattice-Op ⟪ ⟨ L7-lattice ⟩ˡᵃ ⟫ˡᵃ using () renaming ( _∧_ to _∙∧'_ ; _∨_ to _∙∨'_ ) roundtrip-∧-l7 : ∀ (a b : Fin 7) → a ∙∧' b ≡ a ∧ b roundtrip-∧-l7 a b = refl roundtrip-∨-l7 : ∀ (a b : Fin 7) → a ∙∨' b ≡ a ∨ b roundtrip-∨-l7 a b = refl