coq - 错误:无法将此数字解释为 nat 类型的值
问题描述
我目前的目标是:
x - 1 + 1 = x
我尝试使用rewrite -> (Nat.add_comm (-1) 1).
将当前目标更改为x + 1 - 1
,但它给了我错误Error: Cannot interpret this number as a value of type nat
。我该如何解决这个问题?
解决方案
假设x
确实是一个自然数,我相信你的目标是错误的。请注意,自然数的减法会被截断。因此,如果x = 0
,我们所拥有的是
0 - 1 + 1 = (0 - 1) + 1 = 0 + 1 = 1 != 0
我添加的括号已经在那里,我只是将它们明确表示(*)。
你得到的错误是完全有道理的。-1
不是自然数,因此 Coq 不能将其解释为自然数。
(*) 您可以使用Set Printing Parentheses
.
编辑:如果您能够1 <= x
在您的上下文中证明这一点,您可以使用
Nat.sub_add: forall n m : nat, n <= m -> m - n + n = m
Nat.add_sub_swap: forall n m p : nat, p <= n -> n + m - p = n - p + m
我通过像这样导入Arith
和搜索找到了这些结果:
Search (_ - _ + _).
推荐阅读
- assembly - 装配中的除法和舍入
- android - Android OnTouchEvent 在第一次触摸时不会触发
- javascript - 用于选择的自定义 html5 验证
- python-3.x - 为什么我的 kivy 程序没有从另一个类调用函数?
- java - JPA 和 Hibernates 绑定参数的 Java.Util.Date 查询问题
- python - python将字符串拆分成新行到文件中
- php - 媒体未在 Wordpress 库中显示,但在上传文件夹中可用
- javascript - 问题处理在 Web 应用程序中解析用户
- android - 如何触发 ActivityAware 覆盖方法 onAttachedToActivity()?
- c++ - 为什么函数执行后没有释放堆上的元素?