The Coq mailing list

[mulhern <mulhern AT gmail.com>]

Thanks all!

The key points are:
1) Make sure the original theorem is transparent.
2) Perform a delta reduction on the constant corresponding to the
original theorem in order to make the zeta reduced body visible.

-mulhern

On 4/24/06, mulhern 
<mulhern AT gmail.com>
 wrote:
> 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
>