CODEWITHSUNDEEP
coqcoq-tactic
Clément
Clément

Reputation: 12917

Printing a message only if a tactic succeeds

Is there a way to print (using idtac?) a message in Ltac only after a command succeeds? Something like

first [ a; idtac "a did it!" | b; idtac "b did!" | idtac "nope"; fail ]

This almost works, except that multiple subgoals cause multiple messages to be printed:

Goal True /\ True.
  split; idtac "Split did it!".

Filtering on just the first goal seems to work...

Goal True /\ True.
  split; [ idtac "Split did it!" | .. ].

...except when it doesn't:

Goal True /\ True.
  tauto; [ idtac "Tauto did it!" | .. ].

I could probably combine both patterns into one, but I'm not too too keen on the 100% penalty hit. And that would still not solve the case of the tactic discharging the goal entirely.

(I'm mostly interested in answers for Coq before 8.5, since in 8.5 Info and the like offer nice facilities for this. Still even in 8.5 it would be interesting to be able to print debug messages only at certain points)

Upvotes: 2

Views: 193

Answers (1)

Jason Gross
Jason Gross

Reputation: 6128

Just using idtac works in Coq >= 8.5.

This almost works, except that multiple subgoals cause multiple messages to be printed:

Goal True /\ True.
  split; idtac "Split did it!".

This is not true; if it were, let n := numgoals in idtac n would print multiple times as well. Here is the output I see:

$ ~/.local64/coq/coq-8.5pl3/bin/coqtop
Welcome to Coq 8.5pl3 (November 2016)

Coq < Goal True /\ True.
1 subgoal

  ============================
    True /\ True

Unnamed_thm < split; idtac "Split did it!".
Split did it!
2 subgoals

  ============================
    True

subgoal 2 is:
 True

Unnamed_thm <

In Coq <= 8.4, you cannot do this, because Ltac evaluation has a different model. Instead, if you're willing to slightly complicate the proof term, and you have access to the beginning of the tactic sequence, you can do this:

Ltac duplicate_goal :=
  lazymatch goal with
  | [ |- ?G ] => cut G
  end.

Goal True /\ True.
  duplicate_goal; [ | split ]; [ idtac "Split did it!"; exact (fun x => x) | .. ].

The idea is that, by duplicating the goal, you can first run your tactic in one copy of the goal, then, assuming that succeeds, you can idtac in the other copy of the goal (which exists as a single goal whether or not your first tactic created multiple subgoals or solved the goal or whatever), and finally solve the duplicate goal with the identity function.

Upvotes: 1

Related Questions