Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Beginner question: 0 - 1 = 0?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Beginner question: 0 - 1 = 0?


Chronological Thread 
  • From: Ana Borges <ana.agvb AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Beginner question: 0 - 1 = 0?
  • Date: Sun, 23 Jul 2023 17:03:16 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ana.agvb AT gmail.com; spf=Pass smtp.mailfrom=ana.agvb AT gmail.com; spf=None smtp.helo=postmaster AT mail-il1-f173.google.com
  • Ironport-data: A9a23:VSis9qlvtJQSGyiQVaANiWro5gxWIkRdPkR7XQ2eYbSJt1+Wr1Gzt xIYC2qCa/+OMDTyKNsgbISw80oFvMLVxtIxGwtvqi9hEVtH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvymTrSs1hlZHWdMUD0mhQ9oh9k3i4tphcnRKw6Ws LsemeWGULOe82Ayajt8B56r8ks156yt4mhA5DTSWNgS1LPgvylNZH4gDfrpR5fIatE8NvK3Q e/F0Ia48gvxl/v6Io7Nfh7TKyXmc5aKVeS8oiI+t5uK3nCukhcPPpMTb5LwX6v4ZwKhxLidw P0V3XC5pJxA0qfkwIzxWDEAe81y0DEvFBYq7hFTvOTKp3AqfUcAzN1LI3sPGaxJ/t8qPl9h5 /IaImxKKReq0rfeLLKTEoGAh+wmJcjveYIb4zRulG6CS/khRp/HTuPB4towMDUY3JgfW6aDI ZNHN3w2M0+ojx5nYj/7DLo3mu7uj3bheRVXrVuUoew85G27IAlZieG9bouMIYzbLSlTtl2A+ Wzf/UbzOE9EBta6zmGj202TifCayEsXX6pLTOHinhJwu3WYwXVWAxkLX3OgsPyhgwi/XcheI goa4EITQbMa8UWqSpz8W0T9rifb5VgTXN1fF+B84waIokbJ3+qHLk0rdAdlSY0ijZIJexM42 F2Dw5SuAhU65dV5Vkmh3ruTqDqzPw0cImkDeTIIQGM5Dz/L8NFbYvXnHoYLLUKlsjHmMWqvn G3S/UDSk51W3JFbjfzqlbzSq2v0/sChc+Ij2unAsouYAu5RYYekY8mp7QGe468fd8CWSV6Ou HVCkM+bhAzvMX1vvH3VKAnuNOvyjxpgDNE6qQM+d3XG32n8k0NPhagKvFlDyL5Ba67ogwPBb k7Joh9275ROJnasZqIfS9vvWpxykPC+Toy6DaC8gj9yjn5ZJF/vEMZGNR744owRuBVEfVwXY 8fGL5ryUx7294w+l2bnHY/xLoPHNghnnT+JLXwK5xug1rWaaRaopUQtYTOzghQCxPrc+m39q o4BX+PTkkk3eLOkPkH/r9VIRXhUdihTOHwDg5YIHgJ1ClE2Rj9J5j646e9JRrGJaIwOzLiVo C3lBRECoLc97FWeQTi3hrlYQOuHdf5CQbgTZETA5H75gCRxUpXl96oFaZo8cJ8u8eEpn7Y+T OAId4/ESr5DQyjOsWZVJ5Tsjp1QRDLyjyK3Pg2hfGceebxkTFf34dPKRFbk2xQPKSuVjvEAh YOc+DnVerc9YjhzLd33bauvxmyhvHJGl+NVWVDJE+Zpe07t0dZLLnXxh8AoP8gzNgXn+QqK8 RSzHCVC9Pf/+Z8x1Nzvm6q/jpyIFtFmFRFwBFjr7reRNAjb8FG8wIRGbv26QDDFWE7w+4Sgf e9w3dimFNEmxXFk65FdFZRvxoIAv+rfnadQlFlYLS+afmaVBaNFCVjY+8t274lm5KJT4CmyU WKxouhqA62DYp7ZIQRANTgeT7qx0N8PkWPv9tUzGkLx4RF38JehUUl/OxqtijRXHIBqMbEKk PsQh8oL1zOR0hYaEM6KriRxxVS+KnYtV6YGtJZDDrT71Sst6FVJOqLHBgHMvZqgVtRrM2sRG AGyupbsvbpm+xf9QyIBLkSVhet5rrYSiS9O124HdgiomMKap/oZ3y9x0DUQTyZTxCppy+hYZ 2phbRV0AY6s/D5YotdJcE7xOgNGBTyfolfQzXlQnkLnbkCYbE7/B0xjBvSspWcy7HB5UgVA2 o2h2ELJcGrPbd7g+CkfQmtnoKHTdsNw/Qj8h8yXJcSJMJ0kaz7DgKX1R243hzb4IME2lmvVj PJL+btuVKjFKiIgma03JI2E37A2ShrfBmhjQ+lkzZwZD1PnZzC+9jifGX+fIvoXCaTxzna5L MhyKuZkdRe0jn+Opw9GI588GeZ/mfpx6ecSfr/uG3U9jIKeiThX4bbw7Sn1gVE5T+p+yfgdL pzjTBPcM2iyq0YNpUrzgphlAESab+MARjXA58Gu0eBQF5s8oOBmKk4z9b2vvkSqCghs/jPKn QbPe57py/dGzKJylbDNCYRGPR2/cvnoZdSL8SeyktVAVszOOsHwrDEoqkHrEgBVHLkJUfF1q OipnPvo+nja5ZAafnv8mZaTM4Vov+CJQ/txIMb7CFJ4jBmycpbgzDVb8l/pNKETts1W4/eWY jeRaeyyUIUwcMhczngEUBpuOU8RJIqvZ5ixuB7nieqHDyUc9gn1LNmH03vNRkMDfw8qP6zOM CPFi8yM1Pt58rsVXAQlAst4CaBWOFXgAKsqV+PgvAmiU1WHvAmwhavApzEBtxf7U3WKKZOvq 9aNDB3zbw+7t6z03clU+d469AEeCHFmx/I8ZAQB8tpxkCq3F3MCMf9bC5gdF5VIiWbn4fkUv t0WgLcKUk0RnAiocCkQJPzmVwabQ+0KY5L3f2NyuUyTbCiyCcWLB74JGuKMJZtpUmOL8Q1lA Yh2Fr7M0tyZzZRgROJV7fu+6Qui7u2P3WoGoCgRjOSrayvzwtw2OLhJEw9EVCiBGMbI/KkOy a7ZWkgcKHyGpYXN/QqMtpKb9Nz1fN8i8tnwURqy/Q==
  • Ironport-hdrordr: A9a23:S8wze66VLQJKDxS+9APXwPHXdLJyesId70hD6qkRc20tTiX8ra qTdZsgpHrJYVoqKRMdcJW7Scq9qBDnlKKdg7NhWYtKNTOO0ACVxcNZjbcKqAeQfBEWmNQts5 uIsJITNDQzNzVHZArBjzVQ2uxP/OW6
  • Ironport-phdr: A9a23:XK5XaB0t2SGSRmubsmDO2g4yDhhOgF0UFjAc5pdvsb9SaKPrp82kY BaBo6gzxw6VFazgqNt8w9LMtK7hXWFSqb2gi1slNKJ2ahkelM8NlBYhCsPWQWfyLfrtcjBoV J8aDAwt8H60K1VaF9jjbFPOvHKy8SQSGhLiPgZpO+j5AIHfg9q22uyo+5DeYgpEiT6ybLhvM Bi4sALdu9UMj4B/MKgx0BzJonVJe+RS22xlIE+Ykgj/6Mmt4pNt6jxctP09+cFOV6X6ZLk4Q qdDDDs6KWA15dbkugfFQACS+3YTSGQWkh5PAwjY8BH3W4r6vyXmuuZh3iSRIMv7Rq02Vzu/9 admUBDniCkFODA5/m/ZidF+grxHrx+6vRNz35TZbZuJOPZifK7Qe84RS2pbXsZWUixMGp+xb 40VAOEcIOtYqJP9p1QQohulGAKhA/ngyjlSiXPsx6I63PohHhrd0QwvGtIBqnXUrNHvOKgOV uC1ybDFwDPeZPxZxTnz8pLHcgw9of6SR7Jwd9Lcx0YxGg7LkFidt47oMy6I2+kNs2aW7eRuW P6ghWI5pQx8rTaiytkjhITXhowY1E7I+Ct4zYs7O9G1TFJ2bN2mHZZWqiqUNJN2T9s8T210v Cs20L4LtJ6hcCQXyZkqxgTTZ+GFfoWG5B/oSfyfLi1ihH1/fbKynxay/lakyu37TsS01UxFr itBktXVt3AN0wHf5tGJSvdg/Eqs1yyD1w/U6uFDLkA0kbTUJ4Q9zb43k5ofqUXDHinol0Xql KKaaFko9+yy5+nkYrjqvIKQOo51hw3kL6gjmMKyDfw9MgcUXmib/eq81Kfk/U38WLhFlPs2n bPDvJ/AKsQbuLW2DhRa0oYm8Rm/DjOm3M4EknkAKVJJYBSHgJPxNFHUPP/4Feu/g0irkDpz2 vzKJqfhDYnVLnjfjLfheq5w5FJbyAoq1NxQ+5ZUCqwaL//oQU/wtNnYDgcjPACuwubnDs991 oIEVm6VDK+ZKvCajVjd7eU2ZuKIeYU9uTDnKvFj6eS9o2U+nAo0e6Dh95wNZ32jVqBvJUzfa HXyiP8OFG4Lukw1S+m82w7KaiJae3vnB/F03To8Eo/zVe8rJ6ioib2FhmKgG4FOI3pBARaKG GvpcIONX7ENbjiTK4lviG9MTqCvHqkm0xzmrwrm0/x/NOOB8ysR85vsytJd6OjalBV0/jtxX IyGy2/Yd2hvhSsTQiMumqV2oEhz0FCGhKF+irpRGsJZz/xMWwY+c5Xbyr8yEMj8DyTGeNrBU 1O6WpOmDDU2G8o22MMLal1hFs+KixnC22+rB+ZQmeXUX9o79aXT23W3LMF4o5rf/I8miVRuA s5GNGn8w7V66xCWHYnC1UOQi6etc60Ymi/L7maKi2SU7gleV0ZrXKPJUGp6BAOepMnl5k7EU 76lCKg2egpHx8mYL6JWa9rvxVxYTfbnMd7abiq/gWC1TRqPw7qNasLtdQB/lG3UDkFCmg8N9 16JMAE/AmGqpGefRD1iGFTzYl/9pPFkoSDzRUs1wgeWKkx5guDtq1hF2LrFFa1Vh+1f60JD4 31uEV2w3szbEY+FrgtlJuBHZM8lpU1A3iTfvhB8OZqpK+ZjgEQfekJ5pRCLtV0/B4NenMwtt H5vwhB1LPfS2VVIMTqXw5rYNbjeK2209xeqIf2zuBmWwJON96ED5e5t4VzltUegGVQo23pi2 thRlXCb49+ZRBpXWpX3XEEt8hF8rLyPeSgx6bTf0nh0OLW1uDvPsz4wLNMs0Q3oP9JWMafeU RT3D9VfHc+lbuojh1muaBsAeuFU7q89ec28JbOK36uiPeAomzzD7ywP6YZ0lEuD6SBURevB3 pJDyPadlgeKTDbzil69v9u/w9gVI2FPWDPhl269W9UZb7Y6ZYsRDGayP8C7o7c2z4XgXXJV7 h/rBl8L3tOoZQvHalX82QNK0kFE6XejmCa+03l1i2Rz9vvZjHGImrq8MkNYYT0uJiEql1rnL ImqgspPWUGpa1Jsjx65/QPgwKMdoq1jLm7VSEMOfi7sLmgkXLHj09jKK8NJ9p4stj1aFeqmZ lXPALf7ql0T3D3pN2RbzTE/MTqtv9+q+n4ywHLYN3t1oHfDLIt5wx6Z7dPCT9Ze2zMHQG9zj jydVRCsetKu+9uTjZLKtOuzAnmgWpNkei7u1YqctSG/6D4PY1X3j7Wpl9bgCwR/zT7j2owgS 3DTtBilKNqjx+GgPOlgZEUtGFLs958wBNRlioVp4fNYkXkC2sfOoDxewD+1a4kEn/q5NiZFR CZXkYCJplK+gws6cCrPn8WgBz2c2pczOYf8OztMnHp7t4cQUML2pPRFhXcn/AT+916AJ6gl2 G9ak6Nm6WZG0b5T/lNxiHzMWPZKWhAIdS30y0bXs5bn9vgRPCD3NuHusSg21dG5UOPb+lEaA SmmPMdkRWgqt41+KA6eiSKorNi1JJ+IK4pU70Pckg+c3bINedRhy7xT33ohYSWk4hhHg6Y6l UA8h8jk+tXXbTw8puThRUcJfjztO5FJo2+r1/0P2J3MmdjoR8QpDDwPWNGAoeuANjUUuLynM g+PFGd5sXKHAf/FGgTZ7k56rnXJGpTtNneNJXBfw88wDB+abFdShgwZRlBY1tYwCxyqycr9c Ux4+iFZ51j2rQFJw/5pMB+3W3nWpQOhYDM5AJaFKx8e4gZH7kbTecuQi4A7Vzlf5YGkpReRJ 3azYg1JCSQIXhXBCQm8Zf+h4t7P9+XeDe27brPPbbiIte1CRqKIyJaoge4Et36HMsSCOGUnD uVugBISGyAkXZ2HxXNWFHdE8kCFJ9SWrxq95CBt+8W28fCxHRnq+ZPKEbxZd9Nm5xGxh66Hc e+WnidwbzhChfZujTfFzqYS2FkKhmRgbT6oRP4JsyeLRa3OkIdYChcab2V4M84CvMdelkFdf NXWjN/4zOsylvkuF1JMTkDsgOmsbM0OZmC5bRbJXRnQcruBIjLPzof8Zqb2GtgyxK1E8ha3v zicCUrqOD+OwiLoWx6YOuZJlCiHPRZatelVlz5iDGHiSJTtbRjpaLefbBUzyLwww3LObCsSa GcnNUxKqbKU4GVThfAtQwSpAVJqKOCFn2CS6OyKc/4r
  • Ironport-sdr: 64bd4f53_hOtA3vj2EmoYnLGf0haeoLdRIVswYw1VEHi5Rd7hL05xYmz b9mcgKm28azacdoY8JyHLrgOjUzSPtO+KzPKuUA==

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



Archive powered by MHonArc 2.6.19+.

Top of Page