coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Induction Principle

From: Matej Košík <mail AT matej-kosik.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Induction Principle
Date: Tue, 12 Jun 2018 14:22:36 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mail AT matej-kosik.net; spf=SoftFail smtp.mailfrom=mail AT matej-kosik.net; spf=SoftFail smtp.helo=postmaster AT matej-kosik.net
Autocrypt: addr=mail AT matej-kosik.net; prefer-encrypt=mutual; keydata= xsFNBFnmLGQBEACspBbw6ph3XMaOWbIcJr5VVE8n64CSAFd/+mLOYc7qCMm4L1xV8Nqlek7A /c1q6yzgrFL7mUKMJsFnt35grPdYb0jRWZxn7vy+iirAt3BTdK4NuPG2c/DO9bAGe5Qndtm5 eln4zlQPGkXDsHYn5jdHDKDJPoIKGp1pBBlc0P2xE43R1awX5hqQenJXC6qI/MQdS3PqZgEF pvXlw7lnQ8KeXl9rzTg8izpVDnhLVZSdKKmFqaCdbOepvCgsJIrImylx+QDB8xcpn/fqkJES pzvTVTjmc/FV+djJ1groVAOkRdelaIrSpdSDr5GUM35sx//hR+ncH5aL6o+OxjJdTrwjQsgC iBW7IjP5PqoTWxHvk7nFqYvbsZUgWLmpkmSbT4WP7hbIoNVqF8zhjK82hNP+ZEQGp0DrJBF1 D577tBXWwZep+qD2vYh/c93ONXYxEdOLX7LjhOj/ETS/jN4qKvbnX3FC97stJiozFy27lb07 ctWnhfyD5fsudWYxzUsUoFlU4NTlds4lpz6VIOlMch5EO7iTmPgSoFwDWrK6VrdwUcLDOf+6 tLRhWXdiIFsDfW2Oyq1z4zAqDGamW60Y5wwbXB4UirLOeml7MJ2G1Dl0ejs1k092uBYvTvUd LHZBDSPi5kZWUWUryXYFpDvKGLT+WZ6I6YQ3LlpbNxKK2hWD3QARAQABzSRNYXRlaiBLb8Wh w61rIDxtYWlsQG1hdGVqLWtvc2lrLm5ldD7CwY4EEwEIADgWIQQc1B0KUjGdx6vBt59Qr/oS jOSGSQUCWeYsZAIbIwULCQgHAgYVCAkKCwIEFgIDAQIeAQIXgAAKCRBQr/oSjOSGSURJEACd Sg/AOyCv6/yhLuzisU8XeELgc/jkkVs7eZ0AqNbZiKZde8VWszq8i4uCkbL43bkTEYM7msdv vmBwZJwYgCNqlIecJJxdmr6U/lxYICFnXyEdSiZKlH8IDZfIOYA+UbdSdmQGdYr6Wvjjn5uh FhVSf2uqM+xK9G/uzxyBLu8/gcb1YUTAkifbzzo7tMjMV0QpHh1x5tA0LbpOWFTc+HKFhMcA xX3qgF1gOumyh7ojYmNGz+Fj2RAQWqdBGaey70fbkTn1wQtyM7zOStPadE36T5aP/4oNA6oD YdhtFuNxz1kgroSPstfDEjgeq7ldIGRJNCQmujfEUDFNkfP94Rl82Zy/1treCw1Z2bqhUAYz ZxYadLFC84YoCm7VzTuwCPmUoNCpke+kFvDIvtYh80s1CbUkMNHHWV7SV+PkUVdNF1jZrTID VCsdjZepbbG/48u56TyV7fTdHX5kJcUz4qhxX34NTDT3Vm0LiVV2LiogVeUp1+GXc8ghvVvB 35s4JG9JOaN9sRki3VuTssVzL45cgwg4MFDCdHiwwKgiLD9HahXyOIyqzAH1YwnmCZdGz/l2 j4r7ZzADcD8YMXtNJ0XHITpfa15pAx3j3ihoXfFV7jl5mtYVy8P3QPy6LA4HaJhZO+11rVuC bH2WegIPjsheXQ+wucELg7TkwrlRq4fQOc7BTQRZ5ixkARAAuZorllJ3c5j0R0rbbs6OFwUW bM2If75vlI2go9WFJcwZjqWz58fmu3xQQiAKWA2UIdzoTBabBIsI8Yf3Djg5yZsxn+kMcLCC T1i7JIaZyfREvnEhcURYbBZX1qnOK1SvlThFgQ0CCbz7hiPYZSXQTsrAUhskxBTE8tNfTFB7 V+cpgNwWTy/rQyYqGHY1iMThDRhq8ImdpNKjnvq3V7+7aT0atBdHaIfIb4wHIACa7MbPOXwd MPaKqsfhuhxJwQP4OXZNDsAbXFKuaLGAcnjjIsnLYQrSXcy14CINOkaGCJ8ZUdxn8MeuWY27 tR7h/19D2U+0JjmyZ5GB0aUo8LahWCXLJ02vQEF4yWQfwgrjrPT9LM+VZOSqGzFwU4sbaLqN mD49N93bFK80v4Q8bxKKC3WPcnQdI/JHz6FdM53TT51IwyaRPansf5bfpU8DS0i3tf/Stq9D ic38VRLlZxbaWNmbTm+/iwxn6XDJ+VVFOVPdYHb07Ml7tl7eANpmkiBHD1z0JzGMvAWI04xv ZHpLjQG5GhSti2u6H1cE5htAxlUAGQ96yAxUHAW1up7x0+H9FJFuo9HV8toZWJZ5DrUEr4b6 70JW72lj/i/bE0IY6PvcJE7vAZG8kYHvHnKEbIsDtd41BLu13NBXNqFPcKTONLaU/ymECjqA FgCROkvidzEAEQEAAcLBdgQYAQgAIBYhBBzUHQpSMZ3Hq8G3n1Cv+hKM5IZJBQJZ5ixkAhsM AAoJEFCv+hKM5IZJ14sP/3AFubatbWs6MQD+K38zE9bkWavnO4vOkNh328OTV1/iqYBQ4lPS liQ0kljvNu06OUJ7dSoa0k5nWDZDaDkbxpm/+AGBJ+arUEr+VoMKVYOSb/LzyUxQH8uDQbqV lCtXQ1qObLa6b5zT7KCaa7AqDp5CDydqXtAWSu2nHr/41vd21gQEFu1J4K/VrzWvgn+GVMup +VVeXhWBzub+9z9d+q9g6Qi4s5ecXXcEhCWtEhG318tiDMjxT+yI+qWosOlvKjyeaEGFxy6N 9eOI6Ux6tlUiBuVL95X+Ce1/UF1I45Dzfx1KQXc6QQC0SS2r3d27S82MTL7P+XeUMwhm+l/V KHS47vJl9aKQU9mQTKABl5V3gLDN+tuIbOUQl56UY/BOtub4a+Q2e7PU3Ys9D9RJH6oiGnLm 8fsf0w3xUrNUmvSBt3eNQqAuBIs91YOkXj2e6obrA3WYOAc6sPqaHrIj9CpsBGGV3N9BFZB6 QxKjvUCCCFeVrbMmDWRp5+CnzmtE3n1NClu0UzEYvl+MTjXveWWm7a3QRgk0Nd9eqCFhh2R+ tNWpC0LFNJnAV4Ka+tRXmtdMDrVKi130vIA/gxhq0fWrHmYIEeJOHQlL70IYdw/blqdbAHxP MpNpB/ycoDv4xZrwmFOZVnLnwnV9iJF1bnLno5yp0f4FKplO9LpC/2/2
Ironport-phdr: 9a23:XIvizhFuXdAm47ZfVjVuSp1GYnF86YWxBRYc798ds5kLTJ78ocqwAkXT6L1XgUPTWs2DsrQY07eQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDqwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOSMn/mHZisJ+j6xVrxyuqBN934Hab5qYNOZ9c67HYd8WWWRMU8RXWidcAo28dYwPD+8ZMOhftYb9u0UBrRmjDgepA+PsxSFPhnzr1qA91uQuCwDG3Ag7EtILqnvUsMv6NKULXeC2y6nI1jTDb/BM1Tf79ofIbgksrPeRVrx+dsrRzFMgFwLDjliIs4PlOima1+UKs2id9eZvSeWvi2s/pwF1uDeg3d0siojTioIb0FDJ8zhyzoUtJdCgVUJ2bt6pHIFOuyyUM4Z6WMAvTm9ytCon1rELuYa3cDUIxZkk3RLSZOGLf5KM7x/jTuqdPzh1iGxjdbminRi961Kgxff5VsSs0FZFsC5Fkt7Uu3AIzRPT9taISvlk8kei3jaPzAHT6uJeLUAyi6XbN4Ytwr82lpUNrUTOBjL6lUr2gaOMaEkp9Oyl5/7kb7jovJOQKpN4hwHmPqQrgMO/AOA4MgYUX2ic/OSxzLjj8lf4QLVOlfA2l7PWsIzEKsQZv6K5AAhV0p0i6xa8FTum1soXnWUfIFJfZB2Hl5TpO03JIP3gEfi/hE2snC53yPDCI73uGY7ALmPDkbfkZbZy8VRQyAs1zdBF5pJbEKsNIPzpWhy5iNuNBRggdgew3uzPCdNn14pYV3jcLLWeNfb3uEOF5KoMJBsJZ8dBvT/8L9Ag7uLjjzo6nkQcfu+v0IdBOyPwJehvP0jMOSmkudwGC2pf5lNvHtyvs0WLVHtoX1j3Wqs94j8hD4f/UtXGT5yggvmC2zy6HdtQa3wUUQnQQ0etTJ2NXrI3UAzXOtVoy2NWULG9Ro1k1ha1tQy8zbd7fLKNp38o8Kn73d0w3NX90BE/8TstUJaY2n2ATSR3mXgJRHkw0bwt+kE=
Openpgp: id=1CD41D0A52319DC7ABC1B79F50AFFA128CE48649; url=http://matej-kosik.net/doc/kosik.asc

