The Coq mailing list

[Jan-Oliver Kaiser <janno AT mpi-sws.org>]

The easiest way I know to make Coq notice the correct type of f is this:

Fixpoint tabulate (n : nat) (A : Set) (f : Fin n -> A) : Vec A n :=
  match n as n0 return (Fin n0 -> A) -> (Vec A n0) with
  | 0 => fun _ => vzero A
  | S m => fun f => vcons A m (f (fzero m)) _
  end f.

Or, more succinctly:
Fixpoint tabulate (n : nat) (A : Set) : forall (f : Fin n -> A), Vec A n :=
  match n as n0 return (Fin n0 -> A) -> (Vec A n0) with
  | 0 => fun _ => vzero A
  | S m => fun f => vcons A m (f (fzero m)) _
  end.

I don't know how to complete the definition, though.

Best,
Janno

On 09/15/2017 08:49 AM, Terrell, Jeffrey wrote:
> Hi,
>
> In the second branch of the match statement below, I expected f to be of type Fin 
> (S m) -> A. However, it’s reported to be of type Fin n -> A.
>
> Inductive Fin : nat -> Set :=
>    fzero : forall n : nat, Fin (S n) |
>    fsuc : forall n : nat, Fin n -> Fin (S n).
>
> Inductive Vec (A : Set) : nat -> Set :=
>    vzero : Vec A 0 |
>    vcons : forall n : nat, A -> Vec A n -> Vec A (S n).
>
> Fixpoint tabulate (n : nat) (A : Set) (f : Fin n -> A) : Vec A n :=
>    match n as n0 return (Vec A n0) with |
>      0 => vzero A |
>      S m => vcons A m (f (fzero m)) ...
>    end.
>
>  From a purely syntactic point of view, I can see why this is the case. 
> However, I’m not sure how to obtain a function of the required type to apply 
> to (fzero m).
>
> Regards,
> Jeff.