我正试着在Coq中写下Eratosthenes的筛子.我有一个函数crossout：forall {n：nat},vector bool n – > nat – >矢量布尔当筛子找到一个素数时,它会使用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.
但如果我这样写,Coq抱怨v’的长度不是n的子项.我知道它是,但无论我如何构建函数,我似乎无法说服Coq它是.有谁知道我怎么做？
这是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.
注意筛子的标题是如何变化的：现在返回类型实际上是一个帮助Coq类型推断的函数.
有关更多信息,请查看Adam的书：http://adam.chlipala.net/cpdt/html/MoreDep.html.
