Error: Cannot interpret this number as a value of type nat

Question

My current goal is:

x - 1 + 1 = x

I tried to use rewrite -> (Nat.add_comm (-1) 1). to change the current goal to x + 1 - 1, but it gave me the error Error: Cannot interpret this number as a value of type nat. How can I solve this question?

Answer 1

Assuming x is indeed a natural number, I believe your goal is false. Note that subtraction on the natural numbers is truncated. Thus, if x = 0, what we have is

0 - 1 + 1 = (0 - 1) + 1 = 0 + 1 = 1 != 0

where the parenthesis I added are already there, I just made them explicit (*).

The error you get makes perfect sense. -1 is not a natural number, and hence Coq can't interpret it as a natural number.

(*) You can do this with Set Printing Parentheses.

---

Edit: If you are able to prove that 1 <= x in your context, you can use

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

I found these results by importing Arith and searching like so:

Search (_ - _ + _).