The Coq mailing list

[Castéran Pierre <pierre.casteran AT gmail.com>]

Coq just follows the same convention as in some areas of theory of computation : https://proofwiki.org/wiki/Predecessor_Function_is_Primitive_Recursive

Since substraction is an iteration of predecessor, we get a - b = 0 iff a <= b (if a and b are natural numbers).

Best,

Pierre

Le 23 juil. 2023 à 18:03, Ana Borges <ana.agvb AT gmail.com> a écrit :

Crucially, and in addition to what others have already said, 0 - 1 is undefined on the natural numbers. You can't get a proof of 0 = -1 out of defining 0 - 1 := 0. If you were expecting 0 - 1 = -1 then you may want to work with the integers and not with the natural numbers.

On Sun, 23 Jul 2023 at 16:56, Sylvain Boulmé <Sylvain.Boulme AT univ-grenoble-alpes.fr> wrote:

More generally, turning a "usual" partial function into a total function
only allows some "unusual" theorems such that "0 - a = 0", but does not
invalidate any of the partial function (By definition, such a theorem is
valid for any total interpretation of the partial function).

In many cases, these "unsual" theorems simplify the proofs. At least,
because it is simpler to handle total functions than partial ones.
For example, consider the proof of "(c+a) - (c+b) = a - b". With a
partial function, you should prove instead
   "b <= a -> (c+a) - (c+b) = a - b"
and thus, in an induction proof, you would have to prove the "b <= a "
hypothesis of the induction hypothesis. This is not necessary on the
total function.

We only should take care when interpreting theorems about the total
function: they may not directly apply to the partial one. If needed, we
may still introduce a definition for representing the "partial function"
(there are various techniques for that, the most general one is probably
to introduce an inductive relation representing the graph of the partial
function) and proves a correspondence theorem between the "partial
function" and the total one (as skteched for minus by Dominique below).

Best,

Sylvain.


Le 23/07/2023 à 17:04, Dominique Larchey-Wendling a écrit :
> This is from the definition of "minus" in Coq with infix notation "x - y".
> "Print minus" will give you the fixpoint definition.
>   
> If a <= b then  a-b = 0. You can prove this.
>
> You just have to be aware that this is not the usual subtraction
> operation which would be a partial operation on natural numbers
> (positive integers), ie a-b should be undefined when a < b.
>
> a - b has the "usual" meaning if (and only if) a >= b.
>
> This is enough to get (a + b) - b = a for instance
> But (a - b) + b is not equal to a, unless a >= b.
>
> Best,
>
> Dominique
>
> ----- Mail original -----
>> De: "Frank Schwidom" <schwidom AT gmx.net>
>> À: "coq-club" <coq-club AT inria.fr>
>> Envoyé: Dimanche 23 Juillet 2023 16:53:35
>> Objet: [Coq-Club] Beginner question: 0 - 1 = 0?
>
>> Hi,
>>
>> what puzzles me is that I can obviously get a wromg result from the view of the
>> natural understanding:
>>
>> Coq < Compute 0 - 1.
>>      = 0
>>      : nat
>>
>> How can it be clear that this makes no problems in proofs?
>>
>> Regards,
>> Frank