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

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

Answer 1

你不能应用这个定理，因为符号 mod 在你使用自然数的上下文中指的是自然数 Nat.modulo 上的函数，而符号 mod 指的是 Z.modulo 当您指的是 Z.

类型的整数时

使用Search命令，你可以专门搜索关于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。

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

How in Coq to use mod arithmetic (specifically Zplus_mod theorem) for natural numbers?

logic

coq

coq-tactic

mod