The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

nnovak wrote:
> It seems that when a "simpl" tactic is used in a proof, after we
> ask to show us the proof ("Show Proof") the work of this tactic is not
> visible in the outputted proof, moreover it is also not in the
> exported proof ("Show XML Proof").
>   

That's because 'simpl' and the other conversion tactics do no "work" in 
this sense.  They only convert a term to another form that the type 
system identifies as equivalent.  These tactics are valuable because 
they rearrange terms such that certain unifications succeed where they 
failed before, etc., but they are useless if we imagine that we know the 
whole proof ahead of time and are willing to take the time to write it 
out exactly.