如何在 Coq 中只展开一次递归函数答案

【问题标题】：How to unfold a recursive function just once in Coq如何在 Coq 中只展开一次递归函数
【发布时间】：2014-06-19 10:26:52
【问题描述】：

这是一个递归函数all_zero，它检查自然数列表的所有成员是否为零：

Require Import Lists.List.
Require Import Basics.

Fixpoint all_zero ( l : list nat ) : bool :=
  match l with
  | nil => true
  | n :: l' => andb ( beq_nat n 0 ) ( all_zero l' )
  end.

现在，假设我有以下目标

true = all_zero (n :: l')

我想使用unfold 策略将其转换为

true = andb ( beq_nat n 0 ) ( all_zero l' )

不幸的是，我不能用一个简单的unfold all_zero 来做到这一点，因为这种策略会急切地找到并替换所有all_zero 的实例，包括曾经展开形式的那个，它会变成一团糟。有没有办法避免这种情况并只展开一次递归函数？

我知道我可以通过证明与 assert (...) as X 的临时等效性来获得相同的结果，但它效率低下。我想知道是否有类似于unfold 的简单方法。

【问题讨论】：

你也可以证明forall n l, all_zero (n :: l) = andb (beq_nat n 0) (all_zero l)并用它重写。

标签： recursion coq unfold

【解决方案1】：

试试

unfold all_zero; fold all_zero.

至少对我来说是这样：

true = (beq_nat n 0 && all_zero l)%bool

【讨论】：

unfold 后跟fold 确实适用于all_zero，但不适用于多态递归函数。这是一个示例：Fixpoint none {X:Type} (t:X->bool) (l:list X) : bool := match l with | nil => true | h :: l' => andb (negb (t h)) (none t l') end.unfold none 后跟fold none 会导致以下错误消息：Error: Cannot infer the implicit parameter X of none. 所以我认为展开递归函数的通用解决方案必须首先避免使用unfold，除非有某种方法可以向fold 提供参数信息。
您可以通过编写@none 使none 的隐式参数X 显式化。如果你写 fold @none.，那么 Coq 能够明确地给出参数并在当前上下文中搜索合适的 X，就像它搜索其他全量化变量 t 和 l 一样。如果有歧义，您还可以明确指定相应的变量，即fold (@none X)。

【解决方案2】：

在我看来simpl 会做你想做的事。如果您有更复杂的目标，想要应用的功能和想要保持原样的功能，您可能需要使用cbv 策略的各种选项（请参阅http://coq.inria.fr/distrib/current/refman/Reference-Manual010.html#hevea_tactic127）。

【讨论】：