The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 05/06/2015 09:34 AM, Holden Lee wrote:
> 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?

let HT:=type of H in idtac "The type of" H "is" HT

I have a tactic that I use to print out entire goals - it is very useful 
when debugging tactics:

Ltac vgoal :=
  idtac; (*prevents early eval*)
  match reverse goal with
    | H : ?T |- _ =>
      first[let v := eval cbv delta [H] in H in
            idtac H ":=" v ":" T
           |idtac H ":" T];
      fail
    | |- ?G =>
      idtac "======"; idtac G; idtac ""
  end.


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

I would view that as a bug in Coq - but it is easily worked around by doing:

  let H':=H in 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?

You probably need a more recent version of Proof General.  The Coq 
interface there has received a great deal of work recently.  You can get 
the development version from 
:pserver:anon AT cvs.inf.ed.ac.uk:/disk/cvs/proofgen and stay up to date.

-- Jonathan

> 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