From 8de6a4bb4cd30d8a176413dc0eaf3c6698b6c2b9 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Thu, 14 May 2015 14:48:32 +1000 Subject: [PATCH] feat(library/algebra/group_pow.lean,library/data/nat/power.lean): add generic power operation on monoids and groups --- library/algebra/group_pow.lean | 136 ++++++++++++++++++++++++++++ library/data/nat/order.lean | 2 +- library/data/nat/power.lean | 56 +++++------- library/init/reserved_notation.lean | 1 + 4 files changed, 160 insertions(+), 35 deletions(-) create mode 100644 library/algebra/group_pow.lean diff --git a/library/algebra/group_pow.lean b/library/algebra/group_pow.lean new file mode 100644 index 000000000..5915e4e68 --- /dev/null +++ b/library/algebra/group_pow.lean @@ -0,0 +1,136 @@ +/- +Copyright (c) 2015 Jeremy Avigad. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Jeremy Avigad + +The power operation on monoids and groups. We separate this from group, because it depends on +nat, which in turn depends on other parts of algebra. + +We have "pow a n" for natural number powers, and "ipow a i" for integer powers. The notation +a^n is used for the first, but users can locally redefine it to ipow when needed. + +Note: power adopts the convention that 0^0=1. +-/ +import data.nat.basic data.int.basic + +namespace algebra + +variables {A : Type} + +/- monoid -/ + +section monoid +open nat +variable [s : monoid A] +include s + +definition pow (a : A) : ℕ → A +| 0 := 1 +| (n+1) := pow n * a + +infix `^` := pow + +theorem pow_zero (a : A) : a^0 = 1 := rfl +theorem pow_succ (a : A) (n : ℕ) : a^(succ n) = a^n * a := rfl + +theorem pow_succ' (a : A) : ∀n, a^(succ n) = a * a^n +| 0 := by rewrite [pow_succ, *pow_zero, one_mul, mul_one] +| (succ n) := by rewrite [pow_succ, pow_succ' at {1}, pow_succ, mul.assoc] + +theorem one_pow : ∀ n : ℕ, 1^n = 1 +| 0 := rfl +| (succ n) := by rewrite [pow_succ, mul_one, one_pow] + +theorem pow_one (a : A) : a^1 = a := !one_mul + +theorem pow_add (a : A) (m : ℕ) : ∀ n, a^(m + n) = a^m * a^n +| 0 := by rewrite [nat.add_zero, pow_zero, mul_one] +| (succ n) := by rewrite [add_succ, *pow_succ, pow_add, mul.assoc] + +theorem pow_mul (a : A) (m : ℕ) : ∀ n, a^(m * n) = (a^m)^n +| 0 := by rewrite [nat.mul_zero, pow_zero] +| (succ n) := by rewrite [nat.mul_succ, pow_add, pow_succ, pow_mul] + +theorem pow_comm (a : A) (m n : ℕ) : a^m * a^n = a^n * a^m := +by rewrite [-*pow_add, nat.add.comm] + +end monoid + +/- commutative monoid -/ + +section comm_monoid +open nat +variable [s : comm_monoid A] +include s + +theorem mul_pow (a b : A) : ∀ n, (a * b)^n = a^n * b^n +| 0 := by rewrite [*pow_zero, mul_one] +| (succ n) := by rewrite [*pow_succ, mul_pow, *mul.assoc, mul.left_comm a] + +end comm_monoid + +section group +variable [s : group A] +include s + +section nat +open nat +theorem inv_pow (a : A) : ∀n, (a⁻¹)^n = (a^n)⁻¹ +| 0 := by rewrite [*pow_zero, inv_one] +| (succ n) := by rewrite [pow_succ, pow_succ', inv_pow, inv_mul] + +theorem pow_sub (a : A) {m n : ℕ} (H : m ≥ n) : a^(m - n) = a^m * (a^n)⁻¹ := +assert H1 : m - n + n = m, from nat.sub_add_cancel H, +have H2 : a^(m - n) * a^n = a^m, by rewrite [-pow_add, H1], +eq_mul_inv_of_mul_eq H2 + +theorem pow_inv_comm (a : A) : ∀m n, (a⁻¹)^m * a^n = a^n * (a⁻¹)^m +| 0 n := by rewrite [*pow_zero, one_mul, mul_one] +| m 0 := by rewrite [*pow_zero, one_mul, mul_one] +| (succ m) (succ n) := by rewrite [pow_succ at {1}, pow_succ' at {1}, pow_succ, pow_succ', + *mul.assoc, inv_mul_cancel_left, mul_inv_cancel_left, pow_inv_comm] + +end nat + +open int + +definition ipow (a : A) : ℤ → A +| (of_nat n) := a^n +| -[n +1] := (a^(nat.succ n))⁻¹ + +private lemma ipow_add_aux (a : A) (m n : nat) : + ipow a ((of_nat m) + -[n +1]) = ipow a (of_nat m) * ipow a (-[n +1]) := +or.elim (nat.lt_or_ge m (nat.succ n)) + (assume H : (#nat m < nat.succ n), + assert H1 : (#nat nat.succ n - m > nat.zero), from nat.sub_pos_of_lt H, + calc + ipow a ((of_nat m) + -[n +1]) = ipow a (sub_nat_nat m (nat.succ n)) : rfl + ... = ipow a (-[nat.pred (nat.sub (nat.succ n) m) +1]) : {sub_nat_nat_of_lt H} + ... = (pow a (nat.succ (nat.pred (nat.sub (nat.succ n) m))))⁻¹ : rfl + ... = (pow a (nat.succ n) * (pow a m)⁻¹)⁻¹ : + by rewrite [nat.succ_pred_of_pos H1, pow_sub a (nat.le_of_lt H)] + ... = pow a m * (pow a (nat.succ n))⁻¹ : + by rewrite [inv_mul, inv_inv] + ... = ipow a (of_nat m) * ipow a (-[n +1]) : rfl) + (assume H : (#nat m ≥ nat.succ n), + calc + ipow a ((of_nat m) + -[n +1]) = ipow a (sub_nat_nat m (nat.succ n)) : rfl + ... = ipow a (#nat m - nat.succ n) : {sub_nat_nat_of_ge H} + ... = pow a m * (pow a (nat.succ n))⁻¹ : pow_sub a H + ... = ipow a (of_nat m) * ipow a (-[n +1]) : rfl) + +theorem ipow_add (a : A) : ∀i j : int, ipow a (i + j) = ipow a i * ipow a j +| (of_nat m) (of_nat n) := !pow_add +| (of_nat m) -[n +1] := !ipow_add_aux +| -[ m+1] (of_nat n) := by rewrite [int.add.comm, ipow_add_aux, ↑ipow, -*inv_pow, pow_inv_comm] +| -[ m+1] -[n+1] := + calc + ipow a (-[ m+1] + -[n+1]) = (a^(#nat nat.succ m + nat.succ n))⁻¹ : rfl + ... = (a^(nat.succ m))⁻¹ * (a^(nat.succ n))⁻¹ : by rewrite [pow_add, pow_comm, inv_mul] + ... = ipow a (-[ m+1]) * ipow a (-[n+1]) : rfl + +theorem ipow_comm (a : A) (i j : ℤ) : ipow a i * ipow a j = ipow a j * ipow a i := +by rewrite [-*ipow_add, int.add.comm] +end group + +end algebra diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index 7cc9e2d12..0b1a25632 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -169,7 +169,7 @@ section migrate_algebra local attribute nat.linear_ordered_semiring [instance] migrate from algebra with nat - replacing has_le.ge → ge, has_lt.gt → gt + replacing dvd → dvd, has_le.ge → ge, has_lt.gt → gt hiding add_pos_of_pos_of_nonneg, add_pos_of_nonneg_of_pos, add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg, le_add_of_nonneg_of_le, le_add_of_le_of_nonneg, lt_add_of_nonneg_of_lt, lt_add_of_lt_of_nonneg, diff --git a/library/data/nat/power.lean b/library/data/nat/power.lean index 446e7ec78..048b86051 100644 --- a/library/data/nat/power.lean +++ b/library/data/nat/power.lean @@ -1,62 +1,50 @@ /- Copyright (c) 2015 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura, Jeremy Avigad -Module: data.nat.power -Authors: Leonardo de Moura - -Power +The power function on the natural numbers. -/ -import data.nat.basic data.nat.div +import data.nat.basic data.nat.order data.nat.div algebra.group_pow namespace nat -definition pow : nat → nat → nat -| a 0 := 1 -| a (succ b) := a * pow a b +section migrate_algebra + open [classes] algebra + local attribute nat.comm_semiring [instance] + local attribute nat.linear_ordered_semiring [instance] -theorem pow_zero (a : nat) : pow a 0 = 1 := -rfl + definition pow (a : ℕ) (n : ℕ) : ℕ := algebra.pow a n + migrate from algebra with nat + replacing dvd → dvd, has_le.ge → ge, has_lt.gt → gt, pow → pow + hiding add_pos_of_pos_of_nonneg, add_pos_of_nonneg_of_pos, + add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg, le_add_of_nonneg_of_le, + le_add_of_le_of_nonneg, lt_add_of_nonneg_of_lt, lt_add_of_lt_of_nonneg, + lt_of_mul_lt_mul_left, lt_of_mul_lt_mul_right, pos_of_mul_pos_left, pos_of_mul_pos_right +end migrate_algebra -theorem pow_succ (a b : nat) : pow a (succ b) = a * pow a b := -rfl - -theorem one_pow : ∀ (a : nat), pow 1 a = 1 -| 0 := rfl -| (succ a) := by rewrite [pow_succ, one_pow] - -theorem pow_one : ∀ {a : nat}, a ≠ 0 → pow a 1 = a -| 0 h := absurd rfl h -| (succ a) h := by rewrite [pow_succ, pow_zero, mul_one] - -theorem zero_pow : ∀ {a : nat}, a ≠ 0 → pow 0 a = 0 -| 0 h := absurd rfl h -| (succ a) h := by rewrite [pow_succ, zero_mul] - -theorem pow_add : ∀ (a b c : nat), pow a (b + c) = pow a b * pow a c -| a b 0 := by rewrite [add_zero, pow_zero, mul_one] -| a b (succ c) := by rewrite [add_succ, *pow_succ, pow_add a b c, mul.left_comm] +-- TODO: eventually this will be subsumed under the algebraic theorems theorem mul_self_eq_pow_2 (a : nat) : a * a = pow a 2 := show a * a = pow a (succ (succ zero)), from -by rewrite [*pow_succ, *pow_zero, mul_one] +by rewrite [*pow_succ, *pow_zero, one_mul] theorem pow_cancel_left : ∀ {a b c : nat}, a > 1 → pow a b = pow a c → b = c | a 0 0 h₁ h₂ := rfl | a (succ b) 0 h₁ h₂ := - assert aeq1 : a = 1, by rewrite [pow_succ at h₂, pow_zero at h₂]; exact (eq_one_of_mul_eq_one_right h₂), + assert aeq1 : a = 1, by rewrite [pow_succ' at h₂, pow_zero at h₂]; exact (eq_one_of_mul_eq_one_right h₂), assert h₁ : 1 < 1, by rewrite [aeq1 at h₁]; exact h₁, absurd h₁ !lt.irrefl | a 0 (succ c) h₁ h₂ := - assert aeq1 : a = 1, by rewrite [pow_succ at h₂, pow_zero at h₂]; exact (eq_one_of_mul_eq_one_right (eq.symm h₂)), + assert aeq1 : a = 1, by rewrite [pow_succ' at h₂, pow_zero at h₂]; exact (eq_one_of_mul_eq_one_right (eq.symm h₂)), assert h₁ : 1 < 1, by rewrite [aeq1 at h₁]; exact h₁, absurd h₁ !lt.irrefl | a (succ b) (succ c) h₁ h₂ := assert ane0 : a ≠ 0, from assume aeq0, by rewrite [aeq0 at h₁]; exact (absurd h₁ dec_trivial), - assert beqc : pow a b = pow a c, by rewrite [*pow_succ at h₂]; exact (mul_cancel_left_of_ne_zero ane0 h₂), + assert beqc : pow a b = pow a c, by rewrite [*pow_succ' at h₂]; exact (mul_cancel_left_of_ne_zero ane0 h₂), by rewrite [pow_cancel_left h₁ beqc] theorem pow_div_cancel : ∀ {a b : nat}, a ≠ 0 → pow a (succ b) div a = pow a b -| a 0 h := by rewrite [pow_succ, pow_zero, mul_one, div_self (pos_of_ne_zero h)] -| a (succ b) h := by rewrite [pow_succ, mul_div_cancel_left _ (pos_of_ne_zero h)] +| a 0 h := by rewrite [pow_succ', pow_zero, mul_one, div_self (pos_of_ne_zero h)] +| a (succ b) h := by rewrite [pow_succ', mul_div_cancel_left _ (pos_of_ne_zero h)] end nat diff --git a/library/init/reserved_notation.lean b/library/init/reserved_notation.lean index 8867ef0ac..f1233051f 100644 --- a/library/init/reserved_notation.lean +++ b/library/init/reserved_notation.lean @@ -68,6 +68,7 @@ reserve infixl `div`:70 reserve infixl `mod`:70 reserve infixl `/`:70 reserve prefix `-`:100 +reserve infix `^`:80 reserve infix `<=`:50 reserve infix `≤`:50