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!

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.

Hello @Guillaume Dubach . Unfortunately, there is indeed only makeshfit techniques available as of today, to make `ring`

available on type `int`

.

But there are still available options.

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.

@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 :)

Incidentally, is there an equivalent wrapper to use lra on math-component order fields?

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.

@Kazuhiko Sakaguchi Thanks, looking forward to it.

@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.

I see the package requires Coq 8.13. Are there any plans to support Coq 8.12?

will this close this long standing issue: https://github.com/math-comp/math-comp/issues/263 ?

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.

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 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.

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: Jan 29 2023 at 19:02 UTC