coq - Structural recursion on a dependent parameter

Question

I'm trying to write the sieve of Eratosthenes in Coq. I have a function crossout : forall {n:nat}, vector bool n -> nat -> vector bool n. When the sieve finds a number that is prime, it uses crossout to mark all the numbers that are not prime and then recurses on the resulting vector. The sieve obviously can't be structurally recursive on the vector itself, but it is structurally recursive on the length of the vector. What I want is to do something like this:

Fixpoint sieve {n:nat} (v:vector bool n) (acc:nat) {struct n} : list nat :=
  match v with
    | [] => Datatypes.nil
    | false :: v' => sieve v' (S acc)
    | true :: v' => Datatypes.cons acc (sieve (crossout v' acc) (S acc))
  end.

But if I write it like this, Coq complains that the length of v' is not a subterm of n. I know that it is, but no matter how I structure the function, I can't seem to convince Coq that it is. Does anyone know how I can?

Answer 1

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.