coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Sylvain Boulmé <Sylvain.Boulme AT univ-grenoble-alpes.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Beginner question: 0 - 1 = 0?
- Date: Sun, 23 Jul 2023 17:56:21 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Sylvain.Boulme AT univ-grenoble-alpes.fr; spf=Pass smtp.mailfrom=Sylvain.Boulme AT univ-grenoble-alpes.fr; spf=None smtp.helo=postmaster AT zm-mta-out-3.u-ga.fr
- Ironport-sdr: 64bd4db6_uyL7Y5M+bjvglrIu0G1hP4txAjIcMFhWxCb0ZsAJboNftFQ wvHMA2CXletKjLxCWaUI/MRnfcvEu1knWDmZL0Q==
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
- [Coq-Club] Beginner question: 0 - 1 = 0?, Frank Schwidom, 07/23/2023
- Re: [Coq-Club] Beginner question: 0 - 1 = 0?, Dominique Larchey-Wendling, 07/23/2023
- Re: [Coq-Club] Beginner question: 0 - 1 = 0?, Sylvain Boulmé, 07/23/2023
- Re: [Coq-Club] Beginner question: 0 - 1 = 0?, Ana Borges, 07/23/2023
- Re: [Coq-Club] Beginner question: 0 - 1 = 0?, Castéran Pierre, 07/23/2023
- Re: [Coq-Club] Beginner question: 0 - 1 = 0?, Qinshi Wang, 07/24/2023
- Re: [Coq-Club] Beginner question: 0 - 1 = 0?, Hugo Herbelin, 07/26/2023
- Re: [Coq-Club] Beginner question: 0 - 1 = 0?, Qinshi Wang, 07/24/2023
- Re: [Coq-Club] Beginner question: 0 - 1 = 0?, Castéran Pierre, 07/23/2023
- Re: [Coq-Club] Beginner question: 0 - 1 = 0?, Tadeusz Litak, 07/24/2023
- Re: [Coq-Club] Beginner question: 0 - 1 = 0?, Ana Borges, 07/23/2023
- Re: [Coq-Club] Beginner question: 0 - 1 = 0?, Sylvain Boulmé, 07/23/2023
- Re: [Coq-Club] Beginner question: 0 - 1 = 0?, Dominique Larchey-Wendling, 07/23/2023
Archive powered by MHonArc 2.6.19+.