1
------------------------------------------------------------------------
3
------------------------------------------------------------------------
7
module Algebra.Props.BooleanAlgebra.Expression
8
{b} (B : BooleanAlgebra b b)
13
open import Category.Applicative
14
import Category.Applicative.Indexed as Applicative
15
open import Category.Monad
16
open import Category.Monad.Identity
17
open import Data.Fin using (Fin)
19
open import Data.Vec as Vec using (Vec)
20
open import Data.Product
21
import Data.Vec.Properties as VecProp
23
open import Relation.Binary.PropositionalEquality as P using (_≗_)
24
import Relation.Binary.Reflection as Reflection
25
open import Relation.Binary.Vec.Pointwise as PW
26
using (Pointwise; module Pointwise; ext)
32
data Expr n : Set b where
33
var : (x : Fin n) → Expr n
34
_or_ _and_ : (e₁ e₂ : Expr n) → Expr n
35
not : (e : Expr n) → Expr n
41
(A : RawApplicative F)
46
⟦_⟧ : ∀ {n} → Expr n → Vec (F Carrier) n → F Carrier
47
⟦ var x ⟧ ρ = Vec.lookup x ρ
48
⟦ e₁ or e₂ ⟧ ρ = pure _∨_ ⊛ ⟦ e₁ ⟧ ρ ⊛ ⟦ e₂ ⟧ ρ
49
⟦ e₁ and e₂ ⟧ ρ = pure _∧_ ⊛ ⟦ e₁ ⟧ ρ ⊛ ⟦ e₂ ⟧ ρ
50
⟦ not e ⟧ ρ = pure ¬_ ⊛ ⟦ e ⟧ ρ
56
{F₁ F₂ : Set b → Set b}
57
{A₁ : RawApplicative F₁}
58
{A₂ : RawApplicative F₂}
59
(f : Applicative.Morphism A₁ A₂)
63
open Applicative.Morphism f
64
open Semantics A₁ renaming (⟦_⟧ to ⟦_⟧₁)
65
open Semantics A₂ renaming (⟦_⟧ to ⟦_⟧₂)
66
open RawApplicative A₁ renaming (pure to pure₁; _⊛_ to _⊛₁_)
67
open RawApplicative A₂ renaming (pure to pure₂; _⊛_ to _⊛₂_)
69
natural : ∀ {n} (e : Expr n) → op ∘ ⟦ e ⟧₁ ≗ ⟦ e ⟧₂ ∘ Vec.map op
70
natural (var x) ρ = begin
71
op (Vec.lookup x ρ) ≡⟨ P.sym $
72
Applicative.Morphism.op-<$> (VecProp.lookup-morphism x) op ρ ⟩
73
Vec.lookup x (Vec.map op ρ) ∎
74
natural (e₁ or e₂) ρ = begin
75
op (pure₁ _∨_ ⊛₁ ⟦ e₁ ⟧₁ ρ ⊛₁ ⟦ e₂ ⟧₁ ρ) ≡⟨ op-⊛ _ _ ⟩
76
op (pure₁ _∨_ ⊛₁ ⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ) ≡⟨ P.cong₂ _⊛₂_ (op-⊛ _ _) P.refl ⟩
77
op (pure₁ _∨_) ⊛₂ op (⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ) ≡⟨ P.cong₂ _⊛₂_ (P.cong₂ _⊛₂_ (op-pure _) (natural e₁ ρ))
79
pure₂ _∨_ ⊛₂ ⟦ e₁ ⟧₂ (Vec.map op ρ) ⊛₂ ⟦ e₂ ⟧₂ (Vec.map op ρ) ∎
80
natural (e₁ and e₂) ρ = begin
81
op (pure₁ _∧_ ⊛₁ ⟦ e₁ ⟧₁ ρ ⊛₁ ⟦ e₂ ⟧₁ ρ) ≡⟨ op-⊛ _ _ ⟩
82
op (pure₁ _∧_ ⊛₁ ⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ) ≡⟨ P.cong₂ _⊛₂_ (op-⊛ _ _) P.refl ⟩
83
op (pure₁ _∧_) ⊛₂ op (⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ) ≡⟨ P.cong₂ _⊛₂_ (P.cong₂ _⊛₂_ (op-pure _) (natural e₁ ρ))
85
pure₂ _∧_ ⊛₂ ⟦ e₁ ⟧₂ (Vec.map op ρ) ⊛₂ ⟦ e₂ ⟧₂ (Vec.map op ρ) ∎
86
natural (not e) ρ = begin
87
op (pure₁ ¬_ ⊛₁ ⟦ e ⟧₁ ρ) ≡⟨ op-⊛ _ _ ⟩
88
op (pure₁ ¬_) ⊛₂ op (⟦ e ⟧₁ ρ) ≡⟨ P.cong₂ _⊛₂_ (op-pure _) (natural e ρ) ⟩
89
pure₂ ¬_ ⊛₂ ⟦ e ⟧₂ (Vec.map op ρ) ∎
91
op (pure₁ ⊤) ≡⟨ op-pure _ ⟩
94
op (pure₁ ⊥) ≡⟨ op-pure _ ⟩
98
lift : ℕ → BooleanAlgebra b b
100
{ Carrier = Vec Carrier n
101
; _≈_ = Pointwise _≈_
102
; _∨_ = Vec.zipWith _∨_
103
; _∧_ = Vec.zipWith _∧_
105
; ⊤ = Vec.replicate ⊤
106
; ⊥ = Vec.replicate ⊥
107
; isBooleanAlgebra = record
108
{ isDistributiveLattice = record
110
{ isEquivalence = PW.isEquivalence isEquivalence
111
; ∨-comm = λ _ _ → ext λ i →
112
solve i 2 (λ x y → x or y , y or x)
114
; ∨-assoc = λ _ _ _ → ext λ i →
116
(λ x y z → (x or y) or z , x or (y or z))
117
(∨-assoc _ _ _) _ _ _
118
; ∨-cong = λ xs≈us ys≈vs → ext λ i →
119
solve₁ i 4 (λ x y u v → x or y , u or v)
121
(∨-cong (Pointwise.app xs≈us i)
122
(Pointwise.app ys≈vs i))
123
; ∧-comm = λ _ _ → ext λ i →
124
solve i 2 (λ x y → x and y , y and x)
126
; ∧-assoc = λ _ _ _ → ext λ i →
128
(λ x y z → (x and y) and z ,
130
(∧-assoc _ _ _) _ _ _
131
; ∧-cong = λ xs≈ys us≈vs → ext λ i →
132
solve₁ i 4 (λ x y u v → x and y , u and v)
134
(∧-cong (Pointwise.app xs≈ys i)
135
(Pointwise.app us≈vs i))
136
; absorptive = (λ _ _ → ext λ i →
137
solve i 2 (λ x y → x or (x and y) , x)
138
(proj₁ absorptive _ _) _ _) ,
140
solve i 2 (λ x y → x and (x or y) , x)
141
(proj₂ absorptive _ _) _ _)
143
; ∨-∧-distribʳ = λ _ _ _ → ext λ i →
145
(λ x y z → (y and z) or x ,
146
(y or x) and (z or x))
147
(∨-∧-distribʳ _ _ _) _ _ _
149
; ∨-complementʳ = λ _ → ext λ i →
150
solve i 1 (λ x → x or (not x) , top)
152
; ∧-complementʳ = λ _ → ext λ i →
153
solve i 1 (λ x → x and (not x) , bot)
155
; ¬-cong = λ xs≈ys → ext λ i →
156
solve₁ i 2 (λ x y → not x , not y) _ _
157
(¬-cong (Pointwise.app xs≈ys i))
161
⟦_⟧Id : ∀ {n} → Expr n → Vec Carrier n → Carrier
162
⟦_⟧Id = Semantics.⟦_⟧ (RawMonad.rawIApplicative IdentityMonad)
164
⟦_⟧Vec : ∀ {m n} → Expr n → Vec (Vec Carrier m) n → Vec Carrier m
165
⟦_⟧Vec = Semantics.⟦_⟧ Vec.applicative
167
open module R {n} (i : Fin n) =
168
Reflection setoid var
169
(λ e ρ → Vec.lookup i (⟦ e ⟧Vec ρ))
170
(λ e ρ → ⟦ e ⟧Id (Vec.map (Vec.lookup i) ρ))
171
(λ e ρ → sym $ reflexive $
172
Naturality.natural (VecProp.lookup-morphism i) e ρ)
added
removed
src/Algebra/Props/BooleanAlgebra/Expression.agda
