blob: 25bf2ef9a1fc2bfcc3e650c06a1a3b960b2248b1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
|
{-# OPTIONS --without-K --safe #-}
module Data.Boolean.BoundedDistributiveLattice where
import Algebra.Lattice.Bundles as Algebra
import Relation.Binary.Lattice.Bundles as Relation
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
import Algebra.Lattice.Properties.BooleanAlgebra as BA
open import Algebra.Bundles using (Semiring)
open import Algebra.Lattice.Properties.Lattice using (∧-semilattice; ∨-semilattice)
open import Algebra.Lattice.Properties.Lattice using (∨-∧-isOrderTheoreticLattice)
open import Data.Bool using (Bool; not)
open import Data.Bool.Properties using (∨-∧-booleanAlgebra)
open import Data.Product using (_,_)
open import Lattice.Bundle.BoundedDistributive using (BoundedDistributiveLattice)
open import Lattice.Properties.BooleanAlgebra using (boundedDistributiveLattice)
open import Level using (0ℓ)
open import Relation.Binary.Lattice.Properties.Lattice using (isAlgLattice)
open Algebra.BooleanAlgebra ∨-∧-booleanAlgebra
open BA ∨-∧-booleanAlgebra using (∧-identityˡ; ∧-identityʳ; ∧-zeroˡ; ∨-identityˡ)
booleanAlgebra : Relation.BooleanAlgebra 0ℓ 0ℓ 0ℓ
booleanAlgebra = record
{ Carrier = Carrier
; _≈_ = _≈_
; _≤_ = λ x y → x ≈ x ∧ y
; _∨_ = _∨_
; _∧_ = _∧_
; ¬_ = ¬_
; ⊤ = ⊤
; ⊥ = ⊥
; isBooleanAlgebra = record
{ isHeytingAlgebra = record
{ isBoundedLattice = record
{ isLattice = ∨-∧-isOrderTheoreticLattice lattice
; maximum = λ x → sym (∧-identityʳ x)
; minimum = λ x → sym (∧-zeroˡ x)
}
; exponential = λ w x y → to w x y , from w x y
}
}
}
where
open ≈-Reasoning setoid
to : (w x y : Bool) → w ∧ x ≈ (w ∧ x) ∧ y → w ≈ w ∧ (¬ x ∨ y)
to w x y wx≈wxy = begin
w ≈⟨ ∧-identityʳ w ⟨
w ∧ ⊤ ≈⟨ ∧-congˡ {w} (∨-complementˡ x) ⟨
w ∧ (¬ x ∨ x) ≈⟨ ∧-congˡ {w} (∨-comm (¬ x) x) ⟩
w ∧ (x ∨ ¬ x) ≈⟨ ∧-distribˡ-∨ w x (¬ x) ⟩
w ∧ x ∨ w ∧ ¬ x ≈⟨ ∨-congʳ wx≈wxy ⟩
((w ∧ x) ∧ y) ∨ w ∧ ¬ x ≈⟨ ∨-congʳ (∧-assoc w x y) ⟩
w ∧ (x ∧ y) ∨ w ∧ ¬ x ≈⟨ ∧-distribˡ-∨ w (x ∧ y) (¬ x) ⟨
w ∧ (x ∧ y ∨ ¬ x) ≈⟨ ∧-congˡ (∨-distribʳ-∧ (¬ x) x y) ⟩
w ∧ ((x ∨ ¬ x) ∧ (y ∨ ¬ x)) ≈⟨ ∧-congˡ {w} (∧-congʳ (∨-complementʳ x)) ⟩
w ∧ (⊤ ∧ (y ∨ ¬ x)) ≈⟨ ∧-congˡ (∧-identityˡ (y ∨ ¬ x)) ⟩
w ∧ (y ∨ ¬ x) ≈⟨ ∧-congˡ (∨-comm y (¬ x)) ⟩
w ∧ (¬ x ∨ y) ∎
from : (w x y : Bool) → w ≈ w ∧ (¬ x ∨ y) → w ∧ x ≈ (w ∧ x) ∧ y
from w x y w≈¬x∨y = begin
w ∧ x ≈⟨ ∧-congʳ w≈¬x∨y ⟩
(w ∧ (¬ x ∨ y)) ∧ x ≈⟨ ∧-assoc w (¬ x ∨ y) x ⟩
w ∧ (¬ x ∨ y) ∧ x ≈⟨ ∧-congˡ (∧-distribʳ-∨ x (¬ x) y) ⟩
w ∧ (¬ x ∧ x ∨ y ∧ x) ≈⟨ ∧-congˡ (∨-congʳ (∧-complementˡ x)) ⟩
w ∧ (⊥ ∨ y ∧ x) ≈⟨ ∧-congˡ {w} (∨-identityˡ (y ∧ x)) ⟩
w ∧ y ∧ x ≈⟨ ∧-congˡ {w} (∧-comm y x) ⟩
w ∧ x ∧ y ≈⟨ ∧-assoc w x y ⟨
(w ∧ x) ∧ y ∎
𝔹 : BoundedDistributiveLattice 0ℓ 0ℓ 0ℓ
𝔹 = boundedDistributiveLattice booleanAlgebra
module 𝔹 = BoundedDistributiveLattice 𝔹
|
