From Zero to Factorial (part 2)

The one and only Recursion Theorem (for natural numbers)

Frederic Peschanski - LIP6 - Sorbonne Université

This document is copyright (C) 2021 Frederic Peschanski - Creative Commons CC-BY-SA 4.0

(ns latte-next.nats.part2

  "The recursion theorem for natural numbers."

  (:refer-clojure :exclude [and or not int =])

  (:require [latte.core :as latte :refer [defaxiom defthm deflemma definition

                                          proof try-proof assume have pose qed]]

   [latte-prelude.prop :as p :refer [and or not]]

   [latte-prelude.equal :as eq :refer [equal]]

   [latte-prelude.quant :as q :refer [exists single unique the]]

   [latte-prelude.classic :as classic]

   [latte-prelude.fun :as fun]

   [latte-sets.rel :as rel :refer [rel relfun functional]]))

(defaxiom ℕ [] :type)

(def = equal)

(definition ≠ [[n ℕ] [m ℕ]] (not (= n m)))

(defaxiom zero [] ℕ)

(defaxiom succ [n ℕ] ℕ)

(defaxiom zero-not-succ []

  (∀ [n ℕ] (≠ (succ n) zero)))

(defaxiom succ-injective []

  (∀ [n m ℕ] (==> (= (succ n) (succ m))

               (= n m))))

(defaxiom ℕ-induct [P (==> ℕ :type)]

  (==> (P zero)

    (∀ [n ℕ] (==> (P n)

               (P (succ n))))

    (∀ [n ℕ] (P n))))

(defthm ℕ-case [P (==> ℕ :type)]

  (==> (P zero)

    (∀ [n ℕ] (P (succ n)))

    (∀ [n ℕ] (P n))))

(proof 'ℕ-case

  (assume [Hz (P zero)

           Hsucc (∀ [n ℕ] (P (succ n)))]

    (have <a> (P zero) :by Hz)

    (assume [n ℕ

             Hn (P n)]

      (have <b> (P (succ n)) :by (Hsucc n)))

    (have <c> (∀ [n ℕ] (P n)) :by ((ℕ-induct P) <a> <b>)))

  (qed <c>))

(defthm succ-neq []

  (∀ [n ℕ] (≠ (succ n) n)))

(proof 'succ-neq

  (pose P := (λ [n ℕ] (≠ (succ n) n)))

  (have <a> (P zero)

    :by (zero-not-succ zero))

  (assume [n ℕ

           Hn (P n)]

    (assume [Hcontra (= (succ (succ n)) (succ n))]

      (have <b1> (= (succ n) n)

        :by (succ-injective (succ n) n Hcontra))

      (have <b2> p/absurd :by (Hn <b1>)))

    (have <b> (P (succ n)) :by <b2>))

  (qed ((ℕ-induct P) <a> <b>)))

Introduction

This is the second installment of our series From Zero to Factorial in which we (re)construct the natural numbers from scratch, assisted by the LaTTe proof assistant. In the first part, we introduced the axioms of Peano arithmetic. This means that we already have defined the set inline_formula not implemented of natural numbers, the number zero, the successor inline_formula not implemented of a natural number inline_formula not implemented, and most importantly the principle of proof by induction on inline_formula not implemented.

In this document, I will explain, state and demonstrate (both informally and formally) the recursion theorem on natural numbers. This is a fundamental theorem, albeit seldom properly stated and even less often fully and formally demonstrated. The theorem is attributed, like many results about formalizing number systems, to Richard Dedekind. It is still actively studied but it's still part of the mathematical folklore.

Our ultimate goal is the factorial function, and we have still a long way to be able to define it properly. As in the first part of the series, I will explain everything using a rather classical mathematical approach, but I will also formalize everything in the context of the Latte software. There's no need to understand this formal part, although I would be happy if the reader tries to see the tight connection between the two, complementary, explanations.

On the way to recursion

Informally, everyone (of a certain age) knows about multiplication, and thus the following sentence is enough to convey the intended meaning of the factorial :

inline_formula not implemented

The need for a recursion arise from this liberal use of the three dots inline_formula not implemented in mathematics. Personally I find that the three dots are a little bit overused to explain things in mathematics (especially in computer science, my department). I always fill a little unsatisfied if the three dots creep here and there. There is an easy albeit rather useless way of handling the three dots : hide it behind a notation, as in the following :

inline_formula not implemented

But then, we have to define the inline_formula not implemented notation, which would be for example, as follows:

inline_formula not implemented

This looks more formal, but it is not, the three dots cannot be justified apart from a mathematically-trained reader thinks : yeah, got it!

