Stream: Coq users

Topic: Proving forall (n m: nat), n = m + (n - m).

Jerome Hugues (Apr 25 2023 at 14:57):

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!

Pierre Jouvelot (Apr 25 2023 at 15:05):

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.

Jerome Hugues (Apr 25 2023 at 15:35):

Indeed, adding m <= n makes this lemma trivial with lia. But I was looking for a more general solution without this extra hypothesis.

Pierre Castéran (Apr 25 2023 at 15:44):

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.

Paolo Giarrusso (Apr 25 2023 at 15:48):

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

Guillaume Melquiond (Apr 25 2023 at 15:58):

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 13 2024 at 01:02 UTC