Lattices.Examples.M3¶

Worked example: the diamond `M₃`¶

This is the Lattices.Examples.M3 module of the agda-lattices library.

The lattice M₃ has a bottom ⊥, a top ⊤, and three atoms a, b, c between them, any two of which meet to ⊥ and join to ⊤. It is the smallest modular lattice that is not distributive, and it separates the conditions of Lattices.Semidistributive: it satisfies Whitman's condition (W) but neither semidistributive law.

(W) holds. If s₁ and s₂ are comparable, their meet is one of them, so a meet below t₁ ∨ t₂ has a meetand below it. Otherwise their meet is ⊥, which lies below t₁.
SD∨ fails. a ∨ b = ⊤ = a ∨ c, yet a ∨ (b ∧ c) = a ∨ ⊥ = a.
SD∧ fails, dually. a ∧ b = ⊥ = a ∧ c, yet a ∧ (b ∨ c) = a ∧ ⊤ = a.

So M₃ is not a sublattice of any free lattice, although it satisfies (W): the semidistributive laws pass to sublattices, and free lattices satisfy them (Lattices.Free.Semidistributive, over generators with decidable equality). These verdicts are not proved here by hand. The lattice is given by its two operation tables through Lattices.Table, and each verdict is the value of a decision procedure of Lattices.Semidistributive, extracted by from-yes or from-no; a wrong table, or a wrong procedure, would make the module fail to type-check. The three equations of the SD∨ failure above, and their duals, are checked separately by evaluation, as an illustration of what the procedure found.

