```------------------------------------------------------------------------
-- The Agda standard library
--
-- Syntax for the building blocks of equational reasoning modules
------------------------------------------------------------------------

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

open import Level using (Level; _⊔_; suc)
open import Relation.Nullary.Decidable.Core
using (Dec; True; toWitness)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary.Core using (Rel; REL; _⇒_)
open import Relation.Binary.Definitions
open import Relation.Binary.PropositionalEquality.Core as P
using (_≡_)

-- List of `Reasoning` modules that do not use this framework and so
-- need to be updated manually if the syntax changes.
--
--   Data/Vec/Relation/Binary/Equality/Cast
--   Relation/Binary/HeterogeneousEquality
--   Effect/Monad/Partiality
--   Effect/Monad/Partiality/All
--   Codata/Guarded/Stream/Relation/Binary/Pointwise
--   Function/Reasoning

module Relation.Binary.Reasoning.Syntax where

private
variable
a ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level
A B C : Set a
x y z : A

------------------------------------------------------------------------
-- Syntax for beginning a reasoning chain
------------------------------------------------------------------------

------------------------------------------------------------------------
-- Basic begin syntax

module begin-syntax
(R : REL A B ℓ₁)
{S : REL A B ℓ₂}
(reflexive : R ⇒ S)
where

infix 1 begin_

begin_ : R x y → S x y
begin_ = reflexive

------------------------------------------------------------------------
-- Begin subrelation syntax

-- Sometimes we want to support sub-relations with the
-- same reasoning operators as the main relations (e.g. perform equality
-- proofs with non-strict reasoning operators). This record bundles all
-- the parts needed to extract the sub-relation proofs.
record SubRelation {A : Set a} (R : Rel A ℓ₁) ℓ₂ ℓ₃ : Set (a ⊔ ℓ₁ ⊔ suc ℓ₂ ⊔ suc ℓ₃) where
field
S : Rel A ℓ₂
IsS : R x y → Set ℓ₃
IsS? : ∀ (xRy : R x y) → Dec (IsS xRy)
extract : ∀ {xRy : R x y} → IsS xRy → S x y

module begin-subrelation-syntax
(R : Rel A ℓ₁)
(sub : SubRelation R ℓ₂ ℓ₃)
where
open SubRelation sub

infix 1 begin_

begin_ : ∀ {x y} (xRy : R x y) → {s : True (IsS? xRy)} → S x y
begin_ r {s} = extract (toWitness s)

-- Begin equality syntax
module begin-equality-syntax
(R : Rel A ℓ₁)
(sub : SubRelation R ℓ₂ ℓ₃) where

open begin-subrelation-syntax R sub public
renaming (begin_ to begin-equality_)

-- Begin apartness syntax
module begin-apartness-syntax
(R : Rel A ℓ₁)
(sub : SubRelation R ℓ₂ ℓ₃) where

open begin-subrelation-syntax R sub public
renaming (begin_ to begin-apartness_)

-- Begin strict syntax
module begin-strict-syntax
(R : Rel A ℓ₁)
(sub : SubRelation R ℓ₂ ℓ₃) where

open begin-subrelation-syntax R sub public
renaming (begin_ to begin-strict_)

------------------------------------------------------------------------
-- Begin membership syntax

module begin-membership-syntax
(R : Rel A ℓ₁)
(_∈_ : REL B A ℓ₂)
(resp : _∈_ Respectsʳ R) where

infix  1 step-∈

step-∈ : ∀ (x : B) {xs ys} → R xs ys → x ∈ xs → x ∈ ys
step-∈ x = resp

syntax step-∈ x  xs⊆ys x∈xs  = x ∈⟨ x∈xs ⟩ xs⊆ys

------------------------------------------------------------------------
-- Begin contradiction syntax

-- Used with asymmetric subrelations to derive a contradiction from a
-- proof that an element is related to itself.
module begin-contradiction-syntax
(R : Rel A ℓ₁)
(sub : SubRelation R ℓ₂ ℓ₃)
(asym : Asymmetric (SubRelation.S sub))
where

open SubRelation sub

infix 1 begin-contradiction_

begin-contradiction_ : ∀ (xRx : R x x) {s : True (IsS? xRx)} →
∀ {b} {B : Set b} → B
begin-contradiction_ {x} r {s} = contradiction x<x (asym x<x)
where
x<x : S x x
x<x = extract (toWitness s)

------------------------------------------------------------------------
-- Syntax for continuing a chain of reasoning steps
------------------------------------------------------------------------

-- 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.

------------------------------------------------------------------------
-- Syntax for unidirectional relations

-- See https://github.com/agda/agda-stdlib/issues/2150 for a possible
-- simplification.

module _
{R : REL A B ℓ₂}
(S : REL B C ℓ₁)
(T : REL A C ℓ₃)
(step : Trans R S T)
where

forward : ∀ (x : A) {y z} → S y z → R x y → T x z
forward x yRz x∼y = step {x} x∼y yRz

-- Arbitrary relation syntax
module ∼-syntax where
infixr 2 step-∼
step-∼ = forward
syntax step-∼ x yRz x∼y = x ∼⟨ x∼y ⟩ yRz

-- Preorder syntax
module ≲-syntax where
infixr 2 step-≲
step-≲ = forward
syntax step-≲ x yRz x≲y = x ≲⟨ x≲y ⟩ yRz

-- Partial order syntax
module ≤-syntax where
infixr 2 step-≤
step-≤ = forward
syntax step-≤ x yRz x≤y = x ≤⟨ x≤y ⟩ yRz

-- Strict partial order syntax
module <-syntax where
infixr 2 step-<
step-< = forward
syntax step-< x yRz x<y = x <⟨ x<y ⟩ yRz

-- Subset order syntax
module ⊆-syntax where
infixr 2 step-⊆
step-⊆ = forward
syntax step-⊆ x yRz x⊆y = x ⊆⟨ x⊆y ⟩ yRz

-- Strict subset order syntax
module ⊂-syntax where
infixr 2 step-⊂
step-⊂ = forward
syntax step-⊂ x yRz x⊂y = x ⊂⟨ x⊂y ⟩ yRz

-- Square subset order syntax
module ⊑-syntax where
infixr 2 step-⊑
step-⊑ = forward
syntax step-⊑ x yRz x⊑y = x ⊑⟨ x⊑y ⟩ yRz

-- Strict square subset order syntax
module ⊏-syntax where
infixr 2 step-⊏
step-⊏ = forward
syntax step-⊏ x yRz x⊏y = x ⊏⟨ x⊏y ⟩ yRz

-- Divisibility syntax
module ∣-syntax where
infixr 2 step-∣
step-∣ = forward
syntax step-∣ x yRz x∣y = x ∣⟨ x∣y ⟩ yRz

-- Single-step syntax
module ⟶-syntax where
infixr 2 step-⟶
step-⟶ = forward
syntax step-⟶ x yRz x∣y = x ⟶⟨ x∣y ⟩ yRz

-- Multi-step syntax
module ⟶*-syntax where
infixr 2 step-⟶*
step-⟶* = forward
syntax step-⟶* x yRz x∣y = x ⟶*⟨ x∣y ⟩ yRz

------------------------------------------------------------------------
-- Syntax for bidirectional relations

module _
{U : REL B A ℓ₄}
(sym : Sym U R)
where

backward : ∀ x {y z} → S y z → U y x → T x z
backward x yRz x≈y = forward x yRz (sym x≈y)

-- Setoid equality syntax
module ≈-syntax where
infixr 2 step-≈-⟩ step-≈-⟨
step-≈-⟩ = forward
step-≈-⟨ = backward
syntax step-≈-⟩ x yRz x≈y = x ≈⟨ x≈y ⟩ yRz
syntax step-≈-⟨ x yRz y≈x = x ≈⟨ y≈x ⟨ yRz

-- Deprecated
infixr 2 step-≈ step-≈˘
step-≈ = step-≈-⟩
{-# WARNING_ON_USAGE step-≈
"Warning: step-≈ was deprecated in v2.0.
Please use step-≈-⟩ instead."
#-}
step-≈˘ = step-≈-⟨
{-# WARNING_ON_USAGE step-≈˘
"Warning: step-≈˘ and _≈˘⟨_⟩_ was deprecated in v2.0.
Please use step-≈-⟨ and _≈⟨_⟨_ instead."
#-}
syntax step-≈˘ x yRz y≈x = x ≈˘⟨ y≈x ⟩ yRz

-- Container equality syntax
module ≋-syntax where
infixr 2 step-≋-⟩ step-≋-⟨
step-≋-⟩ = forward
step-≋-⟨ = backward
syntax step-≋-⟩ x yRz x≋y = x ≋⟨ x≋y ⟩ yRz
syntax step-≋-⟨ x yRz y≋x = x ≋⟨ y≋x ⟨ yRz

-- Don't remove until https://github.com/agda/agda/issues/5617 fixed.
infixr 2 step-≋ step-≋˘
step-≋ = step-≋-⟩
{-# WARNING_ON_USAGE step-≋
"Warning: step-≋ was deprecated in v2.0.
Please use step-≋-⟩ instead."
#-}
step-≋˘ = step-≋-⟨
{-# WARNING_ON_USAGE step-≋˘
"Warning: step-≋˘ and _≋˘⟨_⟩_ was deprecated in v2.0.
Please use step-≋-⟨ and _≋⟨_⟨_ instead."
#-}
syntax step-≋˘ x yRz y≋x = x ≋˘⟨ y≋x ⟩ yRz

-- Other equality syntax
module ≃-syntax where
infixr 2 step-≃-⟩ step-≃-⟨
step-≃-⟩ = forward
step-≃-⟨ = backward
syntax step-≃-⟩ x yRz x≃y = x ≃⟨ x≃y ⟩ yRz
syntax step-≃-⟨ x yRz y≃x = x ≃⟨ y≃x ⟨ yRz

-- Apartness relation syntax
module #-syntax where
infixr 2 step-#-⟩ step-#-⟨
step-#-⟩ = forward
step-#-⟨ = backward
syntax step-#-⟩ x yRz x#y = x #⟨ x#y ⟩ yRz
syntax step-#-⟨ x yRz y#x = x #⟨ y#x ⟨ yRz

-- Don't remove until https://github.com/agda/agda/issues/5617 fixed.
infixr 2 step-# step-#˘
step-# = step-#-⟩
{-# WARNING_ON_USAGE step-#
"Warning: step-# was deprecated in v2.0.
Please use step-#-⟩ instead."
#-}
step-#˘ = step-#-⟨
{-# WARNING_ON_USAGE step-#˘
"Warning: step-#˘ and _#˘⟨_⟩_ was deprecated in v2.0.
Please use step-#-⟨ and _#⟨_⟨_ instead."
#-}
syntax step-#˘ x yRz y#x = x #˘⟨ y#x ⟩ yRz

-- Bijection syntax
module ⤖-syntax where
infixr 2 step-⤖ step-⬻
step-⤖ = forward
step-⬻ = backward
syntax step-⤖ x yRz x⤖y = x ⤖⟨ x⤖y ⟩ yRz
syntax step-⬻ x yRz y⤖x = x ⬻⟨ y⤖x ⟩ yRz

-- Inverse syntax
module ↔-syntax where
infixr 2 step-↔-⟩ step-↔-⟨
step-↔-⟩ = forward
step-↔-⟨ = backward
syntax step-↔-⟩ x yRz x↔y = x ↔⟨ x↔y ⟩ yRz
syntax step-↔-⟨ x yRz y↔x = x ↔⟨ y↔x ⟨ yRz

-- Inverse syntax
module ↭-syntax where
infixr 2 step-↭-⟩ step-↭-⟨
step-↭-⟩ = forward
step-↭-⟨ = backward
syntax step-↭-⟩ x yRz x↭y = x ↭⟨ x↭y ⟩ yRz
syntax step-↭-⟨ x yRz y↭x = x ↭⟨ y↭x ⟨ yRz

-- Don't remove until https://github.com/agda/agda/issues/5617 fixed.
infixr 2 step-↭ step-↭˘
step-↭ = forward
{-# WARNING_ON_USAGE step-↭
"Warning: step-↭ was deprecated in v2.0.
Please use step-↭-⟩ instead."
#-}
step-↭˘ = backward
{-# WARNING_ON_USAGE step-↭˘
"Warning: step-↭˘ and _↭˘⟨_⟩_ was deprecated in v2.0.
Please use step-↭-⟨ and _↭⟨_⟨_ instead."
#-}
syntax step-↭˘ x yRz y↭x = x ↭˘⟨ y↭x ⟩ yRz

------------------------------------------------------------------------
-- Propositional equality

-- Crucially often the step function cannot just be `subst` or pattern
-- match on `refl` as we often want to compute which constructor the
-- relation begins with, in order for the implicit subrelation
-- arguments to resolve. See `≡-noncomputable-syntax` below if this
-- is not required.
module ≡-syntax
(R : REL A B ℓ₁)
(step : Trans _≡_ R R)
where

infixr 2 step-≡-⟩  step-≡-∣ step-≡-⟨
step-≡-⟩ = forward R R step

step-≡-∣ : ∀ x {y} → R x y → R x y
step-≡-∣ x xRy = xRy

step-≡-⟨ = backward R R step P.sym

syntax step-≡-⟩ x yRz x≡y = x ≡⟨ x≡y ⟩ yRz
syntax step-≡-∣ x xRy     = x ≡⟨⟩ xRy
syntax step-≡-⟨ x yRz y≡x = x ≡⟨ y≡x ⟨ yRz

-- Don't remove until https://github.com/agda/agda/issues/5617 fixed.
infixr 2 step-≡ step-≡˘
step-≡ = step-≡-⟩
{-# WARNING_ON_USAGE step-≡
"Warning: step-≡ was deprecated in v2.0.
Please use step-≡-⟩ instead."
#-}
step-≡˘ = step-≡-⟨
{-# WARNING_ON_USAGE step-≡˘
"Warning: step-≡˘ and _≡˘⟨_⟩_ was deprecated in v2.0.
Please use step-≡-⟨ and _≡⟨_⟨_ instead."
#-}
syntax step-≡˘ x yRz y≡x = x ≡˘⟨ y≡x ⟩ yRz

-- Unlike ≡-syntax above, chains of reasoning using this syntax will not
-- reduce when proofs of propositional equality which are not definitionally
-- equal to `refl` are passed.
module ≡-noncomputing-syntax (R : REL A B ℓ₁) where

private
step : Trans _≡_ R R
step P.refl xRy = xRy

open ≡-syntax R step public

------------------------------------------------------------------------
-- Syntax for ending a chain of reasoning
------------------------------------------------------------------------

module end-syntax
(R : Rel A ℓ₁)
(reflexive : Reflexive R)
where

infix 3 _∎

_∎ : ∀ x → R x x
x ∎ = reflexive

```