依赖参数的结构递归

Question

我正试图在Coq上写Eratosthenes的筛子。我有一个功能crossout : forall {n:nat}, vector bool n -> nat -> vector bool n。当筛子找到一个数字是质数时，它使用crossout来标记所有不是质数的数字，然后在结果矢量上递归。对于矢量本身来说，筛子显然不能在结构上递归，但它在矢量的长度上是结构递归的。我要的是做这样的事情：

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. 

但如果我把它写这样的，勒柯克抱怨的v'的长度不是n一个subterm。我知道这是事实，但不管我如何构造这个功能，我似乎都无法说服Coq。有谁知道我可以怎么做？

Answer 1

这是Coq中依赖类型最常见的陷阱之一。直观地发生的是，只要在v上匹配模式，Coq“忘记”该向量的长度实际上是n，并且丢失了长度为v'和前任n之间的连接。这里的解决方案是应用Adam Chlipala所谓的车队模式，并使模式匹配返回一个函数。虽然可以通过图案v匹配做到这一点，我认为这是比较容易通过图案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. 

通知sieve头是如何改变了一点点：现在的返回类型实际上是帮助Coq的类型推断的一个功能。

欲了解更多信息，检查亚当的书：http://adam.chlipala.net/cpdt/html/MoreDep.html。