在Coq中允许潜在的无限循环。

Question

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

我已经尝试了新的 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.