Factor the Semilattice instances for Nat into their own module

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2023-07-14 19:59:07 -07:00
parent c9b514e9af
commit 1ee6682c1a

View File

@ -106,20 +106,17 @@ module PreorderInstances where
_≼_ : A × B A × B Set a
(a₁ , b₁) (a₂ , b₂) = Preorder._≼_ pA a₁ a₂ × Preorder._≼_ pB b₁ b₂
ispA = Preorder.isPreorder pA
ispB = Preorder.isPreorder pB
≼-refl : {p : A × B} p p
≼-refl {(a , b)} = (IsPreorder.≼-refl ispA {a}, IsPreorder.≼-refl ispB {b})
≼-refl {(a , b)} = (Preorder.≼-refl pA {a}, Preorder.≼-refl pB {b})
≼-trans : {p₁ p₂ p₃ : A × B} p₁ p₂ p₂ p₃ p₁ p₃
≼-trans (a₁≼a₂ , b₁≼b₂) (a₂≼a₃ , b₂≼b₃) =
( IsPreorder.≼-trans ispA a₁≼a₂ a₂≼a₃
, IsPreorder.≼-trans ispB b₁≼b₂ b₂≼b₃
( Preorder.≼-trans pA a₁≼a₂ a₂≼a₃
, Preorder.≼-trans pB b₁≼b₂ b₂≼b₃
)
≼-antisym : {p₁ p₂ : A × B} p₁ p₂ p₂ p₁ p₁ p₂
≼-antisym (a₁≼a₂ , b₁≼b₂) (a₂≼a₁ , b₂≼b₁) = cong₂ (_,_) (IsPreorder.≼-antisym ispA a₁≼a₂ a₂≼a₁) (IsPreorder.≼-antisym ispB b₁≼b₂ b₂≼b₁)
≼-antisym (a₁≼a₂ , b₁≼b₂) (a₂≼a₁ , b₂≼b₁) = cong₂ (_,_) (Preorder.≼-antisym pA a₁≼a₂ a₂≼a₁) (Preorder.≼-antisym pB b₁≼b₂ b₂≼b₁)
ProdPreorder : Preorder (A × B)
ProdPreorder = record
@ -131,72 +128,80 @@ module PreorderInstances where
}
}
module SemilatticeInstances where
module ForNat where
open Nat
open NatProps
open Eq
open PreorderInstances.ForNat
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 y z
max-bound₂ {x} {y} {z} x⊔y≡z rewrite sym x⊔y≡z = m≤n⇒m≤o⊔n x (≤-refl)
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
{ isPreorder = Preorder.isPreorder NatPreorder
; ⊔-assoc = ⊔-assoc
; ⊔-comm = ⊔-comm
; ⊔-idemp = ⊔-idem
; ⊔-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
}
}
private module NatInstances where
open Nat
open NatProps
open Eq
open PreorderInstances.ForNat
open SemilatticeInstances.ForNat
open Data.Product
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 y z
max-bound₂ {x} {y} {z} x⊔y≡z rewrite sym x⊔y≡z = m≤n⇒m≤o⊔n x (≤-refl)
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
{ isPreorder = Preorder.isPreorder NatPreorder
; ⊔-assoc = ⊔-assoc
; ⊔-comm = ⊔-comm
; ⊔-idemp = ⊔-idem
; ⊔-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
}
}
private
minmax-absorb : {x y : } x (x y) x
minmax-absorb {x} {y} = ≤-antisym x⊓x⊔y≤x (helper x⊓x≤x⊓x⊔y (⊓-idem x))
where
x⊓x⊔y≤x = min-bound₁ {x} {x y} {x (x y)} refl
x⊓x≤x⊓x⊔y = ⊓-mono-≤ {x} {x} ≤-refl (max-bound₁ {x} {y} {x y} refl)
x⊓x⊔y≤x = proj₁ (Semilattice.⊔-bound NatMinSemilattice x (x y) (x (x y)) refl)
x⊓x≤x⊓x⊔y = ⊓-mono-≤ {x} {x} ≤-refl (proj₁ (Semilattice.⊔-bound NatMaxSemilattice x y (x y) refl))
-- >:(
helper : x x x (x y) x x x x x (x y)
@ -205,8 +210,8 @@ private module NatInstances where
maxmin-absorb : {x y : } x (x y) x
maxmin-absorb {x} {y} = ≤-antisym (helper x⊔x⊓y≤x⊔x (⊔-idem x)) x≤x⊔x⊓y
where
x≤x⊔x⊓y = max-bound₁ {x} {x y} {x (x y)} refl
x⊔x⊓y≤x⊔x = ⊔-mono-≤ {x} {x} ≤-refl (min-bound₁ {x} {y} {x y} refl)
x≤x⊔x⊓y = proj₁ (Semilattice.⊔-bound NatMaxSemilattice x (x y) (x (x y)) refl)
x⊔x⊓y≤x⊔x = ⊔-mono-≤ {x} {x} ≤-refl (proj₁ (Semilattice.⊔-bound NatMinSemilattice x y (x y) refl))
-- >:(
helper : x (x y) x x x x x x (x y) x