coq - 减少参数(以及什么是程序固定点)

考虑以下修复点：

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之一）。

此answer表明，可以通过使用Program Fixpoint并指定{measure ((length left)+(length right))}来解决此问题。

我的问题是：


常规Fixpoint和Program Fixpoint有什么区别？
是否可以在常规Fixpoint中显式减少参数？
Next Obligation的目标是什么？

最佳答案

Coq中的Fixpoint命令使用Coq的原始fix构造一个递归函数，该函数检查结构递归以确保终止。这是Coq中唯一的递归，所有其他技术最终都将糖降级为某种fix。

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和Program Fixpoint中获得两种目标：第一，每个子调用都有一个较小的参数（使用measure，“ Program Fixpoint不会自动对Nat.lt执行此操作，因为它应该知道相关的定理。请注意，Program具有更多功能，而不仅仅是更一般的递归，因此它还可以生成与这些功能相关的其他目标，具体取决于您编写的定义。