## Stream: math-comp users

### Topic: Working with relative integers

#### 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?

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

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

#### Paolo Giarrusso (Nov 04 2020 at 16:49):

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

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

#### Guillaume Dubach (Nov 04 2020 at 21:40):

All right ! Thanks.

#### 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: Jul 25 2024 at 15:02 UTC