(* Copyright (c) 2011, Thorsten Altenkirch *)
(** %\chapter{%## #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.