coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Type for finite set of naturals [1..N]?

From: Siddharth Bhat <siddu.druid AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Type for finite set of naturals [1..N]?
Date: Wed, 10 Jan 2018 05:58:08 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=siddu.druid AT gmail.com; spf=Pass smtp.mailfrom=siddu.druid AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f174.google.com
Ironport-phdr: 9a23:ky4poRXmlUEAtZJtotrQGjs4ccnV8LGtZVwlr6E/grcLSJyIuqrYYxSBt8tkgFKBZ4jH8fUM07OQ7/i5HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba9vIBmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W7YisJ+gqFVrg+/qRNj2IPbep2ZOeBkc6/BYd8XR2xMVdtRWSxbBYO8apMCAfcAPelFsob9p0EBrQGiBQmsGeji1z9IiWXq3aYn1OkhCgDG0xE9ENITqnjbsc/1NLoTUe+o16TIwjDDYOlX2Tf58oTHbhchofSVUL92bMHfylEvGhvbglmMrYHpJTCY2+QXv2SF8uZtVPijh3Mlpgx+pDWk290ihZPTho0Pz1DJ7SV5z5gxJd2/UEN7ZMSrEJpUty2DLot2Xt8uT3hmuConyLALtoS3fCcNyJQgyB7fb+KIf5KU7RLkUeadOTZ4hHR7d7Kjnxu+71Ssx+nmWsS30FtGtDRJnsTNu3wXyhDe6MeKRuN4/ki72DaP0w7T6vtDIUAxjafbMJ8hzaMtmZoOq0jMAzX2mFj3jKCLbUgk9e2o5P7mYrXivJOTK4h0igTmPqQ0hsO/Gfg4MhQJX2WD5eu806Tj8VTlT7VOk/05ibLUsIvaJMQevq62GRVZ0ocl6xalDjepys4UnXcdLAENRBXShI/wflrKPfrQDPGlgl3qni046erBO+jaA5nBLnHZjLepV7Z09wYI0ws/wc0Z64hJC70pL/f6W0u3v9vdWExqezeoyvrqXY0unrgVXniCV/eU

Hello all, I'm looking for a type that encodes the fact that its inhabitants are naturals from 1 to N.

I believe Fin is the type I am looking for? I'm not sure what Fin represents, exactly. Does Fin act as a witness for the *entire interval* [1..n]? Or can it witness some k \in [1..n]?

Ideally. There would be a type (forall n : nat), "T n" whose inhabitants can be put in bijection with [1..n]

Thanks

Siddharth

Sending this from my phone, please excuse any typos!

[Coq-Club] Type for finite set of naturals [1..N]?, Siddharth Bhat, 01/10/2018
- Re: [Coq-Club] Type for finite set of naturals [1..N]?, ikdc, 01/10/2018
  - Re: [Coq-Club] Type for finite set of naturals [1..N]?, Siddharth Bhat, 01/10/2018
    - Re: [Coq-Club] Type for finite set of naturals [1..N]?, karsar, 01/10/2018
    - Re: [Coq-Club] Type for finite set of naturals [1..N]?, Dominique Larchey-Wendling, 01/10/2018