The Coq mailing list

[Martijn Vermaat <martijn AT vermaat.name>]

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

Thanks (again), I was clearly looking at this function the wrong way.
Although it doesn't make me look very good, it is great that is is
actually such a simple function :)

cheers,
Martijn