Several ways to prove a simple proposition

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.

First, we introduce the two propositions P and 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 \alpha-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 split and left or right respectively.

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 P and 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 HP and 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 tactic.

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 record or 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 and. While 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:

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 (A and 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 A and 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.

The 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 firstorder and intuition produce.

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.

This entry was posted in Coq and tagged . Bookmark the permalink.

Leave a Reply

Your email address will not be published. Required fields are marked *

This site uses Akismet to reduce spam. Learn how your comment data is processed.