Reflexive zify

[pi8027]

Thanks to coq/coq#15921, it should be possible to reimplement mczify in the preprocessing approach of Algebra Tactics. I'm curious how much we could improve the performance (of Apery for example) by reimplementing §5.2 of Algebra Tactics paper in this way.

[pi8027]

I can also imagine that writing such a preprocessor (mainly the Elpi part) dealing with side conditions can be a bit more painful. So generating such reflexive tactics is another thing I would like to try.

[gares]

Isn't zify the job of trakt?

[gares]

Oh but it is not reflexive...

[pi8027]

My main concern regarding standalone preprocessing tactics like ppsimpl, zify, trakt, and simp (of Lean) is that we often seem to make the whole automated proving procedure slower by piling up preprocessing steps. On this point, one thing I would like to achieve in general would be something like a fusion transformation for tactics. Algebra Tactics can be seen as such "fused" (but very simple) tactics made of preprocessors and decision procedures. Hence my initial question.