The Coq mailing list

["Brian E. Aydemir" <baydemir AT cis.upenn.edu>]

On Dec 5, 2006, at 9:14 AM, 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. 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.

I think the following works.

(* *** *)
Definition take : forall (n:nat) (x:list nat), list nat.
  intros n; induction n.
  (* n = 0 *)
  intros; exact nil.

  (* n = S m, for some m *)
  intros x; case x.

    (* x = nil, shouldn't happen *)
    exact nil.

    (* x = z :: zs *)
    intros z zs.
    exact (z :: IHn zs).
Defined.
Extraction take.
(*
let rec take n x =
  match n with
    | O -> Nil
    | S n0 ->
        (match x with
           | Nil -> Nil
           | Cons (z, zs) -> Cons (z, (take n0 zs)))
*)
(* *** *)

The main difference is where the (x:list nat) gets quantified.  You  
want an induction hypothesis here that works for any list, not some  
particular fixed one.  This requires that the list be quantified in  
the goal when you perform the induction.



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

I think the following does what you want for this version.   
Admittedly, I used refine, but only because I didn't feel like  
building up the "sigma term" by hand.  Here, it made more sense to me  
to define the function by induction on x and then use what I know  
about x in each case to learn something about n, since n depends on x  
and not the other way around.

(* *** *)
Definition take3 : forall (x:list nat) (n:{i:nat | i <= length(x)}),  
list nat.
  intros x; induction x as [ | x xs IH ].

  (* case: nil *)
  intros; exact nil.

  (* case: cons x xs *)
  simpl.
  intros (i, pf). induction i as [ | i' _ ].

    (* subcase: i = 0 *)
    exact nil.

    (* subcase: i = S i' *)
    assert (i' <= length xs). auto with arith.
    refine (x :: IH _). exists i'. exact H.
Defined.
Extraction take3.
(*
let rec take3 l n =
  match l with
    | Nil -> Nil
    | Cons (a, l0) ->
        (match n with
           | O -> Nil
           | S n0 -> Cons (a, (take3 l0 n0)))
*)
(* *** *)

Hope that helps,
Brian