------------------------------------------------------------------------
-- The Agda standard library
--
-- Some properties of reflexive closures
------------------------------------------------------------------------
 
{-# OPTIONS --safe --cubical-compatible #-}
 
module Relation.Binary.Construct.Closure.Reflexive.Properties where
 
open import Data.Product.Base as Product
open import Data.Sum.Base as Sum
open import Function.Bundles using (_⇔_; mk⇔)
open import Function.Base using (id)
open import Level
open import Relation.Binary.Core using (Rel; REL; _=[_]⇒_)
open import Relation.Binary.Structures
  using (IsPreorder; IsStrictPartialOrder; IsPartialOrder; IsDecStrictPartialOrder; IsDecPartialOrder; IsStrictTotalOrder; IsTotalOrder; IsDecTotalOrder)
open import Relation.Binary.Definitions
  using (Symmetric; Transitive; Reflexive; Asymmetric; Antisymmetric; Trichotomous; Total; Decidable; DecidableEquality; tri<; tri≈; tri>; _Respectsˡ_; _Respectsʳ_; _Respects_; _Respects₂_)
open import Relation.Binary.Construct.Closure.Reflexive
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
import Relation.Binary.PropositionalEquality.Properties as ≡
open import Relation.Nullary.Negation.Core using (contradiction)
open import Relation.Nullary.Decidable as Dec using (yes; no)
open import Relation.Unary using (Pred)
 
private
  variable
    a b ℓ p q : Level
    A : Set a
    B : Set b
 
------------------------------------------------------------------------
-- Relational properties
 
module _ {P : Rel A p} {Q : Rel B q} where
 
  =[]⇒ : ∀ {f : A → B} → P =[ f ]⇒ Q → ReflClosure P =[ f ]⇒ ReflClosure Q
  =[]⇒ x [ x∼y ] = [ x x∼y ]
  =[]⇒ x refl    = refl
 
module _ {_~_ : Rel A ℓ} where
 
  private
    _~ᵒ_ = ReflClosure _~_
 
  fromSum : ∀ {x y} → x ≡ y ⊎ x ~ y → x ~ᵒ y
  fromSum (inj₁ refl) = refl
  fromSum (inj₂ y) = [ y ]
 
  toSum : ∀ {x y} → x ~ᵒ y → x ≡ y ⊎ x ~ y
  toSum [ x∼y ] = inj₂ x∼y
  toSum refl = inj₁ refl
 
  ⊎⇔Refl : ∀ {a b} → (a ≡ b ⊎ a ~ b) ⇔ a ~ᵒ b
  ⊎⇔Refl = mk⇔ fromSum toSum
 
  sym : Symmetric _~_ → Symmetric _~ᵒ_
  sym ~-sym [ x∼y ] = [ ~-sym x∼y ]
  sym ~-sym refl    = refl
 
  trans : Transitive _~_ → Transitive _~ᵒ_
  trans ~-trans [ x∼y ] [ x∼y₁ ] = [ ~-trans x∼y x∼y₁ ]
  trans ~-trans [ x∼y ] refl     = [ x∼y ]
  trans ~-trans refl    [ x∼y ]  = [ x∼y ]
  trans ~-trans refl    refl     = refl
 
  antisym : (_≈_ : Rel A p) → Reflexive _≈_ →
            Asymmetric _~_ → Antisymmetric _≈_ _~ᵒ_
  antisym _≈_ ref asym [ x∼y ] [ y∼x ] = contradiction x∼y (asym y∼x)
  antisym _≈_ ref asym [ x∼y ] refl    = ref
  antisym _≈_ ref asym refl    _       = ref
 
  total : Trichotomous _≡_ _~_ → Total _~ᵒ_
  total compare x y with compare x y
  ... | tri< a _    _ = inj₁ [ a ]
  ... | tri≈ _ refl _ = inj₁ refl
  ... | tri> _ _    c = inj₂ [ c ]
 
  dec : DecidableEquality A → Decidable _~_ → Decidable _~ᵒ_
  dec ≡-dec ~-dec a b = Dec.map ⊎⇔Refl (≡-dec a b Dec.⊎-dec ~-dec a b)
 
  decidable : Trichotomous _≡_ _~_ → Decidable _~ᵒ_
  decidable ~-tri a b with ~-tri a b
  ... | tri< a~b  _  _ = yes [ a~b ]
  ... | tri≈ _  refl _ = yes refl
  ... | tri> ¬a ¬b   _ = no λ { refl → ¬b refl ; [ p ] → ¬a p }
 
  respˡ : ∀ {P : REL A B p} → P Respectsˡ _~_ → P Respectsˡ _~ᵒ_
  respˡ p-respˡ-~ [ x∼y ] = p-respˡ-~ x∼y
  respˡ _         refl    = id
 
  respʳ : ∀ {P : REL B A p} → P Respectsʳ _~_ → P Respectsʳ _~ᵒ_
  respʳ = respˡ
 
module _ {_~_ : Rel A ℓ} {P : Pred A p} where
 
  resp : P Respects _~_ → P Respects (ReflClosure _~_)
  resp p-resp-~ [ x∼y ] = p-resp-~ x∼y
  resp _        refl    = id
 
module _ {_~_ : Rel A ℓ} {P : Rel A p} where
 
  resp₂ : P Respects₂ _~_ → P Respects₂ (ReflClosure _~_)
  resp₂ = Product.map respˡ respʳ
 
------------------------------------------------------------------------
-- Structures
 
module _ {_~_ : Rel A ℓ} where
 
  private
    _~ᵒ_ = ReflClosure _~_
 
  isPreorder : Transitive _~_ → IsPreorder _≡_ _~ᵒ_
  isPreorder ~-trans = record
    { isEquivalence = ≡.isEquivalence
    ; reflexive     = λ { refl → refl }
    ; trans         = trans ~-trans
    }
 
  isPartialOrder : IsStrictPartialOrder _≡_ _~_ → IsPartialOrder _≡_ _~ᵒ_
  isPartialOrder O = record
    { isPreorder = isPreorder O.trans
    ; antisym    = antisym _≡_ refl O.asym
    } where module O = IsStrictPartialOrder O
 
  isDecPartialOrder : IsDecStrictPartialOrder _≡_ _~_ → IsDecPartialOrder _≡_ _~ᵒ_
  isDecPartialOrder O = record
    { isPartialOrder = isPartialOrder O.isStrictPartialOrder
    ; _≟_            = O._≟_
    ; _≤?_           = dec O._≟_ O._<?_
    } where module O = IsDecStrictPartialOrder O
 
  isTotalOrder : IsStrictTotalOrder _≡_ _~_ → IsTotalOrder _≡_ _~ᵒ_
  isTotalOrder O = record
    { isPartialOrder = isPartialOrder isStrictPartialOrder
    ; total          = total compare
    } where open IsStrictTotalOrder O
 
  isDecTotalOrder : IsStrictTotalOrder _≡_ _~_ → IsDecTotalOrder _≡_ _~ᵒ_
  isDecTotalOrder O = record
    { isTotalOrder = isTotalOrder O
    ; _≟_          = _≟_
    ; _≤?_         = dec _≟_ _<?_
    } where open IsStrictTotalOrder O