coq - 如何让 Coq 接受以下 Fixpoint？

Question

我正在尝试为 lambda 演算编写一个替换函数，并且在递归调用 e 上的替换之前，如果是 lambda 抽象 (\x.e)，我必须重命名 e 中的变量。我如何在 Coq 中表示这种逻辑？

下面是一个最低限度的示例，Coq 给出了无法猜测递减参数的错误。在简化的替换中，为什么 Coq 不能让 e 保持相同的电感大小？

Fixpoint replace (x: nat) (y: nat) (e: exp): exp := e.

Fixpoint substitute (x: nat) (t: exp) (body: exp): exp :=
match body with
| Abs xp e => Abs 0 (substitute x t (replace x 0 e))
| _ => Unit
end.

实际替换看起来像这样

Fixpoint replace (x: nat) (y: nat) (e: exp): exp :=
match e with
| Val => Val
| Var xp => if beq_nat x xp then Var y else e
| Ref f => Ref (replace x y f)
| Abs xp bd => Abs xp (replace x y bd)
| App e1 e2 => App (replace x y e1) (replace x y e2)
| Deref f => Deref (replace x y f)
| Loc l => Loc l
| Assign e1 e2 => Assign (replace x y e1) (replace x y e2)
| Unit => Unit
end.

Answer 1

一般来说，Coq 不会接受 f(x) = f(g(x) 的子项) 形式的递归固定点。当然，这是有道理的，因为 g 可能是一个增加项大小的函数。

一般来说，解决方案是找到终止措施，而不是 Fixpoint 使用的简单“是子术语”。在这里，您可以定义一个函数 height : exp -> nat，对于叶节点，该函数为 0，否则为子树的 max。 Coq 有几种基于这种度量来定义终止函数的方法，例如Program Fixpoint 和 Function，或者您甚至可以手动定义一个 Fixpoint，它采用一个表示高度界限的附加参数(如果该参数曾经达到，则返回一个虚拟值) 0)。程序 Fixpoint 将为您提供证明义务，证明每次递归调用测量值都会减小，并证明您需要证明 replace 保留高度的引理。

在替换的特定情况下，您可以尝试的另一个技巧是定义一个函数来应用多重替换(从变量映射到表达式)，而不是一个函数来替换单个变量。这样，在 Abs 情况下，您可以将重命名添加到要应用的替换中，而不是直接执行，然后该函数在结构上是递归的。