The Coq mailing list

[Benjamin Gregoire <Benjamin.Gregoire AT sophia.inria.fr>]

Sean Wilson wrote:

> 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. 
  Your script is wrong.
  What you want is the following induction hypothesis: 
         IHn: forall (l:list nat), list nat.  (* and not IHn: list nat. *)
  To do so (using the induction tactic) you should first generalize l 
(i.e. x) before the induction :

    Definition take1 : forall (l:list nat) (n:nat), list nat.
     intros l n.
     generalize l;clear l;induction n.
     exact (fun l => @nil nat).
     intros [|a l].
     exact (@nil nat).
     exact (a::IHn l).
   Defined.
  Print take1.
If you prefere a more "readable" version use the following script :

 Definition take2 : forall (l:list nat) (n:nat), list nat.
   fix take_rec 2.
   intros l [|x].
   exact (@nil nat).
   destruct l as [|a l].
   exact (@nil nat).
   exact (a::take_rec l x).
 Defined.
 Print take2.

 If you prefer the first script and but you whant a more readable 
version :
   Definition take3 := Eval cbv beta delta [take1 nat_rect nat_rec] 
zeta in take1.
   Print take3.

 Remark that this version is not exactly what you expect.

> 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.
>
>  
  The fix tactic.

> 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
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>