在Coq中如何对自然数使用mod算术（特别是Zplus_mod定理）？

Question

我想应用library定理：

Theorem Zplus_mod: forall a b n, (a + b) mod n = (a mod n + b mod n) mod n.

其中a b n应该具有类型Z。

我的目标中有一个子表达式(a + b) mod 3，a b : nat。

[rewrite Zplus_mod给出错误Found no subterm matching

[rewrite Zplus_mod with (a := a)给出错误"a" has type "nat" while it is expected to have type "Z".] >>

由于自然数也是整数，如何为nat参数使用Zplus_mod定理

？

我想应用库定理：定理Zplus_mod：总体a b n，（a + b）mod n =（a mod n + b mod n）mod n。其中a b n预期为Z类型。我在...

Answer 1

中有一个子表达式（a + b）mod 3

您无法应用该定理，因为在您使用自然数的情况下，符号mod指代自然数Nat.modulo上的函数，而当您使用自然数时，符号mod指代Z.modulo引用类型为Z的整数。