------------------------------------------------------------------------
-- The Agda standard library
--
-- Convenient syntax for "equational reasoning" in multiple Setoids.
------------------------------------------------------------------------

-- Example use:
--
--   open import Data.Maybe.Properties
--   open import Data.Maybe.Relation.Binary.Equality
--   open import Relation.Binary.Reasoning.MultiSetoid
--
--   begin⟨ S ⟩
--     x ≈⟨ drop-just (begin⟨ setoid S ⟩
--          just x ≈⟨ justx≈mz ⟩
--          mz     ≈⟨ mz≈justy ⟩
--          just y ∎)⟩
--     y ≈⟨ y≈z ⟩
--     z ∎

-- Note this module is not reimplemented in terms of `Reasoning.Setoid`
-- as this introduces unsolved metas as the underlying base module
-- `Base.Single` does not require `_≈_` be symmetric.

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

module Relation.Binary.Reasoning.MultiSetoid where

open import Function.Base using (flip)
open import Level using (_⊔_)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)

import Relation.Binary.Reasoning.Setoid as EqR

------------------------------------------------------------------------
-- Combinators that take the current setoid as an explicit argument.

module _ {c ℓ} (S : Setoid c ℓ) where
  open Setoid S

  data IsRelatedTo (x y : _) : Set (c ⊔ ℓ) where
    relTo : (x∼y : x ≈ y) → IsRelatedTo x y

  infix 1 begin⟨_⟩_

  begin⟨_⟩_ : ∀ {x y} → IsRelatedTo x y → x ≈ y
  begin⟨_⟩_ (relTo eq) = eq

------------------------------------------------------------------------
-- Combinators that take the current setoid as an implicit argument.

module _ {c ℓ} {S : Setoid c ℓ} where

  open Setoid S renaming (_≈_ to _≈_)

  infixr 2 step-≈ step-≈˘ step-≡ step-≡˘ _≡⟨⟩_
  infix 3 _∎

  step-≈ : ∀ x {y z} → IsRelatedTo S y z → x ≈ y → IsRelatedTo S x z
  step-≈ x (relTo y∼z) x∼y = relTo (trans x∼y y∼z)

  step-≈˘ : ∀ x {y z} → IsRelatedTo S y z → y ≈ x → IsRelatedTo S x z
  step-≈˘ x y∼z x≈y = step-≈ x y∼z (sym x≈y)

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

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

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

  _∎ : ∀ x → IsRelatedTo S x x
  _∎ _ = relTo refl

  syntax step-≈  x y∼z x≈y = x ≈⟨  x≈y ⟩ y∼z
  syntax step-≈˘ x y∼z y≈x = x ≈˘⟨ y≈x ⟩ 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