feat(library/algebra/group_pow.lean,library/data/nat/power.lean): add generic power operation on monoids and groups

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

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,

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

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