The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/15/2015 06:13 PM, Vilhelm Sjöberg wrote:
> On 2015-01-15 17:41, Jonathan Leivent wrote:
> > I would like to write a recursive function that takes 3 arguments: an 
> > element index (0-based), a count of elements, and a heterogeneous 
> > tuple containing (usually) that many elements - and have it return 
> > the indexed element of the tuple if it exists.  If the tuple doesn't 
> > contain the right number of elements, I don't care what the function 
> > does, and I don't want to provide a proof that the tuple contains the 
> > right number of elements.  The index < count - and if not, then I 
> > don't care what the function does.
> >
> > Notes: the tuple arg will be strictly right-associated.  If count =1, 
> > then the third arg is just an arbitrarily-typed singleton, and is the 
> > result itself.  If count>1, then the last element is the snd of the 
> > last pair, while all previous elements are the fst of some pair.
> >
> > I know how to do this when the container is homogeneous, as with 
> > lists or vectors - but not with hetero tuples.  I don't even know how 
> > to write the type of the function in this case.
> >
> > Also, I think I may have seen the solution to this somewhere - but 
> > don't remember where...  Was it in CPDT somewhere?
> >
> > Any clues on how to write this function?
>
> I guess your problem is that you can't write down the type "some tuple 
> with n components (of arbitrary types)". However, you can do something 
> similar, where instead of just the number of tuple components, you 
> give a list of the types in it.
>
> The below code differs a little from your definition of 
> right-associated tuple, because I made all the tuples end with a unit 
> value for simplicitly.
>
> There are some very similar functions in CPDT 
> (http://adam.chlipala.net/cpdt/html/DataStruct.html), but I can't find 
> this exact one.
>
>    Require Import List.
>
>    Fixpoint tupleType (ts : list Set) : Set :=
>       match ts with
>         | nil => unit
>         | t::ts => t * tupleType ts
>       end %type.
>
>    Fixpoint get (ts : list Set) : forall (i:nat), tupleType ts -> nth i
>    ts unit :=
>       match ts return forall (i:nat), tupleType ts -> nth i ts unit with
>       | nil => fun i v => match i with 0 => tt | S _ => tt end
>       | t::ts => fun i => match i
>                           with
>                             | 0 => fun v => fst v
>                             | S j => fun v => get ts j (snd v)
>                           end
>       end.
>
>    Eval compute in
>       get (nat::bool::nat::nil) 2 (1,(true,(42,tt))).  (* = 42 *)
>
> Vilhelm

That does look familiar.  However, how to get 'get' to infer the ts arg 
from the tuple?  As this doesn't work:

  get _ 2 (1, (true, (42, tt))).

-- Jonathan