Coq dependent types

3
votes

I am new to Coq and need some help with some of trivial examples to get me started. In particular I am interested in defining some operations of vectors (fixed size lists) using dependent types. I started with Vector package and trying to implement some additional functions. For example I am having difficulty implementing trivial 'take' and 'drop' functions, which take or drop first 'p' elements from the list.

Require Import Vector.

Fixpoint take {A} {n} (p:nat) (a: t A n) : p<=n -> t A p := 
   match a return ( p<=n -> t A p) with
     | cons A v (S m) => cons (hd v) (take m (tl v)) m
     | nil => fun pf => a
   end.

The error (in case of nil) is:

The term "a" has type "t A n" while it is expected to have type "t A p".

Could somebody help me with some starting points? Thanks!

1
coqdependent-type
I don't know how to answer your question, but there's a good book that I bought a while back when I was thinking about getting serious about learning Coq. It's called, "Interactive Theorem Proving and Development." Also, this question might be better suited for cs.se, but I'm not sure. – Philip White
@PhilipWhite This isn't any more on-topic on Computer Science than here, as it's strictly about programming in Coq, and not about understanding the theoretical underpinnings. This question would be fine on Stack Overflow. – Gilles 'SO- stop being evil'
@krokodil -- this question is off-topic here, as it is not about cs theory. I can migrate your question stack overflow if you'd like. Otherwise, this question will be closed soon as off topic. – Lev Reyzin
Sorry for using wrong forum. Feel free to move to stack overflow. – krokodil

1 Answers

5
votes

I don't understand your approach. You're always returning a non-empty vector when the argument is a non-empty vector, but take must return nil when p=0 regardless of the vector.

Here's one approach to building take. Rather than using the hypothesis p <= n, I express the length of the argument n as a sum of the number p of elements to take and the number of trailing elements m, which is possible iff p <= n. This allows for an easier recursive definition, because (S p') + m is structurally equal to S (p' + m). Note that the discrimination is on the number of elements to take: return nil if taking 0, return cons head new_tail otherwise.

This version of the take function has the desired computational behavior, so all that's left is to define one with the desired proof content. I use the Program feature to do this conveniently: fill in the computational content (trivial, I just need to say that I want to use m = n - p), then complete the proof obligations (which are simple arithmetic).

Require Import Arith.
Require Import Vector.

Fixpoint take_plus {A} {m} (p:nat) : t A (p+m) -> t A p := 
   match p return t A (p+m) -> t A p with
     | 0 => fun a => nil _
     | S p' => fun a => cons A (hd a) _ (take_plus p' (tl a))
   end.
Program Definition take A n p (a : t A n) (H : p <= n) : t A p :=
          take_plus (m := n - p) p a.
Solve Obligations using auto with arith.

For your newdrop : forall A n p, t A n -> p <= n -> t A (n-p), the following approach works. You need to help Coq by telling it what p and n become in the recursive call.

Program Fixpoint newdrop  {A} {n} p : t A n -> p <= n -> t A (n-p) :=
   match p return t A n -> p <= n -> t A (n-p) with
     | 0 => fun a H => a
     | S p' => fun a H => newdrop p' (tl a) (_ : p' <= n - 1)
   end.
Next Obligation.
omega.
Qed.
Next Obligation.
omega.
Qed.
Next Obligation.
omega.
Qed.
Next Obligation.
omega.
Qed.

I don't know why Solve Obligations using omega. doesn't work but solving each obligation individually works.