------------------------------------------------------------------------
-- The Agda standard library
--
-- The basic code for equational reasoning with two relations:
-- equality and some other ordering.
------------------------------------------------------------------------
--
-- See `Data.Nat.Properties` or `Relation.Binary.Reasoning.PartialOrder`
-- for examples of how to instantiate this module.

{-# OPTIONS --cubical-compatible --safe #-}

open import Level using (_⊔_)
open import Function.Base using (case_of_)
open import Relation.Nullary.Decidable.Core using (Dec; yes; no)
open import Relation.Binary.Core using (Rel; _⇒_)
open import Relation.Binary.Definitions using (Reflexive; Trans)
open import Relation.Binary.Structures using (IsPreorder)
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
open import Relation.Binary.Reasoning.Syntax


module Relation.Binary.Reasoning.Base.Double {a ℓ₁ ℓ₂} {A : Set a}
  {_≈_ : Rel A ℓ₁} {_≲_ : Rel A ℓ₂} (isPreorder : IsPreorder _≈_ _≲_)
  where

open IsPreorder isPreorder

------------------------------------------------------------------------
-- A datatype to hide the current relation type

infix  _IsRelatedTo_

data _IsRelatedTo_ (x y : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  nonstrict : (x≲y : x ≲ y) → x IsRelatedTo y
  equals    : (x≈y : x ≈ y) → x IsRelatedTo y

start : _IsRelatedTo_ ⇒ _≲_
start (equals x≈y) = reflexive x≈y
start (nonstrict x≲y) = x≲y

≡-go : Trans _≡_ _IsRelatedTo_ _IsRelatedTo_
≡-go x≡y (equals y≈z) = equals (case x≡y of λ where ≡.refl → y≈z)
≡-go x≡y (nonstrict y≤z) = nonstrict (case x≡y of λ where ≡.refl → y≤z)

≲-go : Trans _≲_ _IsRelatedTo_ _IsRelatedTo_
≲-go x≲y (equals y≈z) = nonstrict (∼-respʳ-≈ y≈z x≲y)
≲-go x≲y (nonstrict y≲z) = nonstrict (trans x≲y y≲z)

≈-go : Trans _≈_ _IsRelatedTo_ _IsRelatedTo_
≈-go x≈y (equals y≈z) = equals (Eq.trans x≈y y≈z)
≈-go x≈y (nonstrict y≲z) = nonstrict (∼-respˡ-≈ (Eq.sym x≈y) y≲z)

stop : Reflexive _IsRelatedTo_
stop = equals Eq.refl

------------------------------------------------------------------------
-- A record that is used to ensure that the final relation proved by the
-- chain of reasoning can be converted into the required relation.

data IsEquality {x y} : x IsRelatedTo y → Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  isEquality : ∀ x≈y → IsEquality (equals x≈y)

IsEquality? : ∀ {x y} (x≲y : x IsRelatedTo y) → Dec (IsEquality x≲y)
IsEquality? (nonstrict _) = no λ()
IsEquality? (equals x≈y)  = yes (isEquality x≈y)

extractEquality : ∀ {x y} {x≲y : x IsRelatedTo y} → IsEquality x≲y → x ≈ y
extractEquality (isEquality x≈y) = x≈y

equalitySubRelation : SubRelation  _IsRelatedTo_ _ _
equalitySubRelation = record
  { IsS = IsEquality
  ; IsS? = IsEquality?
  ; extract = extractEquality
  }

------------------------------------------------------------------------
-- Reasoning combinators

open begin-syntax  _IsRelatedTo_ start public
open begin-equality-syntax  _IsRelatedTo_ equalitySubRelation public
open ≡-syntax _IsRelatedTo_ ≡-go public
open ≈-syntax _IsRelatedTo_ _IsRelatedTo_ ≈-go Eq.sym public
open ≲-syntax _IsRelatedTo_ _IsRelatedTo_ ≲-go public
open end-syntax _IsRelatedTo_ stop public


------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 2.0

open ∼-syntax _IsRelatedTo_ _IsRelatedTo_ ≲-go public
{-# WARNING_ON_USAGE step-∼
"Warning: step-∼ and _∼⟨_⟩_ syntax was deprecated in v2.0.
Please use step-≲ and _≲⟨_⟩_ instead. "
#-}