------------------------------------------------------------------------
-- The Agda standard library
--
-- Conversion of _≤_ to _<_
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

open import Relation.Binary

module Relation.Binary.Construct.NonStrictToStrict
  {a ℓ₁ ℓ₂} {A : Set a} (_≈_ : Rel A ℓ₁) (_≤_ : Rel A ℓ₂) where

open import Data.Product 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.Product using (_×-dec_)

private
  _≉_ : Rel A ℓ₁
  x  y = ¬ (x  y)

------------------------------------------------------------------------
-- _≤_ can be turned into _<_ as follows:

infix 4  _<_

_<_ : Rel A _
x < y = x  y × x  y

------------------------------------------------------------------------
-- Relationship between relations

<⇒≤ : _<_  _≤_
<⇒≤ = 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

------------------------------------------------------------------------
-- Relational properties

<-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)

------------------------------------------------------------------------
-- Structures

<-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
  { isEquivalence = isEquivalence
  ; trans         = <-trans isPartialOrder
  ; compare       = <-trichotomous Eq.sym  antisym total
  } where open IsTotalOrder tot

<-isStrictTotalOrder₂ : IsDecTotalOrder _≈_ _≤_ 
                        IsStrictTotalOrder _≈_ _<_
<-isStrictTotalOrder₂ dtot = <-isStrictTotalOrder₁ _≟_ isTotalOrder
  where open IsDecTotalOrder dtot