13

这是一个递归函数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.

4

2 回答 2

6

尝试

unfold all_zero; fold all_zero.

至少对我来说，这会产生：

true = (beq_nat n 0 && all_zero l)%bool
于 2014-06-19T10:51:34.493 回答
5

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

于 2014-06-19T12:01:30.160 回答