在 Coq 中扩展递归函数

Question

背景

我知道 Iota 缩减用于 reduce/expand 递归函数。例如，给定以下简单递归函数的应用（自然数的阶乘）：

((fix fact (n:nat):nat := match n with | O => 1 | S m => n * fact m end) 2)

Iota 缩减扩展了递归调用，有效地迭代了一次递归函数：

Eval lazy iota in ((fix fact (n:nat):nat := match n with | O => 1 | S m => n * fact m end) 2).
 = (fun n:nat =>
    match n with
    | 0 => 1
    | S m =>
        n *
        (fix fact (m : nat) : nat :=
           match m with
           | 0 => 1
           | S m0 => m * fact m0
           end) m
    end) 2.

这种行为可以很好地概括为相互递归函数。例如，给定以下相互递归函数定义：

Fixpoint even (n:nat):Prop := match n with | O => True | S m => odd m end
  with odd (n:nat):Prop := match n with | O => False | S m => even m end.

Iota 缩减将正确地扩展递归调用分别为偶数或奇数。要看到这一点，请考虑：

Theorem even_2 : even 2.
1 subgoal
==========
even 2
> lazy delta.

1 subgoal
==========
(fix even (n:nat):Prop := match n with ... end
 with odd (n:nat):Prop := match n with ... end
 for even) 2
> lazy iota.

1 subgoal
==========
(fun n:nat =>
  match n with
    | O => True
    | S m => (fix even (o:nat):Prop := match o with ... end
              with odd (o:nat):Prop := match o with ... end
              for odd) m
  end) 2

问题

这显然是正确的行为。 不幸的是，而且显然令人费解的是，在递归函数未应用于参数或参数被普遍量化的情况下，Coq 不会应用 Iota 归约。例如，以下内容不起作用：

Theorem even_n : forall n:nat, even n.
1 subgoal
==========
forall n:nat, even n
> intro n.

1 subgoal
n : nat
==========
even n
> lazy delta.

1 subgoal
==========
(fix even (n:nat):Prop := match n with ... end
 with odd (n:nat):Prop := match n with ... end
 for even) n
> lazy iota. (* FAILS TO REDUCE! *)

1 subgoal
==========
(fix even (n:nat):Prop := match n with ... end
 with odd (n:nat):Prop := match n with ... end
 for even) n

我看不出有任何理由说明为什么 Iota 缩减应该取决于周围的上下文，并且已经尝试了上述的多种变体，试图让 Coq 到 Iota reduce 递归函数。不幸的是没有任何效果。

我如何让 Coq 将 Iota 归约应用于未应用于任何参数或应用于通用量化参数的递归函数？

任何帮助将不胜感激。谢谢， -拉里

Answer 1

这里的问题是 iota 规则仅限于定点：Coq manual 明确指出如果递减参数以构造函数开头，iota 只能应用于定点。

这样做是为了确保归纳构造的微积分作为重写系统进行强烈规范化：如果我们始终可以应用 iota，那么就有可能无限地扩展被定义函数的递归出现。

在实践中，如果你想简化这样一个固定点，你可以做两件事：

手动销毁递归参数（n，在你的例子中）然后减少。这在某些情况下更简单，但需要您考虑很多情况。
证明简化引理并重写而不是减少。例如，您可以证明形式为 odd n <-> ~ even n 的引理，这在某些情况下可能对您有所帮助。您还可以将展开明确地证明为引理（这次，使用您对 even 的原始定义）：
```
Goal forall n, even n = match n with | O => False | S m => odd m end.
now destruct n.
Qed.
```

在 Coq 中扩展递归函数

Expanding Recursive Functions In Coq

computer-science

lambda-calculus

theorem-proving

coq

背景

问题