open import 1Lab.Path
open import 1Lab.Type

open import Data.Nat.Base

open import Relation.Order

module Data.Nat.Properties where

Natural Numbers - Properties🔗

This module contains proofs of arithmetic identities for the natural numbers. Since they’re mostly simple inductive arguments written in equational reasoning style, they are very lightly commented:

Addition🔗

+-associative : (x y z : Nat)  (x + y) + z  x + (y + z)
+-associative zero y z = refl
+-associative (suc x) y z =
  suc ((x + y) + z) ≡⟨ ap suc (+-associative x y z) 
  suc (x + (y + z)) 

+-zeror : (x : Nat)  x + 0  x
+-zeror zero = refl
+-zeror (suc x) =
  suc (x + 0) ≡⟨ ap suc (+-zeror x) 
  suc x       

+-sucr : (x y : Nat)  x + suc y  suc (x + y)
+-sucr zero y = refl
+-sucr (suc x) y = ap suc (+-sucr x y)

+-commutative : (x y : Nat)  x + y  y + x
+-commutative zero y = sym (+-zeror y)
+-commutative (suc x) y =
  suc (x + y) ≡⟨ ap suc (+-commutative x y) 
  suc (y + x) ≡⟨ sym (+-sucr y x) 
  y + suc x   

Multiplication🔗

*-distrib-+r : (x y z : Nat)  (x + y) * z  x * z + y * z
*-distrib-+r zero y z = refl
*-distrib-+r (suc x) y z =
  z + (x + y) * z     ≡⟨ ap₂ _+_ refl (*-distrib-+r x y z) 
  z + (x * z + y * z) ≡⟨ sym (+-associative z (x * z) (y * z)) 
  z + x * z + y * z   

*-sucr : (m n : Nat)  m * suc n  m + m * n
*-sucr zero    n = refl
*-sucr (suc m) n =
  suc m * suc n         ≡⟨⟩
  suc n + m * suc n     ≡⟨ ap₂ _+_ refl (*-sucr m n) 
  suc n + (m + m * n)   ≡⟨⟩
  suc (n + (m + m * n)) ≡⟨ ap suc (sym (+-associative n m (m * n))) 
  suc (n + m + m * n)   ≡⟨ ap  x  suc (x + m * n)) (+-commutative n m) 
  suc (m + n + m * n)   ≡⟨ ap suc (+-associative m n (m * n)) 
  suc (m + (n + m * n)) ≡⟨⟩
  suc m + suc m * n     

*-oner : (x : Nat)  x * 1  x
*-oner zero = refl
*-oner (suc x) =
  suc (x * 1) ≡⟨ ap suc (*-oner x) 
  suc x       

*-zeror : (x : Nat)  x * 0  0
*-zeror zero = refl
*-zeror (suc x) = *-zeror x

*-commutative : (x y : Nat)  x * y  y * x
*-commutative zero y    = sym (*-zeror y)
*-commutative (suc x) y =
  y + x * y ≡⟨ ap₂ _+_ refl (*-commutative x y) 
  y + y * x ≡⟨ sym (*-sucr y x) 
  y * suc x 

*-distrib-+l : (x y z : Nat)  z * (x + y)  z * x + z * y
*-distrib-+l x y z =
  z * (x + y)   ≡⟨ *-commutative z (x + y) 
  (x + y) * z   ≡⟨ *-distrib-+r x y z 
  x * z + y * z ≡⟨ ap₂ _+_ (*-commutative x z) (*-commutative y z) 
  z * x + z * y 

*-associative : (x y z : Nat)  (x * y) * z  x * (y * z)
*-associative zero y z = refl
*-associative (suc x) y z =
  (y + x * y) * z     ≡⟨ *-distrib-+r y (x * y) z 
  y * z + (x * y) * z ≡⟨ ap₂ _+_ refl (*-associative x y z) 
  y * z + x * (y * z) 

Exponentiation🔗

^-oner : (x : Nat)  x ^ 1  x
^-oner x = *-oner x

^-onel : (x : Nat)  1 ^ x  1
^-onel zero = refl
^-onel (suc x) =
  (1 ^ x) + 0 ≡⟨ +-zeror (1 ^ x) 
  (1 ^ x)     ≡⟨ ^-onel x 
  1 

