Contents

  1. Main Definitions
  2. Addition, Multiplication, ≤
  3. Peano Axioms
  4. Decidable Equality
  5. Basic Theorems

Main Definitions

{-# OPTIONS --without-K --safe #-}

module naturals where

open import mltt
open import negation

We define the type of natural numbers via axioms similar to the Peano ones. This is the standard definition in the Agda standard library as well as pretty much any other library. We have previously encountered this definition in our simple module Natural Numbers as well as the subsequent pragma:

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

Recall the pragma simply enables the use of digits—0, 1, 2,…—as opposed to zero, suc (zero), suc (suc (zero)),…

We are going to introduce the rest of the type formers for ℕ. The induction principle reads, just like… well, the induction principle:

ℕ-induction : ∀ {ℓ} {A : ℕ → Set ℓ} → A 0 → ( (n : ℕ) → A n → A (suc n)) → (n : ℕ) → A n
ℕ-induction a₀ f zero = a₀
ℕ-induction a₀ f (suc n) = f n (ℕ-induction a₀ f n)

This is a bit more general than the standard induction because the dependent type A : ℕ → Set ℓ is general. It becomes literally the induction principle if A takes values, that is, if in (n : ℕ) → A n the value A n is akin to a “proposition”. This is something that can be characterized once we introduce the univalence principle and the type hierarchy that it entails.

As usual, the ℕ-recursion is the induction principle applied to a non-dependent situation: 
ℕ-recursion : ∀ {ℓ} {A : Set ℓ} → A → (ℕ → A → A) → ℕ → A
ℕ-recursion {ℓ} {A} = ℕ-induction {A = λ _ → A }
There is an even more special case, that of ℕ-iteration: 
ℕ-iteration : ∀ {ℓ} {A : Set ℓ} → A → (A → A) → ℕ → A
ℕ-iteration a f = ℕ-recursion a (λ _ → f )

We have, in a sense, “proved” the induction principle by taking advantage of Agda’s structural recursion: the type checker verifies that the right hand side is, in an appropriate sense, “smaller” than the left hand side so that the definition terminates.

If following MLTT strictly, we ought to introduce every operation and property of ℕ by way of the induction principle. We will also take advantage of Agda’s structural recursion mechanism (as well as reducing to canonical terms by pattern matching on the constructors).

top ⇑

Addition, Multiplication, ≤

Like we previously did in Natural Numbers, we introduce the addition and multiplication operations. Since we have already used + and ×, we use different names. 
module ℕ-ops where

  infix 20 _+ℕ_
  infix 21 _*ℕ_
  
  _+ℕ_ : ℕ → ℕ → ℕ
  zero +ℕ n = n
  suc m +ℕ n = suc (m +ℕ n)

  _*ℕ_ : ℕ → ℕ → ℕ
  zero *ℕ n = zero
  suc m *ℕ n = m *ℕ n +ℕ n
It is possible to provide an equivalent definition of the operations based on induction on the arguments 
module ℕ-ops' where

  infix 20 _+ℕ_
  infix 21 _*ℕ_

  _+ℕ_ : ℕ → ℕ → ℕ
  m +ℕ n = h m where
      h : ℕ → ℕ 
      h = ℕ-iteration n suc

  _*ℕ_ : ℕ → ℕ → ℕ
  m *ℕ n = h m where
    h : ℕ → ℕ
    h = ℕ-iteration 0 (_+ℕ n)

In the last line above, the expression _+ℕ n denotes the function _+ℕ n : ℕ → ℕ that adds n to the right.

Let us introduce the usual order on ℕ by way of a type. We take a cue from our earlier experiment where we associated to a pair of natural number an ad hoc version of the Booleans. Here, in view of subsequent development with univalence, we use our constructed types 𝟘 and 𝟙: 
module ℕ-order where

  infix 10 _≤_
  infix 10 _≥_

  _≤_ : ℕ → ℕ → Set
  zero ≤ n = 𝟙
  suc m ≤ zero = 𝟘
  suc m ≤ suc n = m ≤ n

  _≥_ : ℕ → ℕ → Set
  m ≥ n = n ≤ m

In the above, a term p : m ≤ n constitutes a proof that m preceeds n.

top ⇑

Peano Axioms

The formation and introduction rules for the Natural Numbers given above are reminiscent of the first two Peano axioms. They are supplemented by the ℕ-induction, which would normally count as the fifth axiom. We are not including the equality equivalence relation Informally, the Peano Axioms are:

  1. \(0 ∈ ℕ\).
  2. \(∀ n ∈ ℕ, S(n) ∈ ℕ\).
  3. \(∀ m, n ∈ ℕ\), \(m=n\) if and only if \(S(m)=S(n)\).
  4. \(∀ n ∈ ℕ\), \(S(n)=0\) is false.
  5. Induction: if \(K\) is a set such that:
    • \(0 ∈ K\), and
    • \(∀ n ∈ ℕ, n ∈ K → S(n) ∈ K\),
    then \(K\) contains every natural numbers.

Let us give an account of the remaining two Peano Axioms, namely that zero is not a successor, and that if two natural numbers have equal successors, then they were equal to begin with.

As for the fact that zero is not a successor: 
zero-not-suc : (n : ℕ) → suc n ≢ 0
zero-not-suc n p = one-is-not-zero q
  where
    f : ℕ → Set
    f zero = 𝟘
    f (suc m) = 𝟙

    q : 𝟙 ≡ 𝟘
    q = ap f p

The technique is, as before, to map 0 to 𝟘 and everything else to 𝟙. Then use the previous proof that 𝟙 ≢ 𝟘. Since the latter type is simply 𝟙 ≢ 𝟘 = 𝟙 ≡ 𝟘 → 𝟘, we produce a “proof” q : 𝟙 ≡ 𝟘 by mapping our “proof,” i.e. the “suppose the contrary” statement, p : 1 ≡ 0 to the required one via ap f.

As for the remaining axiom, it amounts to the fact that suc : ℕ → ℕ is left cancellable. We use an auxiliary “predecessor” function 
pred : ℕ → ℕ
pred 0 = 0
pred (suc m) = m

suc-inj : {m n : ℕ} → suc m ≡ suc n → m ≡ n
suc-inj = ap pred

The proof is to simply “apply” the predecessor function to an identification p : suc m ≡ suc n to get one in m ≡ n.

top ⇑

Decidable Equality

ℕ has a decidable equality. This is proved as follows: 
ℕ-decidable-equality : decidable-equality ℕ
ℕ-decidable-equality zero zero = inl (idp 0)
ℕ-decidable-equality zero (suc n) = inr (≢-inv (zero-not-suc n))
ℕ-decidable-equality (suc m) zero = inr (zero-not-suc m)
ℕ-decidable-equality (suc m) (suc n) = f (ℕ-decidable-equality m n)
  where
    f : decidable (m ≡ n) → decidable (suc m ≡ suc n)
    f (inl p) = inl (ap suc p)
    f (inr q) = inr (λ x → q (suc-inj x))

top ⇑

Basic Theorems

Here we establish some basic theorems about ℕ. For the sake of illustration it will be useful to phrase some of the proofs in terms of the functions defined in the module ≡-Reasoning.

module ℕ-basic where

  open ℕ-order --public
  open ℕ-ops renaming (_+ℕ_ to _+ₙ_; _*ℕ_ to _*ₙ_)
  open ≡-Reasoning
We first prove that the operation of addition is associative: 
  +-assoc : ∀ (m n p : ℕ) → (m +ₙ n) +ₙ p ≡ m +ₙ (n +ₙ p)
  +-assoc zero n p = (zero +ₙ n) +ₙ p ≡⟨ idp (n +ₙ p) ⟩
                     (zero +ₙ (n +ₙ p)) ∎
  +-assoc (suc m) n p = ((suc m) +ₙ n) +ₙ p ≡⟨ idp _ ⟩
                        suc ((m +ₙ n) +ₙ p) ≡⟨ ap suc (+-assoc m n p) ⟩
                        suc (m +ₙ (n +ₙ p)) ∎

The above proof is inductive (on the first argument) and we have explicitly recorded the induction step, by way of an application of suc to the identification defined by +-assoc m n p, in the chain of reasoning.

We use the same inductive approach to prove that the addition is commutative. As a preliminary step, we prove that the addition can be defined by induction on the second variable (recall that the definition we gave is recursive on the first). The necessary statements are contained in the sub-module +-steps below. Those statements are used in the inductive proof that addition is commutative. 
  module +-steps where
    P₀ : (x : ℕ) → Set
    P₀ x = x ≡ x +ₙ 0
    ih₀ : (x : ℕ) → (P₀ x)
--    ih₀  = ℕ-induction {A = P₀} (idp 0) (λ _ x → ap suc x)
    ih₀ zero = idp 0
    ih₀ (suc x) = ap suc (ih₀ x)

    Pₛ : (m : ℕ) → ℕ → Set
    Pₛ m = λ y → suc (m +ₙ y) ≡ m +ₙ suc y
    ihₛ : (m y : ℕ) → (Pₛ m y)
--    ihₛ m y = ℕ-induction {A = λ m → Pₛ m y} (idp (suc y)) (λ n x → ap suc x) m
    ihₛ zero y = idp (suc y)
    ihₛ (suc m) y = ap suc (ihₛ m y) 

  +-comm : ∀ (m n : ℕ) → (m +ₙ n) ≡ (n +ₙ m)
  +-comm zero n = 0 +ₙ n ≡⟨ idp n ⟩
                  n ≡⟨ ih₀ n ⟩
                  n +ₙ 0 ∎
    where
      open +-steps

  +-comm (suc m) n = (suc m) +ₙ n ≡⟨ refl ⟩
                     suc (m +ₙ n) ≡⟨ ap suc (+-comm m n) ⟩
                     suc (n +ₙ m) ≡⟨ ihₛ n m ⟩
                     n +ₙ suc m ∎
    where
      open +-steps
Let us also prove that addition can be left and right canceled. Due to the definition of addition, left cancellation is easier. 
  +-lc : (a m n : ℕ) → a +ₙ m ≡ a +ₙ n → m ≡ n
  +-lc zero m n p = p
  +-lc (suc a) m n p = +-lc a m n (ap pred p)

  +-rc : (m n a : ℕ) → m +ₙ a ≡ n +ₙ a → m ≡ n
  +-rc m n zero p = m ≡⟨ ih₀ m ⟩
                    m +ₙ 0 ≡⟨ p ⟩
                    n +ₙ 0 ≡⟨ (ih₀ n) ⁻¹ ⟩
                    n ∎
                    where open +-steps
  +-rc m n (suc a) p = +-rc m n a (suc-inj q)
                    where
                      open +-steps
                      q : suc (m +ₙ a) ≡ suc (n +ₙ a)
                      q = suc (m +ₙ a) ≡⟨ ihₛ m a ⟩
                          m +ₙ suc a ≡⟨ p ⟩
                          n +ₙ suc a ≡⟨ (ihₛ n a) ⁻¹ ⟩
                          suc (n +ₙ a) ∎

As an exercise, prove corresponding properties for the multiplication and prove distributivity.

Continuing within the same module, let us define basic properties of the order ≤ which may be useful later on. 
  ≤-refl : (n : ℕ) → n ≤ n
  ≤-refl zero = *
  ≤-refl (suc n) = ≤-refl n

  ≤-trans : (l m n : ℕ) → l ≤ m → m ≤ n → l ≤ n
  ≤-trans zero m n  = λ _ _ → *
  ≤-trans (suc l) (suc m) (suc n) p q = ≤-trans l m n p q

  ≤-antisym : (m n : ℕ) → m ≤ n → n ≤ m → m ≡ n
  ≤-antisym zero zero p q = idp 0
  ≤-antisym (suc m) (suc n) p q = ap suc (≤-antisym m n p q)

  -- every natural precedes its successor
  ≤-suc : (n : ℕ) → n ≤ suc n
  ≤-suc zero = *
  ≤-suc (suc n) = ≤-suc n

  -- zero is an inf
  zero-inf : (n : ℕ) → 0 ≤ n
  zero-inf n = *

  -- the inf is unique
  unique-inf : (n : ℕ) → n ≤ 0 → n ≡ 0
  unique-inf zero p = refl
  unique-inf (suc n ) p = !𝟘 p -- Agda does not need this
The last line is included for demonstration purposes, but Agda will not propose it while case-splitting. In other words, while case-splitting Agda will skip the cases that compute to absurdities. 
  less-than-suc : (m n : ℕ) → m ≤ n → m ≤ suc n
  less-than-suc m n p = ≤-trans m n (suc n) p (≤-suc n)

  ≤-split : (m n : ℕ) → m ≤ suc n → (m ≤ n) + (m ≡ suc n)
  ≤-split zero n p = ₀
  ≤-split (suc m) zero p = inr (ap suc (unique-inf m p))
  ≤-split (suc m) (suc n) p = +recursion inl (inr ∘′ ap suc ) (≤-split m n p)

  infix 10 _<_
  _<_ : ℕ → ℕ → Set
  m < n = suc m ≤ n

  not<-implies-≥ : (m n : ℕ) → ¬ (m < n) → m ≥ n
  not<-implies-≥ m zero q = *
  not<-implies-≥ zero (suc n) q = q *
  not<-implies-≥ (suc m) (suc n) q = not<-implies-≥ m n q

top ⇑