Refactoring with Equation Command

Stream: Equational

[Shreyas Srinivas]

I am undertaking the refactoring using equation command. One thing right off the bat is that docstring comments don't recognise the equation command as a valid declaration succeeding a docstring.

[Shreyas Srinivas]

Is there a quick fix for this?

[Shreyas Srinivas]

See PR equational#295

[Joachim Breitner]

Actually now that we fixed the conflict with the function composition operator, I would suggest to remove the equation command completely and go back to normal lean definitions.

[Joachim Breitner]

Given that the main motivation for the command was to work around the slow elaboration

[Shreyas Srinivas]

https://github.com/teorth/equational_theories/issues/290
The issue description says this is to collect these equations easily

[Shreyas Srinivas]

Although the command itself at present only creates abbrevs

[Shreyas Srinivas]

I guess that later the command can be modified to add the equations to an external database automatically

[Terence Tao]

One reason I thought equation might still be useful is when we finally link up "shallow" EquationX propositions with "deep" LawX objects of type MagmaLaw, since one could use metaprogramming to define both automatically. But I guess we could just autogenerate both lists once by some external script and not have any metaprogramming for this. But it might also help with the hypothetical Equation<->Law tactics in https://github.com/teorth/equational_theories/issues/147 . These in turn could help implement duality within Lean, rather than through implicit implications.

[Terence Tao]

But perhaps there are better ways to establish all this. In particular I have no experience with metaprogramming and tactic writing, so I don't know what is the most feasible path here.

[Joachim Breitner]

Sure, that might be useful (although maybe more naturally done as an attribute). I'm just a bit wary of (now) unnecessary extra layers of complexity. I think either path is reasonable, and it doesn't matter much either way

[Shreyas Srinivas]

I like the equation command. If only someone can help me make docstrings work with it

[Terence Tao]

One minor nice thing about the equation approach is (once the docstring issue is solved) that it becomes really easy to move an equation from AllEquations.lean to Equations.lean. I guess if we instead spell out EquationX and LawX directly (with all attendant attributes, and API to convert back and forth) one just cut and pastes ten lines instead of one, so it's sort of the same, but I like the current elegant look of AllEquations.lean

[Shreyas Srinivas]

That file is rather large and some renumbering will be needed to move its contents into Equations.lean

[Shreyas Srinivas]

I think it is best to leave that file as is

[Terence Tao]

I don't plan to move all 4694 equations into Equations.lean. Only the ones for which we have specialized theorems about, which can be proved by just loading Equations.lean and not AllEquations.lean

[Shreyas Srinivas]

Okay I see what you mean now.

[Joachim Breitner]

Shreyas Srinivas said:

I like the equation command. If only someone can help me make docstrings work with it

On the phone and sleepless in the bed right now, so can't hack on it, but maybe look at similar commands on mathlib, like lemma, and cargo cult. Probably just a matter of adding the right non-terminal to the syntax and including it in the final command splice

[Shreyas Srinivas]

lemma uses a macro and the others use leading_parser

[Shreyas Srinivas]

I will look into this after getting a night's sleep. If someone wishes to try the file to modify is equational_theories/EquationsCommand.lean

[Shreyas Srinivas]

This is done

[Shreyas Srinivas]

I upgraded the equation command to handle docstrings thanks to @Yury