Add a preorder instance for product
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
2b3d429631
commit
c9b514e9af
59
Lattice.agda
59
Lattice.agda
|
@ -85,21 +85,58 @@ record Lattice {a} (A : Set a) : Set (lsuc a) where
|
|||
|
||||
open IsLattice isLattice public
|
||||
|
||||
module PreorderInstances where
|
||||
module ForNat where
|
||||
open NatProps
|
||||
|
||||
NatPreorder : Preorder ℕ
|
||||
NatPreorder = record
|
||||
{ _≼_ = _≤_
|
||||
; isPreorder = record
|
||||
{ ≼-refl = ≤-refl
|
||||
; ≼-trans = ≤-trans
|
||||
; ≼-antisym = ≤-antisym
|
||||
}
|
||||
}
|
||||
|
||||
module ForProd {a} {A B : Set a} {{ pA : Preorder A }} {{ pB : Preorder B }} where
|
||||
open Eq
|
||||
|
||||
private
|
||||
_≼_ : 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})
|
||||
|
||||
≼-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₃
|
||||
)
|
||||
|
||||
≼-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₁)
|
||||
|
||||
ProdPreorder : Preorder (A × B)
|
||||
ProdPreorder = record
|
||||
{ _≼_ = _≼_
|
||||
; isPreorder = record
|
||||
{ ≼-refl = ≼-refl
|
||||
; ≼-trans = ≼-trans
|
||||
; ≼-antisym = ≼-antisym
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
private module NatInstances where
|
||||
open Nat
|
||||
open NatProps
|
||||
open Eq
|
||||
open Data.Sum
|
||||
|
||||
NatPreorder : Preorder ℕ
|
||||
NatPreorder = record
|
||||
{ _≼_ = _≤_
|
||||
; isPreorder = record
|
||||
{ ≼-refl = ≤-refl
|
||||
; ≼-trans = ≤-trans
|
||||
; ≼-antisym = ≤-antisym
|
||||
}
|
||||
}
|
||||
open PreorderInstances.ForNat
|
||||
|
||||
private
|
||||
max-bound₁ : {x y z : ℕ} → x ⊔ y ≡ z → x ≤ z
|
||||
|
|
Loading…
Reference in New Issue
Block a user