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