Examples.Classical.Lattices.L2

Worked Example: 𝑳𝟚 = (Bool, _∧_, _∨_) as a Boolean lattice

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

Bool under meet and join forms the canonical two-element lattice. Built from stdlib's Data.Bool.Properties lemmas; the only non-trivial step is deriving the (a ∧ b) ∨ a ≡ a form of absorption from stdlib's ∨-absorbs-∧ form via ∨-comm.

{-# OPTIONS --cubical-compatible --exact-split --safe #-}
module Examples.Classical.Lattices.L2 where

-- Imports from the Agda Standard Library -------------------------------------
open import Data.Bool             using ( Bool ; _∧_ ; _∨_ )
open import Data.Bool.Properties  using ( ∧-assoc ; ∧-comm ; ∧-idem ; ∨-assoc ; ∨-comm ; ∨-idem )
                                  renaming ( ∧-abs-∨ to ∧-absorbs-∨ ; ∨-abs-∧ to ∨-absorbs-∧ )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl ; trans )

-- Imports from the Agda Universal Algebra Library ----------------------------
open import Classical.Bundles.Lattice           using ( ⟨_⟩ˡᵃ ; ⟪_⟫ˡᵃ )
open import Classical.Small.Structures.Lattice  using ( Lattice ; eqsToLattice )
import Classical.Structures.Lattice as Polymorphic

Deriving the second absorption equation

Our eqsToLattice takes the second absorption equation in the form (a ∧ b) ∨ a ≡ a (per Th-Lattice absorbʳ = AbsorbsRight ∧-Op ∨-Op refl refl 0F 1F); stdlib's Data.Bool.Properties.∨-absorbs-∧ is a ∨ (a ∧ b) ≡ a. One ∨-comm step bridges them.

Bool-absorbʳ : ∀ a b → (a ∧ b) ∨ a ≡ a
Bool-absorbʳ a b = trans (∨-comm (a ∧ b) a) (∨-absorbs-∧ a b)

The lattice 𝑳𝟚 = (Bool, _∧_, _∨_)

𝑳𝟚 : Lattice
𝑳𝟚 = eqsToLattice Bool _∧_ _∨_
  ∧-assoc ∧-comm ∧-idem ∨-assoc ∨-comm ∨-idem ∧-absorbs-∨ Bool-absorbʳ

Acceptance checks

The Lattice-Op accessors interpret to stdlib's Bool._∧_ and Bool._∨_ on the nose: no opacity from eqsToLattice, from the factoring through opsToBareLattice, or from Curry₂ wrapping; discharged by refl.

open Polymorphic.Lattice-Op 𝑳𝟚 renaming ( _∧_ to _∙∧_ ; _∨_ to _∙∨_ )

∙∧-is-∧-la : ∀ (a b : Bool) → a ∙∧ b ≡ a ∧ b
∙∧-is-∧-la a b = refl

∙∨-is-∨-la : ∀ (a b : Bool) → a ∙∨ b ≡ a ∨ b
∙∨-is-∨-la a b = refl

Round-trip through Algebra.Lattice.Bundles.Lattice

The bundle bridge round-trips on Bool-lattice pointwise on both operations. Both directions reduce by pair a b 0F ⇉ a and pair a b 1F ⇉ b, so propositional refl discharges the obligation at the curried form (per ADR-002 v2 §6).

open Polymorphic.Lattice-Op ⟪ ⟨ 𝑳𝟚 ⟩ˡᵃ ⟫ˡᵃ using ()
  renaming ( _∧_ to _∙∧'_ ; _∨_ to _∙∨'_ )

roundtrip-∧-la : ∀ (a b : Bool) → a ∙∧' b ≡ a ∧ b
roundtrip-∧-la a b = refl

roundtrip-∨-la : ∀ (a b : Bool) → a ∙∨' b ≡ a ∨ b
roundtrip-∨-la a b = refl

This closes the third bullet of the M3-7 acceptance criteria.