Natural Numbers Properties

Table of Contents

1 Natural numbers properties

module Lib.Prop.Nat where

This file contains important properties of natural numbers such as the fact that Nat is a set.

1.1 Packages import

The imported packages can be accessed via the following links: 

import Stdlib.Prelude
import Lib.Hedberg
import Lib.Data.Decidability  
import Lib.Data.Empty
import Lib.Data.Nat
import Lib.Data.Unit

1.2 Observational equality

By double induction on m, n. 

Nat/eq/z : Nat → U = split
  zero → Unit
  suc _ → Empty

Nat/eq/s (n : Nat) (IH : (m : Nat) → U) : Nat → U = split
  zero → Empty
  suc m → IH m

Nat/eq : Nat → Nat → U = split
  zero → Nat/eq/z
  suc n → Nat/eq/s n
            ( Nat/eq n)

This relation is reflexive. 

Nat/eq/refl : (n : Nat) → Nat/eq n n = split
  zero → star
  suc n → Nat/eq/refl n

And coincides with Path. 

Nat/path/eq (m n : Nat) (p : Path Nat m n) : Nat/eq m n =
  J Nat m
    ( λk _. Nat/eq m k)
    ( Nat/eq/refl m) n p

Nat/eq/path/z : (n : Nat) → Nat/eq zero n → Path Nat zero n = split
  zero → λ_. refl Nat zero
  suc n → λf. ex-falso (Path Nat zero (suc n)) f

Nat/eq/path/s (m : Nat) (IH : (n : Nat) → Nat/eq m n → Path Nat m n) : (n : Nat) → Nat/eq (suc m) n → Path Nat (suc m) n = split
  zero → λf. ex-falso (Path Nat (suc m) zero) f
  suc n → λp. ap Nat Nat
                ( λk. suc k) m n
                ( IH n p)

Nat/eq/path : (m n : Nat) → Nat/eq m n → Path Nat m n = split
  zero → Nat/eq/path/z
  suc m → Nat/eq/path/s m
            ( Nat/eq/path m)

1.3 Equality is decidable

Using the observational equality, we show that Nat has a decidable equality. 

Nat/has-decidable-eq/z : (n : Nat) → is-decidable (Nat/eq zero n) = split
  zero → is-decidable/Unit
  suc n → is-decidable/Empty

Nat/has-decidable-eq/s (m : Nat) (IH : (n : Nat) → is-decidable (Nat/eq m n)) : (n : Nat) → is-decidable (Nat/eq (suc m) n) = split
  zero → is-decidable/Empty
  suc n → IH n