^-+-hom-*r : (x y z : Nat)  x ^ (y + z)  (x ^ y) * (x ^ z)
^-+-hom-*r x zero z = sym (+-zeror (x ^ z))
^-+-hom-*r x (suc y) z =
  x * x ^ (y + z)     ≡⟨ ap (x *_) (^-+-hom-*r x y z) 
  x * (x ^ y * x ^ z) ≡⟨ sym (*-associative x (x ^ y) (x ^ z)) 
  x * x ^ y * x ^ z 

^-distrib-*r : (x y z : Nat)  (x * y) ^ z  x ^ z * y ^ z
^-distrib-*r x y zero = refl
^-distrib-*r x y (suc z) =
  x * y * (x * y) ^ z     ≡⟨ ap  a  x * y * a) (^-distrib-*r x y z) 
  x * y * (x ^ z * y ^ z) ≡⟨ sym (*-associative (x * y) (x ^ z) (y ^ z)) 
  x * y * x ^ z * y ^ z   ≡⟨ ap (_* y ^ z) (*-associative x y (x ^ z)) 
  x * (y * x ^ z) * y ^ z ≡⟨ ap  a  x * a * y ^ z) (*-commutative y (x ^ z)) 
  x * (x ^ z * y) * y ^ z ≡⟨ ap (_* y ^ z) (sym (*-associative x (x ^ z) y)) 
  x * x ^ z * y * y ^ z   ≡⟨ *-associative (x * x ^ z) y (y ^ z) 
  x * x ^ z * (y * y ^ z) 

^-*-adjunct : (x y z : Nat)  (x ^ y) ^ z  x ^ (y * z)
^-*-adjunct x zero z = ^-onel z
^-*-adjunct x (suc y) zero = ^-*-adjunct x y zero
^-*-adjunct x (suc y) (suc z) =
  x * x ^ y * (x * x ^ y) ^ z       ≡⟨ ap  a  x * x ^ y * a) (^-distrib-*r x (x ^ y) z) 
  x * x ^ y * (x ^ z * (x ^ y) ^ z) ≡⟨ ap  a  x * x ^ y * (x ^ z * a)) (^-*-adjunct x y z) 
  x * x ^ y * (x ^ z * x ^ (y * z)) ≡⟨ ap  a  x * x ^ y * a) (sym (^-+-hom-*r x z (y * z))) 
  x * x ^ y * (x ^ (z + (y * z)))   ≡⟨ *-associative x (x ^ y) (x ^ (z + y * z)) 
  x * (x ^ y * (x ^ (z + (y * z)))) ≡⟨ ap (x *_) (sym (^-+-hom-*r x y (z + y * z))) 
  x * x ^ (y + (z + y * z))         ≡⟨ ap  a  x * x ^ a) (sym (+-associative y z (y * z))) 
  x * x ^ (y + z + y * z)           ≡⟨ ap  a  x * x ^ (a + y * z)) (+-commutative y z) 
  x * x ^ (z + y + y * z)           ≡⟨ ap  a  x * x ^ a) (+-associative z y (y * z)) 
  x * x ^ (z + (y + y * z))         ≡⟨ ap  a  x * x ^ (z + a)) (sym (*-sucr y z))  
  x * x ^ (z + y * suc z) 

Ordering🔗

The ordering relation on the natural numbers is a partial order:

≤-is-preorder : is-preorder _≤_
≤-is-preorder .is-preorder.reflexive {x} = ≤-refl x
≤-is-preorder .is-preorder.transitive {x} {y} {z} = ≤-trans x y z
≤-is-preorder .is-preorder.propositional {x} {y} = ≤-prop x y

≤-is-partial-order : is-partial-order _≤_
≤-is-partial-order .is-partial-order.preorder = ≤-is-preorder
≤-is-partial-order .is-partial-order.antisym {x} {y} = ≤-antisym x y

We also have that a successor is never smaller than the number it succeeds:

¬sucx≤x : (x : Nat)  suc x  x  
¬sucx≤x (suc x) ord = ¬sucx≤x x ord

Compatibility🔗

The order relation on the natural numbers is also compatible with the arithmetic operators:

