open import Algebra
module Algebra.Properties.BooleanAlgebra.Expression
{b} (B : BooleanAlgebra b b)
where
open BooleanAlgebra B
open import Category.Applicative
import Category.Applicative.Indexed as Applicative
open import Category.Monad
open import Category.Monad.Identity
open import Data.Fin using (Fin)
open import Data.Nat
open import Data.Vec as Vec using (Vec)
open import Data.Product
import Data.Vec.Properties as VecProp
open import Function
open import Relation.Binary.PropositionalEquality as P using (_≗_)
import Relation.Binary.Reflection as Reflection
open import Relation.Binary.Vec.Pointwise as PW
using (Pointwise; module Pointwise; ext)
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
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₂ ⟧ ρ = pure _∨_ ⊛ ⟦ e₁ ⟧ ρ ⊛ ⟦ e₂ ⟧ ρ
⟦ e₁ and e₂ ⟧ ρ = pure _∧_ ⊛ ⟦ e₁ ⟧ ρ ⊛ ⟦ e₂ ⟧ ρ
⟦ not e ⟧ ρ = pure ¬_ ⊛ ⟦ e ⟧ ρ
⟦ top ⟧ ρ = pure ⊤
⟦ bot ⟧ ρ = pure ⊥
module Naturality
{F₁ F₂ : Set b → Set b}
{A₁ : RawApplicative F₁}
{A₂ : RawApplicative F₂}
(f : Applicative.Morphism A₁ A₂)
where
open P.≡-Reasoning
open Applicative.Morphism f
open Semantics A₁ renaming (⟦_⟧ to ⟦_⟧₁)
open Semantics A₂ renaming (⟦_⟧ to ⟦_⟧₂)
open RawApplicative A₁ renaming (pure to pure₁; _⊛_ to _⊛₁_)
open RawApplicative A₂ renaming (pure to pure₂; _⊛_ to _⊛₂_)
natural : ∀ {n} (e : Expr n) → op ∘ ⟦ e ⟧₁ ≗ ⟦ e ⟧₂ ∘ Vec.map op
natural (var x) ρ = begin
op (Vec.lookup x ρ) ≡⟨ P.sym $
Applicative.Morphism.op-<$> (VecProp.lookup-morphism x) op ρ ⟩
Vec.lookup x (Vec.map op ρ) ∎
natural (e₁ or e₂) ρ = begin
op (pure₁ _∨_ ⊛₁ ⟦ e₁ ⟧₁ ρ ⊛₁ ⟦ e₂ ⟧₁ ρ) ≡⟨ op-⊛ _ _ ⟩
op (pure₁ _∨_ ⊛₁ ⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ) ≡⟨ P.cong₂ _⊛₂_ (op-⊛ _ _) P.refl ⟩
op (pure₁ _∨_) ⊛₂ op (⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ) ≡⟨ P.cong₂ _⊛₂_ (P.cong₂ _⊛₂_ (op-pure _) (natural e₁ ρ))
(natural e₂ ρ) ⟩
pure₂ _∨_ ⊛₂ ⟦ e₁ ⟧₂ (Vec.map op ρ) ⊛₂ ⟦ e₂ ⟧₂ (Vec.map op ρ) ∎
natural (e₁ and e₂) ρ = begin
op (pure₁ _∧_ ⊛₁ ⟦ e₁ ⟧₁ ρ ⊛₁ ⟦ e₂ ⟧₁ ρ) ≡⟨ op-⊛ _ _ ⟩
op (pure₁ _∧_ ⊛₁ ⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ) ≡⟨ P.cong₂ _⊛₂_ (op-⊛ _ _) P.refl ⟩
op (pure₁ _∧_) ⊛₂ op (⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ) ≡⟨ P.cong₂ _⊛₂_ (P.cong₂ _⊛₂_ (op-pure _) (natural e₁ ρ))
(natural e₂ ρ) ⟩
pure₂ _∧_ ⊛₂ ⟦ e₁ ⟧₂ (Vec.map op ρ) ⊛₂ ⟦ e₂ ⟧₂ (Vec.map op ρ) ∎
natural (not e) ρ = begin
op (pure₁ ¬_ ⊛₁ ⟦ e ⟧₁ ρ) ≡⟨ op-⊛ _ _ ⟩
op (pure₁ ¬_) ⊛₂ op (⟦ e ⟧₁ ρ) ≡⟨ P.cong₂ _⊛₂_ (op-pure _) (natural e ρ) ⟩
pure₂ ¬_ ⊛₂ ⟦ e ⟧₂ (Vec.map op ρ) ∎
natural top ρ = begin
op (pure₁ ⊤) ≡⟨ op-pure _ ⟩
pure₂ ⊤ ∎
natural bot ρ = begin
op (pure₁ ⊥) ≡⟨ op-pure _ ⟩
pure₂ ⊥ ∎
lift : ℕ → BooleanAlgebra b b
lift n = record
{ Carrier = Vec Carrier n
; _≈_ = Pointwise _≈_
; _∨_ = Vec.zipWith _∨_
; _∧_ = Vec.zipWith _∧_
; ¬_ = Vec.map ¬_
; ⊤ = Vec.replicate ⊤
; ⊥ = Vec.replicate ⊥
; isBooleanAlgebra = record
{ isDistributiveLattice = record
{ isLattice = record
{ isEquivalence = PW.isEquivalence isEquivalence
; ∨-comm = λ _ _ → ext λ i →
solve i 2 (λ x y → x or y , y or x)
(∨-comm _ _) _ _
; ∨-assoc = λ _ _ _ → ext λ i →
solve i 3
(λ x y z → (x or y) or z , x or (y or z))
(∨-assoc _ _ _) _ _ _
; ∨-cong = λ xs≈us ys≈vs → ext λ i →
solve₁ i 4 (λ x y u v → x or y , u or v)
_ _ _ _
(∨-cong (Pointwise.app xs≈us i)
(Pointwise.app ys≈vs i))
; ∧-comm = λ _ _ → ext λ i →
solve i 2 (λ x y → x and y , y and x)
(∧-comm _ _) _ _
; ∧-assoc = λ _ _ _ → ext λ i →
solve i 3
(λ x y z → (x and y) and z ,
x and (y and z))
(∧-assoc _ _ _) _ _ _
; ∧-cong = λ xs≈ys us≈vs → ext λ i →
solve₁ i 4 (λ x y u v → x and y , u and v)
_ _ _ _
(∧-cong (Pointwise.app xs≈ys i)
(Pointwise.app us≈vs i))
; absorptive = (λ _ _ → ext λ i →
solve i 2 (λ x y → x or (x and y) , x)
(proj₁ absorptive _ _) _ _) ,
(λ _ _ → ext λ i →
solve i 2 (λ x y → x and (x or y) , x)
(proj₂ absorptive _ _) _ _)
}
; ∨-∧-distribʳ = λ _ _ _ → ext λ i →
solve i 3
(λ x y z → (y and z) or x ,
(y or x) and (z or x))
(∨-∧-distribʳ _ _ _) _ _ _
}
; ∨-complementʳ = λ _ → ext λ i →
solve i 1 (λ x → x or (not x) , top)
(∨-complementʳ _) _
; ∧-complementʳ = λ _ → ext λ i →
solve i 1 (λ x → x and (not x) , bot)
(∧-complementʳ _) _
; ¬-cong = λ xs≈ys → ext λ i →
solve₁ i 2 (λ x y → not x , not y) _ _
(¬-cong (Pointwise.app xs≈ys i))
}
}
where
⟦_⟧Id : ∀ {n} → Expr n → Vec Carrier n → Carrier
⟦_⟧Id = Semantics.⟦_⟧ (RawMonad.rawIApplicative IdentityMonad)
⟦_⟧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 i (⟦ e ⟧Vec ρ))
(λ e ρ → ⟦ e ⟧Id (Vec.map (Vec.lookup i) ρ))
(λ e ρ → sym $ reflexive $
Naturality.natural (VecProp.lookup-morphism i) e ρ)