依赖参数的结构递归

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

依赖参数的结构递归

相关文章