This is one of the most common pitfalls with dependent types in Coq. What is happening intuitively is that as soon as you pattern match on v
, Coq "forgets" that the length of that vector is actually n
, and loses the connection between the length of v'
and the predecessor of n
. The solution here is to apply what Adam Chlipala calls the convoy pattern, and make the pattern match return a function. While it is possible to do it by pattern matching on v
, I think it is easier to do it by pattern matching on n
:
Require Import Vector.
Axiom crossout : forall {n}, t bool n -> nat -> t bool n.
Fixpoint sieve {n:nat} : t bool n -> nat -> list nat :=
match n with
| 0 => fun _ _ => Datatypes.nil
| S n' => fun v acc =>
if hd v then
Datatypes.cons acc (sieve (crossout (tl v) acc) (S acc))
else
sieve (tl v) (S acc)
end.
Notice how the header of sieve
has changed a little bit: now the return type is actually a function to help Coq's type inference.
For more information, check out Adam's book: http://adam.chlipala.net/cpdt/html/MoreDep.html.