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
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
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
Inductive and (A B : Prop) : Prop := conj : A -> B -> A /\ B.
You see that there's only one constructor,
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
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.