coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: ikdc <ikdc AT mit.edu>
To: coq-club AT inria.fr, Siddharth Bhat <siddu.druid AT gmail.com>
Subject: Re: [Coq-Club] Type for finite set of naturals [1..N]?
Date: Wed, 10 Jan 2018 01:06:03 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=ikdc AT mit.edu; spf=Pass smtp.mailfrom=ikdc AT mit.edu; spf=None smtp.helo=postmaster AT dmz-mailsec-scanner-5.mit.edu
Ironport-phdr: 9a23:+S9vPRZ+E0PjBZ0mfGfgyET/LSx+4OfEezUN459isYplN5qZocWzbnLW6fgltlLVR4KTs6sC17KP9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCagbb9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjAk7m/XhMx+gqFVrh2vqBNwwZLbbo6OOfpifK7QZ88WSXZPU8tTUSFKH4Oyb5EID+oEJetYror9qEYSohCjAgSsBeDvxSJUiXLt2K060vghHRvY0wM9AtIDqXLZp8j2OqcKSe250arFwS/BYv9M2Drw65LEfx4urP2UQL59ctDdxVQsGg7BlFmdrY/oMyma2+kNtWWQ8vBuWvi1i2E9rgF8ujivydkoionOno8a11XE9CRgzIYwP9K4SUp7YcW6H5RMri2aLJd5TdkkQ2Fupik60KQKtJ6hcCgPyZQn2wTTZOKafIiV+h7jVeCRLilkhH99Zb6yhAy+/Eq6xuD9VcS4ylhHoyVdntnJrH8N1hjT6sadSvt6+0eswTeP1wPO5e5YOk00kKvbK4I7zrEui5UTrFzPHjXql0XukK+WakIk9/C05OTge7Xqv4OTN4tpig7lKakugcy+AeEgMgcURWSb+OK81Kfi/ULjWrlKgOc2weHlt8XRIt1eraqkCSdU1Jwi4lCxFXPu69UUkXkONk5FMDiHhpShb0rPLPzlS/ulnlWguDhuzvHCeLbmB8OeAGLEleLgfrp2oxpdywY45dVe+9RZBqxXc6G7YVP4qNGNVkxxCAez2euyUNg=

On 01/10/2018 12:58 AM, Siddharth Bhat wrote:

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

Fin N is indeed such a type. The two constructors represent the following:
- Fin (N + 1) has one element for each element of Fin N
- as well as one extra element

Hopefully that explains its definition.

I believe it is isomorphic to the type { n : nat | n < N } (or alternatively { n : nat | 0 < n /\ n <= N }) which may be easier to work with depending on what you're trying to do.

ikdc

[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