------------------------------------------------------------------------
-- 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.Core using (contradiction)
open import Relation.Binary.Core using (Rel; REL; _⇒_)
open import Relation.Binary.Definitions
  using (_Respectsʳ_; Asymmetric; Trans; Sym; Reflexive)
open import Relation.Binary.PropositionalEquality.Core as ≡
  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  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  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   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  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  step-∼
    step-∼ = forward
    syntax step-∼ x yRz x∼y = x ∼⟨ x∼y ⟩ yRz


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


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


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


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


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


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


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


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


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


  -- Multi-step syntax
  module ⟶*-syntax where
    infixr  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  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  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  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  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  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  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  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  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  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  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  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  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 ≡.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  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 ≡.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  _∎

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