```------------------------------------------------------------------------
-- The Agda standard library
--
-- Boolean algebra expressions
------------------------------------------------------------------------

open import Algebra

module Algebra.Props.BooleanAlgebra.Expression
{b} (B : BooleanAlgebra b b)
where

open BooleanAlgebra B

open import Category.Applicative
import Category.Applicative.Indexed as Applicative
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)

-- 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₂  ⟧ ρ = pure _∨_ ⊛ ⟦ e₁ ⟧ ρ ⊛ ⟦ e₂ ⟧ ρ
⟦ e₁ and e₂ ⟧ ρ = pure _∧_ ⊛ ⟦ e₁ ⟧ ρ ⊛ ⟦ e₂ ⟧ ρ
⟦ not e     ⟧ ρ = pure ¬_ ⊛ ⟦ 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 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₂ ⊥                                                        ∎

-- 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 _≈_
; _∨_              = 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