3

我正在尝试在 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.

但如果我这样写，Coq 会抱怨长度v'不是n. 我知道它是，但无论我如何构造函数，我似乎都无法说服 Coq 它是。有谁知道我该怎么做？

4

1 回答 1

4

这是 Coq 中依赖类型最常见的缺陷之一。直观上发生的事情是，一旦您对 进行模式匹配v，Coq 就会“忘记”该向量的长度实际上是n，并失去 的长度v'和 的前任之间的联系n。这里的解决方案是应用 Adam Chlipala 所谓的convoy 模式，并使模式匹配返回一个函数。虽然可以通过模式匹配来做到这一点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 类型推断的函数。

有关更多信息，请查看 Adam 的书：http ://adam.chlipala.net/cpdt/html/MoreDep.html 。

于 2013-06-06T13:48:59.677 回答