Thankfully, a branch of mathematics, which could be called effective mathematics, exists to fill the gap. This is there that you will find recursion theory, which studies the notion of computable functions (yes, yes, many functions are not computable, but that's another story...). The classical recursive "definition" of factorial is often stated as follows :

inline_formula not implemented

Agreed, the three dots are not part of this statement. And it kind of makes sense intuitively (although, in fact, not much more than the previous attempt). More interestingly, it gives a kind of a recipe to compute the factorial of any natural number, for example :

inline_formula not implemented

This can be expressed, quite literally, in most programming languages, such as in Clojure:

(defn fact [n]

  (if (zero? n)

    1

    (* n (fact (- n 1)))))

(fact 3)

(fact 6)

Nice! It's working ... probably better than with three dots creeping in your programs.

This does not say, though, why this is working, and how it is built in a mathematical way, based on the Peano arithmetic. And this does not say, also, what properties the factorial function has, and how to prove them.

For this we need to state and prove an important recursion theorem, which is what we will do next.

Disclaimer : the recursion theorem and its proof could be qualified as of a medium difficulty. It is not that it is difficult, in fact, because it does not require any advanced mathematical concept (only rather basic set-theory). No, the real difficulty is about finding a good way to decompose the problem into sub-problems (lemmas), and we will need a few of these. So fasten your set-belt and let's go! (typo/bad joke intended).

The recursion theorem for natural numbers

We consider a function, say inline_formula not implemented, from an arbitrary set inline_formula not implemented to itself, i.e. inline_formula not implemented, and we also distinguish a value, say inline_formula not implemented. Given its definition, inline_formula not implemented is an internal operator : given a value (any value) in set inline_formula not implemented it will produce, no matter what, a value in inline_formula not implemented. Said differently and somewhat snobbishly, inline_formula not implemented is a total endo function. Hence, since inline_formula not implemented is in A, we can produce inline_formula not implemented — let's call it inline_formula not implemented — and thus from there inline_formula not implemented, and so on. So for a given inline_formula not implemented, we can produce inline_formula not implemented. One problem, though, is that we are back with our three dots! The trick, now, is to introduce a function — let's call it inline_formula not implemented — and whose purpose is to associate :

• inline_formula not implemented to the value inline_formula not implemented, i.e. inline_formula not implemented

• 1 to the value inline_formula not implemented, i.e. inline_formula not implemented

• inline_formula not implemented (three dots spotted!)

• inline_formula not implemented to the value inline_formula not implemented, i.e. inline_formula not implemented

Now we have even more three dots! Where's the trick? Don't panic, it's right under our eyes... Let's take inline_formula not implemented for example. We have inline_formula not implemented, but notice that inline_formula not implemented. Hence, in fact, inline_formula not implemented. Do you see the trick now ? Let's try again with 2 : inline_formula not implemented.

Exercise : do the same thing for 3, 4, ... until you see the pattern, the recursive pattern!

So we are now down to only two properties defining our inline_formula not implemented operator:

• inline_formula not implemented

• for any inline_formula not implemented

Let's try again with 2, we have :

inline_formula not implemented

Exercise : do the same thing for 3, 4, ... until ... well, you understand

Note that our "function" inline_formula not implemented is now defined without any intervention of the three dots. So all seems fine, but in fact I lied ... I said that inline_formula not implemented was a function but that's more what we would like that what it is for now. This is where things become really interesting (at least for math nerds ?).

Recursion Theorem for Natural Numbers

Given inline_formula not implemented and inline_formula not implemented, then :

inline_formula not implemented such that inline_formula not implemented

This says (through the notation inline_formula not implemented) that the recursion principle inline_formula not implemented must :

1. exists as a function, and

2. be unique (for given inline_formula not implemented, inline_formula not implemented and inline_formula not implemented).

Before starting the (rather long) proof of this (apparently simple) theorem, I will now explain how to formalize it in LaTTe. You can of course skip this part, but we'll see that it's not so distant from the formulation above.

First, we separate the definition of the properties of the rec principle from the theorem statement, for the sake of separation of concern.

(definition ℕ-rec-prop [[?A :type] [x0 A] [f (==> A A)]]

  (λ [rec (==> ℕ A)]

    (and (= (rec zero) x0)

      (∀ [n ℕ] (= (rec (succ n)) (f (rec n)))))))

The three parameters of the definition is the type A, the value x0 associated to zero and the function f from A to A. Note the question mark in ?A, which makes the parameter A implicit. This means that instead of writing (ℕ-rec-prop A x0 f) we just have to write (ℕ-rec-prop x0 f) and the type A will be automatically inferred by LaTTe (from x0 or f).

Note also that rec is introduced by a lambda. In type theory, a statement of the form:

(λ [z T] (P z)) for a given type T and property P means:

"all the z's of T such that (P z) is true".

So here we consider all possible rec satisfying the recursion rules.

Now, the recursion theorem can be stated as follows:

(defthm ℕ-rec [[?A :type] [x0 A] [f (==> A A)]]

  (unique (ℕ-rec-prop x0 f)))

Informally it means there is a unique function inline_formula not implemented satisfying the properties :

inline_formula not implemented

So it is a faithful formalization of the theorem statement given previously.

Now, let's see a little more in detail how uniqueness is defined. The notation inline_formula not implemented for unique existence is called unique in LaTTe. The definition in the latte-prelude is as follows:

(definition unique [[?T :type] [P (==> T :type)]]

  (and (ex P)

       (single P)))

It is thus both existence (ex) and a condition (single) we might call singleness. The first one (existence) states that there is at least one element (of type T) satisfying the property P, and the second one (singleness) that there is at most one such element. The second condition is defined as follows (also in latte-prelude) :

(definition single [[?T :type] [P (==> T :type)]]

  (∀ [x y T] (==> (P x)

                  (P y)

                  (= x y))))

This says that if the property P is true for both x and y, then it must be the case that x equals y.

So now, we have a formal theorem statement, all what remains is to provide a demonstration.

A relational detour

Sadly, there is no direct proof for the ℕ-rec theorem. The main issue, here, is that the recursion principle is introduced as a functional principle, i.e. "something" that takes an input (in inline_formula not implemented) and outputs a result (in inline_formula not implemented), i.e. inline_formula not implemented is all we know. But in order to construct such a function inline_formula not implemented, we need to adopt a relational point of view. In set theory, everything is a set so functions are also represented as sets (unlike in type theory). In our case, we are looking for a subset of inline_formula not implemented, the Cartesian product containing pairs of the form inline_formula not implemented with inline_formula not implemented and inline_formula not implemented. This makes inline_formula not implemented a relation and this is this relational point of view that will prove useful for our demonstration.

The question, now, is how to represent a relation in type theory (and LaTTe)? A function from a type A to a type B has type (==> A B) . For a relation with domain A and range B, the corresponding type is (==> A B :type) which can be abbreviated as (rel A B). Given an x of type A, a function f of type (==> A B) defines (f x) as an object of type B. A relation R relates an antecedent x to an image y through the notation (R x y), stating which properties must verify x and y so that the relation holds. Relations are thus (of course) more general than functions. Let's reformulate the property of our recursion principle but this time adopting a relational point of view:

(definition ℕ-rec-prop-rel [[?A :type] [x0 A] [f (==> A A)]]

  (λ [R (rel ℕ A)]

     (and (R zero x0)

       (∀ [n ℕ] (∀ [xn A] (==> (R n xn)

                               (R (succ n) (f xn))))))))

In a more standard mathematical notation, this define all the possible relations inline_formula not implemented such that inline_formula not implemented is true, provided :

inline_formula not implemented

We will connect this relational principle to the previous, functional one, at the end of our study. Our objective, for now, is to find a suitable relation ... in fact we have to find the right one, one that is indeed functional.

For a relation inline_formula not implemented to be functional, we need the following :

In our case, the relation is inline_formula not implemented and we need :

(Least) fixed points to the rescue

Most people know (or have heard) that the concept of recursion is tightly connected to the notion of (least) fixed point. In a previous article I have discussed at length the famous Knarster-Tarski least fixed point theorem. But we don't need to know about this theorem to build our solution.

First, we can asked whether there are relations (i.e. subsets) of inline_formula not implemented satisfying the property inline_formula not implemented above? In fact there are many of them! First, the complete relation inline_formula not implemented itself satisfies the property. Since all the possible pairs are in the complete relation, the property is vacuously verified. But the complete relation is by no means a function since for a given inline_formula not implemented, we have inline_formula not implemented for all inline_formula not implemented (and we need only one!). Put in other terms, the complete relation is too large.

Suppose now we have two relations inline_formula not implemented and inline_formula not implemented both verifying inline_formula not implemented, and suppose also that they are both too large. We can prove, quite easily, that inline_formula not implemented i.e. their intersection, if not empty, also satisfies the property inline_formula not implemented. To see this, we recall the definition of the intersection :

If there is a pair inline_formula not implemented in the intersection (which means it is not empty), then it is also in both inline_formula not implemented and inline_formula not implemented and thus the pair undoubtedly satisfy the property inline_formula not implemented. It is also obvious that inline_formula not implemented is smaller than both inline_formula not implemented and inline_formula not implemented. In the "worst" case the two relations are the same and the intersection is of the same "size". Now we can generalize this to any number of relations. Given a set of relations inline_formula not implemented that all satisfy inline_formula not implemented, then so is the intersection inline_formula not implemented, which is smaller. But, see! more freakin' three dots! Here it's even worth because the intersection we want is the smallest possible one. And for this, we would have to generalize the previous principle for all possible inline_formula not implemented's ... meaning one more layer of three dots!?!

The solution is in a construction called generalized intersection, which we can write as follows: inline_formula not implemented

It means that we take the intersection of all possible relations inline_formula not implemented satisfying the expected property. I always found this notation rather cryptic and not very well explained or defined. I will now exploit the proof assistant to provide what I think is a much better formulation (the original definition is there).

(definition ⋂ [[T U :type] [PROP (==> (rel T U) :type)]]

  (λ [x T] (λ [y U] (∀ [R (rel T U)]

                     (==> (PROP R)

                          (R x y))))))

This defines, more generally, something like : inline_formula not implemented for an arbitrary property inline_formula not implemented. Literally, this explains the condition under which a given pair inline_formula not implemented is a member of the generalized intersection. And the fact is that if a relation inline_formula not implemented (any relation!) satisfies a property inline_formula not implemented then inline_formula not implemented.

Intuitively, the intersection itself satisfies inline_formula not implemented. But this requires that the intersection is not empty so we cannot state a general theorem for this. Although if we suppose that it indeed satisfies the property, then it is the smallest of such relations, as illustrated by the following lemma.

Lemma : generalized intersection is smallest

Suppose inline_formula not implemented such that inline_formula not implemented , then inline_formula not implemented or, equivalently, inline_formula not implemented

The formulation in LaTTe is straightforward.

(deflemma ⋂-smallest [[T U :type] [PROP (==> (rel T U) :type)] [R (rel T U)]]

  (==> (PROP R)

    (∀ [x T] (∀ [y U] (==> ((⋂ T U PROP) x y) (R x y))))))

The proof is direct by definition, so let's do it directly in the proof assistant.

(proof '⋂-smallest

  (assume [HR (PROP R)

           x T y U

           H⋂ ((⋂ T U PROP) x y)]

    (have <a> (R x y) :by (H⋂ R HR)))

  (qed <a>))

And now we can specialize this generic (and very powerful) concept for the problem at hand.

(definition REC [[?A :type] [x0 A] [f (==> A A)]]

  (⋂ ℕ A (ℕ-rec-prop-rel x0 f)))

Here we define a relation inline_formula not implemented as the smallest one satisfying inline_formula not implemented, given inline_formula not implemented and inline_formula not implemented, i.e. inline_formula not implemented. This is, intuitively, our best candidate for being the unique function identified by the recursion theorem. But we have to prove this of course.

Proof part 1 : the candidate is suitable

Now that we have a candidate, we can summarize what we have to do with it. First, we have to show that the generalized intersection contains the expected pairs. For instance, we would like that inline_formula not implemented, which is trivial.

(deflemma REC-zero [[?A :type] [x0 A] [f (==> A A)]]

  ((REC x0 f) zero x0))

The proof is straightforward and shows the way generalized intersection is used in practice as a proof technique.

(proof 'REC-zero-lemma

  (assume [R (rel ℕ A)

           HR ((ℕ-rec-prop-rel x0 f) R)]

    (have <a> (R zero x0) :by (p/and-elim-left HR)))

  (qed <a>))

We assume an arbitrary relation inline_formula not implemented verifying the property inline_formula not implemented. Since this property is now assumed we can use it and conclude.

Of course, we also have the successor pairs :

Lemma : if inline_formula not implemented.

(deflemma REC-succ [[?A :type] [x0 A] [f (==> A A)]]

  (∀ [n ℕ] (∀ [xn A] (==> ((REC x0 f) n xn)

                       ((REC x0 f) (succ n) (f xn))))))

(proof 'REC-succ-lemma

  (assume [n ℕ xn A

           Hn ((REC x0 f) n xn)]

    (assume [R (rel ℕ A)

             HR ((ℕ-rec-prop-rel x0 f) R)]

      (have <a> (R n xn) :by (Hn R HR))

      (have <b> (R (succ n) (f xn))

        :by ((p/and-elim-right HR) n xn <a>))))

  (qed <b>))))

