------------------------------------------------------------------------
-- The Agda standard library
--
-- Boolean algebra expressions
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Lattice using (BooleanAlgebra; isBooleanAlgebraʳ;
isDistributiveLatticeʳʲᵐ)
module Algebra.Lattice.Properties.BooleanAlgebra.Expression
{b} (B : BooleanAlgebra b b)
where
open BooleanAlgebra B
open import Data.Fin.Base using (Fin)
open import Data.Nat.Base using (ℕ)
open import Data.Product.Base using (_,_; proj₁; proj₂)
open import Data.Vec.Base as Vec using (Vec)
import Data.Vec.Effectful as Vec
import Function.Identity.Effectful as Identity
open import Data.Vec.Properties using (lookup-map)
open import Data.Vec.Relation.Binary.Pointwise.Extensional as PW
using (Pointwise; ext)
open import Effect.Applicative as Applicative
open import Function.Base using (_∘_; _$_; flip)
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≗_)
open import Relation.Binary.PropositionalEquality.Properties
using (module ≡-Reasoning)
import Relation.Binary.Reflection as Reflection
-- Expressions made up of variables and the operations of a boolean
-- algebra.
infixr 7 _and_
infixr 6 _or_
data Expr n : Set b where
var : (x : Fin n) → Expr n
_or_ _and_ : (e₁ e₂ : Expr n) → Expr n
not : (e : Expr n) → Expr n
top bot : Expr n
-- The semantics of an expression, parametrised by an applicative
-- functor.
module Semantics
{F : Set b → Set b}
(A : RawApplicative F)
where
open RawApplicative A
⟦_⟧ : ∀ {n} → Expr n → Vec (F Carrier) n → F Carrier
⟦ var x ⟧ ρ = Vec.lookup ρ x
⟦ e₁ or e₂ ⟧ ρ = _∨_ <$> ⟦ e₁ ⟧ ρ ⊛ ⟦ e₂ ⟧ ρ
⟦ e₁ and e₂ ⟧ ρ = _∧_ <$> ⟦ e₁ ⟧ ρ ⊛ ⟦ e₂ ⟧ ρ
⟦ not e ⟧ ρ = ¬_ <$> ⟦ e ⟧ ρ
⟦ top ⟧ ρ = pure ⊤
⟦ bot ⟧ ρ = pure ⊥
-- flip Semantics.⟦_⟧ e is natural.
module Naturality
{F₁ F₂ : Set b → Set b}
{A₁ : RawApplicative F₁}
{A₂ : RawApplicative F₂}
(f : Applicative.Morphism A₁ A₂)
where
open ≡-Reasoning
open Applicative.Morphism f
open Semantics A₁ renaming (⟦_⟧ to ⟦_⟧₁)
open Semantics A₂ renaming (⟦_⟧ to ⟦_⟧₂)
open RawApplicative A₁ renaming (pure to pure₁; _<$>_ to _<$>₁_; _⊛_ to _⊛₁_)
open RawApplicative A₂ renaming (pure to pure₂; _<$>_ to _<$>₂_; _⊛_ to _⊛₂_)
natural : ∀ {n} (e : Expr n) → op ∘ ⟦ e ⟧₁ ≗ ⟦ e ⟧₂ ∘ Vec.map op
natural (var x) ρ = begin
op (Vec.lookup ρ x) ≡⟨ ≡.sym $ lookup-map x op ρ ⟩
Vec.lookup (Vec.map op ρ) x ∎
natural (e₁ or e₂) ρ = begin
op (_∨_ <$>₁ ⟦ e₁ ⟧₁ ρ ⊛₁ ⟦ e₂ ⟧₁ ρ) ≡⟨ op-⊛ _ _ ⟩
op (_∨_ <$>₁ ⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ) ≡⟨ ≡.cong₂ _⊛₂_ (op-<$> _ _) ≡.refl ⟩
_∨_ <$>₂ op (⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ) ≡⟨ ≡.cong₂ (λ e₁ e₂ → _∨_ <$>₂ e₁ ⊛₂ e₂) (natural e₁ ρ) (natural e₂ ρ) ⟩
_∨_ <$>₂ ⟦ e₁ ⟧₂ (Vec.map op ρ) ⊛₂ ⟦ e₂ ⟧₂ (Vec.map op ρ) ∎
natural (e₁ and e₂) ρ = begin
op (_∧_ <$>₁ ⟦ e₁ ⟧₁ ρ ⊛₁ ⟦ e₂ ⟧₁ ρ) ≡⟨ op-⊛ _ _ ⟩
op (_∧_ <$>₁ ⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ) ≡⟨ ≡.cong₂ _⊛₂_ (op-<$> _ _) ≡.refl ⟩
_∧_ <$>₂ op (⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ) ≡⟨ ≡.cong₂ (λ e₁ e₂ → _∧_ <$>₂ e₁ ⊛₂ e₂) (natural e₁ ρ) (natural e₂ ρ) ⟩
_∧_ <$>₂ ⟦ e₁ ⟧₂ (Vec.map op ρ) ⊛₂ ⟦ e₂ ⟧₂ (Vec.map op ρ) ∎
natural (not e) ρ = begin
op (¬_ <$>₁ ⟦ e ⟧₁ ρ) ≡⟨ op-<$> _ _ ⟩
¬_ <$>₂ op (⟦ e ⟧₁ ρ) ≡⟨ ≡.cong (¬_ <$>₂_) (natural e ρ) ⟩
¬_ <$>₂ ⟦ e ⟧₂ (Vec.map op ρ) ∎
natural top ρ = begin
op (pure₁ ⊤) ≡⟨ op-pure _ ⟩
pure₂ ⊤ ∎
natural bot ρ = begin
op (pure₁ ⊥) ≡⟨ op-pure _ ⟩
pure₂ ⊥ ∎
-- An example of how naturality can be used: Any boolean algebra can
-- be lifted, in a pointwise manner, to vectors of carrier elements.
lift : ℕ → BooleanAlgebra b b
lift n = record
{ Carrier = Vec Carrier n
; _≈_ = Pointwise _≈_
; _∨_ = zipWith _∨_
; _∧_ = zipWith _∧_
; ¬_ = map ¬_
; ⊤ = pure ⊤
; ⊥ = pure ⊥
; isBooleanAlgebra = isBooleanAlgebraʳ $ record
{ isDistributiveLattice = isDistributiveLatticeʳʲᵐ $ record
{ isLattice = record
{ isEquivalence = PW.isEquivalence isEquivalence
; ∨-comm = λ xs ys → ext λ i →
solve i 2 (λ x y → x or y , y or x)
(∨-comm _ _) xs ys
; ∨-assoc = λ xs ys _ → ext λ i →
solve i 3
(λ x y z → (x or y) or z , x or (y or z))
(∨-assoc _ _ _) xs ys _
; ∨-cong = λ {xs} {ys} {us} {vs} xs≈us ys≈vs → ext λ i →
solve₁ i 4 (λ x y u v → x or y , u or v)
xs us ys vs
(∨-cong (Pointwise.app xs≈us i)
(Pointwise.app ys≈vs i))
; ∧-comm = λ xs ys → ext λ i →
solve i 2 (λ x y → x and y , y and x)
(∧-comm _ _) xs ys
; ∧-assoc = λ xs ys _ → ext λ i →
solve i 3
(λ x y z → (x and y) and z ,
x and (y and z))
(∧-assoc _ _ _) xs ys _
; ∧-cong = λ {xs} {ys} {us} {vs} xs≈ys us≈vs → ext λ i →
solve₁ i 4 (λ x y u v → x and y , u and v)
xs us ys vs
(∧-cong (Pointwise.app xs≈ys i)
(Pointwise.app us≈vs i))
; absorptive =
(λ xs ys → ext λ i →
solve i 2 (λ x y → x or (x and y) , x) (∨-absorbs-∧ _ _) xs ys) ,
(λ xs ys → ext λ i →
solve i 2 (λ x y → x and (x or y) , x) (∧-absorbs-∨ _ _) xs ys)
}
; ∨-distribʳ-∧ = λ xs ys zs → ext λ i →
solve i 3
(λ x y z → (y and z) or x ,
(y or x) and (z or x))
(∨-distribʳ-∧ _ _ _) xs ys zs
}
; ∨-complementʳ = λ xs → ext λ i →
solve i 1 (λ x → x or (not x) , top)
(∨-complementʳ _) xs
; ∧-complementʳ = λ xs → ext λ i →
solve i 1 (λ x → x and (not x) , bot)
(∧-complementʳ _) xs
; ¬-cong = λ {xs} {ys} xs≈ys → ext λ i →
solve₁ i 2 (λ x y → not x , not y) xs ys
(¬-cong (Pointwise.app xs≈ys i))
}
}
where
open RawApplicative Vec.applicative
using (pure; zipWith) renaming (_<$>_ to map)
⟦_⟧Id : ∀ {n} → Expr n → Vec Carrier n → Carrier
⟦_⟧Id = Semantics.⟦_⟧ Identity.applicative
⟦_⟧Vec : ∀ {m n} → Expr n → Vec (Vec Carrier m) n → Vec Carrier m
⟦_⟧Vec = Semantics.⟦_⟧ Vec.applicative
open module R {n} (i : Fin n) =
Reflection setoid var
(λ e ρ → Vec.lookup (⟦ e ⟧Vec ρ) i)
(λ e ρ → ⟦ e ⟧Id (Vec.map (flip Vec.lookup i) ρ))
(λ e ρ → sym $ reflexive $
Naturality.natural (Vec.lookup-morphism i) e ρ)