减少参数(以及什么是程序修复点)

Question

考虑以下修复点:

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).

这个答案表明,人们可以通过使用Program Fixpoint和指定一个来解决这个问题{measure ((length left)+(length right))}.

我的问题是:

• 常规Fixpoint和Program Fixpoint？之间有什么区别？
• 是否有可能在常规中明确减少参数Fixpoint？
• Next Obligation目标是什么？

Answer 1

• FixpointCoq中的命令使用Coq原语构造递归函数fix,该原语检查结构递归以确保终止.这是Coq中唯一的递归,而所有其他技术最终fix都是某种类型的desugar .

  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:第一,每个subcall具有较小的参数(使用measure,"较小的"是使用<NATS上定义的),以及第二,在"较小"的关系是有充分理由; 也就是说,它没有无限下降的越来越小的对象序列.鉴于它应该知道相关定理,我不确定为什么Program Fixpoint不自动执行此操作Nat.lt.请注意,Program除了更一般的递归之外,它还具有更多功能,因此它可以生成与这些功能相关的其他目标,具体取决于您编写的定义.