The Coq mailing list

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

On 12/12/2013 12:21 PM, 
michael.soegtrop AT intel.com
 wrote:
> Dear Coq Users,
>
> I wonder if it is possible to create a tatctical, which prints the state of
> the Software Foundation Case annotation tacitcals in the same way as idtac
> "message" prints a message.
>
> 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.
>
> 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?

One way to go is the following trick

Theorem dup : forall A, A -> True -> A.
intros; assumption.
Qed.

Ltac print_solve t s :=
apply dup; [t; fail | idtac s; trivial].

Goal 1 = 1.
print_solve reflexivity foo.



> 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.