------------------------------------------------------------------------ -- 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 4 _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