允许 Coq 中潜在的无限循环

Question

我请求您的帮助，因为我想知道是否有可能允许在Coq中定义潜在的无限固定点，只是为了检查当前定义是否最终产生输出。

我已经尝试了新的Unset Guard Checking命令，我想精确禁用的是递减参数检查(因为我实际上有错误cannot guess decreasing argument of fix.

我知道在 Coq 中禁用此功能有点可惜，但这只是为了获得一个小的实用程序函数来检查当前定义是否正确，以确保提供递减参数将在进一步开发中起作用。

Answer 1

Unset Guard Checking确实禁用了递减参数检查。 您可能必须显式指定您希望系统使用类似此示例{struct foo}假定递减的参数。

Unset Guard Checking.
Fixpoint y {A} (f : A -> A) {struct f} : A := f (y f).

但是，如果您没有充分的理由，定义可能无限函数的更好方法是添加一个参数来强制终止。

Fixpoint y_opt {A} (lim : nat) (f : A -> A) : option A :=
match lim with
| O => None
| S lim' =>
match y_opt lim' f with
| None => None
| Some x => Some (f x)
end
end.