The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Z wrote:
> Here is another example that I have some trouble to understand, where 
> simpl. does not want to unfold gx although it should have considered 
> that "match"
>
> Any ideas?
> ********************
> Definition gx(x: nat) := match x with |_ =>0 end.
> Eval simpl gx in gx 0.
> ********************

Here, the issue is that Coq programs that you type are elaborated into a 
simpler internal language.  For your example, that elaboration includes 
replacing the [match] with its body, since you have just one pattern 
that binds no variables.  You can see this by running [Print gx.].

> Then, in this case, which tactic to do the unfolding work?

In many contexts, there is no need for unfolding.  For instance:

Goal forall x, gx x = 0.
  reflexivity.
Qed.

This works because at the lowest level of Coq's logic, equality is 
defined modulo unfolding.  For more complicated cases where you need to 
massage the form of a goal to get other tactics to apply, you can always 
run [unfold gx] to unfold [gx] in the conclusion.