This helps us to conclude one part of the proof that is most of the time assumed without details, overlooking the non-emptiness issue...

Theorem : inline_formula not implemented

(defthm REC-prop [[?A :type] [x0 A] [f (==> A A)]]

  ((ℕ-rec-prop-rel x0 f) (REC x0 f)))

(proof 'REC-prop-thm

  (qed (p/and-intro (REC-zero x0 f) (REC-succ x0 f))))

Proof part 2 : Existence

Now that we have a good candidate satisfying the expected property, we arrive at the core of the proof : showing that it is indeed functional.

A relation inline_formula not implemented happens to be a function, when it is total, i.e. that for a given inline_formula not implemented in its domain, there must exist (at least) an inline_formula not implemented in its codomain such that inline_formula not implemented. This gives us our first non-trivial lemma.

Lemma : REC is total

inline_formula not implemented

Proof :

We proceed by induction on inline_formula not implemented.

• case inline_formula not implemented

We know that inline_formula not implemented by REC-zero above so it is enough to conclude in this case.

• case inline_formula not implemented

We assume that there exists and inline_formula not implemented such that inline_formula not implemented (induction hypothesis). We have to prove then, that there exists an inline_formula not implemented such that inline_formula not implemented. Thanks to our induction hypothesis, and applying lemma REC-succ, we know that inline_formula not implemented. So posing inline_formula not implemented allows to conclude this case.

By the induction principle on natural numbers, we obtain the desired conclusion

We now give the formal version of the lemma as well as its proof.

