我正在编写一个固定点，它要求在每次迭代时将整数递增“趋向”零。这对于 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但我从未使用过它使用的列表类型，并且它没有解释“可访问”等术语的含义。
最佳答案
基本上，你不需要做有根据的证明，你只需要证明你的函数减少了(自然数)abs(z)。更具体地说，您可以实现 abs (z:Z) : nat := z_to_nat (z * Z.sgn z) (适当转换为 nat)然后将其用作 Function 的度量，类似于 Function foo z {measure abs z} := ... .
The well founded business is for showing relations are well-founded:这个想法是你可以通过展示它“减少”一些有根据的关系来证明你的函数终止R (将其视为 < )；即 f x 的定义进行递归子调用 f y仅当 R y x .为此工作 R必须是有充分根据的，这直观地意味着它没有无限下降的链。 CPDT 的 general recursion chapter很好地解释了这是如何工作的。
这与您的工作有什么关系？标准库证明，对于所有下界 c , x < y在 Z 中是一个有根据的关系如果另外它仅适用于 y >= c .我不认为这适用于你 - 相反你走向零，所以你可以减少 abs z与通常的<关于 nat 的关系秒。标准库已经证明这种关系是有根据的，这就是Function ... {measure ...}。用途。
关于theory - 了解 Coq 中的 "well founded"证明，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/50204730/