------------------------------------------------------------------------
-- The Agda standard library
--
-- Conversion of < to ≤, along with a number of properties
------------------------------------------------------------------------
-- Possible TODO: Prove that a conversion ≤ → < → ≤ returns a
-- relation equivalent to the original one (and similarly for
-- < → ≤ → <).
{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Core using (Rel; _⇒_)
module Relation.Binary.Construct.StrictToNonStrict
{a ℓ₁ ℓ₂} {A : Set a}
(_≈_ : Rel A ℓ₁) (_<_ : Rel A ℓ₂)
where
open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
open import Data.Sum.Base using (inj₁; inj₂; _⊎_; [_,_]; [_,_]′)
open import Data.Empty using (⊥; ⊥-elim)
open import Function.Base using (_∘_; flip; _$_)
open import Relation.Binary.Consequences using (trans∧irr⇒asym)
open import Relation.Binary.Structures
using (IsEquivalence; IsPreorder; IsStrictPartialOrder; IsPartialOrder
; IsStrictTotalOrder; IsTotalOrder; IsDecTotalOrder)
open import Relation.Binary.Definitions
using (Transitive; Symmetric; Irreflexive; Antisymmetric; Trichotomous; Decidable
; Trans; Total; _Respects₂_; _Respectsʳ_; _Respectsˡ_; tri<; tri≈; tri>)
open import Relation.Nullary.Decidable.Core using (_⊎-dec_; yes; no)
open import Relation.Nullary.Negation.Core using (contradiction)
------------------------------------------------------------------------
-- Conversion
-- _<_ can be turned into _≤_ as follows:
infix 4 _≤_
_≤_ : Rel A _
x ≤ y = (x < y) ⊎ (x ≈ y)
------------------------------------------------------------------------
-- The converted relations have certain properties
-- (if the original relations have certain other properties)
<⇒≤ : _<_ ⇒ _≤_
<⇒≤ = inj₁
reflexive : _≈_ ⇒ _≤_
reflexive = inj₂
antisym : IsEquivalence _≈_ → Transitive _<_ → Irreflexive _≈_ _<_ →
Antisymmetric _≈_ _≤_
antisym eq trans irrefl = as
where
module Eq = IsEquivalence eq
as : Antisymmetric _≈_ _≤_
as (inj₂ x≈y) _ = x≈y
as (inj₁ _) (inj₂ y≈x) = Eq.sym y≈x
as (inj₁ x<y) (inj₁ y<x) =
contradiction y<x (trans∧irr⇒asym {_≈_ = _≈_} Eq.refl trans irrefl x<y)
trans : IsEquivalence _≈_ → _<_ Respects₂ _≈_ → Transitive _<_ →
Transitive _≤_
trans eq (respʳ , respˡ) <-trans = tr
where
module Eq = IsEquivalence eq
tr : Transitive _≤_
tr (inj₁ x<y) (inj₁ y<z) = inj₁ $ <-trans x<y y<z
tr (inj₁ x<y) (inj₂ y≈z) = inj₁ $ respʳ y≈z x<y
tr (inj₂ x≈y) (inj₁ y<z) = inj₁ $ respˡ (Eq.sym x≈y) y<z
tr (inj₂ x≈y) (inj₂ y≈z) = inj₂ $ Eq.trans x≈y y≈z
<-≤-trans : Transitive _<_ → _<_ Respectsʳ _≈_ → Trans _<_ _≤_ _<_
<-≤-trans trans respʳ x<y (inj₁ y<z) = trans x<y y<z
<-≤-trans trans respʳ x<y (inj₂ y≈z) = respʳ y≈z x<y
≤-<-trans : Symmetric _≈_ → Transitive _<_ → _<_ Respectsˡ _≈_ → Trans _≤_ _<_ _<_
≤-<-trans sym trans respˡ (inj₁ x<y) y<z = trans x<y y<z
≤-<-trans sym trans respˡ (inj₂ x≈y) y<z = respˡ (sym x≈y) y<z
≤-respʳ-≈ : Transitive _≈_ → _<_ Respectsʳ _≈_ → _≤_ Respectsʳ _≈_
≤-respʳ-≈ trans respʳ y′≈y (inj₁ x<y′) = inj₁ (respʳ y′≈y x<y′)
≤-respʳ-≈ trans respʳ y′≈y (inj₂ x≈y′) = inj₂ (trans x≈y′ y′≈y)
≤-respˡ-≈ : Symmetric _≈_ → Transitive _≈_ → _<_ Respectsˡ _≈_ → _≤_ Respectsˡ _≈_
≤-respˡ-≈ sym trans respˡ x′≈x (inj₁ x′<y) = inj₁ (respˡ x′≈x x′<y)
≤-respˡ-≈ sym trans respˡ x′≈x (inj₂ x′≈y) = inj₂ (trans (sym x′≈x) x′≈y)
≤-resp-≈ : IsEquivalence _≈_ → _<_ Respects₂ _≈_ → _≤_ Respects₂ _≈_
≤-resp-≈ eq (respʳ , respˡ) = ≤-respʳ-≈ Eq.trans respʳ , ≤-respˡ-≈ Eq.sym Eq.trans respˡ
where module Eq = IsEquivalence eq
total : Trichotomous _≈_ _<_ → Total _≤_
total <-tri x y with <-tri x 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 = inj₂ (inj₁ x>y)
decidable : Decidable _≈_ → Decidable _<_ → Decidable _≤_
decidable ≈-dec <-dec x y = <-dec x y ⊎-dec ≈-dec x y
decidable′ : Trichotomous _≈_ _<_ → Decidable _≤_
decidable′ compare x y with compare x y
... | tri< x<y _ _ = yes (inj₁ x<y)
... | tri≈ _ x≈y _ = yes (inj₂ x≈y)
... | tri> x≮y x≉y _ = no [ x≮y , x≉y ]′
------------------------------------------------------------------------
-- Converting structures
isPreorder₁ : IsPreorder _≈_ _<_ → IsPreorder _≈_ _≤_
isPreorder₁ PO = record
{ isEquivalence = S.isEquivalence
; reflexive = reflexive
; trans = trans S.isEquivalence S.∼-resp-≈ S.trans
}
where module S = IsPreorder PO
isPreorder₂ : IsStrictPartialOrder _≈_ _<_ → IsPreorder _≈_ _≤_
isPreorder₂ SPO = record
{ isEquivalence = S.isEquivalence
; reflexive = reflexive
; trans = trans S.isEquivalence S.<-resp-≈ S.trans
}
where module S = IsStrictPartialOrder SPO
isPartialOrder : IsStrictPartialOrder _≈_ _<_ → IsPartialOrder _≈_ _≤_
isPartialOrder SPO = record
{ isPreorder = isPreorder₂ SPO
; antisym = antisym S.isEquivalence S.trans S.irrefl
}
where module S = IsStrictPartialOrder SPO
isTotalOrder : IsStrictTotalOrder _≈_ _<_ → IsTotalOrder _≈_ _≤_
isTotalOrder STO = record
{ isPartialOrder = isPartialOrder S.isStrictPartialOrder
; total = total S.compare
}
where module S = IsStrictTotalOrder STO
isDecTotalOrder : IsStrictTotalOrder _≈_ _<_ → IsDecTotalOrder _≈_ _≤_
isDecTotalOrder STO = record
{ isTotalOrder = isTotalOrder STO
; _≟_ = S._≟_
; _≤?_ = decidable′ S.compare
}
where module S = IsStrictTotalOrder STO
------------------------------------------------------------------------
-- DEPRECATED
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.
-- Version 1.4
decidable' : Trichotomous _≈_ _<_ → Decidable _≤_
decidable' = decidable′
{-# WARNING_ON_USAGE decidable'
"Warning: decidable' (ending in an apostrophe) was deprecated in v1.4.
Please use decidable′ (ending in a prime) instead."
#-}
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