(deflemma REC-exists [[?A :type] [x0 A] [f (==> A A)]]

  (∀ [n ℕ] (exists [y A] ((REC x0 f) n y))))

(proof 'REC-exists-lemma

  "We proceed by induction on `n`."

  (pose R := (REC x0 f)) ;; a shortcut notation

  "Base case n=0 : we want to prove (R zero y) is true for some y."

  (have <a1> (R zero x0) :by (REC-zero x0 f))

  (have <a> (exists [y A] (R zero y))

        :by ((q/ex-intro (λ [y A] (R zero y)) x0) <a1>))

  "Inductive case"

  (assume [n ℕ

           Hn (exists [y A] (R n y))]

    (assume [y A

             Hy (R n y)]

      "We apply the REC-succ lemma with our induction hypothesis"

      (have <b1> (R (succ n) (f y))

        :by ((REC-succ x0 f) n y Hy))

      "And existence follows naturally"

      (have <b2> (exists [z A] (R (succ n) z))

            :by ((q/ex-intro (λ [z A] (R (succ n) z)) (f y)) <b1>)))

    "We can now eliminate the existential induction hypothesis"

    (have <b> (exists [z A] (R (succ n) z))

          :by ((q/ex-elim-rule (λ [y A] (R n y)) (exists [z A] (R (succ n) z)))

               Hn <b2>)))

  "Now we apply the induction principle"

  (have <c> (∀ [n ℕ] (exists [z A] (R n z)))

        :by ((ℕ-induct (λ [n ℕ] (exists [z A] (R n z))))

             <a> <b>))

  (qed <c>))

This formal proof is quite close to the informal one given previously. There is an important difference though, which is the way we deal with existentials. In informal mathematics, we have a tendency to keep implicit the handling of existence. For example, in the base case we said that since inline_formula not implemented we can conclude. In the formal proof, though, we have to add a step to introduce the existential. From what can be called the witness inline_formula not implemented we have to introduce the statement inline_formula not implemented. For this, we must use a rule, named existential introduction, which we can write semi-formally as follows :

More formally, in LaTTe this is defined (there) as follows:

(defthm ex-intro [?T :type, P (==> T :type), x T]

  (==> (P x)

       (ex P)))

In the proof above, we use this introduction for example in the step <a>:

(have <a> (exists [y A] (R zero y))

        :by ((q/ex-intro (λ [y A] (R zero y)) x0) <a1>))

We have a proof <a1> that the property P≡(λ [y A] (R zero y)) is true for y≡x0 (i.e. (P x0)≡(R zero x0) is true), and from this conclude (ex P) which is equivalent to the goal statement (exists [y A] (R zero y)). And this is thanks to the theorem ex-intro of the LaTTe prelude.

Note that there is some redundancy in the introduction rule : we repeat the property P twice. An alternative is to write the following :

(have <a> _ :by ((q/ex-intro (λ [y A] (R zero y)) x0) <a1>))

Here, we replaced the goal with an underscore _, letting LaTTe infer the correct type (and since it's an existential introduction, we know that the type will be an existential property). This is less redundant but also less readable so for the sake of pedagogy I will keep such a goal explicit in this tutorial.

The second important rule we often omit in informal proofs is existential elimination. In the our proof we wrote: "Thanks to our induction hypothesis (...)". But this completely overlooks the fact that the induction hypothesis is existential! I think the way we use the induction hypothesis should be made a little bit more explicit, with something like : "Since we know, by the induction hypothesis, that there exists (...)". In the formal proof, there cannot be any such omission of proof steps.

In LaTTe, the definition of existential elimination (there) is the following one :

(defthm ex-elim-rule [?T :type, P (==> T :type), A :type]

  (==> (ex P)

    (∀ [x T] (==> (P x) A))

    A))

As an inference rule, we would write something like the following :

The objective here is to prove some statement inline_formula not implemented from the existence of some inline_formula not implemented such that inline_formula not implemented is true. The proof method is to assume the property inline_formula not implemented true for any inline_formula not implemented, i.e. without making any assumption about inline_formula not implemented itself (excepted the fact that it satisfies inline_formula not implemented). And from this assumption prove that the goal inline_formula not implemented can be reached. Since we know that there exists a value that makes inline_formula not implemented true, and moreover that inline_formula not implemented can be demonstrated from any value satisfying the property, we can logically deduce that inline_formula not implemented is unconditionally true. This proof method is quite powerful, and we use it at step <b> of the proof:

(have <b> (exists [z A] (R (succ n) z))

          :by ((q/ex-elim-rule (λ [y A] (R n y)) (exists [z A] (R (succ n) z)))

               Hn <b2>)))

The hypothesis Hn is roughly : inline_formula not implemented. The step <b2> is a proof that inline_formula not implemented. By the existential elimination rule we thus obtain that inline_formula not implemented unconditionally.

Note, once again, that we could have reduced the level of redundancy as follows :

(have <b> _ :by ((q/ex-elim-rule (λ [y A] (R n y)) (exists [z A] (R (succ n) z)))

                 Hn <b2>)))

This ends our short but important discussion about the formalization of existential proofs.

Proof part 3 : singleness

As we explained previously, uniqueness is existence together with singleness. Previously, we demonstrated the existence part, we are now left with singleness. What we have to prove is the following.

Lemma : Singleness

In LaTTe, this is defined as follows :

(deflemma REC-single [[?A :type] [x0 A] [f (==> A A)]]

  (∀ [n ℕ] (single (λ [y A] ((REC x0 f) n y)))))

(the definition of single is given in the first part of this document)

This is where things become a little bit "hairy" or let's say a little bit fastidious because there is no deep mathematical difficulty involved.

Proof of Lemma (singleness) :

The proof is, unsurprisingly, by induction on inline_formula not implemented.

• case inline_formula not implemented

Our assumption is that inline_formula not implemented and inline_formula not implemented for some elements inline_formula not implemented. We know that inline_formula not implemented so our objective here is to show that it is not possible to have inline_formula not implemented such that inline_formula not implemented. Assume, on the contrary, that inline_formula not implemented and let's try to establish a contradiction. For this we consider the relation inline_formula not implemented without the pair inline_formula not implemented, i.e. inline_formula not implemented. We want to show that inline_formula not implemented satisfies the property inline_formula not implemented. First, since inline_formula not implemented by hypothesis, we have inline_formula not implemented. Now, if we assume a pair inline_formula not implemented then we know that inline_formula not implemented, which means inline_formula not implemented, because we have inline_formula not implemented. Because inline_formula not implemented (by Axiom 4 of the Peano arithmetic), we have inline_formula not implemented. This means that inline_formula not implemented. Now, since inline_formula not implemented the definition of inline_formula not implemented as a least fixed point tells us that inline_formula not implemented, which is a contradiction.

