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?
Normally for ZArith you need (a <= b)%Z, but math-comp probably has different approaches than ZArith.
@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...
I just typoed the symbol — should have written
(a + b)%Z
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.
All right ! Thanks.
In mathcomp, the preferred type of integer is
int (from library
mathcomp.algebra.ssrint), and you should indeed use the overloaded
+ in the
%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: Feb 08 2023 at 04:04 UTC