The Coq mailing list

["Terrell, Jeffrey" <jeffrey.terrell AT kcl.ac.uk>]

Thanks everyone.

Regards,
Jeff.

Sent from my iPhone

> On 15 Sep 2017, at 09:38, Dominique Larchey-Wendling 
> <dominique.larchey-wendling AT loria.fr>
>  wrote:
> 
> 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
>