------------------------------------------------------------------------
-- The Agda standard library
--
-- The basic code for equational reasoning with a single relation
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
open import Level using (_⊔_)
open import Function.Base using (case_of_)
open import Relation.Binary.Core using (Rel; _⇒_)
open import Relation.Binary.Definitions using (Reflexive; Transitive; Trans)
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
open import Relation.Binary.Reasoning.Syntax
 
module Relation.Binary.Reasoning.Base.Single
  {a ℓ} {A : Set a} (_∼_ : Rel A ℓ)
  (refl : Reflexive _∼_) (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_ (x y : A) : Set ℓ where
  relTo : (x∼y : x ∼ y) → x IsRelatedTo y
 
start : _IsRelatedTo_ ⇒ _∼_
start (relTo x∼y) = x∼y
 
∼-go : Trans _∼_ _IsRelatedTo_ _IsRelatedTo_
∼-go x∼y (relTo y∼z) = relTo (trans x∼y y∼z)
 
≡-go : Trans _≡_ _IsRelatedTo_ _IsRelatedTo_
≡-go x≡y (relTo y∼z) = relTo (case x≡y of λ where ≡.refl → y∼z)
 
stop : Reflexive _IsRelatedTo_
stop = relTo refl
 
------------------------------------------------------------------------
-- Reasoning combinators
 
open begin-syntax _IsRelatedTo_ start public
open ≡-syntax _IsRelatedTo_ ≡-go public
open ∼-syntax _IsRelatedTo_ _IsRelatedTo_ ∼-go public
open end-syntax _IsRelatedTo_ stop public