在 Coq 中定义一个参数化的 Fixpoint答案

【问题标题】：Defining a parameterised Fixpoint in Coq在 Coq 中定义一个参数化的 Fixpoint
【发布时间】：2018-11-22 11:06:45
【问题描述】：

我试图在 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 不接受它。这里有什么错误，我该如何解决？

【问题讨论】：

你的代码很可疑：唯一的base case返回0，对nat没有任何操作。所以如果它终止它只返回 0。这可能不是你想要的。
是的，我已将定义最小化以使其更清晰易读。我的实际用例不那么空洞，但它只会给问题增加更多噪音。（您可以想象实际上递增递归调用的结果以生成更有用的函数。）
正如有人在 IRC 上所说，对于当前示例，“尝试将 wrapper 和 unwrapper 定义为相互感应”，给出Inductive Wrapper := Wrap: Unwrapper -> Wrapper with Unwrapper：Coq 的“subterm”概念假设您的递归遵循数据类型的结构.我想这对原始版本没有帮助，但是最好有一个这样的例子不起作用。我确实有另一个想法......
如果你还包装了其他东西，那么你需要打破相互递归并使函数与数据类型“并行”。所以写Wrapper_size: Wrapper T -> (T -> nat) -> nat. 然后我会尝试在Unwrapper_size 中使用Wrapper_size Unwrapper_size：Coq 可能会在终止检查中做足够的内联来识别这是安全的。（在这个例子中，手动内联也很容易：Unwrapper_size` 将匹配 Unwrap (wrap t) 并递归 t）。
如果所有其他方法都失败了，总有有根据的归纳法，但它很烦人，我会尽量避免它。

标签： coq

【解决方案1】：

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

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

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

【讨论】：