Swapping the argument order in equational reasoning

[maxsnew]

In porting a category solver from the 1lab (https://github.com/maxsnew/multi-poly-cats/tree/main/Cubical/Tactics/CategorySolver), I ran into an issue: the solvers can't work in equational reasoning proofs because they never have the right hand side of the goal inferred. For example this proof:

  ex : ∀ {A B C}(f : 𝓒 [ A , B ])(g : 𝓒 [ B , C ])(h : 𝓒 [ A , C ])
    → (f ⋆ (id ⋆ g)) ≡ h
    → f ⋆ g ≡ h ⋆ id
  ex f g h p =
    f ⋆ g ≡⟨ solveCat! 𝓒 ⟩
    (f ⋆ (id ⋆ g)) ≡⟨ p ⟩
    h ≡⟨ solveCat! 𝓒 ⟩
    h ⋆ id ∎

Doesn't succeed with the current definition of equational reasoning, in each case the call to solveCat! fails because the rhs is an unsolved metavariable.

Reed Mullanix showed me that the issue can be solved by redefining the equational-reasoning syntax to swap the order the arguments are passed:

≡⟨⟩-syntax : ∀ {ℓ} {A : Type ℓ} (x : A) {y z} → y ≡ z → x ≡ y → x ≡ z
≡⟨⟩-syntax x q p = p ∙ q

infixr 2 ≡⟨⟩-syntax

syntax ≡⟨⟩-syntax x q p = x ≡⟨ p ⟩ q

Agda's type checker works from left to right but the equational reasoning macro is right-nested, so swapping the arguments like this gives better type inference and can even lead to performance improvements. With this change the equational reasoning proof above works.

This change has already been done in the agda-stdlib three years ago (agda/agda-stdlib#1045) and is used in the 1lab as well. It seems quite critical for allowing the use of solvers in practice.

[felixwellen]

Wow - this is great! I ran into this problem once, but didn't know it has an easy fix like this. Does it have drawbacks? Does the use of syntax mess up goals?

[MatthewDaggitt]

The issues the stdlib has had with it: i) very verbose to rename the syntax, ii) much more non-obvious what to do when trying to import explicitly using using.

[maxsnew]

What do you mean by it being verbose? Don't we just need to change a couple of definitions to be macros?

[felixwellen]

Maybe we can just try how good or bad it is?
@maxsnew: Can you make a PR (with possibly failing CI) that replaces equational reasoning with what you think we should do?

[maxsnew]

solved by #999