1
1
------------------------------------------------------------------------
2
2
-- The Agda standard library
4
-- Compatibility module. Pending for removal. Use
5
-- Algebra.Properties.Lattice instead.
4
6
------------------------------------------------------------------------
8
10
module Algebra.Props.Lattice {l₁ l₂} (L : Lattice l₁ l₂) where
11
open import Algebra.Structures
12
import Algebra.FunctionProperties as P; open P _≈_
13
open import Relation.Binary
14
import Relation.Binary.EqReasoning as EqR; open EqR setoid
16
open import Function.Equality using (_⟨$⟩_)
17
open import Function.Equivalence using (_⇔_; module Equivalence)
18
open import Data.Product
20
∧-idempotent : Idempotent _∧_
21
∧-idempotent x = begin
22
x ∧ x ≈⟨ refl ⟨ ∧-cong ⟩ sym (proj₁ absorptive _ _) ⟩
23
x ∧ (x ∨ x ∧ x) ≈⟨ proj₂ absorptive _ _ ⟩
26
∨-idempotent : Idempotent _∨_
27
∨-idempotent x = begin
28
x ∨ x ≈⟨ refl ⟨ ∨-cong ⟩ sym (∧-idempotent _) ⟩
29
x ∨ x ∧ x ≈⟨ proj₁ absorptive _ _ ⟩
33
∧-∨-isLattice : IsLattice _≈_ _∧_ _∨_
34
∧-∨-isLattice = record
35
{ isEquivalence = isEquivalence
42
; absorptive = swap absorptive
45
∧-∨-lattice : Lattice _ _
49
; isLattice = ∧-∨-isLattice
57
; _≤_ = λ x y → x ≈ x ∧ y
58
; isPartialOrder = record
60
{ isEquivalence = isEquivalence
61
; reflexive = λ {i} {j} i≈j → begin
62
i ≈⟨ sym $ ∧-idempotent _ ⟩
63
i ∧ i ≈⟨ ∧-cong refl i≈j ⟩
65
; trans = λ {i} {j} {k} i≈i∧j j≈j∧k → begin
67
i ∧ j ≈⟨ ∧-cong refl j≈j∧k ⟩
68
i ∧ (j ∧ k) ≈⟨ sym (∧-assoc _ _ _) ⟩
69
(i ∧ j) ∧ k ≈⟨ ∧-cong (sym i≈i∧j) refl ⟩
72
; antisym = λ {x} {y} x≈x∧y y≈y∧x → begin
81
replace-equality : {_≈′_ : Rel Carrier l₂} →
82
(∀ {x y} → x ≈ y ⇔ x ≈′ y) → Lattice _ _
83
replace-equality {_≈′_} ≈⇔≈′ = record
88
{ isEquivalence = record
90
; sym = λ x≈y → to ⟨$⟩ sym (from ⟨$⟩ x≈y)
91
; trans = λ x≈y y≈z → to ⟨$⟩ trans (from ⟨$⟩ x≈y) (from ⟨$⟩ y≈z)
93
; ∨-comm = λ x y → to ⟨$⟩ ∨-comm x y
94
; ∨-assoc = λ x y z → to ⟨$⟩ ∨-assoc x y z
95
; ∨-cong = λ x≈y u≈v → to ⟨$⟩ ∨-cong (from ⟨$⟩ x≈y) (from ⟨$⟩ u≈v)
96
; ∧-comm = λ x y → to ⟨$⟩ ∧-comm x y
97
; ∧-assoc = λ x y z → to ⟨$⟩ ∧-assoc x y z
98
; ∧-cong = λ x≈y u≈v → to ⟨$⟩ ∧-cong (from ⟨$⟩ x≈y) (from ⟨$⟩ u≈v)
99
; absorptive = (λ x y → to ⟨$⟩ proj₁ absorptive x y)
100
, (λ x y → to ⟨$⟩ proj₂ absorptive x y)
102
} where open module E {x y} = Equivalence (≈⇔≈′ {x} {y})
12
open import Algebra.Properties.Lattice L public
added
removed
src/Algebra/Props/Lattice.agda
