The Coq mailing list

[Tadeusz Litak <tadeusz.litak AT gmail.com>]

On top of what others have said, there are numerous way of handling partial functions in Coq. An obvious way is to use 
the Option (or "Maybe") monad, familiar to all functional programmers, but there are other solutions too. Here is a more 
exhaustive discussion:

http://adam.chlipala.net/cpdt/html/Cpdt.Subset.html

Best,
t.


On 23/7/23 5:56 PM, Sylvain Boulmé 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