这里是一个递归函数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)
并用它重写代码。 - user3551663