recursion - 在 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.