search

math-comp / algebra-tactics

Ring, field, lra, nra, and psatz tactics for Mathematical Components
33 stars 2 forks source link

Reflexive zify #63

Open pi8027 opened 2 years ago

pi8027 commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

Isn't zify the job of trakt?

gares commented 2 years ago

Oh but it is not reflexive...

pi8027 commented 2 years ago

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.