Assuming this auxiliary lemma (proved later on), we have that both inline_formula not implemented and inline_formula not implemented. We can thus conclude (by transitivity) that inline_formula not implemented for this base case.

• case inline_formula not implemented :

Our induction hypothesis is that the singleness property holds for some inline_formula not implemented, and our objective is to demonstrate that it also holds for inline_formula not implemented. We begin by assuming two elements inline_formula not implemented such that inline_formula not implemented and inline_formula not implemented. We have to prove that inline_formula not implemented. The reason why we prefix these elements by inline_formula not implemented is or course their connection to the function inline_formula not implemented our recursion applies. The problem now is that we are a little bit stuck. In most proofs by induction, we must find a way to apply the induction hypothesis to reach our goal. Unfortunately, this hypothesis is kind of waiting for pairs inline_formula not implemented and inline_formula not implemented but what we have are pairs whose first element are successors of inline_formula not implemented.

When there is no obvious solution, like in the present situation, we have to be a little bit more creative. As a first step, we might look at what we already know, and try to see if there is something that could make our proof progress. We know, for example, that inline_formula not implemented satisfies the property inline_formula not implemented. But this is somewhat already covered by the induction hypothesis. A second thing we know is that inline_formula not implemented is total. This is interesting because from this, we can assert that there exists an elements inline_formula not implemented in inline_formula not implemented such that inline_formula not implemented. Let's assume this by existential elimination. Because inline_formula not implemented satisfies inline_formula not implemented we know that inline_formula not implemented.

We would like, now, to show that inline_formula not implemented (and, later, the same for inline_formula not implemented). Because we don't know inline_formula not implemented it seems unlikely we can prove this directly. We will thus proceed by contradiction. Suppose that inline_formula not implemented,

We pose the relation inline_formula not implemented

This is the same set of pairs than inline_formula not implemented but without the pair inline_formula not implemented. Our objective is to show that inline_formula not implemented satisfies the property inline_formula not implemented.

First, we have inline_formula not implemented because inline_formula not implemented by definition, and moreoverinline_formula not implemented (by Axiom 3 of the Peano arithmetic, discussed in the previous part).

Now suppose inline_formula not implemented . Since inline_formula not implemented contains inline_formula not implemented, we know that inline_formula not implemented too. We now consider two possibilities for inline_formula not implemented :

• either inline_formula not implemented

We immediately have inline_formula not implemented . Using our hypothesis of induction it must be the case that inline_formula not implemented. This means, of course, that inline_formula not implemented. Moreover, we have inline_formula not implemented by definition of inline_formula not implemented and since inline_formula not implemented. It cannot be the case that inline_formula not implemented because this would means that inline_formula not implemented which we assumed false. This means that inline_formula not implemented.

• otherwise inline_formula not implemented

Since inline_formula not implemented, we have that inline_formula not implemented. Moreover, inline_formula not implemented because inline_formula not implemented. Thus, inline_formula not implemented.

Since there is no other possible value for inline_formula not implemented (by classical reasoning, which we will comment in the LaTTe version of the proof), we just proved, by induction that inline_formula not implemented satisfies the property inline_formula not implemented.

Remember the hypothesis that inline_formula not implemented. Since we now that inline_formula not implemented satisfies inline_formula not implemented then also inline_formula not implemented by definition of inline_formula not implemented (being the smallest set satisfying inline_formula not implemented). But this is in contradiction with the very definition of inline_formula not implemented, which is not supposed to contain the pair inline_formula not implemented.

This contradiction leads to the fact that inline_formula not implemented. By exactly the same reasoning we have inline_formula not implemented and thus inline_formula not implemented.

This concludes the proof by induction.

And in a way, at least for the informal mathematics, we are finished with our recursion theorem.

The formal proof

Now that we have a rather detailed proof sketch (and indeed almost a complete proof my common mathematical standards), we have everything we need to begin the formalization of the proof with LaTTe. It is a little bit like in software development : now that we have the design, we can start the implementation.

We already formally proved the existence part, so we are left with the "singleness" part, which is the most complicated.

First, for the case inline_formula not implemented we needed an auxiliary lemma, stating that there cannot by a value inline_formula not implemented such that inline_formula not implemented and inline_formula not implemented. This can be written as follows in LaTTe :

(deflemma REC-zero-aux [[?A :type] [x0 A] [f (==> A A)]]

  (∀ [y A] (==> ((REC x0 f) zero y)

                  (= y x0))))

The proof is by assuming that there is such an inline_formula not implemented, and exhibiting a contradiction. The key idea is to show that the relation inline_formula not implemented is such that inline_formula not implemented, and derive from that the fact that inline_formula not implemented, which contradicts its own definition. The formal details follow :

