在 Coq 中扩展递归函数

Question

背景

我了解 Iota 缩减用于缩减/扩展递归函数。例如，给定以下简单递归函数的应用（自然数的阶乘）：

((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 缩减递归函数。不幸的是，没有任何效果。

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

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

Answer 1

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

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

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

1. 手动销毁递归参数（n，在您的情况下），然后减少。这在某些情况下比较简单，但需要您考虑很多情况。

2. 证明简化引理并进行重写而不是归约。例如，您可以证明odd n <-> ~ even n 形式的引理，这在某些情况下可能对您有所帮助。您还可以将展开明确地证明为引理（这一次，使用您对 even 的原始定义）：

   Goal forall n, even n = match n with | O => False | S m => odd m end.
   now destruct n.
   Qed.