Finish up the Nat semilattices
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
97a3f25fd2
commit
422ea93edb
71
Lattice.agda
71
Lattice.agda
|
|
@ -5,7 +5,8 @@ open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym)
|
|||
open import Relation.Binary.Definitions
|
||||
open import Data.Nat as Nat using (ℕ; _≤_)
|
||||
open import Data.Product using (_×_; _,_)
|
||||
open import Agda.Primitive using (lsuc)
|
||||
open import Data.Sum using (_⊎_; inj₁; inj₂)
|
||||
open import Agda.Primitive using (lsuc; Level)
|
||||
|
||||
open import NatMap using (NatMap)
|
||||
|
||||
|
|
@ -15,6 +16,13 @@ record IsPreorder {a} (A : Set a) (_≼_ : A → A → Set a) : Set a where
|
|||
≼-trans : Transitive (_≼_)
|
||||
≼-antisym : Antisymmetric (_≡_) (_≼_)
|
||||
|
||||
isPreorderFlip : {a : Level} → {A : Set a} → {_≼_ : A → A → Set a} → IsPreorder A _≼_ → IsPreorder A (λ x y → y ≼ x)
|
||||
isPreorderFlip isPreorder = record
|
||||
{ ≼-refl = IsPreorder.≼-refl isPreorder
|
||||
; ≼-trans = λ {x} {y} {z} x≽y y≽z → IsPreorder.≼-trans isPreorder y≽z x≽y
|
||||
; ≼-antisym = λ {x} {y} x≽y y≽x → IsPreorder.≼-antisym isPreorder y≽x x≽y
|
||||
}
|
||||
|
||||
record Preorder {a} (A : Set a) : Set (lsuc a) where
|
||||
field
|
||||
_≼_ : A → A → Set a
|
||||
|
|
@ -27,13 +35,12 @@ record IsSemilattice {a} (A : Set a) (_≼_ : A → A → Set a) (_⊔_ : A →
|
|||
field
|
||||
isPreorder : IsPreorder A _≼_
|
||||
|
||||
⊔-assoc : (x : A) → (y : A) → (z : A) → (x ⊔ y) ⊔ z ≡ x ⊔ (y ⊔ z)
|
||||
⊔-comm : (x : A) → (y : A) → x ⊔ y ≡ y ⊔ x
|
||||
⊔-assoc : (x y z : A) → (x ⊔ y) ⊔ z ≡ x ⊔ (y ⊔ z)
|
||||
⊔-comm : (x y : A) → x ⊔ y ≡ y ⊔ x
|
||||
⊔-idemp : (x : A) → x ⊔ x ≡ x
|
||||
|
||||
⊔-bound : (x : A) → (y : A) → (z : A) → x ⊔ y ≡ z → (x ≼ z × y ≼ z)
|
||||
⊔-least : (x : A) → (y : A) → (z : A) → x ⊔ y ≡ z →
|
||||
∀ (z' : A) → (x ≼ z' × y ≼ z') → z ≼ z'
|
||||
⊔-bound : (x y z : A) → x ⊔ y ≡ z → (x ≼ z × y ≼ z)
|
||||
⊔-least : (x y z : A) → x ⊔ y ≡ z → ∀ (z' : A) → (x ≼ z' × y ≼ z') → z ≼ z'
|
||||
|
||||
open IsPreorder isPreorder public
|
||||
|
||||
|
|
@ -55,8 +62,8 @@ record IsLattice {a} (A : Set a) (_≼_ : A → A → Set a) (_⊔_ : A → A
|
|||
joinSemilattice : IsSemilattice A _≼_ _⊔_
|
||||
meetSemilattice : IsSemilattice A _≽_ _⊓_
|
||||
|
||||
absorb-⊔-⊓ : (x : A) → (y : A) → x ⊔ (x ⊓ y) ≡ x
|
||||
absorb-⊓-⊔ : (x : A) → (y : A) → x ⊓ (x ⊔ y) ≡ x
|
||||
absorb-⊔-⊓ : (x y : A) → x ⊔ (x ⊓ y) ≡ x
|
||||
absorb-⊓-⊔ : (x y : A) → x ⊓ (x ⊔ y) ≡ x
|
||||
|
||||
open IsSemilattice joinSemilattice public
|
||||
open IsSemilattice meetSemilattice public renaming
|
||||
|
|
@ -82,6 +89,7 @@ private module NatInstances where
|
|||
open Nat
|
||||
open NatProps
|
||||
open Eq
|
||||
open Data.Sum
|
||||
|
||||
NatPreorder : Preorder ℕ
|
||||
NatPreorder = record
|
||||
|
|
@ -94,14 +102,19 @@ private module NatInstances where
|
|||
}
|
||||
|
||||
private
|
||||
max-bound₁ : (x : ℕ) → (y : ℕ) → (z : ℕ) → x ⊔ y ≡ z → x ≤ z
|
||||
max-bound₁ x y z x⊔y≡z rewrite sym x⊔y≡z rewrite ⊔-comm x y = m≤n⇒m≤o⊔n y (≤-refl)
|
||||
max-bound₁ : {x y z : ℕ} → x ⊔ y ≡ z → x ≤ z
|
||||
max-bound₁ {x} {y} {z} x⊔y≡z rewrite sym x⊔y≡z rewrite ⊔-comm x y = m≤n⇒m≤o⊔n y (≤-refl)
|
||||
|
||||
max-bound₂ : (x : ℕ) → (y : ℕ) → (z : ℕ) → x ⊔ y ≡ z → y ≤ z
|
||||
max-bound₂ x y z x⊔y≡z rewrite sym x⊔y≡z = m≤n⇒m≤o⊔n x (≤-refl)
|
||||
max-bound₂ : {x y z : ℕ} → x ⊔ y ≡ z → y ≤ z
|
||||
max-bound₂ {x} {y} {z} x⊔y≡z rewrite sym x⊔y≡z = m≤n⇒m≤o⊔n x (≤-refl)
|
||||
|
||||
NatMinSemilattice : Semilattice ℕ
|
||||
NatMinSemilattice = record
|
||||
max-least : (x y z : ℕ) → x ⊔ y ≡ z → ∀ (z' : ℕ) → (x ≤ z' × y ≤ z') → z ≤ z'
|
||||
max-least x y z x⊔y≡z z' (x≤z' , y≤z') with (⊔-sel x y)
|
||||
... | inj₁ x⊔y≡x rewrite trans (sym x⊔y≡z) (x⊔y≡x) = x≤z'
|
||||
... | inj₂ x⊔y≡y rewrite trans (sym x⊔y≡z) (x⊔y≡y) = y≤z'
|
||||
|
||||
NatMaxSemilattice : Semilattice ℕ
|
||||
NatMaxSemilattice = record
|
||||
{ _≼_ = _≤_
|
||||
; _⊔_ = _⊔_
|
||||
; isSemilattice = record
|
||||
|
|
@ -109,6 +122,34 @@ private module NatInstances where
|
|||
; ⊔-assoc = ⊔-assoc
|
||||
; ⊔-comm = ⊔-comm
|
||||
; ⊔-idemp = ⊔-idem
|
||||
; ⊔-bound = λ x y z x⊔y≡z → (max-bound₁ x y z x⊔y≡z , max-bound₂ x y z x⊔y≡z)
|
||||
; ⊔-bound = λ x y z x⊔y≡z → (max-bound₁ x⊔y≡z , max-bound₂ x⊔y≡z)
|
||||
; ⊔-least = max-least
|
||||
}
|
||||
}
|
||||
|
||||
private
|
||||
min-bound₁ : {x y z : ℕ} → x ⊓ y ≡ z → z ≤ x
|
||||
min-bound₁ {x} {y} {z} x⊓y≡z rewrite sym x⊓y≡z = m≤n⇒m⊓o≤n y (≤-refl)
|
||||
|
||||
min-bound₂ : {x y z : ℕ} → x ⊓ y ≡ z → z ≤ y
|
||||
min-bound₂ {x} {y} {z} x⊓y≡z rewrite sym x⊓y≡z rewrite ⊓-comm x y = m≤n⇒m⊓o≤n x (≤-refl)
|
||||
|
||||
min-greatest : (x y z : ℕ) → x ⊓ y ≡ z → ∀ (z' : ℕ) → (z' ≤ x × z' ≤ y) → z' ≤ z
|
||||
min-greatest x y z x⊓y≡z z' (z'≤x , z'≤y) with (⊓-sel x y)
|
||||
... | inj₁ x⊓y≡x rewrite trans (sym x⊓y≡z) (x⊓y≡x) = z'≤x
|
||||
... | inj₂ x⊓y≡y rewrite trans (sym x⊓y≡z) (x⊓y≡y) = z'≤y
|
||||
|
||||
|
||||
NatMinSemilattice : Semilattice ℕ
|
||||
NatMinSemilattice = record
|
||||
{ _≼_ = _≥_
|
||||
; _⊔_ = _⊓_
|
||||
; isSemilattice = record
|
||||
{ isPreorder = isPreorderFlip (Preorder.isPreorder NatPreorder)
|
||||
; ⊔-assoc = ⊓-assoc
|
||||
; ⊔-comm = ⊓-comm
|
||||
; ⊔-idemp = ⊓-idem
|
||||
; ⊔-bound = λ x y z x⊓y≡z → (min-bound₁ x⊓y≡z , min-bound₂ x⊓y≡z)
|
||||
; ⊔-least = min-greatest
|
||||
}
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user