Examples.Classical.Lattices.FreeLattice3¶

Worked example: computing in the free lattice on three generators¶

This is the Examples.Classical.Lattices.FreeLattice3 module of the Agda Universal Algebra Library.

The free lattice FL(3) on generators x, y, z is infinite, and every question about its order is decided by Whitman's procedure (_≤ʷ?_ of Classical.Structures.Lattice.Free.Whitman). This module asks a handful of such questions and lets Agda answer them by evaluation: each theorem below is from-yes or from-no applied to a decision, so it type checks only if the procedure computes the expected verdict, and a wrong expectation fails to compile. By Whitman's theorem (Classical.Structures.Lattice.Free.Universal) each verdict is a fact about all lattices: an inequality the procedure accepts holds in every lattice, and one it rejects fails in some lattice, namely in FL(3) itself.

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

module Examples.Classical.Lattices.FreeLattice3 where

-- Imports from Agda and the Agda Standard Library -----------------------------
open import Data.Fin.Base                        using ( Fin )
open import Data.Fin.Patterns                    using ( 0F ; 1F ; 2F )
open import Data.Fin.Properties                  using ( _≟_ )
open import Relation.Binary.Definitions          using ( DecidableEquality )
open import Relation.Binary.PropositionalEquality  using ( refl )
open import Relation.Nullary                     using ( ¬_ )
open import Relation.Nullary.Decidable.Core      using ( from-yes ; from-no )

-- Imports from the Agda Universal Algebra Library -----------------------------
open import Classical.Structures.Lattice.Free.Derivability  using ( E-Lattice ; ⊢? )
open import Classical.Structures.Lattice.Free.Term          using ( LatTerm ; ℊ ; _∧̇_ ; _∨̇_
                                                                  ; toTerm )
open import Classical.Structures.Lattice.Free.Whitman       using ( _≤ʷ_ ; _≈ʷ_
                                                                  ; module Decision
                                                                  ; ℊ≤ℊ ; ℊ≤∨ˡ ; ∧ˡ≤∨ )
open import Setoid.Varieties.SoundAndComplete               using ( _⊢_▹_≈_ )

The generators¶

The three generators are the terms ℊ 0F, ℊ 1F, and ℊ 2F over Fin 3. The procedure compares generators (rule 1) with the standard library's decidable equality of Fin 3, here _≟₃_, the instance at Fin 3 of _≟_; opening Decision at it brings the decision procedures _≤ʷ?_ and _≈ʷ?_ for FL(3) into scope.

x y z : LatTerm (Fin 3)
x = ℊ 0F
y = ℊ 1F
z = ℊ 2F

_≟₃_ : DecidableEquality (Fin 3)
_≟₃_ = _≟_

open Decision _≟₃_ using ( _≤ʷ?_ ; _≈ʷ?_ )

A derivation by hand¶

An inhabitant of s ≤ʷ t is a derivation by Whitman's rules, and small ones can be written out. The meet x ∧ y lies below the join x ∨ z by Whitman's condition (rule 6, the disjunct ∧ˡ≤∨), because its meetand x lies below the join (rule 4, the disjunct ℊ≤∨ˡ), because x is x (rule 1).

meet≤join : x ∧̇ y ≤ʷ x ∨̇ z
meet≤join = ∧ˡ≤∨ (ℊ≤∨ˡ (ℊ≤ℊ refl))

Distributivity fails¶

In a distributive lattice x ∧ (y ∨ z) = (x ∧ y) ∨ (x ∧ z). In every lattice the right side is below the left (distrib-≥), but the free lattice does not satisfy the other inequality (distrib-≰). By hand: the left side is a meet and the right side a join, so only Whitman's condition applies, and each of its four disjuncts fails. The meetand x is not below the join, since by rule 4 it would be below x ∧ y or x ∧ z, hence below y or z. The meetand y ∨ z is not below the join, since by rule 2 its joinand y would be, and y is below neither joinand, not being below x. And the whole meet is below neither joinand, since by rule 3 it would be below y or below z, which by rule 5 needs x or y ∨ z below that generator, and neither is. The diamond M₃ and the pentagon N₅, the two nondistributive lattices on five elements, are both generated by three elements, hence images of FL(3), and in each the inequality fails under a suitable assignment of x, y, and z.

distrib-≥ : (x ∧̇ y) ∨̇ (x ∧̇ z) ≤ʷ x ∧̇ (y ∨̇ z)
distrib-≥ = from-yes ((x ∧̇ y) ∨̇ (x ∧̇ z) ≤ʷ? x ∧̇ (y ∨̇ z))

distrib-≰ : ¬ (x ∧̇ (y ∨̇ z) ≤ʷ (x ∧̇ y) ∨̇ (x ∧̇ z))
distrib-≰ = from-no (x ∧̇ (y ∨̇ z) ≤ʷ? (x ∧̇ y) ∨̇ (x ∧̇ z))

Modularity fails¶

The modular law is the weaker identity x ∧ (y ∨ (x ∧ z)) = (x ∧ y) ∨ (x ∧ z), the distributive law x ∧ (y ∨ w) = (x ∧ y) ∨ (x ∧ w) restricted to elements w = x ∧ z below x. It fails in FL(3) as well (modular-≰), as it must, since the pentagon N₅ is generated by three elements and is not modular.

modular-≰ : ¬ (x ∧̇ (y ∨̇ (x ∧̇ z)) ≤ʷ (x ∧̇ y) ∨̇ (x ∧̇ z))
modular-≰ = from-no (x ∧̇ (y ∨̇ (x ∧̇ z)) ≤ʷ? (x ∧̇ y) ∨̇ (x ∧̇ z))

Absorption holds¶

The two absorption laws of Th-Lattice hold in every lattice, so the procedure must find both sides of each equal in FL(3); equality is mutual _≤ʷ_, decided by _≈ʷ?_.

absorbˡ : x ∧̇ (x ∨̇ y) ≈ʷ x
absorbˡ = from-yes (x ∧̇ (x ∨̇ y) ≈ʷ? x)

absorbʳ : (x ∧̇ y) ∨̇ x ≈ʷ x
absorbʳ = from-yes ((x ∧̇ y) ∨̇ x ≈ʷ? x)

What the lattice axioms derive¶

Through the bridge of Classical.Structures.Lattice.Free.Derivability, the same computations decide derivability in equational logic from the eight axioms of Th-Lattice. The distributive law is not a consequence of them (distrib-underivable), a theorem proved here by evaluation; and the first absorption law, translated to a Term, is derivable (absorbˡ-derivable), by a derivation the bridge constructs from Whitman's verdict through Birkhoff's completeness theorem, not one written by hand.

distrib-underivable :
  ¬ (E-Lattice ⊢ Fin 3 ▹ toTerm (x ∧̇ (y ∨̇ z)) ≈ toTerm ((x ∧̇ y) ∨̇ (x ∧̇ z)))
distrib-underivable = from-no (⊢? _≟₃_ (toTerm (x ∧̇ (y ∨̇ z))) (toTerm ((x ∧̇ y) ∨̇ (x ∧̇ z))))

absorbˡ-derivable : E-Lattice ⊢ Fin 3 ▹ toTerm (x ∧̇ (x ∨̇ y)) ≈ toTerm x
absorbˡ-derivable = from-yes (⊢? _≟₃_ (toTerm (x ∧̇ (x ∨̇ y))) (toTerm x))