gpt4 book ai didi

theory - 了解 Coq 中的 "well founded"证明

转载 作者:行者123 更新时间:2023-12-02 00:34:36 26 4
gpt4 key购买 nike

我正在编写一个固定点,它要求在每次迭代时将整数递增“趋向”零。这对于 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 < yZ 中是一个有根据的关系如果另外它仅适用于 y >= c .我不认为这适用于你 - 相反你走向零,所以你可以减少 abs z与通常的<关于 nat 的关系秒。标准库已经证明这种关系是有根据的,这就是Function ... {measure ...}。用途。

关于theory - 了解 Coq 中的 "well founded"证明,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/50204730/

26 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com