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

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.

Shi*_*iSi 5

尝试

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)

  • 您可以通过编写`@ none`使隐式参数`X`为'none`.如果你写'fold @ none`,那么Coq能够明确地给出参数并在当前上下文中搜索一个合适的`X`,就像它对其他全量化变量`t`和`l`一样. .如果存在歧义,您还可以明确指定相应的变量,即`fold(@none X)`. (2认同)

Vir*_*ile 5

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