(proof 'REC-zero-aux-lemma

  (assume [y A

           Hy ((REC x0 f) zero y)]

    "First, we show that  (zero,x0) is in REC, by definition."

    (have <a> ((REC x0 f) zero x0) :by (REC-zero x0 f))

    "No we assume that y is distinct from x0"

    (assume [Hneq (not (= y x0))]

      "And we define our relation R = RES - {(zero, x0)},

      i.e.  R = {(n,z) | (n,z) in REC  and (n,z)≠(zero,y)."

      (pose R := (λ [n ℕ] (λ [z A] (and ((REC x0 f) n z)

                                     (not (and (= n zero) (= y z)))))))

      "Our objective, now, is to show that R satisfies the recursion

      theorem, i.e. ((ℕ-rec-prop-rel x0 f) R)"

      "First we have (R zero x0) because of <a> and the following :"

      (assume [Hneq2 (and (= zero zero) (= y x0))]

        "we cannot have (= y x0) given our assumption Hneq"

        (have <b1> p/absurd :by (Hneq (p/and-elim-right Hneq2))))

      "By contradiction, <b1> is the proof that:

       (not (and (= zero zero) (= y x0)))

      Hence:"

      (have <b> (R zero x0) :by (p/and-intro <a> <b1>))

      "Now we prove the second property of ℕ-rec-prop-rel"

      (assume [n ℕ xn A

               Hn (R n xn)]

        "We have to show, assuming (R n xn)  for some (n, xn) 

        that (R (succ n) (f xn))"

        "We start by exploiting our hypothesis Hn."

        (have <c1> ((REC x0 f) n xn) :by (p/and-elim-left Hn))

        "This give us the first condition for being in R:"

        (have <c2> ((REC x0 f) (succ n) (f xn))

          :by ((REC-succ x0 f) n xn <c1>))

        "Now we need the second condition, obtained by contradiction."

        (assume [Hneq3 (and (= (succ n) zero) (= y (f xn)))]

          (have <c3> p/absurd :by (zero-not-succ n (p/and-elim-left Hneq3))))

        "Here, <c3> is a proof of (not (and (= (succ n) zero) (= y (f xn))))"

        "And thus all the conditions are satisfied for the following:"

        (have <c> (R (succ n) (f xn)) :by (p/and-intro <c2> <c3>)))

      "So R satisfies the recurion theorem."

      (have <d> ((ℕ-rec-prop-rel x0 f) R)

        :by (p/and-intro <b> <c>))

      "And thus (zero, y) is in R"

      (have <e> (R zero y) :by (Hy R <d>))

      "And since the second condition is trivially contradicted."

      (have <f> (and (= zero zero) (= y y))

        :by (p/and-intro (eq/eq-refl zero) (eq/eq-refl y)))

      "We reached a contradiction for the assumption that y≠x0"

      (have <g> p/absurd :by ((p/and-elim-right <e>) <f>)))

    "Hence, by classical reasoning (double negation),

    the two are equal and we reached our goal!"

    (have <h> (= y x0) :by ((classic/not-not-impl (= y x0)) <g>)))

  (qed <h>))

The formal proof is a little bit more verbose than what we would maybe expect. This is mostly due to the way we expressed the relation inline_formula not implemented.

The condition (not (and (= n zero) (= y z))) has to be proved by contradiction, i.e. assuming (and (= n zero) (= y z)) (for some n and some z) and deriving a contradiction (named absurd in LaTTe) to obtain the negation.

Note, also, that in order to conclude the proof, we make use of a classical reasoning principle (classic/not-not-impl) to obtain inline_formula not implemented from inline_formula not implemented, i.e. inline_formula not implemented). I am not aware of a purely constructive proof of the recursion theorem, i.e. without requiring a classical reasoning principle.

We can now state and prove the core of the second part of the singleness proof, as a lemma.

(deflemma REC-succ-aux [[?A :type] [x0 A] [f (==> A A)]]

  (∀ [n ℕ] (∀ [y fy A]

            (==> ((REC x0 f) n y)

              ((REC x0 f) (succ n) fy)

              (∀ [z A] (==> ((REC x0 f) n z) (= z y)))

              (= fy (f y))))))

Given inline_formula not implemented and inline_formula not implemented, the hypotheses of this lemma are the following one :

1. inline_formula not implemented

2. inline_formula not implemented

3. inline_formula not implemented, which corresponds to the induction hypothesis in the final proof.

From these, the objective is to prove that inline_formula not implemented, i.e. you cannot have something else than inline_formula not implemented as an image to inline_formula not implemented.

The creative part of the prove below is to introduce the relation inline_formula not implemented we defined previously, but using a predicative version, as follows : inline_formula not implemented

