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:

+-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) (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