Lattices.Distributive.Bundle

Bundle bridge for distributive lattices

This is the Lattices.Distributive.Bundle module of the agda-lattices library.

Bridges Lattices.Distributive to the standard library's Algebra.Lattice.Bundles.DistributiveLattice. Like the Lattice bridge, its stdlib target lives in Algebra.Lattice.Bundles.

The forward direction (⟨_⟩ᵈˡ) builds an IsDistributiveLattice from our laws: its isLattice field is the same record the Lattice bridge produces (one ∨-comm step bridges our absorbʳ-law to stdlib's ∨-absorbs-∧), and the two DistributesOver fields each pair a left and a right curried law, both of which DistributiveLattice-Op supplies.

The reverse direction (⟪_⟫ᵈˡ) reads stdlib's ∨-distribˡ-∧ and ∧-distribˡ-∨ back as the two left distributivity equations and reuses the Lattice-bridge derivations (idempotency from absorption, the absorbʳ form by one ∨-comm step) for the eight shared equations.

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

module Lattices.Distributive.Bundle where

-- Imports from the Agda Standard Library -------------------------------------
open import Algebra.Lattice.Bundles  using ()
                                     renaming (  DistributiveLattice
                                                 to stdlib-DistributiveLattice )
open import Data.Fin.Patterns        using ( 0F ; 1F ; 2F )
open import Data.Product             using ( _,_ ; proj₁ )
open import Function                 using ( Func )
open import Level                    using ( Level )
open import Relation.Binary          using ( Setoid )
open import Relation.Binary.PropositionalEquality using (refl)
open Func renaming ( to to _⟨$⟩_ )

-- Imports from the Agda Universal Algebra Library ----------------------------
open import Classical.Signatures.Lattice            using  ( ∧-Op ; ∨-Op ; Sig-Lattice )
open import Lattices.Distributive
                                                    using  ( DistributiveLattice
                                                           ; module DistributiveLattice-Op )
open import Lattices.Distributive.Theory  using  ( ∧-assoc ; ∧-comm ; ∧-idem
                                                           ; ∨-assoc ; ∨-comm ; ∨-idem
                                                           ; absorbˡ ; absorbʳ
                                                           ; ∧-distribˡ ; ∨-distribˡ )
open import Setoid.Algebras.Basic                   using  ( Algebra ; 𝕌[_] ; 𝔻[_] )
open import Setoid.Signatures                       using  ( ⟨_⟩ )

private variable α ρ : Level

⟨_⟩ᵈˡ : DistributiveLattice α ρ → stdlib-DistributiveLattice α ρ
⟨ 𝑫 ⟩ᵈˡ = record
  { Carrier = 𝕌[ proj₁ 𝑫 ]
  ; _≈_     = _≈_
  ; _∨_     = _∨_
  ; _∧_     = _∧_
  ; isDistributiveLattice = record
      { isLattice = record
          { isEquivalence = isEquivalence
          ; ∨-comm        = λ x y → ∨-comm-law {x}{y}
          ; ∨-assoc       = λ x y z → ∨-assoc-law {x}{y}{z}
          ; ∨-cong        = ∨-cong
          ; ∧-comm        = λ x y → ∧-comm-law {x}{y}
          ; ∧-assoc       = λ x y z → ∧-assoc-law {x}{y}{z}
          ; ∧-cong        = ∧-cong
          ; absorptive    = ∨-absorbs-∧ , λ x y → absorbˡ-law {x}{y}
          }
      ; ∨-distrib-∧ = (λ x y z → ∨-distribˡ-law {x}{y}{z}) , λ x y z → ∨-distribʳ-law {x}{y}{z}
      ; ∧-distrib-∨ = (λ x y z → ∧-distribˡ-law {x}{y}{z}) , λ x y z → ∧-distribʳ-law {x}{y}{z}
      }
  }
  where
  open DistributiveLattice-Op 𝑫
  open Setoid 𝔻[ proj₁ 𝑫 ] using ( _≈_ ; isEquivalence) renaming (refl to ≈refl ; trans to ≈trans )

  -- stdlib's first absorption is x ∨ (x ∧ y) ≈ x; our absorbʳ-law is (x ∧ y) ∨ x ≈ x.
  ∨-absorbs-∧ : ∀ x y → x ∨ (x ∧ y) ≈ x
  ∨-absorbs-∧ x y = ≈trans ∨-comm-law absorbʳ-law

⟪_⟫ᵈˡ : stdlib-DistributiveLattice α ρ → DistributiveLattice α ρ
⟪ L ⟫ᵈˡ = 𝑨 , λ { ∧-assoc    ρ → L-∧-assoc (ρ 0F) (ρ 1F) (ρ 2F)
                ; ∧-comm     ρ → L-∧-comm  (ρ 0F) (ρ 1F)
                ; ∧-idem     ρ → ∧-idem-derived (ρ 0F)
                ; ∨-assoc    ρ → L-∨-assoc (ρ 0F) (ρ 1F) (ρ 2F)
                ; ∨-comm     ρ → L-∨-comm  (ρ 0F) (ρ 1F)
                ; ∨-idem     ρ → ∨-idem-derived (ρ 0F)
                ; absorbˡ    ρ → L-∧-absorbs-∨ (ρ 0F) (ρ 1F)
                ; absorbʳ    ρ → absorbʳ-derived (ρ 0F) (ρ 1F)
                ; ∧-distribˡ ρ → L-∧-distribˡ-∨ (ρ 0F) (ρ 1F) (ρ 2F)
                ; ∨-distribˡ ρ → L-∨-distribˡ-∧ (ρ 0F) (ρ 1F) (ρ 2F)
                }
  where
  open stdlib-DistributiveLattice L
      using ( setoid ; ∧-cong ; ∨-cong )
      renaming ( _∨_ to _∨'_ ; _∧_ to _∧'_
               ; ∨-assoc to L-∨-assoc ; ∨-comm to L-∨-comm
               ; ∧-assoc to L-∧-assoc ; ∧-comm to L-∧-comm
               ; ∨-absorbs-∧ to L-∨-absorbs-∧ ; ∧-absorbs-∨ to L-∧-absorbs-∨
               ; ∧-distribˡ-∨ to L-∧-distribˡ-∨ ; ∨-distribˡ-∧ to L-∨-distribˡ-∧ )
  open Setoid setoid using ( _≈_ ) renaming ( refl to ≈refl ; trans to ≈trans ; sym to ≈sym )

  ∧-idem-derived : ∀ x → x ∧' x ≈ x
  ∧-idem-derived x = ≈trans (∧-cong ≈refl (≈sym (L-∨-absorbs-∧ x x))) (L-∧-absorbs-∨ x (x ∧' x))

  ∨-idem-derived : ∀ x → x ∨' x ≈ x
  ∨-idem-derived x = ≈trans (∨-cong ≈refl (≈sym (L-∧-absorbs-∨ x x))) (L-∨-absorbs-∧ x (x ∨' x))

  absorbʳ-derived : ∀ x y → (x ∧' y) ∨' x ≈ x
  absorbʳ-derived x y = ≈trans (L-∨-comm (x ∧' y) x) (L-∨-absorbs-∧ x y)

  𝑨 : Algebra {𝑆 = Sig-Lattice} _ _
  𝑨 = record { Domain = setoid ; Interp = interp }
    where
    interp : Func (⟨ Sig-Lattice ⟩ setoid) setoid
    interp ⟨$⟩ (∧-Op , args) = args 0F ∧' args 1F
    interp ⟨$⟩ (∨-Op , args) = args 0F ∨' args 1F
    cong interp {∧-Op , _} {.∧-Op , _} (refl , args≈) = ∧-cong (args≈ 0F) (args≈ 1F)
    cong interp {∨-Op , _} {.∨-Op , _} (refl , args≈) = ∨-cong (args≈ 0F) (args≈ 1F)

module _ {𝑫 : DistributiveLattice α ρ} where
  open DistributiveLattice-Op 𝑫
  open Setoid 𝔻[ proj₁ 𝑫 ] using ( _≈_ ) renaming ( refl to ≈refl )
  open DistributiveLattice-Op ⟪ ⟨ 𝑫 ⟩ᵈˡ ⟫ᵈˡ renaming ( _∧_ to _∧'_ ; _∨_ to _∨'_ )

  roundtrip-cbc-∧-dl : (a b : 𝕌[ proj₁ 𝑫 ]) → a ∧' b ≈ a ∧ b
  roundtrip-cbc-∧-dl a b = ≈refl

  roundtrip-cbc-∨-dl : (a b : 𝕌[ proj₁ 𝑫 ]) → a ∨' b ≈ a ∨ b
  roundtrip-cbc-∨-dl a b = ≈refl

module _ {L : stdlib-DistributiveLattice α ρ} where
  open stdlib-DistributiveLattice L using ( _≈_ ; _∧_ ; _∨_ ) renaming ( Carrier to A ; refl to ≈refl )
  open stdlib-DistributiveLattice ⟨ ⟪ L ⟫ᵈˡ ⟩ᵈˡ using () renaming ( _∧_ to _∧'_ ; _∨_ to _∨'_ )

  roundtrip-bcb-∧-dl : (a b : A) → (a ∧ b) ≈ (a ∧' b)
  roundtrip-bcb-∧-dl a b = ≈refl

  roundtrip-bcb-∨-dl : (a b : A) → (a ∨ b) ≈ (a ∨' b)
  roundtrip-bcb-∨-dl a b = ≈refl