(proof 'REC-succ-aux-lemma

  (assume [n ℕ y A fy A

           Hn ((REC x0 f) n y)

           Hsn ((REC x0 f) (succ n) fy)

           Hind (∀ [z A] (==> ((REC x0 f) n z) (= z y)))]

    "We proceed by contradiction"

    (assume [Hneq (not (= fy (f y)))]

      (pose Rs := (λ [m ℕ] (λ [z A]

                             (and ((REC x0 f) m z)

                                    (not (and (= m (succ n)) (= z fy)))))))

      "Our objective is to show that Rs satisfies (ℕ-rec-prop-rel x0 f)

      The first case is to show (Rs zero x0)."

      "Zero cannot be the successor of n"

      (assume [Hneq2 (and (= zero (succ n)) (= x0 fy))]

        (have <a1> p/absurd

          :by ((zero-not-succ n) (eq/eq-sym (p/and-elim-left Hneq2)))))

      "And (zero,x0) is in REC so the first case of proved"

      (have <a> (Rs zero x0) :by (p/and-intro (REC-zero x0 f) <a1>))

      "Now, the second case is to show that if (Rs k xk), for some k

      and xk, the also (Rs (succ k) (f xk))."

      (assume [k ℕ xk A

               Hk (Rs k xk)]

        "By definition of RS, we have (succ k, f(xk)) in REC."

        (have <b> ((REC x0 f) (succ k) (f xk))

          :by ((REC-succ x0 f) k xk (p/and-elim-left Hk)))

        "Now, we consider two cases : (1) either k=n or (2) k≠n

        (which relies on the classical excluded middle principle."

        (have <c> (or (= k n) (not (= k n)))

          :by (classic/excluded-middle-ax (= k n)))

        "Case (1) k=n"

        (assume [Hkn1 (= k n)]

          "We show that it cannot be the case that: f(xk)=fy"

          (assume [Hneq3 (and (= (succ k) (succ n)) (= (f xk) fy))]

            "We know that (n,xk) is in REC by definition of Rs"

            (have <d1> ((REC x0 f) n xk)

              :by (eq/rewrite (p/and-elim-left Hk) Hkn1))

            "Taking our induction hypothesis (third hypothesis), this

            means xk=y."

            (have <d2> (= xk y) :by (Hind xk <d1>))

            "Hence their image trough f is equal"

            (have <d3> (= (f xk) (f y)) :by (eq/eq-cong f <d2>))

            "By transitivity of we have: fy=f(y)"

            (have <d4> (= fy (f y))

              :by (eq/eq-trans (eq/eq-sym (p/and-elim-right Hneq3)) <d3>))

            "and this contradicts our hypothesis (Hneq)"

            (have <d> p/absurd :by (Hneq <d4>)))

          "Hence, (succ k,f(xk)) is in Rs as expected"

        (have <e> (Rs (succ k) (f xk)) :by (p/and-intro <b> <d>)))

      "Case (2) k≠n"

      (assume [Hkn2 (not (= k n))]

        "We show that the first condition of Rs is satisfied."

        (assume [Hneq4 (and (= (succ k) (succ n)) (= (f xk) fy))]

          "Since this conditions tells us that succ k=succ n

            and succ is injective, we should have k=n"

          (have <f1> (= k n)

            :by ((succ-injective k n) (p/and-elim-left Hneq4)))

          "But this contradicts the hypothesis."

          (have <f> p/absurd :by (Hkn2 <f1>)))

        "So (succ k,f(xk)) is in Rs also in this case."

        (have <g> (Rs (succ k) (f xk)) :by (p/and-intro <b> <f>)))

      "In both cases we have the same result."

      (have <h> (Rs (succ k) (f xk)) :by (p/or-elim <c> <e> <g>)))

    "From this, we obtain that Rs satisfies the recursion property."

    (have <i> ((ℕ-rec-prop-rel x0 f) Rs) :by (p/and-intro <a> <h>))

    "And since (succ n,fy) is in REC (by hypothesis) 

    it is also in Rs (since REC is smaller)."

    (have <j> (Rs (succ n) fy) :by (Hsn Rs <i>))

    "Now we obtain that the first condition of Rs is not satisfied."

    (have <k1> (and (= (succ n) (succ n)) (= fy fy))

      :by (p/and-intro (eq/eq-refl (succ n)) (eq/eq-refl fy)))

    "Hence we have a contradiction."

    (have <k> p/absurd :by ((p/and-elim-right <j>) <k1>)))

  "Since assuming fy≠f(y) leads to a contradiction, they are indeed equal."

  (have <l> (= fy (f y)) :by ((classic/not-not-impl (= fy (f y))) <k>)))

  "Which concludes the proof."

(qed <l>))

Thanks to the previous two lemmas, the main part of the proof of singleness is relatively straightforward. It is based on the induction principle for natural numbers.

(proof 'REC-single-lemma

  "We give the name P to the property to be proved."

  (pose P := (λ [n ℕ] (q/single (λ [y A] ((REC x0 f) n y)))))

  "First we consider the base case : we want to prove (P zero)"

  "Now we list our assumptions"

  (assume [y1 A y2 A

           Hy1 ((REC x0 f) zero y1)

           Hy2 ((REC x0 f) zero y2)]

    "We have y1 and y2 such that (zero,y1) and (zero,y2) are both in REC.

    And we want to show that y1=y2."

    "First, y1=x0  thanks to the REC-zero-aux lemma above."

    (have <a1> (= y1 x0) :by ((REC-zero-aux x0 f) y1 Hy1))

    "And also y2=x0 of course."

    (have <a2> (= y2 x0) :by ((REC-zero-aux x0 f) y2 Hy2))

    "This makes y1 equal to y2 as expected."

    (have <a3> (= y1 y2) :by (eq/eq-trans <a1> (eq/eq-sym <a2>))))

  "Thus the property is true for zero"

  (have <a> (P zero) :by <a3>)

  "Now we consider the inductive case : assuming (P n) for some n,

  we want to prove that (P (succ n))."

  (assume [n ℕ

           Hind (P n)]

    "We list again our hypotheses"

    (assume [fy1 A fy2 A

             Hfy1 ((REC x0 f) (succ n) fy1)

             Hfy2 ((REC x0 f) (succ n) fy2)]

      "And the objective is to show that fy1=fy2"

      "As explaine in the informal proof, we need to use

      the existential part."

      (have <b> (exists [y A] ((REC x0 f) n y)) :by ((REC-exists x0 f) n))

      (assume [y A

               Hy ((REC x0 f) n y)]

        "Assuming there is some y such that (n,y) is in REC

        we will show that fy1 and fy2 are both equal to (f y)"

        "Since we will use the REC-succ-aux theorem, we need to

        show that its assumptions are met, especially the third one."

        (assume [z A

                 Hz ((REC x0 f) n z)]

          "This is were the induction hypothesis comes in."

          (have <c> (= z y) :by (Hind z y Hz Hy)))

        "And applying the lemma we obtain first that fy1=f(y)."

        (have <d> (= fy1 (f y))

          :by ((REC-succ-aux x0 f) n y fy1 Hy Hfy1 <c>))

        "And also fy2=f(y)"

        (have <e> (= fy2 (f y))

          :by ((REC-succ-aux x0 f) n y fy2 Hy Hfy2 <c>))

        "Thus fy1=fy2"

        (have <f> (= fy1 fy2) :by (eq/eq-trans <d> (eq/eq-sym <e>))))

      "(don't forget the existential elimination)"

      (have <g> (= fy1 fy2) :by (q/ex-elim <b> <f>)))

    "And we obtain (P (succ n))"

    (have <h> (P (succ n)) :by <g>))

  "Thus we can conclude by the induction principle on natural numbers"

  (qed ((ℕ-induct P) <a> <h>)))

The final straw

With the previous proof we finished the set-theoretic part of the proof for the recursion theorem. In most cases the presentation would end at this point. However our formal proof is not based on set theory but on an alternative I find vastly superior (with the biased point of view of a proof assistant implementor): type theory. What we have demonstrated in the previous section is that the relational version of the theorem was true. The relation inline_formula not implemented we defined and studied is functional, in the sense that as a function it enjoys the existential and singleness properties. However, the relation REC has type (==> ℕ A :type), or (rel ℕ A), whereas the actual recursion theorem ℕ-rec-prop requires a function rec of type (==> ℕ A).

Functional relations vs. relational functions

So first, let's discuss what does it means for a relation to be functional. A precise definition can be found in the rel (relation) namespace of the latte-sets library, with the following definition :

(definition functional [[?T ?U :type] [R (rel T U)]]

  (∀ [x T] (q/unique (λ [y U] (R x y)))))

Of course, inline_formula not implemented is functional : that's what we proved in the previous section!

(deflemma REC-functional [[?A :type] [x0 A] [f (==> A A)]]

  (functional (REC x0 f)))

(proof 'REC-functional-lemma

  (assume [n ℕ]

    (have <a> _ :by (p/and-intro ((REC-exists x0 f) n)

                      ((REC-single x0 f) n))))

  (qed <a>))

Each functional relation can be translated to a type-theoretic function, according to the following definition:

(definition relfun [[?T ?U :type] [R (rel T U)] [fproof (functional R)]]

  (λ [x T] (q/the (fproof x))))

The interpretation of this definition is the type theoretic function (of type (==> T U)) that associates each x of type T to the unique image of x in the relation R. There is indeed a unique such image because R is functional. In more informal terms we could have written "To inline_formula not implemented is associated the unique inline_formula not implemented such that inline_formula not implemented". This is called a definite description, quantifying an element (here inline_formula not implemented) that we know is unique.

As an illustration, we can define the function associated to our relation REC, as follows:

(definition REC-fun [[?A :type] [x0 A] [f (==> A A)]]

  (relfun (REC x0 f) (REC-functional x0 f)))

Given a property P and a proof u of (unique P), then the definite description (the u) satisfies (of course!) P, i.e. we have (P (the u)). The proof of this fact is itself written (the-prop U). This is defined in an axiomatic way in the LaTTe prelude.

The important consequence for relfun is the following:

(defthm relfun-img-prop [[?T ?U :type] [R (rel T U)] [fproof (functional R)]]

  (∀ [x T] (R x ((relfun R fproof) x))))

This simply says that x is associated to its relational image y in R.

(we omit this rather trivial proof, to keep our focus on the natural number issues, but of course it is is available).

As a direct consequence, we have the following:

(deflemma REC-fun-img-prop [[?A :type] [x0 A] [f (==> A A)]]

  (∀ [n ℕ] ((REC x0 f) n ((REC-fun x0 f) n))))

(proof 'REC-fun-img-prop-lemma

  (qed (rel/relfun-img-prop (REC x0 f) (REC-functional x0 f))))

The following is most useful :

(defthm relfun-img [[?T ?U :type] [R (rel T U)] [Rfun (functional R)]]

  (∀ [x T] (∀ [y U]

            (==> (R x y) (= ((relfun R Rfun) x) y)))))

And its consequence is the following :

(deflemma REC-fun-img [[?A :type] [x0 A] [f (==> A A)]]

  (∀ [n ℕ] (∀ [xn A] (==> ((REC x0 f) n xn)

                       (= ((REC-fun x0 f) n) xn)))))

(proof 'REC-fun-img-lemma

  (qed (rel/relfun-img (REC x0 f) (REC-functional x0 f))))

For example, let's show that the image of zero through REC-fun is the expected x0:

(deflemma REC-fun-zero [[?A :type] [x0 A] [f (==> A A)]]

  (= ((REC-fun x0 f) zero) x0))

(proof 'REC-fun-zero-lemma

  (have <a> ((REC x0 f) zero x0) :by (REC-zero x0 f))

  (qed ((REC-fun-img x0 f) zero x0 <a>)))

The end of the relational detour

We have now everything we need to prove the following :

(deflemma ℕ-rec-rel-prop

  [[?A :type] [x0 A] [f (==> A A)] [R (rel ℕ A)] [Rfun (functional R)]]

  (==> ((ℕ-rec-prop-rel x0 f) R)

       ((ℕ-rec-prop x0 f) (relfun R Rfun)))))

