Make reasoning syntax actually modular

[MatthewDaggitt]

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∼z

where 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.

[jamesmckinna]

Very cool! (but I might be partisan, seeing the symbols chosen... ;-))
Ah, but you went for the _≈⟨_⟩_/_≈⟨_⟨_ version as opposed to the _≈⟨_⟨_/_≈⟨_⟨_ version? but perhaps because the latter is upwards-compatible with the initial choice above, which is at least backwards-compatible... I think I see.

[MatthewDaggitt]

Sorry, should be clear that I won't touch the symmetry thing in this PR. The above was just an example I was trying to put together after already having tried to start the symmetry changes. I'll use the old notation in the first instance.

[MatthewDaggitt]

Reminder to self to come back to:

• src/Data/Vec/Relation/Binary/Equality/Cast.agda
• src/Relation/Binary/HeterogeneousEquality.agda
• src/Effect/Monad/Partiality.agda
• src/Effect/Monad/Partiality/All.agda
• src/Relation/Binary/PropositionalEquality/Core.agda
• src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda
• src/Codata/Sized/Stream/Bisimilarity.agda
• src/Function/Reasoning.agda