依赖参数的结构递归

前端之家收集整理的这篇文章主要介绍了依赖参数的结构递归前端之家小编觉得挺不错的,现在分享给大家,也给大家做个参考。
我正试着在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.

原文链接:https://www.f2er.com/javaschema/281975.html

猜你在找的设计模式相关文章