{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Core using (Rel; _⇒_)
open import Relation.Binary.Structures
using (IsPartialOrder; IsEquivalence; IsStrictPartialOrder; IsDecPartialOrder; IsDecStrictPartialOrder; IsTotalOrder; IsStrictTotalOrder; IsDecTotalOrder)
open import Relation.Binary.Definitions
using (Trichotomous; Antisymmetric; Symmetric; Total; Decidable; Irreflexive; Transitive; _Respectsʳ_; _Respectsˡ_; _Respects₂_; Trans; Asymmetric; tri≈; tri<; tri>)
module Relation.Binary.Construct.NonStrictToStrict
{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 Function.Base using (_∘_; flip)
open import Relation.Nullary using (¬_; yes; no)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Nullary.Decidable using (¬?; _×-dec_)
private
_≉_ : Rel A ℓ₁
x ≉ y = ¬ (x ≈ y)
infix 4 _<_
_<_ : Rel A _
x < y = x ≤ y × x ≉ y
<⇒≤ : _<_ ⇒ _≤_
<⇒≤ = proj₁
<⇒≉ : ∀ {x y} → x < y → x ≉ y
<⇒≉ = proj₂
≤∧≉⇒< : ∀ {x y} → x ≤ y → x ≉ y → x < y
≤∧≉⇒< = _,_
<⇒≱ : Antisymmetric _≈_ _≤_ → ∀ {x y} → x < y → ¬ (y ≤ x)
<⇒≱ antisym (x≤y , x≉y) y≤x = x≉y (antisym x≤y y≤x)
≤⇒≯ : Antisymmetric _≈_ _≤_ → ∀ {x y} → x ≤ y → ¬ (y < x)
≤⇒≯ antisym x≤y y<x = <⇒≱ antisym y<x x≤y
≰⇒> : Symmetric _≈_ → (_≈_ ⇒ _≤_) → Total _≤_ →
∀ {x y} → ¬ (x ≤ y) → y < x
≰⇒> sym refl total {x} {y} x≰y with total x y
... | inj₁ x≤y = contradiction x≤y x≰y
... | inj₂ y≤x = y≤x , x≰y ∘ refl ∘ sym
≮⇒≥ : Symmetric _≈_ → Decidable _≈_ → _≈_ ⇒ _≤_ → Total _≤_ →
∀ {x y} → ¬ (x < y) → y ≤ x
≮⇒≥ sym _≟_ ≤-refl _≤?_ {x} {y} x≮y with x ≟ y | y ≤? x
... | yes x≈y | _ = ≤-refl (sym x≈y)
... | _ | inj₁ y≤x = y≤x
... | no x≉y | inj₂ x≤y = contradiction (x≤y , x≉y) x≮y
<-irrefl : Irreflexive _≈_ _<_
<-irrefl x≈y (_ , x≉y) = x≉y x≈y
<-trans : IsPartialOrder _≈_ _≤_ → Transitive _<_
<-trans po (x≤y , x≉y) (y≤z , y≉z) =
(trans x≤y y≤z , x≉y ∘ antisym x≤y ∘ trans y≤z ∘ reflexive ∘ Eq.sym)
where open IsPartialOrder po
<-≤-trans : Symmetric _≈_ → Transitive _≤_ → Antisymmetric _≈_ _≤_ →
_≤_ Respectsʳ _≈_ → Trans _<_ _≤_ _<_
<-≤-trans sym trans antisym respʳ (x≤y , x≉y) y≤z =
trans x≤y y≤z , (λ x≈z → x≉y (antisym x≤y (respʳ (sym x≈z) y≤z)))
≤-<-trans : Transitive _≤_ → Antisymmetric _≈_ _≤_ →
_≤_ Respectsˡ _≈_ → Trans _≤_ _<_ _<_
≤-<-trans trans antisym respʳ x≤y (y≤z , y≉z) =
trans x≤y y≤z , (λ x≈z → y≉z (antisym y≤z (respʳ x≈z x≤y)))
<-asym : Antisymmetric _≈_ _≤_ → Asymmetric _<_
<-asym antisym (x≤y , x≉y) (y≤x , _) = x≉y (antisym x≤y y≤x)
<-respˡ-≈ : Transitive _≈_ → _≤_ Respectsˡ _≈_ → _<_ Respectsˡ _≈_
<-respˡ-≈ trans respˡ y≈z (y≤x , y≉x) =
respˡ y≈z y≤x , y≉x ∘ trans y≈z
<-respʳ-≈ : Symmetric _≈_ → Transitive _≈_ →
_≤_ Respectsʳ _≈_ → _<_ Respectsʳ _≈_
<-respʳ-≈ sym trans respʳ y≈z (x≤y , x≉y) =
(respʳ y≈z x≤y) , λ x≈z → x≉y (trans x≈z (sym y≈z))
<-resp-≈ : IsEquivalence _≈_ → _≤_ Respects₂ _≈_ → _<_ Respects₂ _≈_
<-resp-≈ eq (respʳ , respˡ) =
<-respʳ-≈ sym trans respʳ , <-respˡ-≈ trans respˡ
where open IsEquivalence eq
<-trichotomous : Symmetric _≈_ → Decidable _≈_ →
Antisymmetric _≈_ _≤_ → Total _≤_ →
Trichotomous _≈_ _<_
<-trichotomous ≈-sym _≟_ antisym total x y with x ≟ y
... | yes x≈y = tri≈ (<-irrefl x≈y) x≈y (<-irrefl (≈-sym x≈y))
... | no x≉y with total x y
... | inj₁ x≤y = tri< (x≤y , x≉y) x≉y (x≉y ∘ antisym x≤y ∘ proj₁)
... | inj₂ y≤x = tri> (x≉y ∘ flip antisym y≤x ∘ proj₁) x≉y (y≤x , x≉y ∘ ≈-sym)
<-decidable : Decidable _≈_ → Decidable _≤_ → Decidable _<_
<-decidable _≟_ _≤?_ x y = x ≤? y ×-dec ¬? (x ≟ y)
<-isStrictPartialOrder : IsPartialOrder _≈_ _≤_ →
IsStrictPartialOrder _≈_ _<_
<-isStrictPartialOrder po = record
{ isEquivalence = isEquivalence
; irrefl = <-irrefl
; trans = <-trans po
; <-resp-≈ = <-resp-≈ isEquivalence ≤-resp-≈
} where open IsPartialOrder po
<-isDecStrictPartialOrder : IsDecPartialOrder _≈_ _≤_ →
IsDecStrictPartialOrder _≈_ _<_
<-isDecStrictPartialOrder dpo = record
{ isStrictPartialOrder = <-isStrictPartialOrder isPartialOrder
; _≟_ = _≟_
; _<?_ = <-decidable _≟_ _≤?_
} where open IsDecPartialOrder dpo
<-isStrictTotalOrder₁ : Decidable _≈_ → IsTotalOrder _≈_ _≤_ →
IsStrictTotalOrder _≈_ _<_
<-isStrictTotalOrder₁ ≟ tot = record
{ isStrictPartialOrder = <-isStrictPartialOrder isPartialOrder
; compare = <-trichotomous Eq.sym ≟ antisym total
} where open IsTotalOrder tot
<-isStrictTotalOrder₂ : IsDecTotalOrder _≈_ _≤_ →
IsStrictTotalOrder _≈_ _<_
<-isStrictTotalOrder₂ dtot = <-isStrictTotalOrder₁ _≟_ isTotalOrder
where open IsDecTotalOrder dtot