The Coq mailing list

[Holden Lee <holdenl AT princeton.edu>]

Thanks. Some follow-ups:

1. How do I print the type of H in the example? (?x=?y) How can I print out the goal?
   
2. Why does the statement
   idtac "rewriting" H
   work in Ltac but not in a normal proof body? The following gives Error: H not found.
   Theorem thm :
    forall x, x=0 -> x+1=1.
   Proof.
     intros x H.
     idtac "rewriting " H.
3. I see the outputs when using the CoqIDE but not Emacs Proof General. Is there a way to see them for Proof General?

Thanks,

Holden

On Tue, May 5, 2015 at 6:46 PM, Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 05/05/2015 06:25 PM, Holden Lee wrote:

How can I print in Coq? For example, What's the correct way to write this
so that the tactic prints what it's doing?

Ltac some_tactic:=
   match goal with
| [H : ?x = ?y |- _] => print ("rewriting "++(show H)); rewrite H
..

The tactics idtac and fail both can be used to print info during proofs.  The example above becomes:

Ltac some_tactic :=
   match goal with
   | H : ?x = ?y |- _ => idtac "rewriting" H; rewrite H
 ...

More complicated: how can I print in backtracking proofs?

   tactic1 := (...); if succeed then print "Tactic 1 succeeds" else print
"Tactic 1 fails."

   (tactic1 || tactic2)

Ltac tactic1 := tryif (...) then idtac "Tactic 1 succeeds" else fail 0 "Tactic 1 fails".

-- Jonathan