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 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
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,
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.
First, we introduce the two propositions
Q as well as the premise
P /\ Q of the implication into the context. Then we begin building a term of type
Q /\ P from a term of type
P /\ Q by applying the constructor
conj. This leaves us with two goals, namely the arguments of the constructor. By applying the premise
H to both of them we conclude the proof. The resulting proof term is
fun (P Q : Prop) (H : P /\ Q) => conj (let H0 := match H with | conj _ x0 => x0 end in H0) (let H0 := match H with | conj x _ => x end in H0)
We see that the introduction corresponds to an abstraction
fun (P Q : Prop) (H : P /\ Q) which binds the variables we introduced at the beginning of the proof. The body of this function decomposes the premise
H into its arguments (so if we think of conjunction as a binary product now we use the two associated projections) and applies the constructor
conj to build a term whose type is the conclusion
Q /\ P of the implication to be proved. Again, this is in line with the BHK interpretation in that a proof for an implication is a function that takes a proof of the premise and gives as a result a proof of the conclusion. You might wonder whether there are other inhabitants of the type of our proposition that are not -congruent to this one and indeed we’ll see that other interactive proofs yield more concise proof terms.
Instead of given the constructor’s name explicitly, we could use the
constructor tactic which for goals that are inductive types tries to apply all constructors of this type in order until one succeeds or there are no more constructors to try. It comes in handy in situations where we don’t know the constructors’ names or if there are several which one matches. But therein also lies a danger because the first constructor that matches need not be the right one for the situation at hand. So, be careful with
constructor if the (co-) inductive type at hand has more than one constructor and you are not sure which one would advance the proof in the direction you want. For working with types that have one or two constructors like conjunction or disjunction Coq also provides the specialized tactics
Decomposing inductively defined objects
Sometimes it might be necessary to decompose an object of an (co-) inductive type into its arguments. As for other common tasks in proof development there are quite a few different ways to achieve this goal. Let’s assume we want to prove the same proposition as before
Goal forall P Q : Prop, P /\ Q -> Q /\ P. intros P Q H.
and we’d like to decompose the premise
H: P /\ Q into its constituent propositions
Q, basically performing and-elimination like in a natural deduction calculus. We could use the
inversion tactic which does exactly what we want.
inversion H as [HP HQ].
By supplying the optional qualification
as [HP HQ] we instruct Coq to name the resulting terms
HQ respectively. The square bracket indicate a conjunctive pattern in this case which is applicable if the term to be inverted was constructed using a single constructor with exactly the number of arguments as there are names given between the square brackets. For types whose inhabitants can be constructed using a number of different constructors we’d have to use a disjunctive pattern like
[HP | HQ] meaning that there are two constructors that each take exactly one argument. These two patterns can also be used by the
intros P Q [HP HQ].
Another tactic at our disposal is
decompose. This tactic decomposes complex propositions into its constituents. There are essentially two ways to use it. One is to give the names of the inductive types you wish to decompose in square brackets:
decompose [and or] H.
Alternatively, you can either use the qualifier
sum instead of giving the types explicitly. The tactic
decompose record deals with so-called record types (or you might perhaps call them product types), i.e. types that only have one constructor like
decompose sum works on sum types, i.e. types with several constructors like
or. So, in our example we could use
decompose record H.
Induction and recursion principles
For each inductively defined type Coq automatically generates induction and recursion principles that can be used to give more concise proof terms. Let’s have a look at the induction and recursion principles for
and_ind = fun A B P : Prop => and_rect (A:=A) (B:=B) (P:=P) : forall A B P : Prop, (A -> B -> P) -> A /\ B -> P and_rect = fun (A B : Prop) (P : Type) (f : A -> B -> P) (a : A /\ B) => match a with | conj x x0 => f x x0 end : forall (A B : Prop) (P : Type), (A -> B -> P) -> A /\ B -> P
What does the induction principle generated by Coq mean? It captures the notion that if you can deduct a third proposition
P from the left and right hand side (
B respectively) of a conjunction
A /\ B individually, then you may also deduct from the conjunction itself that
P holds. Thus, you have a function of two arguments, the first
(A -> B -> P) it itself a function of two arguments, while the second argument is the conjunction
A /\ B. The actual task of building a proof term for the proposition
forall A B P : Prop, (A -> B -> P) -> A /\ B -> P is performed by the structural recursion principle
and_rect. It decomposes a conjunction
a of whose atomic propositions are
B using a pattern matching construct and applies the function
f : A -> B -> P to them. You may need a while to think about it, but it’s no rocket science, everything can be argued to follow from human intuition about what ought to be provable and how (see, intuition is what it’s all about!).
So, how can we use the induction principle to build a concise proof term for our proposition
forall P Q : Prop, P /\ Q -> Q /\ P? It should be straightforward given the explanation in the previous paragraph:
Goal forall P Q : Prop, P /\ Q -> Q /\ P. intros P Q H. exact (and_ind (fun (x : P) (y : Q) => conj y x) H). Qed.
exact tactic allows you to give a proof term for the current goal directly. What this proof term does is exactly what we have done manually before: Take the premise
P /\ Q, decompose it into its atomic propositions (using the recursion principle), and putting them back together in reverse order using the only constructor of the type
and. This is exactly the proof term (modulo renaming of bound variables of course) that the fully automatic tactics
This concludes our little exploration of (a fragment of) first order intuitionistic logic in Coq with a focus on inductive types and related tactics. I will not claim that there are no typos or other erros in this blog post and I’d be grateful if anyone who found one would write a comment to that effect.