------------------------------------------------------------------------
-- 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 Level using (Level; _⊔_)
open import Function.Base using (case_of_)
open import Relation.Binary.Core using (_⇒_)
open import Relation.Binary.Definitions using (Trans; Reflexive)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
open import Relation.Binary.Reasoning.Syntax

private
  variable
    a ℓ : Level

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

module _ (S : Setoid a ℓ) where
  open Setoid S

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

  start : IsRelatedTo ⇒ _≈_
  start (relTo x≈y) = x≈y

  ≡-go : Trans _≡_ IsRelatedTo IsRelatedTo
  ≡-go x≡y (relTo y∼z) = relTo (case x≡y of λ where P.refl → y∼z)

  ≈-go : Trans _≈_ IsRelatedTo IsRelatedTo
  ≈-go x≈y (relTo y≈z) = relTo (trans x≈y y≈z)

  end : Reflexive IsRelatedTo
  end = relTo refl

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

-- Those that take the current setoid as an explicit argument.
  open begin-syntax IsRelatedTo start public
    renaming (begin_ to begin⟨_⟩_)


-- Those that take the current setoid as an implicit argument.
module _ {S : Setoid a ℓ} where
  open Setoid S

  open ≡-syntax (IsRelatedTo S) (≡-go S)
  open ≈-syntax (IsRelatedTo S) (IsRelatedTo S) (≈-go S) sym public
  open end-syntax (IsRelatedTo S) (end S) public