------------------------------------------------------------------------
-- The Agda standard library
--
-- The basic code for equational reasoning with a non-reflexive relation
------------------------------------------------------------------------

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

open import Function using (case_of_)
open import Level using (_⊔_)
open import Relation.Binary.Core
open import Relation.Binary.Definitions
open import Relation.Nullary.Decidable using (Dec; yes; no)
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
open import Relation.Binary.Reasoning.Syntax


module Relation.Binary.Reasoning.Base.Partial
  {a } {A : Set a} (_∼_ : Rel A ) (trans : Transitive _∼_)
  where

------------------------------------------------------------------------
-- Definition of "related to"

-- This seemingly unnecessary type is used to make it possible to
-- infer arguments even if the underlying equality evaluates.

infix  4 _IsRelatedTo_

data _IsRelatedTo_ : A  A  Set (a  ) where
  singleStep :  x  x IsRelatedTo x
  multiStep  :  {x y} (x∼y : x  y)  x IsRelatedTo y

∼-go : Trans _∼_ _IsRelatedTo_ _IsRelatedTo_
∼-go x∼y (singleStep y) = multiStep x∼y
∼-go x∼y (multiStep y∼z) = multiStep (trans x∼y y∼z)

stop : Reflexive _IsRelatedTo_
stop = singleStep _

------------------------------------------------------------------------
-- Types that are used to ensure that the final relation proved by the
-- chain of reasoning can be converted into the required relation.

data IsMultiStep {x y} : x IsRelatedTo y  Set (a  ) where
  isMultiStep :  x∼y  IsMultiStep (multiStep x∼y)

IsMultiStep? :  {x y} (x∼y : x IsRelatedTo y)  Dec (IsMultiStep x∼y)
IsMultiStep? (multiStep x<y) = yes (isMultiStep x<y)
IsMultiStep? (singleStep _)  = no λ()

extractMultiStep :  {x y} {x∼y : x IsRelatedTo y}  IsMultiStep x∼y  x  y
extractMultiStep (isMultiStep x≈y) = x≈y

multiStepSubRelation : SubRelation _IsRelatedTo_ _ _
multiStepSubRelation = record
  { IsS = IsMultiStep
  ; IsS? = IsMultiStep?
  ; extract = extractMultiStep
  }

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

open begin-subrelation-syntax _IsRelatedTo_ multiStepSubRelation public
open ≡-noncomputing-syntax _IsRelatedTo_ 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 1.6

infix  3 _∎⟨_⟩

_∎⟨_⟩ :  x  x  x  x IsRelatedTo x
_ ∎⟨ x∼x  = multiStep x∼x
{-# WARNING_ON_USAGE _∎⟨_⟩
"Warning: _∎⟨_⟩ was deprecated in v1.6.
Please use _∎ instead if used in a chain, otherwise simply provide
the proof of reflexivity directly without using these combinators."
#-}