The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

By the way, there is a mathematical theory of this truncated
subtraction on natural numbers. In the more general context of
commutative monoids, it is called a monus, see
e.g. https://en.wikipedia.org/wiki/Monus.

Best,

Hugo

On Sun, Jul 23, 2023 at 09:14:16PM -0400, Qinshi Wang wrote:
> (-1) is not a natural number. That's why I recommend using Z instead of nat 
> for
> any realistic proof involving arithmetic.
> 
> Thanks,
> Qinshi
> 
> On Sun, Jul 23, 2023 at 3:11 PM Castéran Pierre <pierre.casteran AT gmail.com>
> wrote:
> 
>     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
> 
> 
>