The Coq mailing list

[Laurent Théry <Laurent.Thery AT inria.fr>]

> As an exerices I tried to do the "advanced expression simplifier" exercise in
> SF Imp.v by just repeatedly trying various tacticals. This works astonishingly
> well and fast (~1s for ~100 intermediate goals with 13 tactics given to try),
> but it is not so easy to understand what tactics are applied to which goal in
> which order. I added some idtac "description" but it would be perfect if one
> could print the values of all the Case, SCase, ... annotations for each tactic
> applied.
This may be of some use in your case but with idtac you can actually 
print value.

Ltac print_assumption H :=
let v := type of H in
idtac "type of "; idtac H; idtac " : ";
idtac v.

Goal 2 = 3 -> 3 = 4 -> 1 = 2.
intros H1 H2.
print_assumption H1.
print_assumption H2.


> And another question: The list of tactics to try starts with reflexivity:
>
>      repeat (
>        try ( reflexivity; idtac "solved" );
>
> but here ; idtac doesn't work, because no new goal is created, so idtac is not
> executed. Is there a way to print something after a tactic which solved the
> current goal?
>
> Thanks & best regards,
>
> Michael
>
> P.S.: I don't want to post the solution of the exercise here so that others
> are not robbed of the fun of doing it on their own, but if my question is not
> understandable without this, I can of cause send it to individuals via mail.