对依赖参数的结构递归 [英] Structural recursion on a dependent parameter

问题描述

我正在尝试用Coq书写Eratosthenes的筛子。我有一个函数 crossout：forall {n：nat}，向量bool n-> nat->向量布尔n 。当筛子找到质数时，它会使用 crossout 标记所有非质数，然后递归到所得向量上。显然，筛子不能在向量本身上进行结构递归，但在向量的长度上可以进行结构递归。我想要做的是这样的事情：

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.

但是，如果我这样写，Coq抱怨 v的长度'不是 n 的子项。我知道是的，但是无论我如何构造函数，我似乎都无法说服Coq。有人知道我能怎么做吗？

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?

推荐答案

这是Coq中依赖类型最常见的陷阱之一。直观上发生的是，一旦在 v 上进行模式匹配，Coq就会忘记该向量的长度实际上是 n ，并且失去了 v'的长度与 n 的前身之间的联系。此处的解决方案是应用Adam Chlipala所谓的车队模式，并使模式匹配返回一个函数。虽然可以通过 v 上的模式匹配来实现，但我认为通过 n ：

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.

注意筛子的标题如何更改一点点：现在返回类型实际上是一个帮助Coq类型推断的函数。

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.

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

For more information, check out Adam's book: http://adam.chlipala.net/cpdt/html/MoreDep.html.

这篇关于对依赖参数的结构递归的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！