# Coq in Coq

Section Meta.

Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Require Import Coq.Program.Equality.

Set Implicit Arguments.

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.

Inductive Formula : Set :=
| Var : string -> Formula
| Impl : Formula -> Formula -> Formula.

Notation "x ==> y" := (Impl x y) (at level 30, right associativity).

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

Definition I (P : Formula) : Formula := P ==> P.

The constant combinator "K".

Definition K (P Q : Formula) : Formula := P ==> Q ==> P.

The (mysterious) combinator "S".

Definition S (P Q R : Formula) : Formula :=
(P ==> Q ==> R)
==> (P ==> Q)
==> P ==> R.

We represent Hypotheses as a list of formula.

Definition Hyps : Set := list 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.

Inductive ND_Proof : Hyps -> Formula -> Prop :=
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).

| nd_ass : forall (Hs : Hyps)(P : Formula),
ND_Proof (P :: Hs) P
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).

| nd_weak : forall (Hs : Hyps)(P Q : Formula),
ND_Proof Hs P -> ND_Proof (Q :: Hs) P
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.

| nd_intro : forall (Hs : Hyps)(P Q : Formula),
ND_Proof (P :: Hs) Q -> ND_Proof Hs (P ==> 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.

| nd_apply : forall (Hs : Hyps)(P Q : Formula),
ND_Proof Hs (P ==> Q) -> ND_Proof Hs P -> ND_Proof Hs 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.

Lemma nd_I : forall (Hs : Hyps)(P : Formula),
ND_Proof Hs (I P).
intros Hs P.
unfold I.
apply nd_intro.
apply nd_ass.
Qed.

To prove K we need to use weak.

Lemma nd_K : forall (Hs : Hyps)(P Q : Formula),
ND_Proof Hs (K P Q).
intros Hs P Q.
unfold K.
apply nd_intro.
apply nd_intro.
apply nd_weak.
apply nd_ass.
Qed.

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.

Lemma nd_S : forall (Hs : Hyps)(P Q R : Formula),
ND_Proof Hs (S P Q R).
intros Hs P Q R.
unfold S.
apply nd_intro.
apply nd_intro.
apply nd_intro.
eapply nd_apply. eapply nd_apply.
apply nd_weak. apply nd_weak. apply nd_ass.
apply nd_ass.
eapply nd_apply.
apply nd_weak. apply nd_ass.
apply nd_ass.
Qed.

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

Inductive CL_Proof : Hyps -> Formula -> Prop :=

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

| cl_ass : forall (Hs : Hyps)(P : Formula),
CL_Proof (P :: Hs) P
| cl_weak : forall (Hs : Hyps)(P Q : Formula),
CL_Proof Hs P -> CL_Proof (Q :: Hs) P

We are adding proofs for K and S as axioms.

| cl_K : forall (Hs : Hyps)(P Q : Formula),
CL_Proof Hs (K P Q)
| cl_S : forall (Hs : Hyps)(P Q R: Formula),
CL_Proof Hs (S P Q R)

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

| cl_apply : forall (Hs : Hyps)(P Q : Formula),
CL_Proof Hs (P ==> Q) -> CL_Proof Hs P -> CL_Proof Hs Q.

We can actually prove I from S and K.

Lemma cl_I : forall (Hs : Hyps)(P : Formula),
CL_Proof Hs (I P).
intros Hs P.
unfold I.
eapply cl_apply.
eapply cl_apply.
apply cl_S.
apply cl_K.

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

instantiate (1:= P ==> P ).
apply cl_K.
Qed.

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.

Lemma cl2nd : forall (Hs : Hyps)(P : Formula),
CL_Proof Hs P -> ND_Proof Hs P.
intros Hs P H.

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.

dependent induction H.

We have now to provide a translation for each case.

ass_cl is translated by nd_ass.

apply nd_ass.

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

apply nd_weak.
exact IHCL_Proof.

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

apply nd_K.

cl_S is translated as nd_S.

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

eapply nd_apply.
apply IHCL_Proof1.
apply IHCL_Proof2.
Qed.

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

Lemma cl_intro : forall (Hs : Hyps)(P Q : Formula),
CL_Proof (P :: Hs) Q -> CL_Proof Hs (P ==> Q).
intros Hs P Q H.

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

dependent induction H.

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

apply cl_I.

In the case for cl_weak we need to use cl_K.

eapply cl_apply.
apply cl_K.
exact H.

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.

eapply cl_apply.
apply cl_K.
apply cl_K.

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

eapply cl_apply.
apply cl_K.
apply cl_S.

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.

eapply cl_apply.
eapply cl_apply.
apply cl_S.
apply IHCL_Proof1.
reflexivity.
apply IHCL_Proof2.
reflexivity.
Qed.

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

Lemma nd2cl : forall (Hs : Hyps)(P : Formula),
ND_Proof Hs P -> CL_Proof Hs P.
intros Hs P H.
dependent induction H.
apply cl_ass.
apply cl_weak. exact IHND_Proof.
apply cl_intro. exact IHND_Proof.
eapply cl_apply.
apply IHND_Proof1.
exact IHND_Proof2.
Qed.

The final theorem

Theorem ndcl : forall (Hs : Hyps)(P : Formula),
ND_Proof Hs P <-> CL_Proof Hs P.
intros Hs P.
split.
apply nd2cl.
apply cl2nd.
Qed.