Examples.Classical.Lattices.L3Heyting¶
Worked example — the three-element chain as a finite Heyting algebra¶
This is the Examples.Classical.Lattices.L3Heyting module of the Agda Universal Algebra Library.
The three-element chain 𝟛 = {0 ≤ 1 ≤ 2} is the smallest non-Boolean Heyting
algebra: as a lattice it is (Fin 3, min, max), and because every chain is
distributive it is a
DistributiveLattice.
What makes it a Heyting algebra is a relative pseudocomplement (an implication)
_⇒_ satisfying the residuation adjunction
a ∧ b ≤ c ⟺ a ≤ (b ⇒ c),
where a ≤ b is the meet order a ∧ b ≡ a. The chain is presented as a lattice
example — concretely a distributive lattice — and the implication is supplied as an
extra operation whose residuation and Heyting identities are proved alongside.
Both the lattice operations and the implication are given by Cayley tables, and
every law — the ten distributive-lattice equations, the residuation adjunction, and
the Heyting identities — is discharged by decision over the finite carrier
(from-yes applied to an all?/_≟_ decision), exactly as in the
finite-group examples. A wrong table would make
the corresponding decision compute to no, and the example would fail to compile.
The Cayley tables¶
The carrier is Fin 3, ordered 0 ≤ 1 ≤ 2, with top element ⊤ = 2. Meet is the
minimum, join is the maximum, and the implication a ⇒ b is the largest x with
a ∧ x ≤ b — on a chain this is ⊤ when a ≤ b and b otherwise.
∧ |
0 | 1 | 2 | ∨ |
0 | 1 | 2 | ⇒ |
0 | 1 | 2 | ||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 0 | 0 | 0 | 0 | 0 | 0 | 1 | 2 | 0 | 2 | 2 | 2 | ||
| 1 | 0 | 1 | 1 | 1 | 1 | 1 | 2 | 1 | 0 | 2 | 2 | ||
| 2 | 0 | 1 | 2 | 2 | 2 | 2 | 2 | 2 | 0 | 1 | 2 |
infixr 7 _∧_ infixr 6 _∨_ infixr 5 _⇒_ ⊤ : Fin 3 ⊤ = 2F ∧-table : Table 3 ∧-table = (0F ∷ 0F ∷ 0F ∷ []) ∷ (0F ∷ 1F ∷ 1F ∷ []) ∷ (0F ∷ 1F ∷ 2F ∷ []) ∷ [] ∨-table : Table 3 ∨-table = (0F ∷ 1F ∷ 2F ∷ []) ∷ (1F ∷ 1F ∷ 2F ∷ []) ∷ (2F ∷ 2F ∷ 2F ∷ []) ∷ [] ⇒-table : Table 3 ⇒-table = (2F ∷ 2F ∷ 2F ∷ []) ∷ (0F ∷ 2F ∷ 2F ∷ []) ∷ (0F ∷ 1F ∷ 2F ∷ []) ∷ [] _∧_ _∨_ _⇒_ : Fin 3 → Fin 3 → Fin 3 _∧_ = ⟦ ∧-table ⟧ _∨_ = ⟦ ∨-table ⟧ _⇒_ = ⟦ ⇒-table ⟧
The chain as a distributive lattice¶
The decidable law-checkers all come from Overture.Operations.Properties:
associativity, commutativity, and idempotency of each operation, and the
two-operation absorption and distributivity laws (Absorbsˡ?, Absorbsʳ?,
Distributesˡ?). Note that the second distributivity law, ∨ over ∧, is
Distributesˡ? with the two operations exchanged.
chain3 : DistributiveLattice chain3 = eqsToDistributiveLattice (Fin 3) _∧_ _∨_ (from-yes (Associative? _∧_)) (from-yes (Commutative? _∧_)) (from-yes (Idempotent? _∧_)) (from-yes (Associative? _∨_)) (from-yes (Commutative? _∨_)) (from-yes (Idempotent? _∨_)) (from-yes (Absorbsˡ? _∧_ _∨_)) (from-yes (Absorbsʳ? _∧_ _∨_)) (from-yes (Distributesˡ? _∧_ _∨_)) (from-yes (Distributesˡ? _∨_ _∧_))
The residuation adjunction¶
The meet order a ≤ b := a ∧ b ≡ a and its decider _≤?_ come from
Classical.Properties.Lattice.FiniteOrder (instantiated at _∧_). The defining
property of the Heyting implication is the residuation adjunction between _∧ b and
b ⇒_: for all a b c, (a ∧ b) ≤ c holds iff a ≤ (b ⇒ c). Both directions are
decidable (each is an implication between decidable meet-order facts), so the
biconditional, quantified over the finite carrier, is decided and extracted by
from-yes.
open FiniteOrder _∧_ residuation? : Dec (∀ a b c → (a ∧ b ≤ c → a ≤ (b ⇒ c)) × (a ≤ (b ⇒ c) → a ∧ b ≤ c)) residuation? = all? (λ a → all? (λ b → all? (λ c → (a ∧ b ≤? c →-dec a ≤? (b ⇒ c)) ×-dec (a ≤? (b ⇒ c) →-dec a ∧ b ≤? c)))) residuation : ∀ a b c → ((a ∧ b) ≤ c → a ≤ (b ⇒ c)) × (a ≤ (b ⇒ c) → (a ∧ b) ≤ c) residuation = from-yes residuation?
Heyting identities¶
Three identities characteristic of the implication, each decided over the carrier:
a ⇒ a ≡ ⊤ (reflexivity); ⊤ ⇒ a ≡ a (the top element is the left unit of ⇒);
and a ∧ (a ⇒ b) ≡ a ∧ b (the equational form of modus ponens).
⇒-refl? : Dec (∀ a → (a ⇒ a) ≡ ⊤) ⇒-refl? = all? (λ a → (a ⇒ a) ≟ ⊤) ⊤-unitˡ? : Dec (∀ a → (⊤ ⇒ a) ≡ a) ⊤-unitˡ? = all? (λ a → (⊤ ⇒ a) ≟ a) modus-ponens? : Dec (∀ a b → a ∧ (a ⇒ b) ≡ a ∧ b) modus-ponens? = all? (λ a → all? (λ b → (a ∧ (a ⇒ b)) ≟ (a ∧ b))) ⇒-refl : ∀ a → (a ⇒ a) ≡ ⊤ ⇒-refl = from-yes ⇒-refl? ⊤-unitˡ : ∀ a → (⊤ ⇒ a) ≡ a ⊤-unitˡ = from-yes ⊤-unitˡ? modus-ponens : ∀ a b → a ∧ (a ⇒ b) ≡ a ∧ b modus-ponens = from-yes modus-ponens?
Acceptance checks¶
The DistributiveLattice-Op accessors interpret to the tabulated meet and join on
the nose, and the bundle bridge round-trips, both discharged by refl.
open Polymorphic.DistributiveLattice-Op chain3 renaming ( _∧_ to _∙∧_ ; _∨_ to _∙∨_ ) ∙∧-is-∧ : ∀ (a b : Fin 3) → a ∙∧ b ≡ a ∧ b ∙∧-is-∧ a b = refl ∙∨-is-∨ : ∀ (a b : Fin 3) → a ∙∨ b ≡ a ∨ b ∙∨-is-∨ a b = refl open Polymorphic.DistributiveLattice-Op ⟪ ⟨ chain3 ⟩ᵈˡ ⟫ᵈˡ using () renaming ( _∧_ to _∙∧'_ ; _∨_ to _∙∨'_ ) roundtrip-∧ : ∀ (a b : Fin 3) → a ∙∧' b ≡ a ∧ b roundtrip-∧ a b = refl roundtrip-∨ : ∀ (a b : Fin 3) → a ∙∨' b ≡ a ∨ b roundtrip-∨ a b = refl