How to unfold a recursive function just once in Coq

Question

Here is a recursive function all_zero that checks whether all members of a list of natural numbers are 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.

Now, suppose I had the following goal

true = all_zero (n :: l')

And I wanted to use the unfold tactic to transform it to

true = andb ( beq_nat n 0 ) ( all_zero l' )

Unfortunately, I can't do it with a simple unfold all_zero because the tactic will eagerly find and replace all instances of all_zero, including the one in the once-unfolded form, and it turns into a mess. Is there a way to avoid this and unfold a recursive function just once?

I know I can achieve the same results by proving an ad hoc equivalence with assert (...) as X, but it is inefficient. I'd like to know if there's an easy way to do it similar to unfold.

Answer 1

Try

unfold all_zero; fold all_zero.

At least here for me that yields:

true = (beq_nat n 0 && all_zero l)%bool

Answer 2

It seems to me that simpl will do what you want. If you have a more complicated goal, with functions that you want to apply and functions that you want to keep as they are, you might need to use the various options of the cbv tactic (see http://coq.inria.fr/distrib/current/refman/Reference-Manual010.html#hevea_tactic127).