Coq in Coq

This chapter is about using Coq to reason about its own logic. This was the title of a paper by Bruno Barras who managed to develop the theory of Coq inside Coq.

Obviously, we won't be able to do this here so we are going to focus on a more modest goal: we are limiting ourselves to propositional logic and to keep things short we will look at propositional logic with implication only.

We are going to develop this logic inside coq using natural deduction. This is very close to the atcual Coq proof objects.

An alternative would be to use combinatory logic. We are going to compare these two approaches and we will show that they are equivalent.

Formulas as trees

We are representing logical formulas as trees. Variables are just representined as strings.

As examples we are going to use three propositions, all of them are tautologies. Two of them will show up as the basic combinators of combinatoric logic later.

The identity combinator "I".

The constant combinator "K".

The (mysterious) combinator "S".

We represent Hypotheses as a list of formula.

Natural deduction

We are ging to represent the proposition that a formula P is provable from a list of assumptions Hs as ND_Proof Hs P. This is an inductive definition, the constructors are nodes in the proof tree.

The first constructor nd_ass allows us to use the last hypothesis from our list of hypotheses (which appears at the head of the list).

To be able to access earlier hypothesis we use nd_weak which allows us to ignore the last hypothesis (i.e. the head of the list).

The next constructor nd_intro corresponds to the intro tactic in coq: to prove P ==> Q we assume P, i.e. we add it to the list of assumptions, and continue to prove Q.

The elimination for application is slightly different from the one in Coq which is hard to state precisely. The rule nd_apply corresponds to modens ponens: if you can prove P ==> Q and also P then you can also prove Q.

As examples we are going to prove that the examples I,K and S are provable.

The proof for I follows almost exactly the proof of the same tautology in Coq.

To prove K we need to use weak.

The proof of S uses nd_apply. It also shows that modens ponens isn't so suitable to interactive proof, because we need some hindsight how to apply it.

Combinatory logic.

Combinatory logic (also sometimes called "Hilbert style logic") is based on the maybe surprising observation that we can replace nd_intro by adding K and S as axioms. This leads to a variable free representation of logic. However, to be able to compare natural deduction and combinatory logic we will consider combinatory logic with variables here. However, if the list of hypotheses is empty we will never need variables unlike natural deduction where the nd_intro rule introduces variables.

We define CL_Proof Hs P to mean that P is provable from Hs in combinatory logic.

The rules relating to hypothesis are exactly the same as the ones for natural deduction.

We are adding proofs for K and S as axioms.

Modus ponens cl_apply is the same rule as for natural deduction.

We can actually prove I from S and K.

We need to instantiate one of the meta variables by hand. This is how we do this in Coq - please check the manual.

Since we did already prove K and S using natural deduction, we can show that every proof in combinatory logic can be turned into one in natural deduction. We prove this by induction over the derivation trees.

Basically we are showing that each node in an CL proof tree can be replaced by a ND tree by replacing the axioms K and S by the corresponding proofs.

Since the derivation trees are depndent, i.e. they depend on the choice of hypotheses and proposition we need to invoke the tactic dependent induction.

We have now to provide a translation for each case.

ass_cl is translated by nd_ass.

And weak_cl by nd_weak. Here we have to use the induction hypothesis to recursively translate the rest of the proof.

cl_K is translated as nd_K. Here on axiom is replaced by a small proof tree.

cl_S is translated as nd_S.

cl_apply is translated by nd_apply. Since there are two subproofs we have to translate them recursively by using the induction hypotheses.

The deduction theorem

The main ingredient to prove the other direction of the equivalence, i.e. that it is possible to simulate natural deduction proofs in combinatory logic, is to show that combinatory logic is closed under the intro rule. This is usually called the deduction theorem.

to prove this we need to perform an induction over the proof tree showing CL_Proof (P :: Hs) Q.

The case for cl_ass can be proven using the identity proof cl_I which we have already derived.

In the case for cl_weak we need to use cl_K.

The case for cl_K can be derived by using cl_K once to ignore the argument and a 2nd time to provide the constant to be actually used.

The case for cl_S is similar only that we use cl_S the 2nd time.

The case for cl_app is the most interesting one. It finally lifts the mystery about S. It is actually what we need to translate this case, ie. to shift abstraction over an application.

Equivalence of natural deduction and combinatory logic.

We have now all the ingredients together to show that natural deduction and combinatory logic prove exactly the same propositions.

To prove the other direction we only need to appeal to the deduction theorem cl_intro when translating nd_intro.

The final theorem