coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Question about inductive definitions

From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Question about inductive definitions
Date: Fri, 16 Feb 2018 10:57:27 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay4-d.mail.gandi.net
Ironport-phdr: 9a23:mLOTIx3/mMs10ZLHsmDT+DRfVm0co7zxezQtwd8ZseIfIvad9pjvdHbS+e9qxAeQG9mDsLQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPbQhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmlTkJNzA5/m/UhMJ/gq1UrxC9qBJw2IPUfIKYOeBicq/Bc94XR2xMVdtRWSxbBYO8apMCAesbMuFEs4nyvV0OogO/CwmtAOPg0SFHhmXq3aYn1OkhHhvJ0xI8H90UtnTYttr1NKYWUe+u0qbI1ynDYuhN2Tf+6InIaRMhofCJXbJ1b8XR01MjFwXbgVWMsIHoOS6e2OoKs2ie9eVgVOSvhnYnqwFrozij3N0shZfSho4Py1DE8z11wJwrKt2kUk57ZsKkH4VftiGGLIt6WMUiTH90uCs817YIuoa7cTAUxJg6xRPTcf6Kf5SS7h7+V+ucLy10iG9hdb++nxq+71KvxvHhWsSxzllHoCpIn9zPu38W1hHf982KReVj8kqhxTqC0g7T5+5FLE02kKfXNYItzaA+m5cWvknOEDT5l1vzgaKWeUgo5PWn5uL6abv8vJCcLZV7igTmP6QuhMO/BeM4PxAUX2eF/eSzzr3i8ELgTLpXlPE2l7PWsJHeJcgBqa62GQlV3Zsi6xqlCTepzsgYkWEGLFJDZh2Hk5DkN0/TLP36F/uygUignC12y/3FMLDtGIjBI3zCnbv5eLZy8U9cyA49zdBF4JJUD6kMIP3pVUDvqNzXFBk5Pxa7w+bmDNVyzZ0RWXiTAqKCK6PSsl+J5vksI+mNYY8VvSjyK+I/6/7ok3A5hUcRfbO10psPdHC4AvNmLl2Fbnrrm9cNCHsFvg4jTOPxk1CCSj5SZ3OqX60m/D07CYSmDZ3CRo+3mrCB0j27TdVqYTVNDUnJGnP1fa2FXe0NYWScOJxPiDsBAJeoyJMo0yaBtQvwxqB7Zr7b8yAEvJSl29lx7eDJiTkp9i1vDMWY1myXCWd5gjVbFHcNwKljrBklmR+42q9ijqkATI0B17ZySg4/cKXk4al/AtH2VBjGe47XGk2lU86lADQ0Q8h3xdISMR8kR4eSyyvb1i/vOIc70qSRDcVqoLnfzmPyJsN4xmyA0qQ93QF/H5l/cFa+j6s6zDD9Qo7El0LDyvSweKAVzXKI+CGGxGuK+k5RVgJxF6PIQSJHaw==

The destructors are different but equivalent, it should be possible to define each from the other.

Depending on your options (-indices-matter, universe cumulative inductive types) there can be subtle differences related to universe levels. I recommend not worrying about universes until and unless you get a related error.

Gaëtan Gilbert

On 16/02/2018 10:52, N. Raghavendra wrote:

Is it possible to write the definition

Inductive total (X : Type) (P : X -> Type) : Type
:= pair : forall (x : X) , (P x -> total X P).

without using parameters, that is, in the form

Inductive total : ... := ... ?

I tried

Inductive total : forall (X : Type) , (X -> Type) -> Type
:= pair : forall (X : Type) (P : X -> Type) (x : X) , P x -> total X P.

But the latter definition gives a destructor total_rect which is
different from the destructor total_rect given by the first definition.

Thanks,
Raghu.

--
N. Raghavendra
<raghu AT hri.res.in>,
http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/

[Coq-Club] Question about inductive definitions, N. Raghavendra, 02/16/2018
- Re: [Coq-Club] Question about inductive definitions, Gaëtan Gilbert, 02/16/2018
  - Re: [Coq-Club] Question about inductive definitions, N. Raghavendra, 02/16/2018