+-preserves-≤l : (x y z : Nat)  x  y  z + x  z + y
+-preserves-≤l x y zero prf = prf
+-preserves-≤l x y (suc z) prf = +-preserves-≤l x y z prf

+-preserves-≤r : (x y z : Nat)  x  y  x + z  y + z
+-preserves-≤r x y z prf = subst  a  a  y + z) (+-commutative z x)
  (subst  a  z + x  a) (+-commutative z y) (+-preserves-≤l x y z prf))

+-preserves-≤ : (x y x' y' : Nat)  x  y  x'  y'  x + x'  y + y'
+-preserves-≤ x y x' y' prf prf' = ≤-trans (x + x') (y + x') (y + y')
  (+-preserves-≤r x y x' prf) (+-preserves-≤l x' y' y prf')

*-preserves-≤l : (x y z : Nat)  x  y  z * x  z * y
*-preserves-≤l x y zero prf = tt
*-preserves-≤l x y (suc z) prf = +-preserves-≤ x y (z * x) (z * y) prf
  (*-preserves-≤l x y z prf)

*-preserves-≤r : (x y z : Nat)  x  y  x * z  y * z
*-preserves-≤r x y z prf = subst  a  a  y * z) (*-commutative z x)
  (subst  a  z * x  a) (*-commutative z y) (*-preserves-≤l x y z prf))

*-preserves-≤ : (x y x' y' : Nat)  x  y  x'  y'  x * x'  y * y'
*-preserves-≤ x y x' y' prf prf' = ≤-trans (x * x') (y * x') (y * y')
  (*-preserves-≤r x y x' prf) (*-preserves-≤l x' y' y prf')

+-reflects-≤l : (x y z : Nat)  z + x  z + y  x  y
+-reflects-≤l x y zero prf = prf
+-reflects-≤l x y (suc z) prf = +-reflects-≤l x y z prf

+-reflects-≤r : (x y z : Nat)  x + z  y + z  x  y
+-reflects-≤r x y z prf =
  +-reflects-≤l x y z
    (subst (_≤ z + y) (+-commutative x z)
    (subst (x + z ≤_) (+-commutative y z) prf))

Maximum🔗

max-assoc : (x y z : Nat)  max x (max y z)  max (max x y) z
max-assoc zero zero zero = refl
max-assoc zero zero (suc z) = refl
max-assoc zero (suc y) zero = refl
max-assoc zero (suc y) (suc z) = refl
max-assoc (suc x) zero zero = refl
max-assoc (suc x) zero (suc z) = refl
max-assoc (suc x) (suc y) zero = refl
max-assoc (suc x) (suc y) (suc z) = ap suc (max-assoc x y z)

max-≤l : (x y : Nat)  x  max x y
max-≤l zero zero = tt
max-≤l zero (suc y) = tt
max-≤l (suc x) zero = ≤-refl (suc x)
max-≤l (suc x) (suc y) = max-≤l x y

max-≤r : (x y : Nat)  y  max x y
max-≤r zero zero = tt
max-≤r zero (suc y) = ≤-refl (suc y)
max-≤r (suc x) zero = tt
max-≤r (suc x) (suc y) = max-≤r x y

Minimum🔗

min-assoc : (x y z : Nat)  min x (min y z)  min (min x y) z
min-assoc zero zero zero = refl
min-assoc zero zero (suc z) = refl
min-assoc zero (suc y) zero = refl
min-assoc zero (suc y) (suc z) = refl
min-assoc (suc x) zero zero = refl
min-assoc (suc x) zero (suc z) = refl
min-assoc (suc x) (suc y) zero = refl
min-assoc (suc x) (suc y) (suc z) = ap suc (min-assoc x y z)

min-≤l : (x y : Nat)  min x y  x
min-≤l zero zero = tt
min-≤l zero (suc y) = tt
min-≤l (suc x) zero = tt
min-≤l (suc x) (suc y) = min-≤l x y

min-≤r : (x y : Nat)  min x y  y
min-≤r zero zero = tt
min-≤r zero (suc y) = tt
min-≤r (suc x) zero = tt
min-≤r (suc x) (suc y) = min-≤r x y