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

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

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

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   _IsRelatedTo_

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

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

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

-- Note that the arguments to the `step`s are not provided in their
-- "natural" order and syntax declarations are later used to re-order
-- them. This is because the `step` ordering allows the type-checker to
-- better infer the middle argument `y` from the `_IsRelatedTo_`
-- argument (see issue 622).
--
-- This has two practical benefits. First it speeds up type-checking by
-- approximately a factor of 5. Secondly it allows the combinators to be
-- used with macros that use reflection, e.g. `Tactic.RingSolver`, where
-- they need to be able to extract `y` using reflection.

infix   begin_
infixr  step-∼ step-≡ step-≡˘
infixr  _≡⟨⟩_
infix   _∎⟨_⟩ _∎

-- Beginning of a proof

begin_ : ∀ {x y} (x∼y : x IsRelatedTo y) → {True (IsMultiStep? x∼y)} → x ∼ y
begin (multiStep x∼y) = x∼y

-- Standard step with the relation

step-∼ : ∀ x {y z} → y IsRelatedTo z → x ∼ y → x IsRelatedTo z
step-∼ _ (singleStep _) x∼y  = multiStep x∼y
step-∼ _ (multiStep y∼z) x∼y = multiStep (trans x∼y y∼z)

-- Step with a non-trivial propositional equality

step-≡ : ∀ x {y z} → y IsRelatedTo z → x ≡ y → x IsRelatedTo z
step-≡ _ x∼z P.refl = x∼z

-- Step with a flipped non-trivial propositional equality

step-≡˘ : ∀ x {y z} → y IsRelatedTo z → y ≡ x → x IsRelatedTo z
step-≡˘ _ x∼z P.refl = x∼z

-- -- Step with a trivial propositional equality

_≡⟨⟩_ : ∀ x {y} → x IsRelatedTo y → x IsRelatedTo y
_ ≡⟨⟩ x∼y = x∼y

-- Termination

_∎ : ∀ x → x IsRelatedTo x
_∎ = singleStep

-- Syntax declarations

syntax step-∼  x y∼z x∼y = x ∼⟨  x∼y ⟩ y∼z
syntax step-≡  x y≡z x≡y = x ≡⟨  x≡y ⟩ y≡z
syntax step-≡˘ x y≡z y≡x = x ≡˘⟨ y≡x ⟩ y≡z


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

-- Version 1.6

_∎⟨_⟩ : ∀ 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."
#-}