理解 Coq 中“有根据的”证明

Question

我正在编写一个固定点，该固定点需要在每次迭代时将整数“朝向”零递增。这对于 Coq 来说太复杂了，无法自动识别为递减参数，我正在尝试证明我的固定点将终止。

我一直在复制（我相信是）标准库中 Z 上的阶跃函数的一个有根据的证明示例。 (Here)

Require Import ZArith.Zwf.

Section wf_proof_wf_inc.
  Variable c : Z.
  Let Z_increment (z:Z) := (z + ((Z.sgn c) * (-1)))%Z.

  Lemma Zwf_wf_inc : well_founded (Zwf c).
  Proof.
    unfold well_founded.
    intros a.
  Qed.

End wf_proof_wf_inc.

创建以下上下文：

  c : Z
  wf_inc := fun z : Z => (z + Z.sgn c * -1)%Z : Z -> Z
  a : Z
  ============================
  Acc (Zwf c) a

我的问题是这个目标实际上意味着什么？

我认为我必须为此证明的目标至少涉及我想要展示的具有“有根据的”属性“Z_increment”的阶跃函数。

我看过的最有用的解释是this，但我从未使用过它使用的列表类型，它也没有解释“可访问”等术语的含义。

Answer 1

基本上，你不需要做一个有根据的证明，你只需要证明你的函数减少了（自然数）abs(z)。更具体地说，您可以实现abs (z:Z) : nat := z_to_nat (z * Z.sgn z)（通过一些适当的转换为nat），然后将其用作Function 的度量，类似于Function foo z {measure abs z} := ...。

有根据的业务是为了证明关系是有根据的：这个想法是，您可以通过显示“减少”一些有根据的关系R 来证明您的函数终止（想想它为<);也就是说，f x 的定义只在R y x 时才进行递归子调用f y。要使其工作R 必须有充分的基础，这直观地意味着它没有无限下降的链。 CPDT 的 general recursion chapter 很好地解释了它是如何工作的。

这与您正在做的事情有什么关系？标准库证明，对于所有下界c，x < y 是Z 中的一个有根据的关系，如果另外它仅适用于y >= c。我认为这不适用于您 - 相反，您会趋向于零，因此您可以在 nats 上使用通常的 < 关系减少 abs z。标准库已经证明这种关系是有根据的，这就是Function ... {measure ...} 使用的。