There are several ways to look at what is happening under the hood.
TL; DR: Put info in front of your tactics or use Show Proof. before and after calling tactics and spot the differences.
To find out what a particular tactical challenge is doing, you can prefix with info to show the specific steps of the evidence that it took.
(This can be broken with Coq 8.4, I see that they provide t12 versions for some tactics, read the error message if you need to.)
This is probably what you want at the entry level, it can already be pretty brief.
Another way to see what is happening in the proof is to use the Show Proof. command Show Proof. . It will show you the currently constructed term with holes and show you which hole each of your current goals should fulfill.
This is probably more advanced, especially if you use tactics such as induction or inversion , as the term you create will be quite attractive and require you to understand the fundamental nature of induction schemes or dependent ones (which CPDT should teach you soon enough).
Once you finish the proof with Qed. (or Defined. ), you can also ask for a look at a term that was built using Print term. where term is the name of the theorem / term.
This will often be a large and ugly term, and it needs some training to be able to read them for the terms involved. In particular, if this term was built using powerful tactics (e.g. omega , crush , etc.), it is likely to be unreadable. You would mostly use this only to scan at a specific place in your term. If it is longer than 10 lines, don’t even bother reading it in such a rough format! :)
With all the previous ones, you can use Set Printing All. in advance, so Coq prints detailed, explicit versions of everything. It is also detailed, but it can help when you are wondering what values of implicit parameters are.
That’s all I can think of at the top of my head, maybe more.
As for tactics, the usual answer can be found in the documentation:
http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual011.html#@tactic155
Basically, auto tries to use all the hints provided (depending on the database you are using) and solve your goal by combining them to a certain depth (which you can specify). The default database is core , and the depth is 5 .
You can learn more about this here:
http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual011.html#Hints-databases