Hi,

https://www.labri.fr/perso/casteran/CoqArt/coqartF.pdf,
in Section 15.1.3 : Comment se construit le principe de récurrence

There is also an official english translation of the text
https://www.amazon.com/Interactive-Theorem-Proving-Program-Development/dp/3540208542
See Section 14.1.3 : Building the Induction Principle

On 06/12/2018 02:03 PM, Carmine Abate wrote:
> Hi everybody,
> can some-one tell me how does Coq write the term α_ind
> (and eventually α_rect) for a generic inductive type α, like the following?
>
> Inductive α (b₁ : B₁) .. (bᵤ : Bᵤ) : ∏_{ z₁ : Q₁ .. zₘ : Qₘ} s :=
> | c₁ : ∏_{x₁ : P₁₁ .. xₖ₁ : P₁ₖ₁} α (b₁ : B₁) .. (bᵤ : Bᵤ) M₁₁ .. M₁ₘ
> ...
> | cₙ : ∏_{x₁ : Pn₁ .. xₖₙ : P₁ₖₙ} α (b₁ : B₁) .. (bᵤ : Bᵤ) Mₙ₁ .. Mₙₘ

[Coq-Club] Induction Principle, Carmine Abate, 06/12/2018
- Re: [Coq-Club] Induction Principle, Pierre Courtieu, 06/12/2018
  - Re: [Coq-Club] Induction Principle, Carmine Abate, 06/12/2018
    - Re: [Coq-Club] Induction Principle, karsar, 06/12/2018
      - Re: [Coq-Club] Induction Principle, Carmine Abate, 06/12/2018
    - Re: [Coq-Club] Induction Principle, Ambrus Kaposi, 06/12/2018
- Re: [Coq-Club] Induction Principle, Matej Košík, 06/12/2018