如何在Coq中仅展开一次递归函数

Question

这里是一个递归函数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的简单方法。

- user287393

---

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

Answer 1

尝试

unfold all_zero; fold all_zero.

至少对我来说，这样做会产生以下结果：

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

- Volker Stolz

---

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提供参数信息。 - user287393

你可以通过写@none来使隐式参数X变为显式。如果你写fold @none.，那么Coq就能够显式地给出该参数，并在当前上下文中搜索一个合适的X，就像对于其他全量化变量t和l一样。如果存在歧义，你也可以明确指定相应的变量，即fold (@none X)。 - m0rphism

Answer 2

我认为简化命令可以实现您的需求。如果您有更复杂的目标，需要应用某些函数和保留某些函数，则可能需要使用cbv策略的各种选项（参见http://coq.inria.fr/distrib/current/refman/Reference-Manual010.html#hevea_tactic127）。

- Virgile