------------------------------------------------------------------------
-- The Agda standard library
--
-- Lexicographic products of binary relations
------------------------------------------------------------------------
-- The definition of lexicographic product used here is suitable if
-- the left-hand relation is a (non-strict) partial order.
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Product.Relation.Binary.Lex.NonStrict where
open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
open import Data.Product.Relation.Binary.Pointwise.NonDependent as Pointwise
using (Pointwise)
import Data.Product.Relation.Binary.Lex.Strict as Strict
open import Data.Sum.Base using (inj₁; inj₂)
open import Level using (Level)
open import Relation.Binary.Core using (Rel; _⇒_)
open import Relation.Binary.Bundles
using (Poset; DecTotalOrder; TotalOrder)
open import Relation.Binary.Structures
using (IsPartialOrder; IsEquivalence; IsTotalOrder; IsDecTotalOrder)
open import Relation.Binary.Definitions
using (Transitive; Symmetric; Decidable; Antisymmetric; Total; Trichotomous
; Irreflexive; Asymmetric; _Respects₂_; tri<; tri>; tri≈)
open import Relation.Binary.Consequences
import Relation.Binary.Construct.NonStrictToStrict as Conv
private
variable
a b ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level
A : Set a
B : Set b
------------------------------------------------------------------------
-- Definition
×-Lex : (_≈₁_ : Rel A ℓ₁) (_≤₁_ : Rel A ℓ₂) (_≤₂_ : Rel B ℓ₃) →
Rel (A × B) _
×-Lex _≈₁_ _≤₁_ _≤₂_ = Strict.×-Lex _≈₁_ (Conv._<_ _≈₁_ _≤₁_) _≤₂_
------------------------------------------------------------------------
-- Properties
×-reflexive : (_≈₁_ : Rel A ℓ₁) (_≤₁_ : Rel A ℓ₂)
{_≈₂_ : Rel B ℓ₃} (_≤₂_ : Rel B ℓ₄) →
_≈₂_ ⇒ _≤₂_ →
(Pointwise _≈₁_ _≈₂_) ⇒ (×-Lex _≈₁_ _≤₁_ _≤₂_)
×-reflexive _≈₁_ _≤₁_ _≤₂_ refl₂ =
Strict.×-reflexive _≈₁_ (Conv._<_ _≈₁_ _≤₁_) _≤₂_ refl₂
module _ {_≈₁_ : Rel A ℓ₁} {_≤₁_ : Rel A ℓ₂} {_≤₂_ : Rel B ℓ₃} where
private
_≤ₗₑₓ_ = ×-Lex _≈₁_ _≤₁_ _≤₂_
×-transitive : IsPartialOrder _≈₁_ _≤₁_ → Transitive _≤₂_ →
Transitive _≤ₗₑₓ_
×-transitive po₁ trans₂ =
Strict.×-transitive {_≈₁_ = _≈₁_} {_<₂_ = _≤₂_}
isEquivalence (Conv.<-resp-≈ _ _ isEquivalence ≤-resp-≈)
(Conv.<-trans _ _ po₁)
trans₂
where open IsPartialOrder po₁
×-total : Symmetric _≈₁_ → Decidable _≈₁_ → Antisymmetric _≈₁_ _≤₁_ →
Total _≤₁_ → Total _≤₂_ → Total _≤ₗₑₓ_
×-total sym₁ dec₁ antisym₁ total₁ total₂ =
total
where
tri₁ : Trichotomous _≈₁_ (Conv._<_ _≈₁_ _≤₁_)
tri₁ = Conv.<-trichotomous _ _ sym₁ dec₁ antisym₁ total₁
total : Total _≤ₗₑₓ_
total x y with tri₁ (proj₁ x) (proj₁ y)
... | tri< x₁<y₁ x₁≉y₁ x₁≯y₁ = inj₁ (inj₁ x₁<y₁)
... | tri> x₁≮y₁ x₁≉y₁ x₁>y₁ = inj₂ (inj₁ x₁>y₁)
... | tri≈ x₁≮y₁ x₁≈y₁ x₁≯y₁ with total₂ (proj₂ x) (proj₂ y)
... | inj₁ x₂≤y₂ = inj₁ (inj₂ (x₁≈y₁ , x₂≤y₂))
... | inj₂ x₂≥y₂ = inj₂ (inj₂ (sym₁ x₁≈y₁ , x₂≥y₂))
×-decidable : Decidable _≈₁_ → Decidable _≤₁_ → Decidable _≤₂_ →
Decidable _≤ₗₑₓ_
×-decidable dec-≈₁ dec-≤₁ dec-≤₂ =
Strict.×-decidable dec-≈₁ (Conv.<-decidable _ _ dec-≈₁ dec-≤₁)
dec-≤₂
module _ {_≈₁_ : Rel A ℓ₁} {_≤₁_ : Rel A ℓ₂}
{_≈₂_ : Rel B ℓ₃} {_≤₂_ : Rel B ℓ₄}
where
private
_≤ₗₑₓ_ = ×-Lex _≈₁_ _≤₁_ _≤₂_
_≋_ = Pointwise _≈₁_ _≈₂_
×-antisymmetric : IsPartialOrder _≈₁_ _≤₁_ → Antisymmetric _≈₂_ _≤₂_ →
Antisymmetric _≋_ _≤ₗₑₓ_
×-antisymmetric po₁ antisym₂ =
Strict.×-antisymmetric {_≈₁_ = _≈₁_} {_<₂_ = _≤₂_}
≈-sym₁ irrefl₁ asym₁ antisym₂
where
open IsPartialOrder po₁
open Eq renaming (refl to ≈-refl₁; sym to ≈-sym₁)
irrefl₁ : Irreflexive _≈₁_ (Conv._<_ _≈₁_ _≤₁_)
irrefl₁ = Conv.<-irrefl _≈₁_ _≤₁_
asym₁ : Asymmetric (Conv._<_ _≈₁_ _≤₁_)
asym₁ = trans∧irr⇒asym {_≈_ = _≈₁_}
≈-refl₁ (Conv.<-trans _ _ po₁) irrefl₁
×-respects₂ : IsEquivalence _≈₁_ →
_≤₁_ Respects₂ _≈₁_ → _≤₂_ Respects₂ _≈₂_ →
_≤ₗₑₓ_ Respects₂ _≋_
×-respects₂ eq₁ resp₁ resp₂ =
Strict.×-respects₂ eq₁ (Conv.<-resp-≈ _ _ eq₁ resp₁) resp₂
------------------------------------------------------------------------
-- Structures
×-isPartialOrder : IsPartialOrder _≈₁_ _≤₁_ →
IsPartialOrder _≈₂_ _≤₂_ →
IsPartialOrder _≋_ _≤ₗₑₓ_
×-isPartialOrder po₁ po₂ = record
{ isPreorder = record
{ isEquivalence = Pointwise.×-isEquivalence
(isEquivalence po₁)
(isEquivalence po₂)
; reflexive = ×-reflexive _≈₁_ _≤₁_ _≤₂_ (reflexive po₂)
; trans = ×-transitive {_≤₂_ = _≤₂_} po₁ (trans po₂)
}
; antisym = ×-antisymmetric po₁ (antisym po₂)
}
where open IsPartialOrder
×-isTotalOrder : Decidable _≈₁_ →
IsTotalOrder _≈₁_ _≤₁_ →
IsTotalOrder _≈₂_ _≤₂_ →
IsTotalOrder _≋_ _≤ₗₑₓ_
×-isTotalOrder ≈₁-dec to₁ to₂ = record
{ isPartialOrder = ×-isPartialOrder
(isPartialOrder to₁) (isPartialOrder to₂)
; total = ×-total (Eq.sym to₁) ≈₁-dec
(antisym to₁) (total to₁)
(total to₂)
}
where open IsTotalOrder
×-isDecTotalOrder : IsDecTotalOrder _≈₁_ _≤₁_ →
IsDecTotalOrder _≈₂_ _≤₂_ →
IsDecTotalOrder _≋_ _≤ₗₑₓ_
×-isDecTotalOrder to₁ to₂ = record
{ isTotalOrder = ×-isTotalOrder (_≟_ to₁)
(isTotalOrder to₁)
(isTotalOrder to₂)
; _≟_ = Pointwise.×-decidable (_≟_ to₁) (_≟_ to₂)
; _≤?_ = ×-decidable (_≟_ to₁) (_≤?_ to₁) (_≤?_ to₂)
}
where open IsDecTotalOrder
------------------------------------------------------------------------
-- Bundles
×-poset : Poset a ℓ₁ ℓ₂ → Poset b ℓ₃ ℓ₄ → Poset _ _ _
×-poset p₁ p₂ = record
{ isPartialOrder = ×-isPartialOrder O₁.isPartialOrder O₂.isPartialOrder
} where module O₁ = Poset p₁; module O₂ = Poset p₂
×-totalOrder : DecTotalOrder a ℓ₁ ℓ₂ →
TotalOrder b ℓ₃ ℓ₄ →
TotalOrder _ _ _
×-totalOrder t₁ t₂ = record
{ isTotalOrder = ×-isTotalOrder T₁._≟_ T₁.isTotalOrder T₂.isTotalOrder
} where module T₁ = DecTotalOrder t₁; module T₂ = TotalOrder t₂
×-decTotalOrder : DecTotalOrder a ℓ₁ ℓ₂ →
DecTotalOrder b ℓ₃ ℓ₄ →
DecTotalOrder _ _ _
×-decTotalOrder t₁ t₂ = record
{ isDecTotalOrder = ×-isDecTotalOrder O₁.isDecTotalOrder O₂.isDecTotalOrder
} where module O₁ = DecTotalOrder t₁; module O₂ = DecTotalOrder t₂
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4