------------------------------------------------------------------------
-- Conversion of ≤ to <, along with a number of properties
------------------------------------------------------------------------

{-# OPTIONS --universe-polymorphism #-}

-- Possible TODO: Prove that a conversion ≤ → < → ≤ returns a
-- relation equivalent to the original one (and similarly for
-- < → ≤ → <).

open import Relation.Binary

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

open import Relation.Nullary
open import Relation.Binary.Consequences
open import Function
open import Data.Product
open import Data.Sum

------------------------------------------------------------------------
-- Conversion

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

_<_ : Rel A _
x < y = (x  y) × ¬ (x  y)

------------------------------------------------------------------------
-- The converted relations have certain properties
-- (if the original relations have certain other properties)

irrefl : Irreflexive _≈_ _<_
irrefl x≈y x<y = proj₂ x<y x≈y

trans : IsPartialOrder _≈_ _≤_  Transitive _<_
trans po = λ x<y y<z 
  ( PO.trans (proj₁ x<y) (proj₁ y<z)
  , λ x≈z  proj₂ x<y $ lemma (proj₁ x<y) (proj₁ y<z) x≈z
  )
  where
  module PO = IsPartialOrder po

  lemma :  {x y z}  x  y  y  z  x  z  x  y
  lemma x≤y y≤z x≈z =
    PO.antisym x≤y $ PO.trans y≤z (PO.reflexive $ PO.Eq.sym x≈z)

antisym⟶asym : Antisymmetric _≈_ _≤_  Asymmetric _<_
antisym⟶asym antisym (x≤y , ¬x≈y) (y≤x , ¬y≈x) =
  ¬x≈y (antisym x≤y y≤x)

<-resp-≈ : IsEquivalence _≈_  _≤_ Respects₂ _≈_  _<_ Respects₂ _≈_
<-resp-≈ eq ≤-resp-≈ =
   {x y' y} y'≈y x<y' 
    ( proj₁ ≤-resp-≈ y'≈y (proj₁ x<y')
    , λ x≈y  proj₂ x<y' (Eq.trans x≈y (Eq.sym y'≈y))
    )
  ) ,
   {y x' x} x'≈x x'<y 
    ( proj₂ ≤-resp-≈ x'≈x (proj₁ x'<y)
    , λ x≈y  proj₂ x'<y (Eq.trans x'≈x x≈y)
    ))
  where module Eq = IsEquivalence eq

trichotomous : Symmetric _≈_  Decidable _≈_ 
               Antisymmetric _≈_ _≤_  Total _≤_ 
               Trichotomous _≈_ _<_
trichotomous ≈-sym ≈-dec antisym total x y with ≈-dec 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₂ x≥y = tri> (x≉y  flip antisym x≥y  proj₁) x≉y
                        (x≥y , x≉y  ≈-sym)

decidable : Decidable _≈_  Decidable _≤_  Decidable _<_
decidable ≈-dec ≤-dec x y with ≈-dec x y | ≤-dec x y
... | yes x≈y | _       = no (flip proj₂ x≈y)
... | no  x≉y | yes x≤y = yes (x≤y , x≉y)
... | no  x≉y | no  x≰y = no (x≰y  proj₁)

isPartialOrder⟶isStrictPartialOrder :
  IsPartialOrder _≈_ _≤_  IsStrictPartialOrder _≈_ _<_
isPartialOrder⟶isStrictPartialOrder po = record
  { isEquivalence = PO.isEquivalence
  ; irrefl        = irrefl
  ; trans         = trans po
  ; <-resp-≈      = <-resp-≈ PO.isEquivalence PO.≤-resp-≈
  } where module PO = IsPartialOrder po

isTotalOrder⟶isStrictTotalOrder :
  Decidable _≈_  IsTotalOrder _≈_ _≤_  IsStrictTotalOrder _≈_ _<_
isTotalOrder⟶isStrictTotalOrder dec-≈ tot = record
  { isEquivalence = TO.isEquivalence
  ; trans         = trans TO.isPartialOrder
  ; compare       = trichotomous TO.Eq.sym dec-≈ TO.antisym TO.total
  ; <-resp-≈      = <-resp-≈ TO.isEquivalence TO.≤-resp-≈
  } where module TO = IsTotalOrder tot

isDecTotalOrder⟶isStrictTotalOrder :
  IsDecTotalOrder _≈_ _≤_  IsStrictTotalOrder _≈_ _<_
isDecTotalOrder⟶isStrictTotalOrder dtot =
  isTotalOrder⟶isStrictTotalOrder DTO._≟_ DTO.isTotalOrder
  where module DTO = IsDecTotalOrder dtot