Magma reasoning

[alexarice]

Added a new module magma reasoning, which allows automation of congs in proofs.
See README.Algebra.Reasoning.Magma for an example

Extends #1144
Built on top of #1145

This is a non reflection based approach to #1136 which is specific to Magmas. Most of the syntax is pulled from the discussion in that issue

EDIT: WIP because I have realised I still need to think about how tightly the Expr builders bind
Have put something in but am not sure if it is the best

[martinescardo]

Nice.

[MatthewDaggitt]

@alexarice thanks for the PR. This is incredibly cool, I wouldn't have guessed you could do this without reflection! I guess my main question is what are the advantages of this over #1136?

It's true that it doesn't use reflection, but I don't think that's going to be a big selling point. Reflection doesn't require us to introduce any more rules, especially as #1136 uses --safe. This approach is alsos going require quite a lot of work to generalise it to other algebraic structures, whereas #1136 should work with everything out of the box.

[alexarice]

The limitations of reflection I have seen when I try to use it are the following:

• It seem quite slow, though this may just be anecdotal and more based on the one time I tried to use it.
• Agda didn't seem to be able to give a good indication on the type needed to fill metavariables. Maybe there are there ways in the reflection machinery to specify what type is wanted in holes though I could not work it out when I was having a play round with it.

Further briefly reading #1136 suggested it relied on having a full cong operation and so I think it might not work with the algebra structures that are setoid enriched. Again I could be incorrect here.

[alexarice]

Further, this can be used reasonably well with at least single operation structures (although it does not cope with inverse cong).

[MatthewDaggitt]

Further briefly reading #1136 suggested it relied on having a full cong operation and so I think it might not work with the algebra structures that are setoid enriched. Again I could be incorrect here.

From the sound of it should be able to work with arbitrary setoids.

If it's okay with you, I suggest we wait until @dylanede opens a PR for it and then we can do an actual comparison rather than discussing hypotheticals?

[alexarice]

sounds good to me

[laMudri]

This reminds me of Conor's category/functor solver, which shows how this sort of thing can be integrated with algebraic laws. There's a fairly broad and largely untested design space here. One thing I thought of in particular is that it's possible to have multiple foci, which might help in some situations and also simplify the syntax (the distinction between _◂_ and _▸_ becomes unnecessary).

[alexarice]

I can't immediately see how having multiple foci simplifies the syntax, could you explain? Thanks for the link, I'll try to have a read through it at some point

[laMudri]

It simplifies the interface you can give to users. The distinction between _◂_ and _▸_ basically encodes a proof that there is exactly one focus, so if you allow for multiple foci, you don't need to encode that proof. The syntax of expressions can then be just the magma operation + embedding + focus.

To deal with multiple foci requires a little bit more from the implementation to present the equations arising from the foci. Conor does a particularly cheap thing in Reduced, but you could imagine traversing a tree like this to present the equations as a list/All. You probably could have a special case for a single focus so as to maintain compatibility (including not being too noisy with the list machinery).

[alexarice]

Ah I see, this is currently representing the focus as a path through the tree, so there isn't a reason that there could be a list of foci instead, putting some arbitrary order on (likely left to right)

[alexarice]

I remember part of the problem I had is allowing an unfocused variable to be treated as an expression. From my understanding, allowing multiple foci would allow you to have just one syntax for combining two sub expressions, however I can't see how you would avoid having to introduce syntax for an "unfocused leaf"

[MatthewDaggitt]

Closing this as I think the tactic-based approach added in #1658 is more powerful and has better syntax.