{-# OPTIONS --without-K --exact-split --safe #-}

module Lattices.Examples.M3 where

-- Imports from the Agda Standard Library ---------------------------------------
open import Data.Fin.Base                          using ( Fin )
open import Data.Fin.Patterns                      using ( 0F ; 1F ; 2F ; 3F ; 4F )
open import Data.Product                           using ( _×_ ; _,_ ; proj₁ )
open import Data.Vec.Base                          using ( _∷_ ; [] )
open import Level                                  using ( 0ℓ )
open import Relation.Binary.PropositionalEquality  using ( _≡_ ; refl )
open import Relation.Nullary.Decidable.Core        using ( from-no )
open import Relation.Nullary.Negation.Core         using ( ¬_ )

-- Imports from the Agda Universal Algebra Library ------------------------------
open import Lattices.Semidistributive
  using  ( IsJoinSemidistributive ; IsMeetSemidistributive ; SatisfiesW
         ; isJoinSemidistributive? ; isMeetSemidistributive? ; satisfiesW? )
open import Classical.Structures.Lattice.Basic  using ( Lattice )
open import Lattices.Table  using ( LatticeTableLaws ; latticeTableLaws?
                                                      ; tableLattice ; tableLattice-FiniteAlgebra )
open import Overture.Cayley                     using ( Table ; ⟦_⟧ ; from-yes )
open import Setoid.Algebras.Finite              using ( FiniteAlgebra )

The tables¶

The carrier is Fin 5, with ⊥, a, b, c, ⊤ numbered 0 to 4.

`∧`	⊥	a	b	c	⊤	`∨`	⊥	a	b	c	⊤
⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥	a	b	c	⊤
a	⊥	a	⊥	⊥	a	a	a	a	⊤	⊤	⊤
b	⊥	⊥	b	⊥	b	b	b	⊤	b	⊤	⊤
c	⊥	⊥	⊥	c	c	c	c	⊤	⊤	c	⊤
⊤	⊥	a	b	c	⊤	⊤	⊤	⊤	⊤	⊤	⊤

infixl 7 _∧_ _∨_

⊥ a b c ⊤ : Fin 5
⊥ = 0F
a = 1F
b = 2F
c = 3F
⊤ = 4F

∧-table : Table 5
∧-table = (0F ∷ 0F ∷ 0F ∷ 0F ∷ 0F ∷ [])
        ∷ (0F ∷ 1F ∷ 0F ∷ 0F ∷ 1F ∷ [])
        ∷ (0F ∷ 0F ∷ 2F ∷ 0F ∷ 2F ∷ [])
        ∷ (0F ∷ 0F ∷ 0F ∷ 3F ∷ 3F ∷ [])
        ∷ (0F ∷ 1F ∷ 2F ∷ 3F ∷ 4F ∷ [])
        ∷ []

∨-table : Table 5
∨-table = (0F ∷ 1F ∷ 2F ∷ 3F ∷ 4F ∷ [])
        ∷ (1F ∷ 1F ∷ 4F ∷ 4F ∷ 4F ∷ [])
        ∷ (2F ∷ 4F ∷ 2F ∷ 4F ∷ 4F ∷ [])
        ∷ (3F ∷ 4F ∷ 4F ∷ 3F ∷ 4F ∷ [])
        ∷ (4F ∷ 4F ∷ 4F ∷ 4F ∷ 4F ∷ [])
        ∷ []

_∧_ _∨_ : Fin 5 → Fin 5 → Fin 5
_∧_ = ⟦ ∧-table ⟧
_∨_ = ⟦ ∨-table ⟧

The lattice¶

The eight lattice laws of the two tables are decided together, and from-yes of the decision is their proof (M₃-laws); M₃ is the lattice they make, and M₃-finite its enumeration by the identity on Fin 5.

M₃-laws : LatticeTableLaws _∧_ _∨_
M₃-laws = from-yes (latticeTableLaws? _∧_ _∨_)

M₃ : Lattice 0ℓ 0ℓ
M₃ = tableLattice _∧_ _∨_ M₃-laws

M₃-finite : FiniteAlgebra (proj₁ M₃)
M₃-finite = tableLattice-FiniteAlgebra _∧_ _∨_ M₃-laws

The verdicts¶

Each verdict is a decision procedure evaluated on M₃: from-yes when it answers yes, from-no when it answers no. The sweep for (W) visits all 5⁴ = 625 quadruples, and each semidistributive law 5³ = 125 triples.

M₃-satisfiesW : SatisfiesW M₃
M₃-satisfiesW = from-yes (satisfiesW? M₃ M₃-finite)

M₃-not-joinSemidistributive : ¬ IsJoinSemidistributive M₃
M₃-not-joinSemidistributive = from-no (isJoinSemidistributive? M₃ M₃-finite)

M₃-not-meetSemidistributive : ¬ IsMeetSemidistributive M₃
M₃-not-meetSemidistributive = from-no (isMeetSemidistributive? M₃ M₃-finite)

The failing instances¶

The instance of SD∨ that fails is a ∨ b = ⊤ = a ∨ c with a ∨ (b ∧ c) = a, and the instance of SD∧ that fails is its dual; both hold by evaluating the tables.

M₃-SD∨-failure : (a ∨ b ≡ ⊤) × (a ∨ c ≡ ⊤) × (a ∨ (b ∧ c) ≡ a)
M₃-SD∨-failure = refl , refl , refl

M₃-SD∧-failure : (a ∧ b ≡ ⊥) × (a ∧ c ≡ ⊥) × (a ∧ (b ∨ c) ≡ a)
M₃-SD∧-failure = refl , refl , refl

`∧`	⊥	a	b	c	⊤	`∨`	⊥	a	b	c	⊤
⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥	a	b	c	⊤
a	⊥	a	⊥	⊥	a	a	a	a	⊤	⊤	⊤
b	⊥	⊥	b	⊥	b	b	b	⊤	b	⊤	⊤
c	⊥	⊥	⊥	c	c	c	c	⊤	⊤	c	⊤
⊤	⊥	a	b	c	⊤	⊤	⊤	⊤	⊤	⊤	⊤

`∧`	⊥	a	b	c	⊤	`∨`	⊥	a	b	c	⊤
⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥	a	b	c	⊤
a	⊥	a	⊥	⊥	a	a	a	a	⊤	⊤	⊤
b	⊥	⊥	b	⊥	b	b	b	⊤	b	⊤	⊤
c	⊥	⊥	⊥	c	c	c	c	⊤	⊤	c	⊤
⊤	⊥	a	b	c	⊤	⊤	⊤	⊤	⊤	⊤	⊤