forked from agda/agda-stdlib
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathLatticeMonomorphism.agda
123 lines (104 loc) · 5.17 KB
/
LatticeMonomorphism.agda
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
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
------------------------------------------------------------------------
-- The Agda standard library
--
-- Consequences of a monomorphism between lattice-like structures
------------------------------------------------------------------------
-- See Data.Nat.Binary.Properties for examples of how this and similar
-- modules can be used to easily translate properties between types.
{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra
open import Algebra.Lattice
open import Algebra.Lattice.Morphism.Structures
import Algebra.Consequences.Setoid as Consequences
import Algebra.Morphism.MagmaMonomorphism as MagmaMonomorphisms
import Algebra.Lattice.Properties.Lattice as LatticeProperties
open import Data.Product.Base using (_,_; map)
open import Relation.Binary.Bundles using (Setoid)
import Relation.Binary.Morphism.RelMonomorphism as RelMonomorphisms
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
module Algebra.Lattice.Morphism.LatticeMonomorphism
{a b ℓ₁ ℓ₂} {L₁ : RawLattice a ℓ₁} {L₂ : RawLattice b ℓ₂} {⟦_⟧}
(isLatticeMonomorphism : IsLatticeMonomorphism L₁ L₂ ⟦_⟧)
where
open IsLatticeMonomorphism isLatticeMonomorphism
open RawLattice L₁ renaming (_≈_ to _≈₁_; _∨_ to _∨_; _∧_ to _∧_)
open RawLattice L₂ renaming (_≈_ to _≈₂_; _∨_ to _⊔_; _∧_ to _⊓_)
------------------------------------------------------------------------
-- Re-export all properties of magma monomorphisms
open MagmaMonomorphisms ∨-isMagmaMonomorphism public
using () renaming
( cong to ∨-cong
; assoc to ∨-assoc
; comm to ∨-comm
; idem to ∨-idem
; sel to ∨-sel
; cancelˡ to ∨-cancelˡ
; cancelʳ to ∨-cancelʳ
; cancel to ∨-cancel
)
open MagmaMonomorphisms ∧-isMagmaMonomorphism public
using () renaming
( cong to ∧-cong
; assoc to ∧-assoc
; comm to ∧-comm
; idem to ∧-idem
; sel to ∧-sel
; cancelˡ to ∧-cancelˡ
; cancelʳ to ∧-cancelʳ
; cancel to ∧-cancel
)
------------------------------------------------------------------------
-- Lattice-specific properties
module _ (⊔-⊓-isLattice : IsLattice _≈₂_ _⊔_ _⊓_) where
open IsLattice ⊔-⊓-isLattice using (isEquivalence) renaming
( ∨-congˡ to ⊔-congˡ
; ∨-congʳ to ⊔-congʳ
; ∧-cong to ⊓-cong
; ∧-congˡ to ⊓-congˡ
; ∨-absorbs-∧ to ⊔-absorbs-⊓
; ∧-absorbs-∨ to ⊓-absorbs-⊔
)
setoid : Setoid b ℓ₂
setoid = record { isEquivalence = isEquivalence }
open ≈-Reasoning setoid
∨-absorbs-∧ : _Absorbs_ _≈₁_ _∨_ _∧_
∨-absorbs-∧ x y = injective (begin
⟦ x ∨ x ∧ y ⟧ ≈⟨ ∨-homo x (x ∧ y) ⟩
⟦ x ⟧ ⊔ ⟦ x ∧ y ⟧ ≈⟨ ⊔-congˡ (∧-homo x y) ⟩
⟦ x ⟧ ⊔ ⟦ x ⟧ ⊓ ⟦ y ⟧ ≈⟨ ⊔-absorbs-⊓ ⟦ x ⟧ ⟦ y ⟧ ⟩
⟦ x ⟧ ∎)
∧-absorbs-∨ : _Absorbs_ _≈₁_ _∧_ _∨_
∧-absorbs-∨ x y = injective (begin
⟦ x ∧ (x ∨ y) ⟧ ≈⟨ ∧-homo x (x ∨ y) ⟩
⟦ x ⟧ ⊓ ⟦ x ∨ y ⟧ ≈⟨ ⊓-congˡ (∨-homo x y) ⟩
⟦ x ⟧ ⊓ (⟦ x ⟧ ⊔ ⟦ y ⟧) ≈⟨ ⊓-absorbs-⊔ ⟦ x ⟧ ⟦ y ⟧ ⟩
⟦ x ⟧ ∎)
absorptive : Absorptive _≈₁_ _∨_ _∧_
absorptive = ∨-absorbs-∧ , ∧-absorbs-∨
distribʳ : _DistributesOverʳ_ _≈₂_ _⊔_ _⊓_ → _DistributesOverʳ_ _≈₁_ _∨_ _∧_
distribʳ distribʳ x y z = injective (begin
⟦ y ∧ z ∨ x ⟧ ≈⟨ ∨-homo (y ∧ z) x ⟩
⟦ y ∧ z ⟧ ⊔ ⟦ x ⟧ ≈⟨ ⊔-congʳ (∧-homo y z) ⟩
⟦ y ⟧ ⊓ ⟦ z ⟧ ⊔ ⟦ x ⟧ ≈⟨ distribʳ ⟦ x ⟧ ⟦ y ⟧ ⟦ z ⟧ ⟩
(⟦ y ⟧ ⊔ ⟦ x ⟧) ⊓ (⟦ z ⟧ ⊔ ⟦ x ⟧) ≈⟨ ⊓-cong (∨-homo y x) (∨-homo z x) ⟨
⟦ y ∨ x ⟧ ⊓ ⟦ z ∨ x ⟧ ≈⟨ ∧-homo (y ∨ x) (z ∨ x) ⟨
⟦ (y ∨ x) ∧ (z ∨ x) ⟧ ∎)
isLattice : IsLattice _≈₂_ _⊔_ _⊓_ → IsLattice _≈₁_ _∨_ _∧_
isLattice isLattice = record
{ isEquivalence = RelMonomorphisms.isEquivalence isRelMonomorphism L.isEquivalence
; ∨-comm = ∨-comm LP.∨-isMagma L.∨-comm
; ∨-assoc = ∨-assoc LP.∨-isMagma L.∨-assoc
; ∨-cong = ∨-cong LP.∨-isMagma
; ∧-comm = ∧-comm LP.∧-isMagma L.∧-comm
; ∧-assoc = ∧-assoc LP.∧-isMagma L.∧-assoc
; ∧-cong = ∧-cong LP.∧-isMagma
; absorptive = absorptive isLattice
} where
module L = IsLattice isLattice
module LP = LatticeProperties (record { isLattice = isLattice })
isDistributiveLattice : IsDistributiveLattice _≈₂_ _⊔_ _⊓_ →
IsDistributiveLattice _≈₁_ _∨_ _∧_
isDistributiveLattice isDL = isDistributiveLatticeʳʲᵐ (record
{ isLattice = isLattice L.isLattice
; ∨-distribʳ-∧ = distribʳ L.isLattice L.∨-distribʳ-∧
}) where module L = IsDistributiveLattice isDL