recursion - 如何在 Coq 中只展开一次递归函数

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

最佳答案

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

关于recursion - 如何在 Coq 中只展开一次递归函数，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/24304345/