The Coq mailing list

[karsar <karen.sarkisyan AT gmail.com>]

you may want to read CPDT chapter 

(http://adam.chlipala.net/cpdt/html/Cpdt.Subset.html)

for {_:_|_} subset types. 

For Fin (definition is from CPDT here, Coq.Vectors.Fin gives the same up to constructor names)

  Inductive fin : nat -> Set :=

  | First : forall n, fin (S n)

  | Next : forall n, fin n -> fin (S n).

So, we can construct terms of (fin 2) as (First 1) and (Next (First 0))

values of (fin 3) are (First 2), (Next (First 1)) and (Next (Next (First 0))

This way we get for fin 3 terms that may be associated with  1, 2 and 3.

Pay attention that terms of (fin 3) are different from terms of (fin 2). This is because

(fin 2) and (fin 3) are different types! So you don't pass (fin 2) terms to a function

which expects (fin 3) elements, although you may expect that according

to 'common sense' 2 belongs to both sets of  {1,2} and {1,2,3}.

Fin might be used if you define lists of given length and want to extract an element

by a given index. Knowing the length of the list you may use Fin n to ensure that

your index is never out of range.

Best,

Karen

On Wed, Jan 10, 2018 at 2:55 PM, Siddharth Bhat <siddu.druid AT gmail.com> wrote:

Thank you, that does help.

How does the set notation work? I haven't seen that before, that is cool.

Is there some place that uses Fin in some trivial way? Eg. Establishes a bijection with [1..n]? If not, I suppose I can stumble through :)

Thanks
Siddharth

On Wed 10 Jan, 2018, 11:36 ikdc, <ikdc AT mit.edu> wrote:

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

--

Sending this from my phone, please excuse any typos!