From Zero to Factorial (part 3)

The basic operations on 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.part3

  "Addition on 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]]

   [latte-nats.core :as nats :refer [nat = zero succ nat-induct]

    :rename {nat ℕ,nat-induct ℕ-induct}]

   [latte-nats.rec :as rec :refer [nat-recur nat-recur-prop]

    :rename {nat-recur ℕ-rec, nat-recur-prop ℕ-rec-prop}]))

Introduction

This is the third 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 the second part, we stated and demonstrated the fundamental theorem of recursion. In the LaTTe proof assistant the theorem was expressed as follows:

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

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

provided :

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

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

    (and (= (rec zero) x0)

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

In more traditional mathematics notation, the theorem says that given a function inline_formula not implemented and inline_formula not implemented, then there exists a unique function inline_formula not implemented such that: inline_formula not implemented

We spent quite some effort to prove this theorem, and in this third part we will make advantage of it to formalize the addition function for natural numbers.

What is addition ?

Addition is probably the first numerical operation we learn, at a very young age. We know, without thinking, that the addition of inline_formula not implemented and inline_formula not implemented gives inline_formula not implemented., or that inline_formula not implemented plus anything gives back that anything, ... In set theory, functions are just subsets, thus the addition is something like :

inline_formula not implemented such that inline_formula not implemented

This is not very useful because this "definition" only appeals to our intuitive understanding of addition. A better approach is to consider a recursive definition. The idea, of course, is to only use what we already defined : zero and the successor function. The following looks like an interesting starting point:

Given inline_formula not implemented, inline_formula not implemented

For example :

inline_formula not implemented

(note that when we say e.g. 3, we actually mean inline_formula not implemented, i.e. we're still in Peano arithmetics)

One slight inconvenience is that the recursion theorem expects one argument, while the addition function seems to expect two. However, we see in the definition that the first argument inline_formula not implemented is kept untouched, so we can rewrite things as follows:

Given inline_formula not implemented, inline_formula not implemented

This looks like a good candidate for the recursion theorem, maybe it's clearer with the following hints:

Given inline_formula not implemented, inline_formula not implemented

Applying the recursion theorem we obtain that the function inline_formula not implemented is unique, for an arbitrary inline_formula not implemented.

The addition function, formally

We now have everything we need to formalize the addition function in LaTTe. Of course, we begin with the function inline_formula not implemented which we define as follows:

(definition plus [m ℕ]

  (q/the (ℕ-rec m succ)))

The properties of the inline_formula not implemented function, given in the previous section (taking inline_formula not implemented and inline_formula not implemented), corresponds to the following LaTTe expression: (ℕ-rec-prop m succ) . Thanks to the recursion theorem we know that there is a single function satisfying these properties, the uniqueness property being expressed as (ℕ-rec m succ).

Since there is a single object (here, a function) satisfying these properties, it is important to be able to construct it, which relies on the definite descriptor (the) that we discussed in the previous part of the series.

What is important is that the function possesses the expected properties.

(defthm plus-zero [m ℕ]

  (= ((plus m) zero) m))

(proof 'plus-zero

  (qed (p/and-elim-left (q/the-prop (ℕ-rec m succ)))))

(defthm plus-succ [m ℕ]

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

(proof 'plus-succ

  (qed (p/and-elim-right (q/the-prop (ℕ-rec m succ)))))

These are simple (one liner) consequences of the recursion theorem.

Now, the binary addition operator is simply something like the following:

inline_formula not implemented

The formal definition is as follows:

(definition + [[m ℕ] [n ℕ]]

  ((plus m) n))

One important take away here is that if the recursion theorem is not so trivial to demonstrate, its effective use, here to define addition, is rather straightforward. I would say that this is a distinctive characteristic of important theorems.

The properties of addition

The intent of our mathematical formulation of addition is to be able to prove important properties, but what properties? There is a whole branch of mathematics that spun off the study of numbers: algebra. The basic properties of the addition operator on natural numbers are elegantly summarized by the notion of a commutative monoid. This means that addition:

• is associative: inline_formula not implemented

• has inline_formula not implemented as an identity element: inline_formula not implemented

• is commutative: inline_formula not implemented

The simplest of these is undoubtedly the identity element, we already (quasi-)proved it!

(defthm zero-identity []

  (∀ [n ℕ] (= (+ n zero) n)))

(proof 'zero-identity

  (assume [n ℕ]

    (have <a> (= (+ n zero) n) :by (plus-zero n)))

  (qed <a>))

Since zero-identity is just a rephrasing of plus-zero, unsurprisingly we can do the same with plus-succ.

(defthm add-succ []

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

(proof 'add-succ

  (assume [m ℕ

           n ℕ]

    (have <a> _ :by ((plus-succ m) n)))

  (qed <a>))

Associativity

The property of associativity is of primary importance. It says two important things :

• addition is not "just" a binary operator, it can be applied to an arbitrary number of operand, e.g. inline_formula not implemented is a legitimate notation

• the order in which the underlying inline_formula not implemented operations are applied is not significant, e.g. we can "perform" inline_formula not implemented and then inline_formula not implemented or, alternatively inline_formula not implemented and then inline_formula not implemented.

Let's first state the property in LaTTe.

(defthm add-assoc []

  (forall [m n p ℕ] (= (+ (+ m n) p)

                      (+ m (+ n p)))))

For the proof, it is of course based on the induction principle on natural numbers, but what should apply induction to: inline_formula not implemented, inline_formula not implemented or inline_formula not implemented ? Since there are only three possible choices, we could try them in turn. First, we could first prove commutativity, which would simplify the problem. But it is interesting to highlight the fact that the two properties are in fact independent. So let's try to find an alternative approach. We know that inline_formula not implemented is in fact inline_formula not implemented and thus the right argument is let's say "more" concerned by the induction definition. So a good hint is to prioritize the rightmost argument. In the theorem statement, inline_formula not implemented is always on the left, inline_formula not implemented occurs both on the left and on the right, and inline_formula not implemented is always rightmost. Thus, intuitively it seems that inline_formula not implemented would be our "best" candidate.

So let's try to prove our property by induction on inline_formula not implemented.

• case inline_formula not implemented

inline_formula not implemented

• case inline_formula not implemented

Suppose inline_formula not implemented (induction hypothesis).

inline_formula not implemented

Thus the property is true for inline_formula not implemented, which finishes the proof.

Exercise : try to prove associativity by induction on n, by induction on m. Is communtativity needed ?

The formal proof

(proof 'add-assoc

  (assume [m ℕ n ℕ]

    (pose P := (lambda [p ℕ] (= (+ (+ m n) p)

                               (+ m (+ n p)))))

    "Case (P zero)"

    (have <a1> (= (+ (+ m n) zero) (+ m n))

      :by (zero-identity (+ m n)))

    (have <a2> (= (+ m n) (+ m (+ n zero)))

      :by (eq/eq-cong (plus m) (eq/eq-sym (zero-identity n))))

    (have <a> (P zero) :by (eq/eq-trans <a1> <a2>))

    "Case (P (succ p))"

    (assume [p ℕ

             Hind (P p)]

      (have <b1> (= (+ (+ m n) (succ p))

                   (succ (+ (+ m n) p)))

        :by (add-succ (+ m n) p))

      (have <b2> (= (succ (+ (+ m n) p))

                   (succ (+ m (+ n p))))

        :by (eq/eq-cong succ Hind))

      (have <b3> (= (succ (+ m (+ n p)))

                   (+ m (succ (+ n p))))

        :by (eq/eq-sym (add-succ m (+ n p))))

      (have <b4> (= (+ m (succ (+ n p)))

                   (+ m (+ n (succ p))))

        :by (eq/eq-cong (plus m) (eq/eq-sym (add-succ n p))))

      (have <b> (P (succ p)) :by (eq/eq-trans* <b1> <b2> <b3> <b4>)))

    "We apply the induction principle"

    (have <c> _ :by ((ℕ-induct P) <a> <b>)))

  (qed <c>))

Commutativity

For commutativity, the proof is a little bit more involved, and relies on the induction principle for natural numbers. The property to prove is inline_formula not implemented with inline_formula not implemented, for an arbitrary inline_formula not implemented.

• case inline_formula not implemented

we have to prove inline_formula not implemented and we already know, by zero-identity, that inline_formula not implemented. We need also to demonstrate that inline_formula not implemented, which requires a proof by induction. We have inline_formula not implemented as a special case of zero-identity, and if we suppose that inline_formula not implemented for an arbitrary inline_formula not implemented, then:

inline_formula not implemented

Hence inline_formula not implemented as expected, and thus inline_formula not implemented is true.

• case inline_formula not implemented

For an arbitrary inline_formula not implemented we assume inline_formula not implemented as an hypothesis of induction. Now we must demonstrate inline_formula not implemented i.e. inline_formula not implemented.

inline_formula not implemented

The last step cannot be justified yet. We need to show that inline_formula not implemented.

Assuming this (and proved in the next section), we have inline_formula not implemented, which concludes the demonstration

The formal proof

We have almost everything we need to formalize the commutativity of addition in LaTTe.

(defthm add-commute []

  (∀ [m n ℕ] (= (+ m n) (+ n m))))

Before starting the proof, let's state and prove the auxiliary lemma that is hinted in the informal proof (case inline_formula not implemented).

(deflemma zero-identity-right []

  (∀ [n ℕ] (= (+ zero n) n)))

(proof 'zero-identity-right

  (pose P := (lambda [n ℕ] (= (+ zero n) n)))

  "Case (P zero)"

  (have <a> (P zero) :by (zero-identity zero))

  "Inductive case"

  (assume [n ℕ

           Hind (P n)]

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

                 (succ (+ zero n))) :by (add-succ zero n))

    (have <b2> (= (succ (+ zero n))

                 (succ n)) :by (eq/eq-cong succ Hind))

    (have <b> (P (succ n)) :by (eq/eq-trans <b1> <b2>)))

  "We apply the induction principle."

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

The second auxiliary lemma that we need is about a variant of add-succ.

(deflemma add-succ-swap []

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

(proof 'add-succ-swap

  (assume [m ℕ]

    (pose P := (lambda [n ℕ] (= (+ (succ m) n) (succ (+ m n)))))

    "The proof is by induction on n"  

    "Case (P zero)"

    (have <a1> (= (+ (succ m) zero) (succ m)) :by (zero-identity (succ m)))

    (have <a2> (= (succ m) (succ (+ m zero)))

      :by (eq/eq-cong succ (eq/eq-sym (zero-identity m))))

    (have <a> (P zero) :by (eq/eq-trans <a1> <a2>))

    "Case (P (succ n))"

    (assume [n ℕ

             Hind (P n)]

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

                   (succ (+ (succ m) n))) :by (add-succ (succ m) n))

      (have <b2> (= (succ (+ (succ m) n))

                   (succ (succ (+ m n)))) :by (eq/eq-cong succ Hind))

      (have <b3> (= (succ (succ (+ m n)))

                   (succ (+ m (succ n))))

        :by (eq/eq-cong succ (eq/eq-sym (add-succ m n))))

      (have <b> (P (succ n)) :by (eq/eq-trans* <b1> <b2> <b3>)))

    "We apply the induction principle."

    (have <c> _ :by ((ℕ-induct P) <a> <b>)))

  (qed <c>))  

And now we can finalize the commutativity proof.

(proof 'add-commute

  (assume [m ℕ]

    (pose P := (lambda [n ℕ] (= (+ m n) (+ n m))))

    "Case (P zero)"

    (have <a1> (= (+ m zero) m) :by (zero-identity m))

    (have <a2> (= m (+ zero m)) :by (eq/eq-sym (zero-identity-right m)))

    (have <a> (P zero) :by (eq/eq-trans <a1> <a2>))

    "Case (P (succ n))"

    (assume [n ℕ

             Hind (P n)]

      (have <b1> (= (+ m (succ n)) (succ (+ m n))) :by (add-succ m n))

      (have <b2> (= (succ (+ m n)) (succ (+ n m))) :by (eq/eq-cong succ Hind))

      (have <b3> (= (succ (+ n m)) (+ (succ n) m))

        :by (eq/eq-sym (add-succ-swap n m)))

      (have <b> (P (succ n)) :by (eq/eq-trans* <b1> <b2> <b3>)))

    "We apply the induction principle."

    (have <c> _ :by ((ℕ-induct P) <a> <b>)))

  (qed <c>))

Exercises

There are other important properties to prove about addition... Your mission, if you accept it, will be to (1) find such properties, (2) prove them (in LaTTe). This message will not destroy itself at the end...

Multiplication

It is now quite easy to define the multiplication function. Indeed, we saw that addition was a kind of iteration of the successor function. Multiplication is similarly a kind of iteration of addition. This can be made a little bit more precise with the following definition :

inline_formula not implemented

Put in more conventional terms, inline_formula not implemented and inline_formula not implemented.

In LaTTe we obtain the following.

(definition times [m ℕ]

  (q/the (ℕ-rec zero (plus m))))

The two defining properties can be made explicit thanks to the recursion theorem.

(defthm times-zero [m ℕ]

  (= ((times m) zero) zero))

(proof 'times-zero

  (qed (p/and-elim-left (q/the-prop (ℕ-rec zero (plus m))))))

(defthm times-succ [m ℕ]

  (∀ [n ℕ] (= ((times m) (succ n)) ((plus m) ((times m) n))))) 

(proof 'times-succ

  (qed (p/and-elim-right (q/the-prop (ℕ-rec zero (plus m))))))

And we are now ready for the formalization of the binary operator.

(definition × [[m ℕ] [n ℕ]]

  ((times m) n))

The properties of multiplication

Multiplication is also a commutative monoid with unit inline_formula not implemented.

Exercise : prove the commutative monoid laws

• unit element: inline_formula not implemented

• associativity: inline_formula not implemented

• commutativity: inline_formula not implemented

... and well ... the (multiplication) sky is the limit!

We're there : factorial from scratch!

(definition one []

  (succ zero))

(definition factorial [n ℕ]

  (q/the (ℕ-rec one (times (succ n)))))

Hint :

inline_formula not implemented

And that's all folks!