13

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.

user287393
  • 1,221
  • 8
  • 13
  • You could also prove `forall n l, all_zero (n :: l) = andb (beq_nat n 0) (all_zero l)` and rewrite with that. –  Jun 19 '14 at 12:53

2 Answers2

6

Try

unfold all_zero; fold all_zero.

At least here for me that yields:

true = (beq_nat n 0 && all_zero l)%bool
Volker Stolz
  • 7,274
  • 1
  • 32
  • 50
  • 1
    `unfold` followed by `fold` indeed works for `all_zero`, but not for polymorphic recursive functions. Here's one example: `Fixpoint none {X:Type} (t:X->bool) (l:list X) : bool := match l with | nil => true | h :: l' => andb (negb (t h)) (none t l') end.` `unfold none` followed by `fold none` results in the following error message: `Error: Cannot infer the implicit parameter X of none.` So I think a generic solution for unfolding a recursive function once will have to avoid using `unfold` in the first place, unless there is some way to supply parametric information to `fold`. – user287393 Jun 19 '14 at 11:23
  • 2
    You can make the implicit Parameter `X` of `none` explicit by writing `@none`. If you write `fold @none.`, then Coq is able to give the argument explictly and searches for a suitable `X` in the current context, just as it does for the other all-quantified variables `t` and `l`. If there is ambiguity you can also specify the corresponding variables explicitly, i.e. `fold (@none X)`. – m0rphism May 16 '15 at 08:09
6

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).

Virgile
  • 9,724
  • 18
  • 42