Coq provides many tactics. In this post we show a number of proofs that use different tactics to prove a simple proposition of first order logic, namely \(\forall P\;Q,\, P \wedge Q \rightarrow Q \wedge P\) which in Coq translates to

forall P Q : Prop, P /\ Q -> Q /\ P

First, we’ll peel off all the syntactic sugar and look at what makes up the encoding of this proposition in Coq’s logic, the Calculus of (co-) inductive constructions or CiC for short. Implication -> and universall quantification forall are part of the logic, so we’ll only have to look at the two conjunctions. To find out what the meaning of the /\ operator is, issue the command

Locate "/\".

This will produce the response

Notation            Scope     
"A /\ B" := and A B  : type_scope
                      (default interpretation)

meaning that in the scope type_scope (which is active by default when you start the Coq interpreter) the term A /\ B really stands for and A B. Let us now examine the inductive type and (using the command Print and):

Inductive and (A B : Prop) : Prop :=  conj : A -> B -> A /\ B.

You see that there's only one constructor, conj, and that in order to construct a term of type and A B you'll have to provide two terms of type Prop. Look up the BHK interpretation of intuitionistic logic to find out more about this sort of encoding. For an in depth treatmet of the connection between type theory, intuitionistic logic, and functional programming have a look at the excellent textbook Type Theory and Functional Programming by Simon Thompson which is available online in PostScript and PDF format.

The first proof uses the information we have gathered so far, spelling out all the details:

Goal forall P Q : Prop, P /\ Q -> Q /\ P.
intros P Q H.
apply conj.
apply H.
apply H.
Qed.