首页
学习
活动
专区
圈层
工具
发布
首页
学习
活动
专区
圈层
工具
社区首页 >问答首页 >如何在Coq中使用mod算法(特别是Zplus_mod定理)来处理自然数?

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

Stack Overflow用户
提问于 2020-06-14 12:10:21
回答 1查看 203关注 0票数 0

我想应用图书馆定理:

代码语言:javascript
代码运行次数:0
运行
复制
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参数

EN

回答 1

Stack Overflow用户

回答已采纳

发布于 2020-06-15 06:15:50

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

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

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

代码语言:javascript
代码运行次数:0
运行
复制
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是内射的。我是通过输入以下命令找到它的。

代码语言:javascript
代码运行次数:0
运行
复制
Search Z.of_nat "inj".

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

代码语言:javascript
代码运行次数:0
运行
复制
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_lNat.add_mod_idemp_r

票数 1
EN
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接:

https://stackoverflow.com/questions/62372315

复制
相关文章

相似问题

领券
问题归档专栏文章快讯文章归档关键词归档开发者手册归档开发者手册 Section 归档