The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

May I suggest writing tabulate in "proof style" and then look
at the generated code :

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) { struct n } :
Vec A n.
Proof.
  destruct n as [ | n ].
  exact (@vzero _).
  apply vcons.
  exact (f (fzero _)).
  exact (tabulate _ _ (fun x => f (fsuc _ x))).
Defined.

Print tabulate.

You get exactly what Jan-Oliver Kaiser wrote:

> 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.

More generally, with dependent pattern matching, using
tactics to design computational terms could give very
useful hints.

Best,

Dominique