ring tactic for math-comp integers

I made the math-comp type int work with the ring tactic (https://coq.inria.fr/refman/addendum/ring.html) in much the same way the math-comp type nat already does. Is this of general interest?

One caveat is that to solve general equations like forall (x y : int), x + y = y + x one must first unfold to forall (x y : int), addz x y = addz y x before applying the ring tactic (which can be done with a short ltac expression).

Dear @bshvass, thanks for your interest. Yes this is a long standing problem in mathcomp. Any suggestion on the topic is welcome, we may discuss concrete proposals in PR threads. I think @amahboubi gave a go at the technique you are suggesting a few years ago. There is also https://github.com/strub/elliptic-curves-ssr/blob/631af893e591466207929714c45b5f7476d579d0/common/ssrring.v which should be considered for integration. Best wishes.

Hi @bshvass. Thanks for resurrecting this topic. Indeed, I have some Ltac code that makes the ring tactic operational for the rat type in a robust way, that can also be transposed for other types. This was instrumental in a proof of Apéry's theorem. I will put the code online by the end of the week. I have not done so before because I believe we should be able to do something more satisfactory.

Hi @bshvass, thanks for resurrecting this topic. Indeed, this is an old known issue... @CohenCyril is right, a few years ago I wrote some Ltac code for making the ring and field tactics operational on the rat type, that should be straightforward to transpose on the int type. Type rat was a slightly more involved example because of the proof hidden in the data structure. This instance of ring was instrumental in a proof of Apéry's theorem. The link in the paper still works, but I plan to put online the updated version of the library (with the complete proof) later this week. However, I believe that we should be able to do something more satisfactory...

About elliptic curves. We are currently considering whether it is feasible to integrate elliptic https://github.com/strub/elliptic-curves-ssr and fiat-crypto. So far things look positive. Is there a plan on integrating elliptic curves into math-comp? Any other issues we should be aware of? @strub @jasongross ?

@spitters I think this topic deserves a specific issue...

Hello. Sorry for multi-posting but I implemented ring and field tactics for MathComp (NB: This is highly experimental and everything is subject to change) with help from Assia and Enrico. These tactics work with any comRingType and fieldType instances respectively. While there are some performance issues on the reflection side, which I'm going to fix, the reification process that uses conversion extensively seems quite efficient.

This issue seems to be solved by the new algebra-tactics package, so we close, please reopen if we are mistaken.