问如何在Coq中使用mod算法(特别是Zplus_mod定理)来处理自然数？

EN

您不能应用这个定理，因为表示法mod在使用自然数的上下文中引用了自然数Nat.modulo上的函数，而当您引用Z类型的整数时，表示法mod是指Z.modulo。

使用Search命令ou可以专门搜索关于Nat.modulo和(_ + _)%nat的定理，您将看到一些现有的定理实际上非常接近您的需要(Nat.add_mod_idemp_l和Nat.add_mod_idemp_r)。

你也可以找一个把Z.modulo和Nat.modulo联系起来的定理。这给了mod_Zmod。但这迫使您在整数类型中工作：

Require Import Arith ZArith.

Search Z.modulo Nat.modulo.

 (* The answer is :  
    mod_Zmod: forall n m, m <> 0 -> Z.of_nat (n mod m) = 
       (Z.of_nat n mod Z.of_nat m)%Z  *)

一种方法是找到一个定理，它告诉你函数Z.of_nat是内射的。我是通过输入以下命令找到它的。

Search Z.of_nat "inj".

在产生的长列表中，相关的定理是Nat2Z.inj，然后您需要展示Z.of_nat如何与所涉及的所有操作符交互作用。大部分这些定理都要求n是非零的，所以我把它作为一个条件。这是一个例子。

Lemma example (a b n : nat) : 
   n <> 0 -> (a + b) mod n = (a mod n + b mod n) mod n.
Proof.
intro nn0.
apply Nat2Z.inj.
rewrite !mod_Zmod; auto.
rewrite !Nat2Z.inj_add.
rewrite !mod_Zmod; auto.
rewrite Zplus_mod.
easy.
Qed.

这回答了您的问题，但坦率地说，我相信您最好使用引理Nat.add_mod_idemp_l和Nat.add_mod_idemp_r。