3

考虑以下固定点：

Require Import Coq.Lists.List.
Import ListNotations.

Inductive my_type: Type:=
| Left: my_type
| Right: my_type
.

Fixpoint decrease (which: my_type) (left right: list my_type) : list my_type :=
match which with
| Left =>
  match left with
  | [] => []
  | a::tl => decrease a tl right
  end
| Right =>
  match right with
  | [] => []
  | a::tl => decrease a left tl
  end
end.

Coq 拒绝以下固定点，因为它无法猜测递减的固定点（有时left列表会失去理智，有时它就是那个right）。

这个答案表明可以通过使用 aProgram Fixpoint并指定 a来解决这个问题{measure ((length left)+(length right))}。

我的问题是：

  • 普通Fixpoint和 a 和有什么不一样Program Fixpoint？
  • 是否可以在常规中显式减少参数Fixpoint？
  • 目标是什么Next Obligation？
4

1 回答 1

7

  • Coq 中的Fixpoint命令使用 Coq 的原语构造一个递归函数fix，它检查结构递归以确保终止。这是 Coq 中唯一的递归，所有其他技术最终都脱糖为fix某种类型的 a。

    Program Fixpoint是Program的一个特性，它允许用稍微扩展的语言编写定义，然后编译成 Coq 定义。Program Fixpoint接受任何递归函数，生成显示函数终止的适当证明义务（通过在每个递归子调用上减少其参数的某种度量），然后将定义和终止证明打包到结构上减少参数的 Coq 定义中。如果这听起来很神奇，它基本上是，但CPDT很好地解释了如何进行这种编码。

  • 是的，您可以添加{struct arg}注释以明确指定哪个参数在结构上递减: Fixpoint decrease (which: my_type) (left right: list my_type) {struct right} : list my_type。这对您的示例没有帮助，因为您的函数通常不会在结构上减少任何一个参数。所有原始fix构造都有一个struct注解，但 Coq 通常可以在您编写Fixpoint. 例如，这里是Nat.add：

    Nat.add = 
  fix add (n m : nat) {struct n} : nat :=
  match n with
  | 0 => m
  | S p => S (add p m)
  end : nat -> nat -> nat

  • Next Obligation你从with得到两种类型的目标Program Fixpoint：首先，每个子调用都有一个更小的参数（使用measure，“更小”是使用 < 在 nats 上定义的），第二，“更小的”关系是有根据的；也就是说，它没有越来越小的对象的无限下降序列。我不确定为什么Program Fixpoint不自动执行此操作Nat.lt，因为它应该知道相关定理。请注意，它Program具有比更一般的递归更多的功能，因此它也可以生成与这些功能相关的其他目标，具体取决于您编写的定义。

于 2017-12-14T15:45:16.463 回答