How do you lookup the definition or implementation of Coq proof tactics?

Question

I am looking at this:

Theorem eq_add_1 : forall n m,
  n + m == 1 -> n == 1 /\ m == 0 \/ n == 0 /\ m == 1.
Proof.
intros n m. rewrite one_succ. intro H.
assert (H1 : exists p, n + m == S p) by now exists 0.
apply eq_add_succ in H1. destruct H1 as [[n' H1] | [m' H1]].
left. rewrite H1 in H; rewrite add_succ_l in H; apply succ_inj in H.
apply eq_add_0 in H. destruct H as [H2 H3]; rewrite H2 in H1; now split.
right. rewrite H1 in H; rewrite add_succ_r in H; apply succ_inj in H.
apply eq_add_0 in H. destruct H as [H2 H3]; rewrite H3 in H1; now split.
Qed.

How do I find what the thing like intros or destruct mean exactly, like looking up an implementation (or if not possible, a definition)? What is the way to do this efficiently?

Answer 1

As Blaisorblade mentioned, it can be difficult to understand exactly what tactics are doing, and it is easier to look at the reference manual to find out how to use them. However, at a conceptual level, tactics are not that complicated. Via the Curry-Howard correspondence, Coq proofs are represented using the same functional language you use to write regular programs. Tactics like intros or destruct are just metaprograms that write programs in this language.

For instance, suppose that you need to prove A -> B. This means that you need to write a program with a function type A -> B. When you write intros H., Coq builds a partial proof fun (H : A) => ?, where the ? denotes a hole that should have type B. Similarly, destruct adds a match expression to your proof to do case analysis, and asks you to produce proofs for each match branch. As you add more tactics, you keep filling in these holes until you have a complete proof.

The language of Coq is quite minimal, so there is only so much that tactics can do to build a proof: function application and abstraction, constructors, pattern matching, etc. In principle, it would be possible to have only a handful of tactics, one for each syntactic construct in Coq, and this would allow you to build any proof! The reason we don't do this is that using these core constructs directly is too low level, and tactics use automated proof search, unification and other features to simplify the process of writing a proof.