The Coq mailing list

[mulhern <mulhern AT gmail.com>]

Hi!

Suppose I have developed a proof in the normal way.

Theorem name : <goal>.
Proof.
<lots of tactics>.
Qed.

I want to apply zeta reductions to the body of the proof once it has
been generated.

Currently the way I do this is:

Print name.

Then I copy the generated output and paste it into the command.

Definition name_reduced := Eval cbv zeta in
(
  <big chunk of text goes here at the paste operation>
).

Is there any way to do this through Coq instead of by this cumbersome
and not really scalable cut and paste method?

I have tried

Definition name_reduced := Eval cbv zeta in name.

The problem with that is that I can't tell what the body of
name_reduced consists of because I cannot Print it. When I use the
Print command I just get
name_reduced
=
name : goal

My purpose in performing these reductions is to transform the proof to
one that is more readily accepted by the refine tactic.

-mulhern