170 lines
6.7 KiB
Agda
170 lines
6.7 KiB
Agda
|
open import Lattice
|
||
|
|
|
||
|
|
module Lattice.ExtendBelow {a} (A : Set a)
|
||
|
|
{_≈₁_ : A → A → Set a} {_⊔₁_ : A → A → A} {_⊓₁_ : A → A → A}
|
||
|
|
{{lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_}} where
|
||
|
|
|
||
|
|
open import Equivalence
|
||
|
|
open import Showable using (Showable; show)
|
||
|
|
open import Relation.Binary.Definitions using (Decidable)
|
||
|
|
open import Relation.Binary.PropositionalEquality using (refl)
|
||
|
|
open import Relation.Nullary using (Dec; ¬_; yes; no)
|
||
|
|
|
||
|
|
open IsLattice lA using ()
|
||
|
|
renaming ( ≈-equiv to ≈₁-equiv
|
||
|
|
; ≈-⊔-cong to ≈₁-⊔₁-cong
|
||
|
|
; ⊔-assoc to ⊔₁-assoc; ⊔-comm to ⊔₁-comm; ⊔-idemp to ⊔₁-idemp
|
||
|
|
; ≈-⊓-cong to ≈₁-⊓₁-cong
|
||
|
|
; ⊓-assoc to ⊓₁-assoc; ⊓-comm to ⊓₁-comm; ⊓-idemp to ⊓₁-idemp
|
||
|
|
; absorb-⊔-⊓ to absorb-⊔₁-⊓₁; absorb-⊓-⊔ to absorb-⊓₁-⊔₁
|
||
|
|
)
|
||
|
|
|
||
|
|
open IsEquivalence ≈₁-equiv using ()
|
||
|
|
renaming (≈-refl to ≈₁-refl; ≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans)
|
||
|
|
|
||
|
|
data ExtendBelow : Set a where
|
||
|
|
[_] : A → ExtendBelow
|
||
|
|
⊥ : ExtendBelow
|
||
|
|
|
||
|
|
instance
|
||
|
|
showable : {{ showableA : Showable A }} → Showable ExtendBelow
|
||
|
|
showable = record
|
||
|
|
{ show = (λ
|
||
|
|
{ ⊥ → "⊥"
|
||
|
|
; [ a ] → show a
|
||
|
|
})
|
||
|
|
}
|
||
|
|
|
||
|
|
data _≈_ : ExtendBelow → ExtendBelow → Set a where
|
||
|
|
≈-⊥-⊥ : ⊥ ≈ ⊥
|
||
|
|
≈-lift : ∀ {x y : A} → x ≈₁ y → [ x ] ≈ [ y ]
|
||
|
|
|
||
|
|
≈-refl : ∀ {ab : ExtendBelow} → ab ≈ ab
|
||
|
|
≈-refl {⊥} = ≈-⊥-⊥
|
||
|
|
≈-refl {[ x ]} = ≈-lift ≈₁-refl
|
||
|
|
|
||
|
|
≈-sym : ∀ {ab₁ ab₂ : ExtendBelow} → ab₁ ≈ ab₂ → ab₂ ≈ ab₁
|
||
|
|
≈-sym ≈-⊥-⊥ = ≈-⊥-⊥
|
||
|
|
≈-sym (≈-lift x≈₁y) = ≈-lift (≈₁-sym x≈₁y)
|
||
|
|
|
||
|
|
≈-trans : ∀ {ab₁ ab₂ ab₃ : ExtendBelow} → ab₁ ≈ ab₂ → ab₂ ≈ ab₃ → ab₁ ≈ ab₃
|
||
|
|
≈-trans ≈-⊥-⊥ ≈-⊥-⊥ = ≈-⊥-⊥
|
||
|
|
≈-trans (≈-lift a₁≈a₂) (≈-lift a₂≈a₃) = ≈-lift (≈₁-trans a₁≈a₂ a₂≈a₃)
|
||
|
|
|
||
|
|
instance
|
||
|
|
≈-equiv : IsEquivalence ExtendBelow _≈_
|
||
|
|
≈-equiv = record
|
||
|
|
{ ≈-refl = ≈-refl
|
||
|
|
; ≈-sym = ≈-sym
|
||
|
|
; ≈-trans = ≈-trans
|
||
|
|
}
|
||
|
|
|
||
|
|
_⊔_ : ExtendBelow → ExtendBelow → ExtendBelow
|
||
|
|
_⊔_ ⊥ x = x
|
||
|
|
_⊔_ [ a₁ ] ⊥ = [ a₁ ]
|
||
|
|
_⊔_ [ a₁ ] [ a₂ ] = [ a₁ ⊔₁ a₂ ]
|
||
|
|
|
||
|
|
_⊓_ : ExtendBelow → ExtendBelow → ExtendBelow
|
||
|
|
_⊓_ ⊥ x = ⊥
|
||
|
|
_⊓_ [ _ ] ⊥ = ⊥
|
||
|
|
_⊓_ [ a₁ ] [ a₂ ] = [ a₁ ⊓₁ a₂ ]
|
||
|
|
|
||
|
|
≈-⊔-cong : ∀ {x₁ x₂ x₃ x₄} → x₁ ≈ x₂ → x₃ ≈ x₄ →
|
||
|
|
(x₁ ⊔ x₃) ≈ (x₂ ⊔ x₄)
|
||
|
|
≈-⊔-cong .{⊥} .{⊥} {x₃} {x₄} ≈-⊥-⊥ [a₃]≈[a₄] = [a₃]≈[a₄]
|
||
|
|
≈-⊔-cong {x₁ = [ a₁ ]} {x₂ = [ a₂ ]} .{⊥} .{⊥} [a₁]≈[a₂] ≈-⊥-⊥ = [a₁]≈[a₂]
|
||
|
|
≈-⊔-cong {x₁ = [ a₁ ]} {x₂ = [ a₂ ]} {x₃ = [ a₃ ]} {x₄ = [ a₄ ]} (≈-lift a₁≈a₂) (≈-lift a₃≈a₄) = ≈-lift (≈₁-⊔₁-cong a₁≈a₂ a₃≈a₄)
|
||
|
|
|
||
|
|
⊔-assoc : ∀ (x₁ x₂ x₃ : ExtendBelow) → ((x₁ ⊔ x₂) ⊔ x₃) ≈ (x₁ ⊔ (x₂ ⊔ x₃))
|
||
|
|
⊔-assoc ⊥ x₁ x₂ = ≈-refl
|
||
|
|
⊔-assoc [ a₁ ] ⊥ x₂ = ≈-refl
|
||
|
|
⊔-assoc [ a₁ ] [ a₂ ] ⊥ = ≈-refl
|
||
|
|
⊔-assoc [ a₁ ] [ a₂ ] [ a₃ ] = ≈-lift (⊔₁-assoc a₁ a₂ a₃)
|
||
|
|
|
||
|
|
⊔-comm : ∀ (x₁ x₂ : ExtendBelow) → (x₁ ⊔ x₂) ≈ (x₂ ⊔ x₁)
|
||
|
|
⊔-comm ⊥ ⊥ = ≈-refl
|
||
|
|
⊔-comm ⊥ [ a₂ ] = ≈-refl
|
||
|
|
⊔-comm [ a₁ ] ⊥ = ≈-refl
|
||
|
|
⊔-comm [ a₁ ] [ a₂ ] = ≈-lift (⊔₁-comm a₁ a₂)
|
||
|
|
|
||
|
|
⊔-idemp : ∀ (x : ExtendBelow) → (x ⊔ x) ≈ x
|
||
|
|
⊔-idemp ⊥ = ≈-refl
|
||
|
|
⊔-idemp [ a ] = ≈-lift (⊔₁-idemp a)
|
||
|
|
|
||
|
|
≈-⊓-cong : ∀ {x₁ x₂ x₃ x₄} → x₁ ≈ x₂ → x₃ ≈ x₄ →
|
||
|
|
(x₁ ⊓ x₃) ≈ (x₂ ⊓ x₄)
|
||
|
|
≈-⊓-cong .{⊥} .{⊥} {x₃} {x₄} ≈-⊥-⊥ [a₃]≈[a₄] = ≈-⊥-⊥
|
||
|
|
≈-⊓-cong {x₁ = [ a₁ ]} {x₂ = [ a₂ ]} .{⊥} .{⊥} [a₁]≈[a₂] ≈-⊥-⊥ = ≈-⊥-⊥
|
||
|
|
≈-⊓-cong {x₁ = [ a₁ ]} {x₂ = [ a₂ ]} {x₃ = [ a₃ ]} {x₄ = [ a₄ ]} (≈-lift a₁≈a₂) (≈-lift a₃≈a₄) = ≈-lift (≈₁-⊓₁-cong a₁≈a₂ a₃≈a₄)
|
||
|
|
|
||
|
|
⊓-assoc : ∀ (x₁ x₂ x₃ : ExtendBelow) → ((x₁ ⊓ x₂) ⊓ x₃) ≈ (x₁ ⊓ (x₂ ⊓ x₃))
|
||
|
|
⊓-assoc ⊥ x₁ x₂ = ≈-refl
|
||
|
|
⊓-assoc [ a₁ ] ⊥ x₂ = ≈-refl
|
||
|
|
⊓-assoc [ a₁ ] [ a₂ ] ⊥ = ≈-refl
|
||
|
|
⊓-assoc [ a₁ ] [ a₂ ] [ a₃ ] = ≈-lift (⊓₁-assoc a₁ a₂ a₃)
|
||
|
|
|
||
|
|
⊓-comm : ∀ (x₁ x₂ : ExtendBelow) → (x₁ ⊓ x₂) ≈ (x₂ ⊓ x₁)
|
||
|
|
⊓-comm ⊥ ⊥ = ≈-refl
|
||
|
|
⊓-comm ⊥ [ a₂ ] = ≈-refl
|
||
|
|
⊓-comm [ a₁ ] ⊥ = ≈-refl
|
||
|
|
⊓-comm [ a₁ ] [ a₂ ] = ≈-lift (⊓₁-comm a₁ a₂)
|
||
|
|
|
||
|
|
⊓-idemp : ∀ (x : ExtendBelow) → (x ⊓ x) ≈ x
|
||
|
|
⊓-idemp ⊥ = ≈-refl
|
||
|
|
⊓-idemp [ a ] = ≈-lift (⊓₁-idemp a)
|
||
|
|
|
||
|
|
absorb-⊔-⊓ : (x₁ x₂ : ExtendBelow) → (x₁ ⊔ (x₁ ⊓ x₂)) ≈ x₁
|
||
|
|
absorb-⊔-⊓ ⊥ ⊥ = ≈-refl
|
||
|
|
absorb-⊔-⊓ ⊥ [ a₂ ] = ≈-refl
|
||
|
|
absorb-⊔-⊓ [ a₁ ] ⊥ = ≈-refl
|
||
|
|
absorb-⊔-⊓ [ a₁ ] [ a₂ ] = ≈-lift (absorb-⊔₁-⊓₁ a₁ a₂)
|
||
|
|
|
||
|
|
absorb-⊓-⊔ : (x₁ x₂ : ExtendBelow) → (x₁ ⊓ (x₁ ⊔ x₂)) ≈ x₁
|
||
|
|
absorb-⊓-⊔ ⊥ ⊥ = ≈-refl
|
||
|
|
absorb-⊓-⊔ ⊥ [ a₂ ] = ≈-refl
|
||
|
|
absorb-⊓-⊔ [ a₁ ] ⊥ = ⊓-idemp [ a₁ ]
|
||
|
|
absorb-⊓-⊔ [ a₁ ] [ a₂ ] = ≈-lift (absorb-⊓₁-⊔₁ a₁ a₂)
|
||
|
|
|
||
|
|
instance
|
||
|
|
isJoinSemilattice : IsSemilattice ExtendBelow _≈_ _⊔_
|
||
|
|
isJoinSemilattice = record
|
||
|
|
{ ≈-equiv = ≈-equiv
|
||
|
|
; ≈-⊔-cong = ≈-⊔-cong
|
||
|
|
; ⊔-assoc = ⊔-assoc
|
||
|
|
; ⊔-comm = ⊔-comm
|
||
|
|
; ⊔-idemp = ⊔-idemp
|
||
|
|
}
|
||
|
|
|
||
|
|
isMeetSemilattice : IsSemilattice ExtendBelow _≈_ _⊓_
|
||
|
|
isMeetSemilattice = record
|
||
|
|
{ ≈-equiv = ≈-equiv
|
||
|
|
; ≈-⊔-cong = ≈-⊓-cong
|
||
|
|
; ⊔-assoc = ⊓-assoc
|
||
|
|
; ⊔-comm = ⊓-comm
|
||
|
|
; ⊔-idemp = ⊓-idemp
|
||
|
|
}
|
||
|
|
|
||
|
|
isLattice : IsLattice ExtendBelow _≈_ _⊔_ _⊓_
|
||
|
|
isLattice = record
|
||
|
|
{ joinSemilattice = isJoinSemilattice
|
||
|
|
; meetSemilattice = isMeetSemilattice
|
||
|
|
; absorb-⊔-⊓ = absorb-⊔-⊓
|
||
|
|
; absorb-⊓-⊔ = absorb-⊓-⊔
|
||
|
|
}
|
||
|
|
|
||
|
|
module _ {{≈₁-Decidable : IsDecidable _≈₁_}} where
|
||
|
|
open IsDecidable ≈₁-Decidable using () renaming (R-dec to ≈₁-dec)
|
||
|
|
|
||
|
|
≈-dec : Decidable _≈_
|
||
|
|
≈-dec ⊥ ⊥ = yes ≈-⊥-⊥
|
||
|
|
≈-dec [ a₁ ] [ a₂ ]
|
||
|
|
with ≈₁-dec a₁ a₂
|
||
|
|
... | yes a₁≈a₂ = yes (≈-lift a₁≈a₂)
|
||
|
|
... | no a₁̷≈a₂ = no (λ { (≈-lift a₁≈a₂) → a₁̷≈a₂ a₁≈a₂ })
|
||
|
|
≈-dec ⊥ [ _ ] = no (λ ())
|
||
|
|
≈-dec [ _ ] ⊥ = no (λ ())
|
||
|
|
|
||
|
|
instance
|
||
|
|
≈-Decidable : IsDecidable _≈_
|
||
|
|
≈-Decidable = record { R-dec = ≈-dec }
|