Closed
Description
While trying to fix #2145 and #1138 I've realised quite how much duplication has crept into the many many Reasoning modules we have in the library. Trying to change the syntax is incredibly painful as you have to do it all over the library.
I think a modular approach along the lines of:
module Relation.Binary.Reasoning.Base.Syntax
{a ℓ} {A : Set a} (_R_ : Rel A ℓ) where
------------------------------------------------------------------------
-- Propositional equality syntax
module ≡-step-syntax where
-- Step with a non-trivial propositional equality
step-≡ : ∀ x {y z} → y R z → x ≡ y → x R z
step-≡ _ x∼z refl = x∼z
-- Step with a definition identity
step-≡-refl : ∀ (x : A) {y} → x R y → x R y
step-≡-refl x xRy = xRy
-- Step with a flipped non-trivial propositional equality
step-≡-sym : ∀ x {y z} → y R z → y ≡ x → x R z
step-≡-sym _ x∼z refl = x∼z
infixr 2 step-≡ step-≡-refl step-≡-sym
syntax step-≡-refl x xRy = x ≡⟨⟩ xRy
syntax step-≡-sym x yRz y≡x = x ≡⟨ y≡x ⟨ yRz
syntax step-≡ x yRz x≡y = x ≡⟨ x≡y ⟩ yRz
------------------------------------------------------------------------
-- Setoid equality syntax
module ≈-syntax
{ℓ₂} {_≈_ : Rel A ℓ₂}
(sym : Symmetric _≈_)
(step : Trans _≈_ _R_ _R_)
where
-- Step with the setoid equality
step-≈ : ∀ (x : A) {y z} → y R z → x ≈ y → x R z
step-≈ x yRz x≈y = step {x} x≈y yRz
-- Flipped step with the setoid equality
step-≈-sym : ∀ x {y z} → y R z → y ≈ x → x R z
step-≈-sym x y∼z x≈y = step-≈ x y∼z (sym x≈y)
syntax step-≈ x y∼z x≈y = x ≈⟨ x≈y ⟩ y∼z
syntax step-≈-sym x y∼z y≈x = x ≈⟨ y≈x ⟨ y∼zwhere we can then use these modules to mix and match whatever syntax we want for a particular Reasoning module.
I'm going to try and squeeze this in for v2.0 as this will make the two issues above almost trivial to do.