Guillaume Dubach (Mar 30 2021 at 06:58): Guillaume Dubach (Mar 30 2021 at 06:58):I am struggling to apply the instructions of https://coq.inria.fr/refman/addendum/ring.html in order to use the ring tactic on expressions involving the type int. Apparently I should declare explicitly that int has a ring structure with "Add Ring"? But I am guessing this must be the case automatically with the right imports, scopes, etc. If someone could give me a minimal working example of preamble for this it would be great!
Kazuhiko Sakaguchi (Mar 30 2021 at 07:11):See https://github.com/math-comp/math-comp/issues/401. The solutions currently available are unsatisfactory (for performance reasons IIUC), and I will try to implement a better reification in Coq-Elpi soon.
Assia Mahboubi (Mar 30 2021 at 12:29):Hello @Guillaume Dubach . Unfortunately, there is indeed only makeshfit techniques available as of today, to make ring available on type int.
Assia Mahboubi (Mar 30 2021 at 12:29):But there are still available options.
Assia Mahboubi (Mar 30 2021 at 12:35):One would be to mimic what was done for the type rat of rational numbers, e.g. here. You will also need to adapt this file. (It should work well, and efficiently but it is quite unsatisfactory to have to do so much boilerplate code for every instance of ring structure. ) Another possible option would be to zify your goals, before calling ring. And for this task, may be @Kazuhiko Sakaguchi 's `mczify tool could help.
Anton Trunov (Mar 31 2021 at 07:35):@Kazuhiko Sakaguchi Hi, are there any plans to publish mczify on opam? I'd like to reuse it in a project. As of now we have to copy around Assia's excellent ssrlia tactic :)
Yves Bertot (Mar 31 2021 at 12:39):Incidentally, is there an equivalent wrapper to use lra on math-component order fields?
Kazuhiko Sakaguchi (Apr 01 2021 at 06:31):Anton Trunov said:
Kazuhiko Sakaguchi Hi, are there any plans to publish mczify on opam? I'd like to reuse it in a project. As of now we have to copy around Assia's excellent ssrlia tactic :)
Sure. I will do that soon but would like to wait to have coq/coq#14043 fixed.
Anton Trunov (Apr 01 2021 at 08:44):@Kazuhiko Sakaguchi Thanks, looking forward to it.
Kazuhiko Sakaguchi (Apr 22 2021 at 06:53):@Anton Trunov Hi, I released mczify 1.0.0, which is also available on OPAM now.
$ opam install coq-mathcomp-zify
Awesome news @Kazuhiko Sakaguchi ! Thank you.
Anton Trunov (Apr 22 2021 at 06:58):I see the package requires Coq 8.13. Are there any plans to support Coq 8.12?
Reynald Affeldt (Apr 22 2021 at 06:58):will this close this long standing issue: https://github.com/math-comp/math-comp/issues/263 ?
Kazuhiko Sakaguchi (Apr 22 2021 at 07:13):Anton Trunov said:
I see the package requires Coq 8.13. Are there any plans to support Coq 8.12?
I have a branch that works with Coq 8.12 which I can release if needed. But, there is a performance issue and it is probably less powerful than one for 8.13. Both issues come from a limitation of the zify tactic (bool had to be translated to Z) in Coq 8.12. So, I am a bit hesitant to release it, and strongly recommend using Coq 8.13 in any case.
Kazuhiko Sakaguchi (Apr 22 2021 at 07:16):Reynald Affeldt said:
will this close this long standing issue: https://github.com/math-comp/math-comp/issues/263 ?
I think so. Mczify still has many limitations and issues, but we can open such issues in https://github.com/math-comp/mczify/issues.
Kazuhiko Sakaguchi (Apr 23 2021 at 02:09):Kazuhiko Sakaguchi said:
See https://github.com/math-comp/math-comp/issues/401. The solutions currently available are unsatisfactory (for performance reasons IIUC), and I will try to implement a better reification in Coq-Elpi soon.
BTW, as I said here, I'm working on a better reification for the ring tactic that works with MathComp. After comparing what is available in ssralg and setoid_ring, I think it would also be nice to support ring morphisms (indeed it requires reimplementing the whole ring tactic). If someone has this kind of wish, please let me know.
Kazuhiko Sakaguchi (May 21 2021 at 21:21):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.
Last updated: Apr 20 2024 at 13:01 UTC