Nat/has-decidable-eq' : (m n : Nat) → is-decidable (Nat/eq m n) = split
  zero → Nat/has-decidable-eq/z
  suc m → Nat/has-decidable-eq/s m
            ( Nat/has-decidable-eq' m)

Nat/has-decidable-eq : has-decidable-equality Nat =
  λm n. Coprod/map
          ( Nat/eq m n)
          ( neg (Nat/eq m n))
          ( Path Nat m n)
          ( neg (Path Nat m n))
          ( Nat/eq/path m n)
          ( λf p. f (Nat/path/eq m n p))
          ( Nat/has-decidable-eq' m n)

1.4 Nat is a set

Nat/is-set : is-set Nat =
  hedberg Nat
    ( Nat/has-decidable-eq)

1.5 Equality of nat live in propositions

Nat/eq/Prop (m n : Nat) : UU-Prop =
  ( Path Nat m n,
    Nat/is-set m n)

1.6 Ordering relation

We define the ordering relation ≤ on Nat. 

le/s (m : Nat) (IH : Nat → Prop) : Nat → Prop = split
  zero → Empty/Prop
  suc n → IH n

le : Nat → Nat → Prop = split
  zero → λ_. Unit/Prop
  suc m → le/s m (le m)

This relation defines a poset; that is, it is reflexive, transitive and antisymmetric. 

le/is-reflexive : (n : Nat) → Prop/type (le n n) = split
  zero → star
  suc n → le/is-reflexive n

le/lower-bound : (n : Nat) → Prop/type (le zero n) = split
  zero → star
  suc n → le/lower-bound n

le/suc/s (m : Nat) (IH : (n : Nat) → Prop/type (le m n) → Prop/type (le m (suc n)))
            : (n : Nat) → Prop/type (le (suc m) n) → Prop/type (le (suc m) (suc n)) = split
  zero → ex-falso (Prop/type (le (suc m) one-Nat))
  suc n → λle-sm-sn. IH n le-sm-sn

le/suc : (m n : Nat) (le-m-n : Prop/type (le m n)) → Prop/type (le m (suc n)) = split
  zero → λn _. le/lower-bound (suc n)
  suc m → le/suc/s m (le/suc m)

le/left-inj (m : Nat) : (n : Nat) → Prop/type (le (suc m) n) → Prop/type (le m n) = split
  zero → ex-falso (Prop/type (le m zero)) 
  suc n → λle-sm-sn. le/suc m n le-sm-sn

le/is-antisymmetric/z : (n : Nat) → Prop/type (le zero n) → Prop/type (le n zero) → Path Nat zero n = split
  zero → λ_ _. refl Nat zero
  suc n → λ_ x. ex-falso (Path Nat zero (suc n)) x

le/is-antisymmetric/s (m : Nat) (IH : (n : Nat) → Prop/type (le m n) → Prop/type (le n m) → Path Nat m n)
                         : (n : Nat) → Prop/type (le (suc m) n) → Prop/type (le n (suc m)) → Path Nat (suc m) n = split
  zero → λx _. ex-falso (Path Nat (suc m) zero) x
  suc n → λle-sm-sn le-sn-sm. ap Nat Nat (λz. suc z) m n (IH n le-sm-sn le-sn-sm)

le/is-antisymmetric : (m n : Nat) → Prop/type (le m n) → Prop/type (le n m) → Path Nat m n = split
  zero → le/is-antisymmetric/z
  suc m → le/is-antisymmetric/s m (le/is-antisymmetric m)

le/is-transitive/s' (m n : Nat) (le-sm-sn : Prop/type (le (suc m) (suc n)))
                    (IH : (p : Nat) → Prop/type (le m n) → Prop/type (le n p) → Prop/type (le m p))
                        : (p : Nat) → Prop/type (le (suc n) p) → Prop/type (le (suc m) p) = split
  zero → ex-falso (Prop/type (le (suc m) zero))
  suc p → IH p le-sm-sn

le/is-transitive/s (m : Nat) (IH : (n p : Nat) → Prop/type (le m n) → Prop/type (le n p) → Prop/type (le m p))
                      : (n p : Nat) → Prop/type (le (suc m) n) → Prop/type (le n p)
                        → Prop/type (le (suc m) p) = split
  zero → λp x _. ex-falso (Prop/type (le (suc m) p)) x
  suc n → λp le-sm-sn. le/is-transitive/s' m n le-sm-sn (IH n) p

le/is-transitive : (m n p : Nat) → Prop/type (le m n) → Prop/type (le n p)
                                 → Prop/type (le m p) = split
  zero → λ_ p _ _. le/lower-bound p
  suc m → le/is-transitive/s m (le/is-transitive m)

The ≤ relation is decidable. 

le/is-decidable/s (m : Nat) (H : (n : Nat) → is-decidable (Prop/type (le m n)))
                     : (n : Nat) → is-decidable (Prop/type (le (suc m) n)) = split
  zero → is-decidable/Empty
  suc n → H n

le/is-decidable : (m n : Nat) → is-decidable (Prop/type (le m n)) = split
  zero → λ_. is-decidable/Unit
  suc m → le/is-decidable/s m (le/is-decidable m)

We can do something friendlier, by using the fact that ¬(m ≤ n) is n ≤ m. 

le/neg' (m : Nat) (IH : (n : Nat) → neg (Prop/type (le m n)) → Prop/type (le n m))
           : (n : Nat) → (neg (Prop/type (le (suc m) n))) → Prop/type (le n (suc m)) = split
  zero → λ_. le/lower-bound (suc m)
  suc n → λf. IH n f

le/neg : (m n : Nat) (f : neg (Prop/type (le m n))) → Prop/type (le n m) = split
  zero → λn f. ex-falso (Prop/type (le n zero)) (f (le/lower-bound n))
  suc m → le/neg' m (le/neg m)

Hence: 

le/is-total' (m n : Nat) : Coprod (Prop/type (le m n)) (neg (Prop/type (le m n)))
                  → Coprod (Prop/type (le m n)) (Prop/type (le n m)) = split
  inl x → inl x
  inr nx → inr (le/neg m n nx)

le/is-total (m n : Nat) : Coprod (Prop/type (le m n)) (Prop/type (le n m)) =
  le/is-total' m n
    ( le/is-decidable m n)

We have that 1 ≤ suc k for any k. 

one-le-suc : (k : Nat) → Prop/type (le one-Nat (suc k)) = split
  zero → le/is-reflexive one-Nat
  suc k → one-le-suc k

le/double-suc/s (m : Nat) : (n : Nat) → Prop/type (le (suc m) n) → Prop/type (le (suc (suc m)) (suc n)) = split
  zero → ex-falso (Prop/type (le (suc (suc m)) one-Nat))
  suc n → λx. x

le/double-suc : (m n : Nat) → Prop/type (le m n) → Prop/type (le (suc m) (suc n)) = split
  zero → λn _. one-le-suc n
  suc m → le/double-suc/s m

1.7 Strict relation

We define the strict version of ≤. 

lt (m n : Nat) : Prop =
  le (suc m) n

Some basic properties: 

lt/suc-right (m n : Nat) (lt-m-n : Prop/type (lt m n)) : Prop/type (lt m (suc n)) =
  le/suc (suc m) n lt-m-n

lt/next (n : Nat) : Prop/type (lt n (suc n)) =
  le/is-reflexive n

lt/irreflexive : (n : Nat) → neg (Prop/type (lt n n)) = split
  zero → λx. x
  suc n → lt/irreflexive n

lt/double-suc (m n : Nat) (lt-m-n : Prop/type (lt m n)) : Prop/type (lt (suc m) (suc n)) =
  le/double-suc (suc m) n lt-m-n

If k ≤ n and n ≠ k, then k < n. 

le-neq-lt/z : (n : Nat) (f : neg (Path Nat zero n))              
                 → Prop/type (lt zero n) = split
  zero → λf. ex-falso (Prop/type (lt zero zero)) (f (refl Nat zero))
  suc n → λ_. one-le-suc n

le-neq-lt/s (k : Nat) (IH : (n : Nat) → Prop/type (le k n) → neg (Path Nat k n) → Prop/type (lt k n))
               : (n : Nat) → Prop/type (le (suc k) n) → neg (Path Nat (suc k) n)
                           → Prop/type (lt (suc k) n) = split
  zero → λx _. ex-falso (Prop/type (lt (suc k) zero)) x
  suc n → λle-sk-sn f.
    IH n le-sk-sn (λp. f (ap Nat Nat (λx. suc x) k n p))

le-neq-lt : (k n : Nat) (le-k-n : Prop/type (le k n)) (f : neg (Path Nat k n))
                 → Prop/type (lt k n) = split
  zero → λn _ f. le-neq-lt/z n f
  suc k → le-neq-lt/s k (le-neq-lt k)

If k < n, then k ≠ n. 

lt-neq (k n : Nat) (lt-k-n : Prop/type (lt k n)) : neg (Path Nat k n) =
  λp. lt/irreflexive n
        ( tr Nat k n p (λx. Prop/type (lt x n)) lt-k-n)

Of course, < is decidable. 

lt/is-decidable (k n : Nat) : is-decidable (Prop/type (lt k n)) =
  le/is-decidable (suc k) n

1.8 Well-ordering of Nat

If P is a family over Nat, we define the lower bound of P. 

is-lower-bound (P : Nat → U) (n : Nat) : U =
  (x : Nat) → P x → Prop/type (le n x)

Then, if P is a decidable family over Nat, where d witnesses the decidability, there is a function Σ(n: Nat)P(n) → Σ(m: Nat)P(m) × is-lower-boundP(m). We show a more general version of this: 

well-ordering-principle'' (Q : Nat → U) (qnz : neg (Q zero)) (n : Nat) (H : (x : Nat) → is-decidable (Q x))
                          (H' : is-lower-bound (λx. Q (suc x)) n)
                             : (x : Nat) → (q : Q x) → Prop/type (le (suc n) x) = split
  zero → λq. ex-falso (Prop/type (le (suc n) zero)) (qnz q)
  suc x → H' x

well-ordering-principle' (Q : Nat → U) (n : Nat) (H : (x : Nat) → is-decidable (Q x))
                         (IH : (Q' : Nat → U) → ((x : Nat) → is-decidable (Q' x)) → Q' n → Σ Nat (λm. (Q' m) * is-lower-bound Q' m))
                         (q : Q (suc n)) : Coprod (Q zero) (neg (Q zero))
                          → Σ Nat (λm. (Q m) * is-lower-bound Q m) = split
  inl qz → (zero, (qz, λx _. le/lower-bound x))
  inr qnz →
    let t : Σ Nat (λm. (Q (suc m)) * is-lower-bound (λx. Q (suc x)) m) = IH (λm. Q (suc m)) (λm. H (suc m)) q in
    ( suc t.1, (t.2.1, well-ordering-principle'' Q qnz t.1 H t.2.2))

well-ordering-principle-bis : (n : Nat) (Q : Nat → U) → ((x : Nat) → is-decidable (Q x)) → Q n
                             → Σ Nat (λm. (Q m) * is-lower-bound Q m) = split
  zero → λQ _ q. (zero, (q, λx _. le/lower-bound x))
  suc n → λQ H q. well-ordering-principle' Q n H (well-ordering-principle-bis n) q (H zero)

which allows us to state the actual version: 

well-ordering-principle (P : Nat → U) (H : (x : Nat) → is-decidable (P x))
                           : (Σ Nat P) → (Σ Nat (λn. (P n) * (is-lower-bound P n))) =
  λt.
    well-ordering-principle-bis t.1 P H t.2

Author: Johann Rosain

Created: 2024-07-23 Tue 13:51

Validate