Grace/Cumulus/Int/Pow.g17

Open in Workbench Download source

Imports

AbsoluteValueOrder · Nat.PowLemmas

Declarations

Source

1-- Integer powers with natural-number exponents2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Int.Pow8import AbsoluteValueOrder9import Nat.PowLemmas1011def integerPow (z : Integer, n : Nat) → Integer12  | z, zero => integerOne13  | z, succ(k) => z * integerPow(z, k)1415theorem integerPow.zero (z : Integer)16  shows integerPow(z, 0) = 117proof18  simp [integerPow]1920theorem integerPow.succ (z : Integer, n : Nat)21  shows integerPow(z, succ(n)) = z * integerPow(z, n)22proof23  simp [integerPow]2425theorem integerPow.add_one (z : Integer, n : Nat)26  shows integerPow(z, n + 1) = z * integerPow(z, n)27proof28  have shape := add.right_one at n29  rw shape30  exact integerPow.succ with *3132theorem integerPow.integer (z : Integer, n : Nat)33  shows Integer(integerPow(z, n))34proof35  induction n36  | zero =>37    rw integerPow.zero38    exact integerOne.integer39  | succ(k) using ih =>40    rw integerPow.succ41    exact integerMulValue.integer with *4243theorem integerPow.one_right (z : Integer)44  shows integerPow(z, 1) = z45proof46  simp [integerPow, integerMulValue.one_right]4748theorem integerPow.two (z : Integer)49  shows integerPow(z, 2) = z * z50proof51  simp [integerPow, integerMulValue.one_right]5253theorem integerPow.one_left (n : Nat)54  shows integerPow(integerOne, n) = 155proof56  induction n57  | zero => exact integerPow.zero at integerOne58  | succ(k) using ih =>59    rw [integerPow.succ, ih]60    ring6162theorem integerPow.zero_left (n : Nat)63  shows integerPow(integerZero, n + 1) = 064proof65  have powInteger := integerPow.integer at integerZero, n66  rw integerPow.add_one67  ring6869theorem integerPow.add (z : Integer, m n : Nat)70  shows integerPow(z, m + n) = integerPow(z, m) * integerPow(z, n)71proof72  induction n73  | zero =>74    have unit := add.right_unit at m75    have powInteger := integerPow.integer at z, m76    rw [unit, integerPow.zero]77    ring78  | succ(k) using ih =>79    have shape := add.succ_right at k, m80    have left := integerPow.integer at z, m81    have right := integerPow.integer at z, k82    rw [shape, integerPow.succ, integerPow.succ, ih]83    ring8485theorem integerPow.mul_base (x y : Integer, n : Nat)86  shows integerPow(x * y, n) = integerPow(x, n) * integerPow(y, n)87proof88  induction n89  | zero =>90    rw [integerPow.zero, integerPow.zero, integerPow.zero]91    ring92  | succ(k) using ih =>93    have product := integerMulValue.integer at x, y94    have left := integerPow.integer at x, k95    have right := integerPow.integer at y, k96    rw [integerPow.succ, integerPow.succ, integerPow.succ, ih]97    ring9899theorem integerPow.mul_exponent (z : Integer, m n : Nat)100  shows integerPow(integerPow(z, m), n) = integerPow(z, m * n)101proof102  induction n103  | zero =>104    have vanish := mul.right_zero at m105    rw [vanish, integerPow.zero, integerPow.zero]106    rfl107  | succ(k) using ih =>108    have base := integerPow.integer at z, m109    have productNat : Nat(m * k) by typecheck110    have shape : m * succ(k) = m + m * k by ring111    rw [integerPow.succ, ih, shape]112    have split := integerPow.add at z, m, m * k113    rw split114    rfl115116theorem integerPow.ofNat (a n : Nat)117  shows integerPow(integerOfNat(a), n) = integerOfNat(a ^ n)118proof119  induction n120  | zero =>121    rw [integerPow.zero, pow.zero]122    unfold integerOne123    rfl124  | succ(k) using ih =>125    have powNat := pow.closed at a, k126    rw [integerPow.succ, ih, pow.succ]127    exact integerMulValue.ofNat with *128129theorem integerPow.nonneg (z : Integer, n : Nat)130  requires nonnegative : 0 ≤ z131  shows 0 ≤ integerPow(z, n)132proof133  induction n134  | zero =>135    rw integerPow.zero136    exact integerLe.zero_one137  | succ(k) using ih =>138    have powInteger := integerPow.integer at z, k139    rw integerPow.succ140    exact integerLe.mul_nonneg with nonnegative, ih141142theorem integerPow.positive (z : Integer, n : Nat)143  requires positive : 0 < z144  shows 0 < integerPow(z, n)145proof146  induction n147  | zero =>148    rw integerPow.zero149    exact integerLess.zero_one150  | succ(k) using ih =>151    have powInteger := integerPow.integer at z, k152    rw integerPow.succ153    exact integerLess.mul_positive with positive, ih154155theorem integerPow.square_nonneg (z : Integer)156  shows 0 ≤ integerPow(z, 2)157proof158  rw integerPow.two159  exact integerLe.square_nonneg with *160161theorem integerPow.square_eq_zero_iff (z : Integer)162  shows integerPow(z, 2) = 0 ↔ z = 0163proof164  rw integerPow.two165  exact integerMulValue.square_eq_zero_iff with *166167theorem integerPow.eq_zero (z : Integer, n : Nat)168  requires zero : integerPow(z, n) = 0169  shows z = 0170proof171  induction n172  | zero =>173    intro zero174    rw integerPow.zero at zero175    have strict := integerLess.zero_one176    rw zero at strict177    exfalso178    exact integerLess.irreflexive with strict179  | succ(k) using ih =>180    intro zero181    have powInteger := integerPow.integer at z, k182    rw integerPow.succ at zero183    have split := integerMulValue.eq_zero with zero184    cases split with base | tail185    . exact base186    . exact ih with tail187188theorem integerPow.ne_zero (z : Integer, n : Nat)189  requires nonzero : z ≠ 0190  shows integerPow(z, n) ≠ 0191proof192  intro zero193  have same := integerPow.eq_zero with zero194  exact nonzero with same195196theorem integerPow.abs (z : Integer, n : Nat)197  shows integerAbs(integerPow(z, n)) = integerPow(integerAbs(z), n)198proof199  induction n200  | zero =>201    rw [integerPow.zero, integerPow.zero]202    exact integerAbs.one203  | succ(k) using ih =>204    have powInteger := integerPow.integer at z, k205    rw [integerPow.succ, integerPow.succ, integerAbs.mul, ih]206    rfl207208theorem integerPow.abs_square (z : Integer)209  shows integerPow(integerAbs(z), 2) = integerPow(z, 2)210proof211  rw [integerPow.two, integerPow.two]212  exact integerAbs.square with *213214theorem integerPow.neg_double (z : Integer, k : Nat)215  shows integerPow(-z, k + k) = integerPow(z, k + k)216proof217  have split := integerPow.add at -z, k, k218  have splitZ := integerPow.add at z, k, k219  have negPow := integerPow.integer at -z, k220  have zPow := integerPow.integer at z, k221  have square : integerPow(-z, k) * integerPow(-z, k) =222      integerPow(z, k) * integerPow(z, k)223    have product := integerPow.mul_base at -z, -z, k224    have productZ := integerPow.mul_base at z, z, k225    have shape : (-z) * (-z) = z * z by ring226    rw [← product, shape, productZ]227    rfl228  rw [split, splitZ, square]229  rfl230231theorem integerPow.neg_double_add_one (z : Integer, k : Nat)232  shows integerPow(-z, k + k + 1) = -integerPow(z, k + k + 1)233proof234  have doubleNeg := integerPow.integer at -z, k + k235  have doubleZ := integerPow.integer at z, k + k236  have even := integerPow.neg_double at z, k237  rw [integerPow.add_one, integerPow.add_one, even]238  ring239240theorem integerPow.base_monotone (x y : Integer, n : Nat)241  requires nonnegative : 0 ≤ x242  requires below : x ≤ y243  shows integerPow(x, n) ≤ integerPow(y, n)244proof245  induction n246  | zero =>247    rw [integerPow.zero, integerPow.zero]248    exact integerLe.reflexive with *249  | succ(k) using ih =>250    have xPow := integerPow.integer at x, k251    have yPow := integerPow.integer at y, k252    have xPowNonnegative := integerPow.nonneg at x, k with nonnegative253    rw [integerPow.succ, integerPow.succ]254    exact integerLe.mul with nonnegative, below, xPowNonnegative, ih255