Stream: math-comp users

Topic: Working with relative integers


view this post on Zulip Guillaume Dubach (Nov 04 2020 at 09:08):

I have an issue when trying to work with the type Z: after importing ZArith and writing a theorem that has (a:Z) (b:Z) in its context and then an expression involving (a+b) in the statement, I get the error message " The term "a" has type "Z" while it is expected to have type "nat" ".

More generally, I wanted to ask: is Z the best (or the only) type to work with relative integers? Do the tactics simpl and ring work well with this?

view this post on Zulip Paolo Giarrusso (Nov 04 2020 at 12:35):

Normally for ZArith you need (a <= b)%Z, but math-comp probably has different approaches than ZArith.

view this post on Zulip Guillaume Dubach (Nov 04 2020 at 15:58):

@Paolo Giarrusso Why would I need to assume an inequality if I am adding them?... And even if I subtract them, why should this be an issue in Z? My current problem is about natural numbers, but the reason why I want to work with Z is precisely to avoid structural paradoxes like (2-3)^2=0...

view this post on Zulip Paolo Giarrusso (Nov 04 2020 at 16:49):

I just typoed the symbol — should have written (a + b)%Z

view this post on Zulip Paolo Giarrusso (Nov 04 2020 at 16:51):

but this uses the stdlib's addition, and I expect that in math-comp you're just not supposed to use that, and you should use the operators that are overloaded via canonical structures.

view this post on Zulip Guillaume Dubach (Nov 04 2020 at 21:40):

All right ! Thanks.

view this post on Zulip Cyril Cohen (Nov 04 2020 at 22:35):

In mathcomp, the preferred type of integer is int (from library mathcomp.algebra.ssrint), and you should indeed use the overloaded + in the ring_scope (denoted %R), as in (m + n)%R, since it is canonically a totally ordered integral domain. Unfortunately, ring for this datatype is not yet available officially, although there are have been several attempts that you might get inspiration from (cf math-comp/math-comp#401).


Last updated: Mar 28 2024 at 20:01 UTC