1
------------------------------------------------------------------------
2
-- Boolean algebra expressions
3
------------------------------------------------------------------------
5
{-# OPTIONS --universe-polymorphism #-}
9
module Algebra.Props.BooleanAlgebra.Expression
10
{b} (B : BooleanAlgebra b b)
15
open import Category.Applicative
16
import Category.Applicative.Indexed as Applicative
17
open import Category.Monad
18
open import Category.Monad.Identity
19
open import Data.Fin using (Fin)
21
open import Data.Vec as Vec using (Vec)
22
open import Data.Product
23
import Data.Vec.Properties as VecProp
25
open import Relation.Binary.PropositionalEquality as P using (_≗_)
26
import Relation.Binary.Reflection as Reflection
27
open import Relation.Binary.Vec.Pointwise as PW
28
using (Pointwise; module Pointwise; ext)
30
-- Expressions made up of variables and the operations of a boolean
36
data Expr n : Set b where
37
var : (x : Fin n) → Expr n
38
_or_ _and_ : (e₁ e₂ : Expr n) → Expr n
39
not : (e : Expr n) → Expr n
42
-- The semantics of an expression, parametrised by an applicative
47
(A : RawApplicative F)
52
⟦_⟧ : ∀ {n} → Expr n → Vec (F Carrier) n → F Carrier
53
⟦ var x ⟧ ρ = Vec.lookup x ρ
54
⟦ e₁ or e₂ ⟧ ρ = pure _∨_ ⊛ ⟦ e₁ ⟧ ρ ⊛ ⟦ e₂ ⟧ ρ
55
⟦ e₁ and e₂ ⟧ ρ = pure _∧_ ⊛ ⟦ e₁ ⟧ ρ ⊛ ⟦ e₂ ⟧ ρ
56
⟦ not e ⟧ ρ = pure ¬_ ⊛ ⟦ e ⟧ ρ
60
-- flip Semantics.⟦_⟧ e is natural.
63
{F₁ F₂ : Set b → Set b}
64
{A₁ : RawApplicative F₁}
65
{A₂ : RawApplicative F₂}
66
(f : Applicative.Morphism A₁ A₂)
70
open Applicative.Morphism f
71
open Semantics A₁ renaming (⟦_⟧ to ⟦_⟧₁)
72
open Semantics A₂ renaming (⟦_⟧ to ⟦_⟧₂)
73
open RawApplicative A₁ renaming (pure to pure₁; _⊛_ to _⊛₁_)
74
open RawApplicative A₂ renaming (pure to pure₂; _⊛_ to _⊛₂_)
76
natural : ∀ {n} (e : Expr n) → op ∘ ⟦ e ⟧₁ ≗ ⟦ e ⟧₂ ∘ Vec.map op
77
natural (var x) ρ = begin
78
op (Vec.lookup x ρ) ≡⟨ P.sym $
79
Applicative.Morphism.op-<$> (VecProp.lookup-morphism x) op ρ ⟩
80
Vec.lookup x (Vec.map op ρ) ∎
81
natural (e₁ or e₂) ρ = begin
82
op (pure₁ _∨_ ⊛₁ ⟦ e₁ ⟧₁ ρ ⊛₁ ⟦ e₂ ⟧₁ ρ) ≡⟨ op-⊛ _ _ ⟩
83
op (pure₁ _∨_ ⊛₁ ⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ) ≡⟨ P.cong₂ _⊛₂_ (op-⊛ _ _) P.refl ⟩
84
op (pure₁ _∨_) ⊛₂ op (⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ) ≡⟨ P.cong₂ _⊛₂_ (P.cong₂ _⊛₂_ (op-pure _) (natural e₁ ρ))
86
pure₂ _∨_ ⊛₂ ⟦ e₁ ⟧₂ (Vec.map op ρ) ⊛₂ ⟦ e₂ ⟧₂ (Vec.map op ρ) ∎
87
natural (e₁ and e₂) ρ = begin
88
op (pure₁ _∧_ ⊛₁ ⟦ e₁ ⟧₁ ρ ⊛₁ ⟦ e₂ ⟧₁ ρ) ≡⟨ op-⊛ _ _ ⟩
89
op (pure₁ _∧_ ⊛₁ ⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ) ≡⟨ P.cong₂ _⊛₂_ (op-⊛ _ _) P.refl ⟩
90
op (pure₁ _∧_) ⊛₂ op (⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ) ≡⟨ P.cong₂ _⊛₂_ (P.cong₂ _⊛₂_ (op-pure _) (natural e₁ ρ))
92
pure₂ _∧_ ⊛₂ ⟦ e₁ ⟧₂ (Vec.map op ρ) ⊛₂ ⟦ e₂ ⟧₂ (Vec.map op ρ) ∎
93
natural (not e) ρ = begin
94
op (pure₁ ¬_ ⊛₁ ⟦ e ⟧₁ ρ) ≡⟨ op-⊛ _ _ ⟩
95
op (pure₁ ¬_) ⊛₂ op (⟦ e ⟧₁ ρ) ≡⟨ P.cong₂ _⊛₂_ (op-pure _) (natural e ρ) ⟩
96
pure₂ ¬_ ⊛₂ ⟦ e ⟧₂ (Vec.map op ρ) ∎
98
op (pure₁ ⊤) ≡⟨ op-pure _ ⟩
100
natural bot ρ = begin
101
op (pure₁ ⊥) ≡⟨ op-pure _ ⟩
104
-- An example of how naturality can be used: Any boolean algebra can
105
-- be lifted, in a pointwise manner, to vectors of carrier elements.
107
lift : ℕ → BooleanAlgebra b b
109
{ Carrier = Vec Carrier n
110
; _≈_ = Pointwise _≈_
111
; _∨_ = Vec.zipWith _∨_
112
; _∧_ = Vec.zipWith _∧_
114
; ⊤ = Vec.replicate ⊤
115
; ⊥ = Vec.replicate ⊥
116
; isBooleanAlgebra = record
117
{ isDistributiveLattice = record
119
{ isEquivalence = PW.isEquivalence isEquivalence
120
; ∨-comm = λ _ _ → ext λ i →
121
solve i 2 (λ x y → x or y , y or x)
123
; ∨-assoc = λ _ _ _ → ext λ i →
125
(λ x y z → (x or y) or z , x or (y or z))
126
(∨-assoc _ _ _) _ _ _
127
; ∨-cong = λ xs≈us ys≈vs → ext λ i →
128
solve₁ i 4 (λ x y u v → x or y , u or v)
130
(∨-cong (Pointwise.app xs≈us i)
131
(Pointwise.app ys≈vs i))
132
; ∧-comm = λ _ _ → ext λ i →
133
solve i 2 (λ x y → x and y , y and x)
135
; ∧-assoc = λ _ _ _ → ext λ i →
137
(λ x y z → (x and y) and z ,
139
(∧-assoc _ _ _) _ _ _
140
; ∧-cong = λ xs≈ys us≈vs → ext λ i →
141
solve₁ i 4 (λ x y u v → x and y , u and v)
143
(∧-cong (Pointwise.app xs≈ys i)
144
(Pointwise.app us≈vs i))
145
; absorptive = (λ _ _ → ext λ i →
146
solve i 2 (λ x y → x or (x and y) , x)
147
(proj₁ absorptive _ _) _ _) ,
149
solve i 2 (λ x y → x and (x or y) , x)
150
(proj₂ absorptive _ _) _ _)
152
; ∨-∧-distribʳ = λ _ _ _ → ext λ i →
154
(λ x y z → (y and z) or x ,
155
(y or x) and (z or x))
156
(∨-∧-distribʳ _ _ _) _ _ _
158
; ∨-complementʳ = λ _ → ext λ i →
159
solve i 1 (λ x → x or (not x) , top)
161
; ∧-complementʳ = λ _ → ext λ i →
162
solve i 1 (λ x → x and (not x) , bot)
164
; ¬-cong = λ xs≈ys → ext λ i →
165
solve₁ i 2 (λ x y → not x , not y) _ _
166
(¬-cong (Pointwise.app xs≈ys i))
170
⟦_⟧Id : ∀ {n} → Expr n → Vec Carrier n → Carrier
171
⟦_⟧Id = Semantics.⟦_⟧ (RawMonad.rawIApplicative IdentityMonad)
173
⟦_⟧Vec : ∀ {m n} → Expr n → Vec (Vec Carrier m) n → Vec Carrier m
174
⟦_⟧Vec = Semantics.⟦_⟧ Vec.applicative
176
open module R {n} (i : Fin n) =
177
Reflection setoid var
178
(λ e ρ → Vec.lookup i (⟦ e ⟧Vec ρ))
179
(λ e ρ → ⟦ e ⟧Id (Vec.map (Vec.lookup i) ρ))
180
(λ e ρ → sym $ reflexive $
181
Naturality.natural (VecProp.lookup-morphism i) e ρ)
added
removed
src/Algebra/Props/BooleanAlgebra/Expression.agda
