coq - 在 Coq 中定义参数化的 Fixpoint

Question

我试图在 Coq 中定义一个固定点，其中一个函数定义通过参数引用另一个函数定义，但我遇到了一些令人困惑的错误。

我已将定义最小化为:

Require Import Coq.Init.Notations.
Require Import Coq.Init.Datatypes.

Inductive Wrapper (T : Type) :=
  | Wrap : T -> Wrapper T
  .
Inductive Unwrapper :=
  | Empty : Unwrapper
  | Unwrap : Wrapper Unwrapper -> Unwrapper
  .

Fixpoint Unwrapper_size (u : Unwrapper) {struct u} : nat :=
  match u with
  | Empty => O
  | Unwrap w => Wrapper_size w
  end

with Wrapper_size (w : Wrapper Unwrapper) {struct w} : nat :=
  match w with
  | Wrap _ t => Unwrapper_size t
  end.

这会导致此错误:

Recursive definition of Wrapper_size is ill-formed.
In environment
Unwrapper_size : Unwrapper -> nat
Wrapper_size : Wrapper Unwrapper -> nat
w : Wrapper Unwrapper
t : Unwrapper
Recursive call to Unwrapper_size has principal argument equal to
"t" instead of a subterm of "w".
Recursive definition is:
"fun w : Wrapper Unwrapper =>
match w with
| Wrap _ t => Unwrapper_size t
end".

在这里，t显然是 w 的子项— w就是我们要匹配的 t ，但 Coq 不接受。这里有什么错误，我该如何解决它？

Answer 1

假设您还在其他参数上使用Wrapper。然后，您需要打破相互递归并使函数与数据类型“并行”。所以你想写Wrapper_size: Wrapper T -> (T -> nat) -> nat。

然后你可以在 Unwrapper_size 中使用 Wrapper_size Unwrapper_size:Coq 应该在终止检查中进行足够的内联以识别这是安全的。

在此示例中，手动内联也很容易:Unwrapper_size 将匹配 Unwrap (Wrap _ t) 并在 t 上递归>.