Lattices.Distributive¶
Distributive lattices¶
This is the Lattices.Distributive module of the agda-lattices library.
A distributive lattice inhabits Σ[ 𝑨 ∈ Algebra α ρ ] 𝑨 ⊨ Th-DistributiveLattice
over the same Sig-Lattice signature as Lattice.
It is an equation-only extension of Lattice: the forgetful
distributiveLattice→lattice is a pure theory-reindex (the two distributivity
equations are dropped, the remaining eight map across definitionally), and
DistributiveLattice-Op inherits _∧_, _∨_, both congruences, the node bridges,
and all eight lattice laws through it. This is the two-operation analogue of how
CommutativeMonoid extends Monoid.
On top of the inherited laws this module adds four distributivity laws in curried
form: the two left laws ∧-distribˡ-law and ∨-distribˡ-law come straight from
the theory's two witnesses (the proof shape is Ring's rg-distribˡ), and the two
right laws ∧-distribʳ-law and ∨-distribʳ-law are derived from them by
commutativity. All four are what the bundle bridge feeds to the standard library's
IsDistributiveLattice, whose ∨-distrib-∧ and ∧-distrib-∨ fields each pair a
left and a right law.
The satisfaction predicate and the type of distributive lattices¶
infix 4 _⊨ᵈˡ_ _⊨ᵈˡ_ : (𝑨 : Algebra {𝑆 = Sig-Lattice} α ρ) (ℰ : Eq-DistributiveLattice → Term (Fin 3) × Term (Fin 3)) → Type (α ⊔ ρ) 𝑨 ⊨ᵈˡ ℰ = ∀ i → 𝑨 ⊧ proj₁ (ℰ i) ≈ proj₂ (ℰ i) DistributiveLattice : (α ρ : Level) → Type (suc α ⊔ suc ρ) DistributiveLattice α ρ = Σ[ 𝑨 ∈ Algebra {𝑆 = Sig-Lattice} α ρ ] 𝑨 ⊨ᵈˡ Th-DistributiveLattice
The forgetful projection to lattices¶
The eight lattice equations are dropped from Th-DistributiveLattice to Th-Lattice.
Because each shared equation is built by the same Classical.Equations builder on
both sides, Th-Lattice c and Th-DistributiveLattice c are definitionally equal,
so the witnesses transport with no work; the two distributivity equations are simply
not requested.
distributiveLattice→lattice : DistributiveLattice α ρ → Lattice α ρ distributiveLattice→lattice (𝑨 , mod) = 𝑨 , λ { ∧-assocˡᵃ → mod ∧-assoc ; ∧-commˡᵃ → mod ∧-comm ; ∧-idemˡᵃ → mod ∧-idem ; ∨-assocˡᵃ → mod ∨-assoc ; ∨-commˡᵃ → mod ∨-comm ; ∨-idemˡᵃ → mod ∨-idem ; absorbˡˡᵃ → mod absorbˡ ; absorbʳˡᵃ → mod absorbʳ }
The DistributiveLattice-Op module¶
DistributiveLattice-Op re-exports the meet/join operations, congruences, node
bridges, and eight lattice laws from the inherited Lattice-Op, and adds the four
distributivity laws.
module DistributiveLattice-Op {α ρ : Level} (𝑫 : DistributiveLattice α ρ) where private 𝑨 = proj₁ 𝑫 open Setoid 𝔻[ 𝑨 ] open Environment 𝑨 using ( ⟦_⟧ ) open SetoidReasoning 𝔻[ 𝑨 ] open Lattice-Op (distributiveLattice→lattice 𝑫) public using ( _∧_ ; ∧-cong ; interp-node-∧ ; ∧-assoc-law ; ∧-comm-law ; ∧-idem-law ; _∨_ ; ∨-cong ; interp-node-∨ ; ∨-assoc-law ; ∨-comm-law ; ∨-idem-law ; absorbˡ-law ; absorbʳ-law ) equations : 𝑨 ⊨ᵈˡ Th-DistributiveLattice equations = proj₂ 𝑫 -- x ∧ (y ∨ z) ≈ (x ∧ y) ∨ (x ∧ z) (meet distributes over join, on the left) ∧-distribˡ-law : ∀ {x y z} → x ∧ (y ∨ z) ≈ (x ∧ y) ∨ (x ∧ z) ∧-distribˡ-law {x} {y} {z} = begin x ∧ (y ∨ z) ≈⟨ ∧-cong refl (sym (interp-node-∨ (ℊ 1F) (ℊ 2F) {η})) ⟩ x ∧ ⟦ y∨z ⟧ ⟨$⟩ η ≈˘⟨ interp-node-∧ (ℊ 0F) y∨z {η} ⟩ ⟦ lhsT ⟧ ⟨$⟩ η ≈⟨ equations ∧-distribˡ η ⟩ ⟦ rhsT ⟧ ⟨$⟩ η ≈⟨ interp-node-∨ xy xz {η} ⟩ ⟦ xy ⟧ ⟨$⟩ η ∨ ⟦ xz ⟧ ⟨$⟩ η ≈⟨ ∨-cong (interp-node-∧ (ℊ 0F) (ℊ 1F) {η}) (interp-node-∧ (ℊ 0F) (ℊ 2F) {η}) ⟩ (x ∧ y) ∨ (x ∧ z) ∎ where η : Fin 3 → 𝕌[ 𝑨 ] η = λ { 0F → x ; 1F → y ; 2F → z } y∨z xy xz lhsT rhsT : Term (Fin 3) y∨z = node ∨-Op (pair (ℊ 1F) (ℊ 2F)) xy = node ∧-Op (pair (ℊ 0F) (ℊ 1F)) xz = node ∧-Op (pair (ℊ 0F) (ℊ 2F)) lhsT = node ∧-Op (pair (ℊ 0F) y∨z) rhsT = node ∨-Op (pair xy xz) -- x ∨ (y ∧ z) ≈ (x ∨ y) ∧ (x ∨ z) (join distributes over meet, on the left) ∨-distribˡ-law : ∀ {x y z} → x ∨ (y ∧ z) ≈ (x ∨ y) ∧ (x ∨ z) ∨-distribˡ-law {x} {y} {z} = begin x ∨ (y ∧ z) ≈⟨ ∨-cong refl (sym (interp-node-∧ (ℊ 1F) (ℊ 2F) {η})) ⟩ x ∨ ⟦ y∧z ⟧ ⟨$⟩ η ≈˘⟨ interp-node-∨ (ℊ 0F) y∧z {η} ⟩ ⟦ lhsT ⟧ ⟨$⟩ η ≈⟨ equations ∨-distribˡ η ⟩ ⟦ rhsT ⟧ ⟨$⟩ η ≈⟨ interp-node-∧ xy xz {η} ⟩ ⟦ xy ⟧ ⟨$⟩ η ∧ ⟦ xz ⟧ ⟨$⟩ η ≈⟨ ∧-cong (interp-node-∨ (ℊ 0F) (ℊ 1F) {η}) (interp-node-∨ (ℊ 0F) (ℊ 2F) {η}) ⟩ (x ∨ y) ∧ (x ∨ z) ∎ where η : Fin 3 → 𝕌[ 𝑨 ] η = λ { 0F → x ; 1F → y ; 2F → z } y∧z xy xz lhsT rhsT : Term (Fin 3) y∧z = node ∧-Op (pair (ℊ 1F) (ℊ 2F)) xy = node ∨-Op (pair (ℊ 0F) (ℊ 1F)) xz = node ∨-Op (pair (ℊ 0F) (ℊ 2F)) lhsT = node ∨-Op (pair (ℊ 0F) y∧z) rhsT = node ∧-Op (pair xy xz) -- (y ∨ z) ∧ x ≈ (y ∧ x) ∨ (z ∧ x) (right form, by ∧-commutativity) ∧-distribʳ-law : ∀ {x y z} → (y ∨ z) ∧ x ≈ (y ∧ x) ∨ (z ∧ x) ∧-distribʳ-law {x} {y} {z} = begin (y ∨ z) ∧ x ≈⟨ ∧-comm-law ⟩ x ∧ (y ∨ z) ≈⟨ ∧-distribˡ-law ⟩ (x ∧ y) ∨ (x ∧ z) ≈⟨ ∨-cong ∧-comm-law ∧-comm-law ⟩ (y ∧ x) ∨ (z ∧ x) ∎ -- (y ∧ z) ∨ x ≈ (y ∨ x) ∧ (z ∨ x) (right form, by ∨-commutativity) ∨-distribʳ-law : ∀ {x y z} → (y ∧ z) ∨ x ≈ (y ∨ x) ∧ (z ∨ x) ∨-distribʳ-law {x} {y} {z} = begin (y ∧ z) ∨ x ≈⟨ ∨-comm-law ⟩ x ∨ (y ∧ z) ≈⟨ ∨-distribˡ-law ⟩ (x ∨ y) ∧ (x ∨ z) ≈⟨ ∧-cong ∨-comm-law ∨-comm-law ⟩ (y ∨ x) ∧ (z ∨ x) ∎
eqsToDistributiveLattice¶
eqsToDistributiveLattice reuses opsToBareLattice to build the underlying
Sig-Lattice-algebra from a carrier and two operations, then attaches the ten
equation proofs. The two distributivity arguments are taken in their left form
a ∧' (b ∨' c) ≡ (a ∧' b) ∨' (a ∧' c) and dually.
open Algebra eqsToDistributiveLattice : (A : Type α) (_∧'_ _∨'_ : A → A → A) → (∧-assoc-≡ : ∀ a b c → (a ∧' b) ∧' c ≡ a ∧' (b ∧' c)) → (∧-comm-≡ : ∀ a b → a ∧' b ≡ b ∧' a) → (∧-idem-≡ : ∀ a → a ∧' a ≡ a) → (∨-assoc-≡ : ∀ a b c → (a ∨' b) ∨' c ≡ a ∨' (b ∨' c)) → (∨-comm-≡ : ∀ a b → a ∨' b ≡ b ∨' a) → (∨-idem-≡ : ∀ a → a ∨' a ≡ a) → (absorbˡ-≡ : ∀ a b → a ∧' (a ∨' b) ≡ a) → (absorbʳ-≡ : ∀ a b → (a ∧' b) ∨' a ≡ a) → (∧-distribˡ-≡ : ∀ a b c → a ∧' (b ∨' c) ≡ (a ∧' b) ∨' (a ∧' c)) → (∨-distribˡ-≡ : ∀ a b c → a ∨' (b ∧' c) ≡ (a ∨' b) ∧' (a ∨' c)) → DistributiveLattice α α eqsToDistributiveLattice A _∧'_ _∨'_ ∧-assoc-≡ ∧-comm-≡ ∧-idem-≡ ∨-assoc-≡ ∨-comm-≡ ∨-idem-≡ absorbˡ-≡ absorbʳ-≡ ∧-distribˡ-≡ ∨-distribˡ-≡ = opsToBareLattice A _∧'_ _∨'_ , proof where proof : opsToBareLattice A _∧'_ _∨'_ ⊨ᵈˡ Th-DistributiveLattice proof ∧-assoc ρ = ∧-assoc-≡ (ρ 0F) (ρ 1F) (ρ 2F) proof ∧-comm ρ = ∧-comm-≡ (ρ 0F) (ρ 1F) proof ∧-idem ρ = ∧-idem-≡ (ρ 0F) proof ∨-assoc ρ = ∨-assoc-≡ (ρ 0F) (ρ 1F) (ρ 2F) proof ∨-comm ρ = ∨-comm-≡ (ρ 0F) (ρ 1F) proof ∨-idem ρ = ∨-idem-≡ (ρ 0F) proof absorbˡ ρ = absorbˡ-≡ (ρ 0F) (ρ 1F) proof absorbʳ ρ = absorbʳ-≡ (ρ 0F) (ρ 1F) proof ∧-distribˡ ρ = ∧-distribˡ-≡ (ρ 0F) (ρ 1F) (ρ 2F) proof ∨-distribˡ ρ = ∨-distribˡ-≡ (ρ 0F) (ρ 1F) (ρ 2F)
The structure and the predicate¶
Lattices.Modular states distributivity as a predicate,
IsDistributive, on a given lattice; this module packages a
lattice with its distributive laws as a structure,
DistributiveLattice. The two are the predicate and the
structure of one concept, in the standard library's IsX and X idiom, and
the two lemmas below pass between them. The lattice underlying a distributive
lattice satisfies the predicate, by its left distributive law
(distributiveLattice→isDistributive). Conversely, a lattice
satisfying the predicate is a distributive lattice on the same algebra, so with
the same operations (isDistributive→distributiveLattice and
isDistributive→distributiveLattice-algebra): the eight lattice
equations are the lattice's own, the meet's distributive law is the predicate
read through the interpretation of terms, and the join's is the dual law that
Lattices.Modular derives from it (IsDistributive-dual).
-- The lattice of a distributive lattice satisfies the distributive law. distributiveLattice→isDistributive : (𝑫 : DistributiveLattice α ρ) → IsDistributive (distributiveLattice→lattice 𝑫) distributiveLattice→isDistributive 𝑫 x y z = DistributiveLattice-Op.∧-distribˡ-law 𝑫 module _ (𝑳 : Lattice α ρ) (d : IsDistributive 𝑳) where private 𝑨 = proj₁ 𝑳 open Setoid 𝔻[ 𝑨 ] using ( _≈_ ) renaming ( refl to ≈refl ) open Environment 𝑨 using ( ⟦_⟧ ) open SetoidReasoning 𝔻[ 𝑨 ] open Lattice-Op 𝑳 using ( _∧_ ; _∨_ ; ∧-cong ; ∨-cong ; interp-node-∧ ; interp-node-∨ ) -- A distributive law read off a lattice term, for an operation and its dual. private distrib-term : (η : Fin 3 → 𝕌[ 𝑨 ]) → let x = η 0F ; y = η 1F ; z = η 2F in x ∧ (y ∨ z) ≈ (x ∧ y) ∨ (x ∧ z) → ⟦ node ∧-Op (pair (ℊ 0F) (node ∨-Op (pair (ℊ 1F) (ℊ 2F)))) ⟧ ⟨$⟩ η ≈ ⟦ node ∨-Op (pair (node ∧-Op (pair (ℊ 0F) (ℊ 1F))) (node ∧-Op (pair (ℊ 0F) (ℊ 2F)))) ⟧ ⟨$⟩ η distrib-term η e = begin ⟦ node ∧-Op (pair (ℊ 0F) y∨z) ⟧ ⟨$⟩ η ≈⟨ interp-node-∧ (ℊ 0F) y∨z ⟩ η 0F ∧ ⟦ y∨z ⟧ ⟨$⟩ η ≈⟨ ∧-cong ≈refl (interp-node-∨ (ℊ 1F) (ℊ 2F)) ⟩ η 0F ∧ (η 1F ∨ η 2F) ≈⟨ e ⟩ (η 0F ∧ η 1F) ∨ (η 0F ∧ η 2F) ≈˘⟨ ∨-cong (interp-node-∧ (ℊ 0F) (ℊ 1F)) (interp-node-∧ (ℊ 0F) (ℊ 2F)) ⟩ ⟦ xy ⟧ ⟨$⟩ η ∨ ⟦ xz ⟧ ⟨$⟩ η ≈˘⟨ interp-node-∨ xy xz ⟩ ⟦ node ∨-Op (pair xy xz) ⟧ ⟨$⟩ η ∎ where y∨z xy xz : Term (Fin 3) y∨z = node ∨-Op (pair (ℊ 1F) (ℊ 2F)) xy = node ∧-Op (pair (ℊ 0F) (ℊ 1F)) xz = node ∧-Op (pair (ℊ 0F) (ℊ 2F)) dual-term : (η : Fin 3 → 𝕌[ 𝑨 ]) → let x = η 0F ; y = η 1F ; z = η 2F in x ∨ (y ∧ z) ≈ (x ∨ y) ∧ (x ∨ z) → ⟦ node ∨-Op (pair (ℊ 0F) (node ∧-Op (pair (ℊ 1F) (ℊ 2F)))) ⟧ ⟨$⟩ η ≈ ⟦ node ∧-Op (pair (node ∨-Op (pair (ℊ 0F) (ℊ 1F))) (node ∨-Op (pair (ℊ 0F) (ℊ 2F)))) ⟧ ⟨$⟩ η dual-term η e = begin ⟦ node ∨-Op (pair (ℊ 0F) y∧z) ⟧ ⟨$⟩ η ≈⟨ interp-node-∨ (ℊ 0F) y∧z ⟩ η 0F ∨ ⟦ y∧z ⟧ ⟨$⟩ η ≈⟨ ∨-cong ≈refl (interp-node-∧ (ℊ 1F) (ℊ 2F)) ⟩ η 0F ∨ (η 1F ∧ η 2F) ≈⟨ e ⟩ (η 0F ∨ η 1F) ∧ (η 0F ∨ η 2F) ≈˘⟨ ∧-cong (interp-node-∨ (ℊ 0F) (ℊ 1F)) (interp-node-∨ (ℊ 0F) (ℊ 2F)) ⟩ ⟦ xy ⟧ ⟨$⟩ η ∧ ⟦ xz ⟧ ⟨$⟩ η ≈˘⟨ interp-node-∧ xy xz ⟩ ⟦ node ∧-Op (pair xy xz) ⟧ ⟨$⟩ η ∎ where y∧z xy xz : Term (Fin 3) y∧z = node ∧-Op (pair (ℊ 1F) (ℊ 2F)) xy = node ∨-Op (pair (ℊ 0F) (ℊ 1F)) xz = node ∨-Op (pair (ℊ 0F) (ℊ 2F)) -- A lattice satisfying the distributive law is a distributive lattice. isDistributive→distributiveLattice : DistributiveLattice α ρ isDistributive→distributiveLattice = 𝑨 , equations where equations : 𝑨 ⊨ᵈˡ Th-DistributiveLattice equations ∧-assoc = proj₂ 𝑳 ∧-assocˡᵃ equations ∧-comm = proj₂ 𝑳 ∧-commˡᵃ equations ∧-idem = proj₂ 𝑳 ∧-idemˡᵃ equations ∨-assoc = proj₂ 𝑳 ∨-assocˡᵃ equations ∨-comm = proj₂ 𝑳 ∨-commˡᵃ equations ∨-idem = proj₂ 𝑳 ∨-idemˡᵃ equations absorbˡ = proj₂ 𝑳 absorbˡˡᵃ equations absorbʳ = proj₂ 𝑳 absorbʳˡᵃ equations ∧-distribˡ η = distrib-term η (d (η 0F) (η 1F) (η 2F)) equations ∨-distribˡ η = dual-term η (IsDistributive-dual 𝑳 d (η 0F) (η 1F) (η 2F)) -- The distributive lattice has the lattice's algebra, so its operations. isDistributive→distributiveLattice-algebra : proj₁ isDistributive→distributiveLattice ≡ 𝑨 isDistributive→distributiveLattice-algebra = ≡-refl