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