------------------------------------------------------------------------
-- The Agda standard library
--
-- Sums of binary relations
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Sum.Relation.Binary.LeftOrder where
open import Data.Sum.Base as Sum using (inj₁; inj₂; _⊎_)
open import Data.Sum.Relation.Binary.Pointwise as PW
using (Pointwise; inj₁; inj₂)
open import Data.Product.Base using (_,_)
open import Data.Empty using (⊥)
open import Function.Base using (_$_; _∘_)
open import Induction.WellFounded
open import Level using (Level; _⊔_)
open import Relation.Nullary.Negation.Core using (¬_)
open import Relation.Nullary.Decidable.Core using (yes; no)
import Relation.Nullary.Decidable as Dec using (Dec; map; map′)
open import Relation.Binary.Core using (Rel; _⇒_)
open import Relation.Binary.Bundles
using (Preorder; Poset; StrictPartialOrder; TotalOrder; DecTotalOrder
; StrictTotalOrder)
open import Relation.Binary.Structures
using (IsPreorder; IsPartialOrder; IsStrictPartialOrder; IsTotalOrder
; IsDecTotalOrder; IsStrictTotalOrder)
open import Relation.Binary.Definitions
using (Reflexive; Transitive; Asymmetric; Total; Decidable; Irreflexive
; Antisymmetric; Trichotomous; _Respectsʳ_; _Respectsˡ_; _Respects₂_
; tri<; tri>; tri≈)
open import Relation.Binary.PropositionalEquality.Core using (_≡_)
------------------------------------------------------------------------
-- Definition
infixr 1 _⊎-<_
data _⊎-<_ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂}
{ℓ₁ ℓ₂} (_∼₁_ : Rel A₁ ℓ₁) (_∼₂_ : Rel A₂ ℓ₂) :
Rel (A₁ ⊎ A₂) (a₁ ⊔ a₂ ⊔ ℓ₁ ⊔ ℓ₂) where
₁∼₂ : ∀ {x y} → (_∼₁_ ⊎-< _∼₂_) (inj₁ x) (inj₂ y)
₁∼₁ : ∀ {x y} (x∼₁y : x ∼₁ y) → (_∼₁_ ⊎-< _∼₂_) (inj₁ x) (inj₁ y)
₂∼₂ : ∀ {x y} (x∼₂y : x ∼₂ y) → (_∼₁_ ⊎-< _∼₂_) (inj₂ x) (inj₂ y)
------------------------------------------------------------------------
-- Some properties which are preserved by _⊎-<_
module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂}
{ℓ₁ ℓ₂} {∼₁ : Rel A₁ ℓ₁} {∼₂ : Rel A₂ ℓ₂}
where
drop-inj₁ : ∀ {x y} → (∼₁ ⊎-< ∼₂) (inj₁ x) (inj₁ y) → ∼₁ x y
drop-inj₁ (₁∼₁ x∼₁y) = x∼₁y
drop-inj₂ : ∀ {x y} → (∼₁ ⊎-< ∼₂) (inj₂ x) (inj₂ y) → ∼₂ x y
drop-inj₂ (₂∼₂ x∼₂y) = x∼₂y
⊎-<-refl : Reflexive ∼₁ → Reflexive ∼₂ →
Reflexive (∼₁ ⊎-< ∼₂)
⊎-<-refl refl₁ refl₂ {inj₁ x} = ₁∼₁ refl₁
⊎-<-refl refl₁ refl₂ {inj₂ y} = ₂∼₂ refl₂
⊎-<-transitive : Transitive ∼₁ → Transitive ∼₂ →
Transitive (∼₁ ⊎-< ∼₂)
⊎-<-transitive trans₁ trans₂ ₁∼₂ (₂∼₂ x∼₂y) = ₁∼₂
⊎-<-transitive trans₁ trans₂ (₁∼₁ x∼₁y) ₁∼₂ = ₁∼₂
⊎-<-transitive trans₁ trans₂ (₁∼₁ x∼₁y) (₁∼₁ x∼₁y₁) = ₁∼₁ (trans₁ x∼₁y x∼₁y₁)
⊎-<-transitive trans₁ trans₂ (₂∼₂ x∼₂y) (₂∼₂ x∼₂y₁) = ₂∼₂ (trans₂ x∼₂y x∼₂y₁)
⊎-<-asymmetric : Asymmetric ∼₁ → Asymmetric ∼₂ →
Asymmetric (∼₁ ⊎-< ∼₂)
⊎-<-asymmetric asym₁ asym₂ (₁∼₁ x∼₁y) (₁∼₁ x∼₁y₁) = asym₁ x∼₁y x∼₁y₁
⊎-<-asymmetric asym₁ asym₂ (₂∼₂ x∼₂y) (₂∼₂ x∼₂y₁) = asym₂ x∼₂y x∼₂y₁
⊎-<-total : Total ∼₁ → Total ∼₂ → Total (∼₁ ⊎-< ∼₂)
⊎-<-total total₁ total₂ = total
where
total : Total (_ ⊎-< _)
total (inj₁ x) (inj₁ y) = Sum.map ₁∼₁ ₁∼₁ $ total₁ x y
total (inj₁ x) (inj₂ y) = inj₁ ₁∼₂
total (inj₂ x) (inj₁ y) = inj₂ ₁∼₂
total (inj₂ x) (inj₂ y) = Sum.map ₂∼₂ ₂∼₂ $ total₂ x y
⊎-<-decidable : Decidable ∼₁ → Decidable ∼₂ →
Decidable (∼₁ ⊎-< ∼₂)
⊎-<-decidable dec₁ dec₂ (inj₁ x) (inj₁ y) = Dec.map′ ₁∼₁ drop-inj₁ (dec₁ x y)
⊎-<-decidable dec₁ dec₂ (inj₁ x) (inj₂ y) = yes ₁∼₂
⊎-<-decidable dec₁ dec₂ (inj₂ x) (inj₁ y) = no λ()
⊎-<-decidable dec₁ dec₂ (inj₂ x) (inj₂ y) = Dec.map′ ₂∼₂ drop-inj₂ (dec₂ x y)
⊎-<-wellFounded : WellFounded ∼₁ → WellFounded ∼₂ → WellFounded (∼₁ ⊎-< ∼₂)
⊎-<-wellFounded wf₁ wf₂ x = acc (⊎-<-acc x)
where
⊎-<-acc₁ : ∀ {x} → Acc ∼₁ x → WfRec (∼₁ ⊎-< ∼₂) (Acc (∼₁ ⊎-< ∼₂)) (inj₁ x)
⊎-<-acc₁ (acc rec) (₁∼₁ x∼₁y) = acc (⊎-<-acc₁ (rec x∼₁y))
⊎-<-acc₂ : ∀ {x} → Acc ∼₂ x → WfRec (∼₁ ⊎-< ∼₂) (Acc (∼₁ ⊎-< ∼₂)) (inj₂ x)
⊎-<-acc₂ (acc rec) {inj₁ x} ₁∼₂ = acc (⊎-<-acc₁ (wf₁ x))
⊎-<-acc₂ (acc rec) (₂∼₂ x∼₂y) = acc (⊎-<-acc₂ (rec x∼₂y))
⊎-<-acc : ∀ x → WfRec (∼₁ ⊎-< ∼₂) (Acc (∼₁ ⊎-< ∼₂)) x
⊎-<-acc (inj₁ x) = ⊎-<-acc₁ (wf₁ x)
⊎-<-acc (inj₂ x) = ⊎-<-acc₂ (wf₂ x)
module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂}
{ℓ₁ ℓ₂} {∼₁ : Rel A₁ ℓ₁} {≈₁ : Rel A₁ ℓ₂}
{ℓ₃ ℓ₄} {∼₂ : Rel A₂ ℓ₃} {≈₂ : Rel A₂ ℓ₄}
where
⊎-<-reflexive : ≈₁ ⇒ ∼₁ → ≈₂ ⇒ ∼₂ →
(Pointwise ≈₁ ≈₂) ⇒ (∼₁ ⊎-< ∼₂)
⊎-<-reflexive refl₁ refl₂ (inj₁ x) = ₁∼₁ (refl₁ x)
⊎-<-reflexive refl₁ refl₂ (inj₂ x) = ₂∼₂ (refl₂ x)
⊎-<-irreflexive : Irreflexive ≈₁ ∼₁ → Irreflexive ≈₂ ∼₂ →
Irreflexive (Pointwise ≈₁ ≈₂) (∼₁ ⊎-< ∼₂)
⊎-<-irreflexive irrefl₁ irrefl₂ (inj₁ x) (₁∼₁ x∼₁y) = irrefl₁ x x∼₁y
⊎-<-irreflexive irrefl₁ irrefl₂ (inj₂ x) (₂∼₂ x∼₂y) = irrefl₂ x x∼₂y
⊎-<-antisymmetric : Antisymmetric ≈₁ ∼₁ → Antisymmetric ≈₂ ∼₂ →
Antisymmetric (Pointwise ≈₁ ≈₂) (∼₁ ⊎-< ∼₂)
⊎-<-antisymmetric antisym₁ antisym₂ (₁∼₁ x∼₁y) (₁∼₁ x∼₁y₁) = inj₁ (antisym₁ x∼₁y x∼₁y₁)
⊎-<-antisymmetric antisym₁ antisym₂ (₂∼₂ x∼₂y) (₂∼₂ x∼₂y₁) = inj₂ (antisym₂ x∼₂y x∼₂y₁)
⊎-<-respectsʳ : ∼₁ Respectsʳ ≈₁ → ∼₂ Respectsʳ ≈₂ →
(∼₁ ⊎-< ∼₂) Respectsʳ (Pointwise ≈₁ ≈₂)
⊎-<-respectsʳ resp₁ resp₂ (inj₁ x₁) (₁∼₁ x∼₁y) = ₁∼₁ (resp₁ x₁ x∼₁y)
⊎-<-respectsʳ resp₁ resp₂ (inj₂ x₁) ₁∼₂ = ₁∼₂
⊎-<-respectsʳ resp₁ resp₂ (inj₂ x₁) (₂∼₂ x∼₂y) = ₂∼₂ (resp₂ x₁ x∼₂y)
⊎-<-respectsˡ : ∼₁ Respectsˡ ≈₁ → ∼₂ Respectsˡ ≈₂ →
(∼₁ ⊎-< ∼₂) Respectsˡ (Pointwise ≈₁ ≈₂)
⊎-<-respectsˡ resp₁ resp₂ (inj₁ x) ₁∼₂ = ₁∼₂
⊎-<-respectsˡ resp₁ resp₂ (inj₁ x) (₁∼₁ x∼₁y) = ₁∼₁ (resp₁ x x∼₁y)
⊎-<-respectsˡ resp₁ resp₂ (inj₂ x) (₂∼₂ x∼₂y) = ₂∼₂ (resp₂ x x∼₂y)
⊎-<-respects₂ : ∼₁ Respects₂ ≈₁ → ∼₂ Respects₂ ≈₂ →
(∼₁ ⊎-< ∼₂) Respects₂ (Pointwise ≈₁ ≈₂)
⊎-<-respects₂ (r₁ , l₁) (r₂ , l₂) = ⊎-<-respectsʳ r₁ r₂ , ⊎-<-respectsˡ l₁ l₂
⊎-<-trichotomous : Trichotomous ≈₁ ∼₁ → Trichotomous ≈₂ ∼₂ →
Trichotomous (Pointwise ≈₁ ≈₂) (∼₁ ⊎-< ∼₂)
⊎-<-trichotomous tri₁ tri₂ (inj₁ x) (inj₂ y) = tri< ₁∼₂ (λ()) (λ())
⊎-<-trichotomous tri₁ tri₂ (inj₂ x) (inj₁ y) = tri> (λ()) (λ()) ₁∼₂
⊎-<-trichotomous tri₁ tri₂ (inj₁ x) (inj₁ y) with tri₁ x y
... | tri< x<y x≉y x≯y = tri< (₁∼₁ x<y) (x≉y ∘ PW.drop-inj₁) (x≯y ∘ drop-inj₁)
... | tri≈ x≮y x≈y x≯y = tri≈ (x≮y ∘ drop-inj₁) (inj₁ x≈y) (x≯y ∘ drop-inj₁)
... | tri> x≮y x≉y x>y = tri> (x≮y ∘ drop-inj₁) (x≉y ∘ PW.drop-inj₁) (₁∼₁ x>y)
⊎-<-trichotomous tri₁ tri₂ (inj₂ x) (inj₂ y) with tri₂ x y
... | tri< x<y x≉y x≯y = tri< (₂∼₂ x<y) (x≉y ∘ PW.drop-inj₂) (x≯y ∘ drop-inj₂)
... | tri≈ x≮y x≈y x≯y = tri≈ (x≮y ∘ drop-inj₂) (inj₂ x≈y) (x≯y ∘ drop-inj₂)
... | tri> x≮y x≉y x>y = tri> (x≮y ∘ drop-inj₂) (x≉y ∘ PW.drop-inj₂) (₂∼₂ x>y)
------------------------------------------------------------------------
-- Some collections of properties which are preserved
module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂}
{ℓ₁ ℓ₂} {≈₁ : Rel A₁ ℓ₁} {∼₁ : Rel A₁ ℓ₂}
{ℓ₃ ℓ₄} {≈₂ : Rel A₂ ℓ₃} {∼₂ : Rel A₂ ℓ₄} where
⊎-<-isPreorder : IsPreorder ≈₁ ∼₁ → IsPreorder ≈₂ ∼₂ →
IsPreorder (Pointwise ≈₁ ≈₂) (∼₁ ⊎-< ∼₂)
⊎-<-isPreorder pre₁ pre₂ = record
{ isEquivalence = PW.⊎-isEquivalence (isEquivalence pre₁) (isEquivalence pre₂)
; reflexive = ⊎-<-reflexive (reflexive pre₁) (reflexive pre₂)
; trans = ⊎-<-transitive (trans pre₁) (trans pre₂)
}
where open IsPreorder
⊎-<-isPartialOrder : IsPartialOrder ≈₁ ∼₁ →
IsPartialOrder ≈₂ ∼₂ →
IsPartialOrder (Pointwise ≈₁ ≈₂) (∼₁ ⊎-< ∼₂)
⊎-<-isPartialOrder po₁ po₂ = record
{ isPreorder = ⊎-<-isPreorder (isPreorder po₁) (isPreorder po₂)
; antisym = ⊎-<-antisymmetric (antisym po₁) (antisym po₂)
}
where open IsPartialOrder
⊎-<-isStrictPartialOrder : IsStrictPartialOrder ≈₁ ∼₁ →
IsStrictPartialOrder ≈₂ ∼₂ →
IsStrictPartialOrder (Pointwise ≈₁ ≈₂) (∼₁ ⊎-< ∼₂)
⊎-<-isStrictPartialOrder spo₁ spo₂ = record
{ isEquivalence = PW.⊎-isEquivalence (isEquivalence spo₁) (isEquivalence spo₂)
; irrefl = ⊎-<-irreflexive (irrefl spo₁) (irrefl spo₂)
; trans = ⊎-<-transitive (trans spo₁) (trans spo₂)
; <-resp-≈ = ⊎-<-respects₂ (<-resp-≈ spo₁) (<-resp-≈ spo₂)
}
where open IsStrictPartialOrder
⊎-<-isTotalOrder : IsTotalOrder ≈₁ ∼₁ →
IsTotalOrder ≈₂ ∼₂ →
IsTotalOrder (Pointwise ≈₁ ≈₂) (∼₁ ⊎-< ∼₂)
⊎-<-isTotalOrder to₁ to₂ = record
{ isPartialOrder = ⊎-<-isPartialOrder (isPartialOrder to₁) (isPartialOrder to₂)
; total = ⊎-<-total (total to₁) (total to₂)
}
where open IsTotalOrder
⊎-<-isDecTotalOrder : IsDecTotalOrder ≈₁ ∼₁ →
IsDecTotalOrder ≈₂ ∼₂ →
IsDecTotalOrder (Pointwise ≈₁ ≈₂) (∼₁ ⊎-< ∼₂)
⊎-<-isDecTotalOrder to₁ to₂ = record
{ isTotalOrder = ⊎-<-isTotalOrder (isTotalOrder to₁) (isTotalOrder to₂)
; _≟_ = PW.⊎-decidable (_≟_ to₁) (_≟_ to₂)
; _≤?_ = ⊎-<-decidable (_≤?_ to₁) (_≤?_ to₂)
}
where open IsDecTotalOrder
⊎-<-isStrictTotalOrder : IsStrictTotalOrder ≈₁ ∼₁ →
IsStrictTotalOrder ≈₂ ∼₂ →
IsStrictTotalOrder (Pointwise ≈₁ ≈₂) (∼₁ ⊎-< ∼₂)
⊎-<-isStrictTotalOrder sto₁ sto₂ = record
{ isStrictPartialOrder = ⊎-<-isStrictPartialOrder (isStrictPartialOrder sto₁) (isStrictPartialOrder sto₂)
; compare = ⊎-<-trichotomous (compare sto₁) (compare sto₂)
}
where open IsStrictTotalOrder
------------------------------------------------------------------------
-- "Bundles" can also be combined.
module _ {a b c d e f} where
⊎-<-preorder : Preorder a b c →
Preorder d e f →
Preorder _ _ _
⊎-<-preorder p₁ p₂ = record
{ isPreorder =
⊎-<-isPreorder (isPreorder p₁) (isPreorder p₂)
} where open Preorder
⊎-<-poset : Poset a b c →
Poset a b c →
Poset _ _ _
⊎-<-poset po₁ po₂ = record
{ isPartialOrder =
⊎-<-isPartialOrder (isPartialOrder po₁) (isPartialOrder po₂)
} where open Poset
⊎-<-strictPartialOrder : StrictPartialOrder a b c →
StrictPartialOrder d e f →
StrictPartialOrder _ _ _
⊎-<-strictPartialOrder spo₁ spo₂ = record
{ isStrictPartialOrder =
⊎-<-isStrictPartialOrder (isStrictPartialOrder spo₁) (isStrictPartialOrder spo₂)
} where open StrictPartialOrder
⊎-<-totalOrder : TotalOrder a b c →
TotalOrder d e f →
TotalOrder _ _ _
⊎-<-totalOrder to₁ to₂ = record
{ isTotalOrder = ⊎-<-isTotalOrder (isTotalOrder to₁) (isTotalOrder to₂)
} where open TotalOrder
⊎-<-decTotalOrder : DecTotalOrder a b c →
DecTotalOrder d e f →
DecTotalOrder _ _ _
⊎-<-decTotalOrder to₁ to₂ = record
{ isDecTotalOrder = ⊎-<-isDecTotalOrder (isDecTotalOrder to₁) (isDecTotalOrder to₂)
} where open DecTotalOrder
⊎-<-strictTotalOrder : StrictTotalOrder a b c →
StrictTotalOrder a b c →
StrictTotalOrder _ _ _
⊎-<-strictTotalOrder sto₁ sto₂ = record
{ isStrictTotalOrder = ⊎-<-isStrictTotalOrder (isStrictTotalOrder sto₁) (isStrictTotalOrder sto₂)
} where open StrictTotalOrder
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