This file is a short showcase of Church-encoded natural numbers in Coq. Our particular interest is to prove that induction is possible on them (lemma nat_ind).
It is customary to introduce Church-encodings to show that a minimal language (say untyped pure lambda-calculus) is enough to represent and compute with natural numbers. It is more uncommon to try and reason about that representation, in particular the induction principle might seem elusive.
Deriving an induction principle for Church naturals is so elusive that in fact it has been shown not to be provable in several type theories and constructive logics like second order dependent type theory (see Herman Geuvers, "Induction Is Not Derivable in Second Order Dependent Type Theory"). But it's not because someone showed it impossible that we should stop! As we will see, what we are missing is propositional irrelevance: the fact that two elements (proofs) of a proposition are always equal. This is a perfectly fine thing to have and Coq has recently introduced a new universe SProp for (definitionally) irrelevant propositions, so we can even avoid using any axiom.
The crux of the derivation is to define the usual Church encodings, define the statement of the induction principle and construct the subset of natural numbers validating it. This subset is well-behaved and we can show that this one satisfies the induction principle of natural numbers:
I got the idea of this trick from Aaron Stump, "From realizability to induction via dependent intersection" and Denis Firsov & Aaron Stump, "Generic Derivation of Induction for Impredicative Encodings in Cedille". Their work is based on dependent intersection types, of which we are making a poor man's version using SProp here.
Remark: Because I felt like having fun, there will be universe level trickery! The side-challenge was to show that the "inherent" impredicativity of church encodings is not so problematic. So I took a predicative version of the encoding of natural numbers: ∀ X : Type, X → (X → X) → X. Since Type is a predicative hierachy, there is a hidden level and this is actually a level-polymorphic definition. Usually this is not a problem since Coq has a default hidden method for handling level constraints: We write everything as if Type was impredicative while everything is sorted out behind the scenes. In this file however, we will do some brutal "pseudo self-instanciation" (instanciation of the encoding with itself at a lower level) so I went with the manual universe management. Adding the Set Printing Universes. and Set Printing Coercions. flags is encouraged to understand what is going on: I am using pretty cursed coercions and have elided annotations where Coq could infer the proper ones!
Maybe it would have been more idiomatic in Coq to embrace impredicativity and replace Type by Set (using the coq option -impredicative-set) this is what I do in the file nat-set.v.
Set Universe Polymorphism.While we are at it, we also enable the new native records which have eta-equality. Although we could do without it, I really think that they should be enabled by default!
Set Primitive Projections.We start off with a very minimal prelude defining the usual inductive identity type, but in the universe SProp.
Inductive eq_s@{i} (A : Type@{i}) (x : A) : A -> SProp := | eq_refl : eq_s A x x. Arguments eq_refl {A x}. Notation "a =ₛ b" := (eq_s _ a b) (at level 70).
Together with the only two helpers we will need: congruence ...
Definition eq_cong {A B : Type} (f : A -> B) {x y} (H : x =ₛ y)
: f x =ₛ f y
:= match H in _ =ₛ a return f x =ₛ f a with
| eq_refl => eq_refl
end.... and substitution.
Definition eq_subst {A : Type} (P : A -> SProp) {x y} (H : x =ₛ y)
(p : P x) : P y
:= match H in _ =ₛ a return P a with
| eq_refl => p
end.Nothing too suprising:
Definition nat_r@{i} : Type@{i+1} := forall X : Type@{i}, X -> (X -> X) -> X. Definition ze_r : nat_r := fun X z s => z. Definition su_r (n : nat_r) : nat_r := fun X z s => s (n X z s).
Now we show that Church naturals are contravariant in their universe level: we can embed Church naturals of some level into a lower one. The intuition is that Church naturals encode function iteration at an arbitrary type, hence if know how to iterate at a large type, we know how to iterate at any smaller type. As you can see by the implementation, this is purely bookkeeping and is in fact computationally the identity function, but we cannot prove it since the input and output live in different universes.
Definition lower_r@{i j | j <= i}
: nat_r@{i} -> nat_r@{j}
:= fun n X => n X.We then register lowering as a coercion to hide it from sight.
Coercion lower_r : nat_r >-> nat_r.We define the statement of the induction principle on our encoded naturals. Several things are important. First, we adopt an unusual order of arguments and make this statement a predicate on the natural number appearing in the conclusion. Second, we parametrize on predicates valued in SProp. And third, the whole statement lives in SProp itself.
Definition nat_ok (n : nat_r) : SProp :=
forall P : nat_r -> SProp,
P ze_r
-> (forall m, P m -> P (su_r m))
-> P n.This predicate is true for zero and preserved by successor.
Definition ze_ok : nat_ok ze_r := fun P pz ps => pz. Definition su_ok {n} (H : nat_ok n) : nat_ok (su_r n) := fun P pz ps => ps n (H P pz ps).
It is also preserved by lowering.
Definition lower_ok@{i j | j <= i} {n}
: nat_ok n -> nat_ok (lower_r@{i j} n)
:= fun H P pz ps => H (fun x => P (lower_r x)) pz (fun _ p => ps _ p).We have arrived at our final definition: the subset of Church naturals for which the induction predicate is true.
Record nat@{i} : Type@{i+1} := { rec : nat_r@{i} ; ind : nat_ok rec }.As the predicate is preserved by the constructors, we can again construct a zero and a sucessor.
Definition ze : nat := {| rec := ze_r ; ind := ze_ok |}. Definition su (n : nat) : nat := {| rec := su_r (rec n) ; ind := su_ok (ind n) |}.
And again we can lower the universe level.
Definition lower@{i j | j <= i} (n : nat@{i}) : nat@{j} := {| rec := lower_r (rec n) ; ind := lower_ok (ind n) |} . Coercion lower : nat >-> nat.
Now since this is a subset type by an irrelevant proposition, the projection to "normal" Church naturals is an injection.
Definition nat_eq {a b} (H : rec a =ₛ rec b) : a =ₛ b := match H in _ =ₛ rb return forall ib, a =ₛ {| rec := rb; ind := ib |} with | eq_refl => fun _ => eq_refl end (ind b). Arguments nat_eq &.
This "recomputation" lemma is the magic trick. We prove that applying a natural to zero and successor — that is, iterating the sucessor n times starting from zero — gives back the same natural number.
Some trickery is hidden under the rug: nat_mk instanciates the type parameter of the Church natural with nat itself, so it will give back a number living at a smaller lever. Hence the right hand-side of the equation is implicitely lowered.
Definition nat_mk (n : nat_r) : nat := n nat ze su. Definition nat_recompute {n} : nat_mk (rec n) =ₛ n := nat_eq (ind n (fun x => rec (nat_mk x) =ₛ x) eq_refl (fun _ => eq_cong su_r)).
Finally we prove the induction principle. We need the recomputation trick in the proof, so the natural number must live at a larger level than what the predicate accepts.
Definition nat_ind@{i j | j < i} (P : nat@{j} -> SProp)
(pz : P ze) (ps : forall n, P n -> P (su n))
(n : nat@{i}) : P n
:= eq_subst P nat_recompute
(ind n (fun x => P (nat_mk x))
pz
(fun _ h => ps _ h)).