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

open import Data.Nat.Order
open import Data.Dec.Base
open import Data.Nat.Base
open import Data.Sum

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   ∎

+-inj : βˆ€ k x y β†’ k + x ≑ k + y β†’ x ≑ y
+-inj zero x y p = p
+-inj (suc k) x y p = +-inj k x y (suc-inj p)

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     ∎

*-onel : (x : Nat) β†’ 1 * x ≑ x
*-onel x = +-zeror x

*-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) ∎

*-suc-inj : βˆ€ k x y β†’ x * suc k ≑ y * suc k β†’ x ≑ y
*-suc-inj k zero zero p = refl
*-suc-inj k zero (suc y) p = absurd (zero≠suc p)
*-suc-inj k (suc x) zero p = absurd (zero≠suc (sym p))
*-suc-inj k (suc x) (suc y) p = ap suc (*-suc-inj k x y (+-inj _ _ _ p))

*-suc-injβ€² : βˆ€ k x y β†’ suc k * x ≑ suc k * y β†’ x ≑ y
*-suc-injβ€² k x y p = *-suc-inj k x y (*-commutative x (suc k) Β·Β· p Β·Β· *-commutative (suc k) y)

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) ∎

CompatibilityπŸ”—

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

+-≀l : (x y : Nat) β†’ x ≀ (x + y)
+-≀l zero y = 0≀x
+-≀l (suc x) y = s≀s (+-≀l x y)

+-≀r : (x y : Nat) β†’ y ≀ (x + y)
+-≀r x zero = 0≀x
+-≀r x (suc y) = subst (Ξ» p β†’ suc y ≀ p) (sym (+-sucr x y)) (s≀s (+-≀r x y))

+-preserves-≀l : (x y z : Nat) β†’ x ≀ y β†’ (z + x) ≀ (z + y)
+-preserves-≀l .0 y zero 0≀x = 0≀x
+-preserves-≀l .0 y (suc z) 0≀x =
  s≀s (+-preserves-≀l zero y z 0≀x)
+-preserves-≀l .(suc _) .(suc _) zero (s≀s p) = s≀s p
+-preserves-≀l .(suc _) .(suc _) (suc z) (s≀s p) =
  s≀s (+-preserves-≀l (suc _) (suc _) z (s≀s p))

+-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
  (+-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 = 0≀x
*-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
  (*-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) (s≀s 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))

difference→≀ : βˆ€ {x z} y β†’ x + y ≑ z β†’ x ≀ z
difference→≀ {x} {z} zero p            = subst (x ≀_) (sym (+-zeror x) βˆ™ p) ≀-refl
difference→≀ {zero}  {z}     (suc y) p = 0≀x
difference→≀ {suc x} {zero}  (suc y) p = absurd (zeroβ‰ suc (sym p))
difference→≀ {suc x} {suc z} (suc y) p = s≀s (difference→≀ (suc y) (suc-inj p))

MonusπŸ”—

monus-zero : βˆ€ a β†’ 0 - a ≑ 0
monus-zero zero = refl
monus-zero (suc a) = refl

monus-cancell : βˆ€ k m n β†’ (k + m) - (k + n) ≑ m - n
monus-cancell zero    = Ξ» _ _ β†’ refl
monus-cancell (suc k) = monus-cancell k

monus-distribr : βˆ€ m n k β†’ (m - n) * k ≑ m * k - n * k
monus-distribr m       zero    k = refl
monus-distribr zero    (suc n) k = sym (monus-zero (k + n * k))
monus-distribr (suc m) (suc n) k =
  monus-distribr m n k βˆ™ sym (monus-cancell k (m * k) (n * k))

monus-cancelr : βˆ€ m n k β†’ (m + k) - (n + k) ≑ m - n
monus-cancelr m n k = (Ξ» i β†’ +-commutative m k i - +-commutative n k i) βˆ™ monus-cancell k m n

monus-addl : βˆ€ m n k β†’ m - (n + k) ≑ m - n - k
monus-addl zero zero k = refl
monus-addl zero (suc n) k = sym (monus-zero k)
monus-addl (suc m) zero k = refl
monus-addl (suc m) (suc n) k = monus-addl m n k

monus-commute : βˆ€ m n k β†’ m - n - k ≑ m - k - n
monus-commute m n k =
  m - n - k   β‰‘Λ˜βŸ¨ monus-addl m n k βŸ©β‰‘Λ˜
  m - (n + k) β‰‘βŸ¨ ap (m -_) (+-commutative n k) βŸ©β‰‘
  m - (k + n) β‰‘βŸ¨ monus-addl m k n βŸ©β‰‘
  m - k - n   ∎

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 = 0≀x
max-≀l zero (suc y) = 0≀x
max-≀l (suc x) zero = ≀-refl
max-≀l (suc x) (suc y) = s≀s (max-≀l x y)

max-≀r : (x y : Nat) β†’ y ≀ max x y
max-≀r zero zero = 0≀x
max-≀r zero (suc y) = ≀-refl
max-≀r (suc x) zero = 0≀x
max-≀r (suc x) (suc y) = s≀s (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 = 0≀x
min-≀l zero (suc y) = 0≀x
min-≀l (suc x) zero = 0≀x
min-≀l (suc x) (suc y) = s≀s (min-≀l x y)

min-≀r : (x y : Nat) β†’ min x y ≀ y
min-≀r zero zero = 0≀x
min-≀r zero (suc y) = 0≀x
min-≀r (suc x) zero = 0≀x
min-≀r (suc x) (suc y) = s≀s (min-≀r x y)