The Coq mailing list

[Sean Wilson <sean.wilson AT ed.ac.uk>]

Hi,

I have a couple of questions about programming in Coq that I cannot seem to 
work out. As an example of my issue, I want to program a list 'take' function 
that takes items n from the front of a list e.g. take [1,2,3] 1 = [1] and 
take [1,2,3] 2 = [1,2]. In ML, you might implement it with:

fun take (_, 0)    = [ ]
| take ([ ], _)    = raise Subscript
| take (h :: t, n) = h::take (t, n – 1) handle Overflow => raise Subscript

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.

The actual Coq term produced isn't very readable, so here is the extracted 
version:

let rec take x = function
  | O -> Nil
  | S n0 ->
      (match x with
         | Nil -> Nil
         | Cons (a, l) -> Cons (a, (take x n0)))
 
This is wrong: the last match clause should be Cons (a, (take l n0))). The 
counter is getting smaller each recursive call but the list is not. If I use 
"apply (cons a IHx)" instead, only the list gets smaller each call; I need 
both to get smaller for it to work but none of the terms in the hypothesis 
does this. I can get the result I want by using the refine tactic:

Definition take2 : forall (x:list nat) (n:nat), list nat.
refine (fix take2 (x:list nat) (n:nat) {struct n} : list nat := _).
(* Same as above up to the last line... *)
  apply (cons a (take2 x n)).
Qed.

Is there any way to get this result without using refine? I'd like to know if 
there was a way to do this.

Closer to the actual example I want to do is this, using a sigma type to 
constrain the value of the counter:

Definition take3 : forall (x:list nat) (n:{i:nat | i <= length(x)}), list nat.
refine (fix take2 (x:list nat) (n:{i:nat | i <= length(x)}) {struct n} : list 
nat := _).

destruct n as [n].
induction n.

  apply (nil:list nat).

  induction x.
  apply (nil:list nat). (* error *)

  (* Construct the counter term (with proof) for the recursive call *)
  assert({i : nat | i <= length x}).
  exists n.
  intuition.

  apply (cons a (take3 x H)).
Qed.

This is the same as the previous example with refine except there is a little 
more work in taking apart and building sigma type terms for the counter. 
However, I get an error at the Qed. Coq says:

Recursive call to take3 has principal argument equal to
"exist (fun i : nat => i <= length l2) n2
   (let H :=
      let H :=
        fun _ : n2 <= length l2 =>
        let H1 := F0 l2 (fun _ : n2 <= length l2 => l2) in l2 in
      F0 l2 H in
    lt_n_Sm_le n2 (length l2) l3)"
instead of a subterm of n

I suspect that this is because what I said was my structurally recursive 
parameter is not accurate. What I really want to say in the "refine" line is 
that take3 is structurally recursive on the first member of the pair that is 
n. I tried to do this with:

refine (fix take2 (x:list nat) (n:{i:nat | i <= length(x)}) {struct 
(proj1_sig 
n)} : list nat := _).

Coq gives this error:

"Syntax error: [Prim.name] expected after 'struct' (in [fixannot])"

How can I get this to work?

Any help would be greatly appreciated.

Regards,

Sean