coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] natural numbers as a datatype and as decimal numerals

From: Gergely Buday <gbuday AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] natural numbers as a datatype and as decimal numerals
Date: Mon, 14 May 2018 11:30:59 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gbuday AT gmail.com; spf=Pass smtp.mailfrom=gbuday AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua0-f179.google.com
Ironport-phdr: 9a23:F8YGnBPENxXje2UJYYAl6mtUPXoX/o7sNwtQ0KIMzox0LPT5rarrMEGX3/hxlliBBdydt6ofzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlGiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSgFOT438G/ZhM9tgqxFvB2vqAdyw5LNYIyPKPZyYr/RcNEcSGFcXshRTStBAoakYoUOEeUBJ+lYoJf5p1oOsBCzGBSsC/71xT5Im3T72qI63P88EQ7bxgMhH8kDsHvRrNrvNacSVfq5w7XPzTXGdv5b3yr25ovQch05v/2AQbZ9fdDSxEQvDQ/JkEicpI7/Mz+I1OkAt26W5Pd6W+21kW4osQRxryCvxsgyjonJgZoYylXe+iV4xIY5PMC4R1RnbdK9HptcqiOXOo9sTsMtRGFovyk6yrkYtpKhYCcKz5Enywbea/yBbYeI/gruWPiNLTp8nn5oe7Kyiwys/US9yODwTNS43VROoyZdl9nDrHEN1xjd6sidTft9+1+s2TmU2ADO9+5LO0A1mLHUK54k2LEwl54TvV7fES/xnUX6lLWWeVk8+ui09+TnZa3rqYObN49tkw3xLqAumtGkDukjKQgPX22b+fym27H5/E35Rq9KjvwsnaXDvpDaP5dTmqnsCAhMl40n9hyXDjG80d1ek2NUAkhCfUeogpLmNlXfaNrlAf6uywCjmipnzuHuMbjoA5GLJX/GxuSyNY1h4lJRnVJghetU4IhZX+lYcaDDH3TpvdmdNScXdgm9wuLpEtJ4j9pMVmeGA6vfO6TX4wbRurAfZtKUbYpQgw7TbuA/7qe333A8kF4ZO6Ku2MlPMS3qLrFdO0ycJEHUrJIBHGMN5FRsSeXrjBifWGYWaS/tDuQz4TY0DI/gBoDGFNig

Yes this is obvious and other theorem provers do the same.

The question is: what is the machinery behind this? Does the system
recognizes that this definition is indeed a definition for the natural
numbers?

On 14 May 2018 at 10:44, David P Á <david AT picon.email> wrote:
> On 14/05/2018 10:34, Gergely Buday wrote:
>>
>> How does Coq relate the above user definition to the standard way of
>> writing natural numbers?
>
>
> It's Coq syntactic sugar, as Software Foundations points out eventually. It
> would otherwise become far too tedious to represent naturals.
>
> --David.
>

[Coq-Club] natural numbers as a datatype and as decimal numerals, Gergely Buday, 05/14/2018
- Re: [Coq-Club] natural numbers as a datatype and as decimal numerals, David P Á, 05/14/2018
  - Re: [Coq-Club] natural numbers as a datatype and as decimal numerals, Gergely Buday, 05/14/2018
    - RE: [Coq-Club] natural numbers as a datatype and as decimal numerals, Soegtrop, Michael, 05/14/2018
      - Re: [Coq-Club] natural numbers as a datatype and as decimal numerals, Théo Zimmermann, 05/14/2018
        
        RE: [Coq-Club] natural numbers as a datatype and as decimal numerals, Soegtrop, Michael, 05/14/2018
        
        Re: [Coq-Club] natural numbers as a datatype and as decimal numerals, Théo Zimmermann, 05/14/2018
        
        Re: [Coq-Club] natural numbers as a datatype and as decimal numerals, José Manuel Rodriguez Caballero, 05/14/2018
        Re: [Coq-Club] natural numbers as a datatype and as decimal numerals, Gaëtan Gilbert, 05/14/2018
        Re: [Coq-Club] natural numbers as a datatype and as decimal numerals, Maxime Dénès, 05/14/2018
    - Re: [Coq-Club] natural numbers as a datatype and as decimal numerals, Li-yao Xia, 05/14/2018