The Coq mailing list

[Vilhelm Sjöberg <vilhelm AT cis.upenn.edu>]

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