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) β‘β¨ +-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 (+-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 (sucβ zero 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) *-injr : β k x y .β¦ _ : Positive k β¦ β x * k β‘ y * k β x β‘ y *-injr (suc k) x y p = *-suc-inj k x y p *-injl : β k x y .β¦ _ : Positive k β¦ β k * x β‘ k * y β x β‘ y *-injl (suc k) x y p = *-suc-inj' k x y p *-is-onel : β x n β x * n β‘ 1 β x β‘ 1 *-is-onel zero n p = p *-is-onel (suc zero) zero p = refl *-is-onel (suc (suc x)) zero p = absurd (zeroβ suc (sym (*-zeror x) β p)) *-is-onel (suc x) (suc zero) p = ap suc (sym (*-oner x)) β p *-is-onel (suc x) (suc (suc n)) p = absurd (zeroβ suc (sym (suc-inj p))) *-is-oner : β x n β x * n β‘ 1 β n β‘ 1 *-is-oner x n p = *-is-onel n x (*-commutative n x β p) *-is-zero : β x y β x * y β‘ 0 β (x β‘ 0) β (y β‘ 0) *-is-zero zero y p = inl refl *-is-zero (suc x) zero p = inr refl *-is-zero (suc x) (suc y) p = absurd (sucβ zero p) *-is-zerol : β x y β¦ _ : Positive y β¦ β x * y β‘ 0 β x β‘ 0 *-is-zerol x (suc y) p with *-is-zero x (suc y) p ... | inl p = p ... | inr q = absurd (sucβ zero q) *-is-zeror : β x y β¦ _ : Positive x β¦ β x * y β‘ 0 β y β‘ 0 *-is-zeror (suc x) y p with *-is-zero (suc x) y p ... | inl p = absurd (sucβ zero p) ... | inr q = q
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) (+-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)) monus-β€ : (x y : Nat) β x - y β€ x monus-β€ x zero = xβ€x monus-β€ zero (suc y) = 0β€x monus-β€ (suc x) (suc y) = β€-sucr (monus-β€ 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 (suc y) z (sβ€s p) = β€-trans (sβ€s (+-preserves-β€l x y z p)) (β€-refl' (sym (+-sucr z y))) +-preserves-<r : (x y z : Nat) β x < y β (x + z) < (y + z) +-preserves-<r x y z p = substβ _<_ (+-commutative z x) (+-commutative z y) (+-preserves-<l x y z p) +-preserves-< : β x y x' y' β x < y β x' < y' β (x + x') < (y + y') +-preserves-< x y x' y' p q = <-trans _ _ _ (+-preserves-<r x y x' p) (+-preserves-<l x' y' y q) *-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 (sucβ zero p) differenceββ€ {suc x} {suc z} (suc y) p = sβ€s (differenceββ€ (suc y) (suc-inj p)) nonzeroβpositive : β {x} β x β 0 β 0 < x nonzeroβpositive {zero} p = absurd (p refl) nonzeroβpositive {suc x} p = sβ€s 0β€x *-cancel-β€r : β x {y z} .β¦ _ : Positive x β¦ β (y * x) β€ (z * x) β y β€ z *-cancel-β€r (suc x) {zero} {z} p = 0β€x *-cancel-β€r (suc x) {suc y} {suc z} (sβ€s p) = sβ€s (*-cancel-β€r (suc x) {y} {z} (+-reflects-β€l (y * suc x) (z * suc x) x 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 β monus-swapl : β x y z β x + y β‘ z β y β‘ z - x monus-swapl x y z p = sym (monus-cancell x y 0) β ap (x + y -_) (+-zeror x) β ap (_- x) p monus-swapr : β x y z β x + y β‘ z β x β‘ z - y monus-swapr x y z p = sym (monus-cancelr x 0 y) β ap (_- y) p
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) max-univ : (x y z : Nat) β x β€ z β y β€ z β max x y β€ z max-univ zero zero z 0β€x 0β€x = 0β€x max-univ zero (suc y) (suc z) 0β€x (sβ€s q) = sβ€s q max-univ (suc x) zero (suc z) (sβ€s p) 0β€x = sβ€s p max-univ (suc x) (suc y) (suc z) (sβ€s p) (sβ€s q) = sβ€s (max-univ x y z p q) max-zerol : (x : Nat) β max 0 x β‘ x max-zerol zero = refl max-zerol (suc x) = refl max-zeror : (x : Nat) β max x 0 β‘ x max-zeror zero = refl max-zeror (suc x) = refl
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) min-univ : (x y z : Nat) β z β€ x β z β€ y β z β€ min x y min-univ x y zero 0β€x 0β€x = 0β€x min-univ (suc x) (suc y) (suc z) (sβ€s p) (sβ€s q) = sβ€s (min-univ x y z p q) min-zerol : (x : Nat) β min 0 x β‘ 0 min-zerol zero = refl min-zerol (suc x) = refl min-zeror : (x : Nat) β min x 0 β‘ 0 min-zeror zero = refl min-zeror (suc x) = refl
The factorial functionπ
factorial-positive : β n β Positive (factorial n) factorial-positive zero = sβ€s 0β€x factorial-positive (suc n) = *-preserves-β€ 1 (suc n) 1 (factorial n) (sβ€s 0β€x) (factorial-positive n) β€-factorial : β n β n β€ factorial n β€-factorial zero = 0β€x β€-factorial (suc n) = subst (_β€ factorial (suc n)) (*-oner (suc n)) (*-preserves-β€ (suc n) (suc n) 1 (factorial n) β€-refl (factorial-positive n))