(proof 'ℕ-rec-rel-prop-lemma

  (assume [H _]

    (pose g := (relfun R Rfun))

    "First conjunct"

    (have <a1> (R zero x0) :by (p/and-elim-left H))

    (have <a> (= (g zero) x0)

          :by ((rel/relfun-img R Rfun) zero x0 <a1>))

    "Second conjunct"

    (assume [n ℕ]

      (have <b1> (R n (g n)) :by ((rel/relfun-img-prop R Rfun) n))

      (have <b2> (R (succ n) (f (g n)))

            :by ((p/and-elim-right H) n (g n) <b1>))

      (have <b> (= (g (succ n)) (f (g n)))

            :by ((rel/relfun-img R Rfun) (succ n) (f (g n)) <b2>)))

    (have <c> _ :by (p/and-intro <a> <b>)))

  (qed <c>))

And thus our function (extracted from inline_formula not implemented) satisfies inline_formula not implemented:

(defthm REC-fun-prop [[?A :type] [x0 A] [f (==> A A)]]

  ((ℕ-rec-prop x0 f) (REC-fun x0 f)))

(proof 'REC-fun-prop-thm

  (have <a> ((ℕ-rec-prop-rel x0 f) (REC x0 f)) :by (REC-prop x0 f))

  (have <b> ((ℕ-rec-prop x0 f) (REC-fun x0 f)) 

    :by ((ℕ-rec-rel-prop x0 f (REC x0 f) (REC-functional x0 f)) <a>))

  (qed <b>))

The goal is near ...

(and let's try without an informal explanation)

(deflemma ℕ-rec-ex [[?A :type] [x0 A] [f (==> A A)]]

  (exists [rec (==> ℕ A)] ((ℕ-rec-prop x0 f) rec)))

(proof 'ℕ-rec-ex-lemma

  (qed ((q/ex-intro (λ [rec (==> ℕ A)]

                      ((ℕ-rec-prop x0 f) rec))

                    (REC-fun x0 f))

        (REC-fun-prop x0 f))))

(deflemma ℕ-rec-single [[?A :type] [x0 A] [f (==> A A)]]

  (∀ [g1 g2 (==> ℕ A)]

   (==> ((ℕ-rec-prop x0 f) g1)

        ((ℕ-rec-prop x0 f) g2)

        (= g1 g2))))

(proof 'ℕ-rec-single-lemma

  (assume [g1 _ g2 _

           Hg1 _ Hg2 _]

    "We proceed by induction"

    "Case zero"

    (have <a1> (= (g1 zero) x0) :by (p/and-elim-left Hg1))

    (have <a2> (= (g2 zero) x0) :by (p/and-elim-left Hg2))

    (have <a> (= (g1 zero) (g2 zero)) :by (eq/eq-trans <a1> (eq/eq-sym <a2>)))

    "Case successor"

    (assume [n ℕ

             Hn (= (g1 n) (g2 n))]

      (have <b1> (= (g1 (succ n)) (f (g1 n)))

            :by ((p/and-elim-right Hg1) n))

      (have <b2> (= (g1 (succ n)) (f (g2 n)))

            :by (eq/rewrite <b1> Hn))

      (have <b3> (= (g2 (succ n)) (f (g2 n)))

            :by ((p/and-elim-right Hg2) n))

      (have <b> (= (g1 (succ n)) (g2 (succ n)))

            :by (eq/eq-trans <b2> (eq/eq-sym <b3>))))

    "We apply the induction principle"

    (have <c> (∀ [n ℕ] (= (g1 n) (g2 n)))

          :by ((ℕ-induct (λ [n ℕ] (= (g1 n) (g2 n))))

               <a> <b>))

    "And now we use functional extensionality"

    (have <d> (= g1 g2)

          :by ((fun/functional-extensionality g1 g2) <c>)))

  (qed <d>))

In the proof above we used an important (axiomatic) principle : functional extensionality. It says that if for all possible inline_formula not implemented, we have inline_formula not implemented then we can lift the equality to the functions, concluding inline_formula not implemented (the formal definition is there).

what about a one-liner proof as a conclusion ?

;;; Made it, yaye !

(proof 'ℕ-rec-thm

  (qed (p/and-intro (ℕ-rec-ex x0 f) (ℕ-rec-single x0 f))))