coq - 错误：无法将此数字解释为 nat 类型的值

Question

我目前的目标是：

x - 1 + 1 = x

我尝试使用rewrite -> (Nat.add_comm (-1) 1).将当前目标更改为x + 1 - 1，但它给了我错误Error: Cannot interpret this number as a value of type nat。我该如何解决这个问题？

Answer 1

假设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 (_ - _ + _).