Hi,

As part of my development, I need to prove the following:

`Lemma foo: forall (n m: nat), n = m + (n - m).`

This is problematic with the current definition of "-" for `Nat`

and the order of operations.

I wonder if there is another definition of natural numbers that would help working-around this.

One solution is to do the proof in Z of course, but that creates other issues like adding additional predicates in other places.

Thanks!

You can look at what is done in `nat.v`

, part of the Mathematical Components library (https://math-comp.github.io/htmldoc/mathcomp.ssreflect.ssrnat.html). This lemma (`subnKC`

) is only true if the additional condition `m <= n`

is added.

Indeed, adding `m <= n`

makes this lemma trivial with `lia`

. But I was looking for a more general solution without this extra hypothesis.

Jerome Hugues said:

Indeed, adding

`m <= n`

makes this lemma trivial with`lia`

. But I was looking for a more general solution without this extra hypothesis.

Indeed, the considered equality is equivalent to this hypothesis.

```
Lemma foo: forall (n m: nat), n = m + (n - m) <-> m <= n.
Proof. intros; lia. Qed.
```

I wonder if there is another definition of natural numbers that would help working-around this.

if you're just changing minus, I think not: take `n = 0, m = 1`

, we search `X := minus' n m`

such that `n = m + X`

, that is `0 = 1 + X`

. But `X := -1`

is the unique solution for that equation

Jerome Hugues said:

`Lemma foo: forall (n m: nat), n = m + (n - m).`

One solution is to do the proof in Z of course

That is worse than that. If you look at the instance `(foo 0)`

, it actually states `forall m, 0 = m + (0 - m)`

. In other words, any element has an inverse for addition, which precisely characterizes the difference between `nat`

and `Z`

. So, it is not just that you could do the proof in `Z`

; you have to do the proof in `Z`

(or any superset).

Last updated: Oct 04 2023 at 23:01 UTC