The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>]

On Mon, Dec 04, 2006 at 09:45:50PM +0000, Sean Wilson wrote:

> You can write a similar version directly in Coq, but I'm interested in how 
> to 
> write it using only the tactic language (I find this easier when I need to 
> use dependently typed terms). Here is one of my attempts:
> 
> Definition take : forall (x:list nat) (n:nat), list nat.
> intros.
> induction n.
> 
>   apply (nil:list nat). (* Counter is zero *)
> 
>   induction x.
>   apply (nil:list nat).(* This case shouldn't happen; return nil by default 
> *)
> 
>   apply (cons a IHn). (* Recursive call *)
> Qed.
> 

Two points in addition to Benjamin's answer: 

First, the easiest way to get the right generalisation of x is ... to
swap the order of n and x in the signature of take. If this order
of parameters is crucial, you can define later a 
 take_rightorder x n := take n x.

Secondly, building via tactics such a function whose final type is not
dependent (list nat, nat, etc) is higly error-prone: There is always
the temptation to take a shortcut like "apply nil" or "apply IHn", and
as soon as the type is right, Coq can't pinpoint the mistake for
you. So my advice is: if you want to use tactics, let's prove a few
things on the way... For instance, your function take may become:

Require Import Arith.
Require Import Min.
Require Import List.

Definition take : forall (n:nat)(x:list nat), 
  { y : list nat | length y = min n (length x) /\ exists z, x = y++z}.
Proof.
induction n.
 
  exists (nil:list nat).
   (* start justification *)
   split; simpl; auto.
   exists x; auto.
   (* end justification *)
 
  destruct x as [ | a l ].   (* btw, no induction needed here *)

   exists (nil:list nat).
    (* start justification *)
    split; simpl; auto.
    exists (nil:list nat); auto.
    (* end justification *)

   destruct (IHn l) as [y Hy].
   exists (a::y).
    (* start justification *)
    split; simpl; intuition.
    destruct H0 as [z Hz].
    exists z; simpl; subst l; auto.
    (* end justification *)
Qed.

Extraction take. (* produce back your desired pure function *)


Best regards, 
Pierre Letouzey

PS: Can somebody explain to me why firstorder isn't able to solve
goals like: 

exists z : list nat, x = z 

or 

exists z : list nat, nil = z

??