use*_*393 11 recursion coq unfold
这是一个递归函数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.
Run Code Online (Sandbox Code Playgroud)
现在,假设我有以下目标
true = all_zero (n :: l')
Run Code Online (Sandbox Code Playgroud)
我想用这个unfold
策略将其转化为
true = andb ( beq_nat n 0 ) ( all_zero l' )
Run Code Online (Sandbox Code Playgroud)
不幸的是,我不能用一个简单的方法来做,unfold all_zero
因为战术会急切地找到并替换所有的实例all_zero
,包括一次展开形式的实例,它变成一团糟.有没有办法避免这种情况并只展开一次递归函数?
我知道我可以通过证明临时等价来获得相同的结果assert (...) as X
,但效率很低.我想知道是否有一种简单的方法可以做到这一点unfold
.
尝试
unfold all_zero; fold all_zero.
Run Code Online (Sandbox Code Playgroud)
至少在这里,我产生:
true = (beq_nat n 0 && all_zero l)%bool
Run Code Online (Sandbox Code Playgroud)
在我看来,这simpl
会做你想做的。如果你有一个更复杂的目标,你想要应用的函数和你想要保持原样的函数,你可能需要使用cbv
策略的各种选项(参见http://coq.inria.fr/distrib /current/refman/Reference-Manual010.html#hevea_tactic127)。