在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手册明确指出,如果减少的参数以构造函数开头,则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.