The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Martijn Vermaat wrote:
> In the definitions of functions on vectors such as take, drop, and nth,
> we would use proofs of 'le' ord 'lt', e.g.:
>
>    Definition vtake (n m : nat) : n<= m ->  vector m ->  vector n.
>
> But unfortunately, we cannot deconstruct the proof of n<= m since it
> lives in Prop. Now, my guess is that there is no real solution to this
> problem, but then again, I'm still quite new to Coq.

This is actually pretty easy to do.  You just need to find a decidable 
alternative to the predicate you're using.  The proof then only comes 
into the picture to derive contradictions.

Require Import Omega.

Definition vtake (n m : nat) : vector m -> n <= m -> vector n.
  refine (fix vtake (n m : nat) : vector m -> n <= m -> vector n :=
    match n return vector m -> n <= m -> vector n with
      | O => fun _ _ => vnil
      | S n' => match m return vector m -> S n' <= m -> vector (S n') with
                  | O => fun _ _ => False_rect _ _
                  | S m' => fun v _ => vcons (vhead v) (vtake n' m' 
(vtail v) _)
                end
  end); omega.
Defined.