refactor(*): import content from lean/library/data and library_dev

Author: digama0

.gitignore

@@ -0,0 +1,3 @@
+*.olean
+/_target
+/leanpkg.path

algebra/group.lean

@@ -0,0 +1,206 @@
+/-
+Copyright (c) 2014 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Avigad, Leonardo de Moura
+
+Various multiplicative and additive structures.
+-/
+import pending
+
+universe variable uu
+variable {A : Type uu}
+
+section group
+  variable [group A]
+
+  variable (A)
+  theorem left_inverse_inv : function.left_inverse (λ a : A, a⁻¹) (λ a, a⁻¹) :=
+  assume a, inv_inv a
+  variable {A}
+
+  theorem inv_eq_inv_iff_eq (a b : A) : a⁻¹ = b⁻¹ ↔ a = b :=
+  iff.intro inv_inj (begin intro h, simp [h] end)
+
+  theorem inv_eq_one_iff_eq_one (a : A) : a⁻¹ = 1 ↔ a = 1 :=
+  have a⁻¹ = 1⁻¹ ↔ a = 1, from inv_eq_inv_iff_eq a 1,
+  begin rewrite this^.symm, simp end
+
+  theorem eq_one_of_inv_eq_one (a : A) : a⁻¹ = 1 → a = 1 :=
+  iff.mp (inv_eq_one_iff_eq_one a)
+
+  theorem eq_inv_iff_eq_inv (a b : A) : a = b⁻¹ ↔ b = a⁻¹ :=
+  iff.intro eq_inv_of_eq_inv eq_inv_of_eq_inv
+
+  theorem eq_of_mul_inv_eq_one {a b : A} (H : a * b⁻¹ = 1) : a = b :=
+  calc
+    a    = a * b⁻¹ * b : by simp
+     ... = b           : begin rewrite H, simp end
+
+  theorem mul_eq_iff_eq_inv_mul (a b c : A) : a * b = c ↔ b = a⁻¹ * c :=
+  iff.intro eq_inv_mul_of_mul_eq mul_eq_of_eq_inv_mul
+
+  theorem mul_eq_iff_eq_mul_inv (a b c : A) : a * b = c ↔ a = c * b⁻¹ :=
+  iff.intro eq_mul_inv_of_mul_eq mul_eq_of_eq_mul_inv
+end group
+
+/- transport versions to additive -/
+run_cmd transport_multiplicative_to_additive'
+  [  (`left_inverse_inv, `left_inverse_neg),
+     (`inv_eq_inv_iff_eq, `neg_eq_neg_iff_eq),
+     (`inv_eq_one_iff_eq_one, `neg_eq_zero_iff_eq_zero),
+     (`eq_one_of_inv_eq_one, `eq_zero_of_neg_eq_zero),
+     (`eq_inv_iff_eq_inv, `eq_neg_iff_eq_neg),
+     (`mul_right_inv, `add_right_inv),
+     (`eq_of_mul_inv_eq_one, `eq_of_add_neg_eq_zero),
+     (`mul_eq_iff_eq_inv_mul, `add_eq_iff_eq_neg_add),
+     (`mul_eq_iff_eq_mul_inv, `add_eq_iff_eq_add_neg)
+     -- (`mul_eq_one_of_mul_eq_one, `add_eq_zero_of_add_eq_zero)   not needed for commutative groups
+     -- (`muleq_one_iff_mul_eq_one, `add_eq_zero_iff_add_eq_zero)
+  ]
+
+section add_group
+  variable [add_group A]
+
+  local attribute [simp] sub_eq_add_neg
+
+  theorem eq_iff_sub_eq_zero (a b : A) : a = b ↔ a - b = 0 :=
+  iff.intro (assume h, by simp [h]) (assume h, eq_of_sub_eq_zero h)
+
+  theorem sub_eq_iff_eq_add (a b c : A) : a - b = c ↔ a = c + b :=
+  iff.intro (assume H, eq_add_of_add_neg_eq H) (assume H, add_neg_eq_of_eq_add H)
+
+  theorem eq_sub_iff_add_eq (a b c : A) : a = b - c ↔ a + c = b :=
+  iff.intro (assume H, add_eq_of_eq_add_neg H) (assume H, eq_add_neg_of_add_eq H)
+
+  theorem eq_iff_eq_of_sub_eq_sub {a b c d : A} (H : a - b = c - d) : a = b ↔ c = d :=
+  calc
+    a = b ↔ a - b = 0   : eq_iff_sub_eq_zero a b
+      ... = (c - d = 0) : by rewrite H
+      ... ↔ c = d       : iff.symm (eq_iff_sub_eq_zero c d)
+
+  theorem left_inverse_sub_add_left (c : A) : function.left_inverse (λ x, x - c) (λ x, x + c) :=
+  assume x, add_sub_cancel x c
+
+  theorem left_inverse_add_left_sub (c : A) : function.left_inverse (λ x, x + c) (λ x, x - c) :=
+  assume x, sub_add_cancel x c
+
+  theorem left_inverse_add_right_neg_add (c : A) :
+      function.left_inverse (λ x, c + x) (λ x, - c + x) :=
+  assume x, add_neg_cancel_left c x
+
+  theorem left_inverse_neg_add_add_right (c : A) :
+      function.left_inverse (λ x, - c + x) (λ x, c + x) :=
+  assume x, neg_add_cancel_left c x
+end add_group
+
+
+/-
+namespace norm_num
+reveal add.assoc
+
+def add1 [has_add A] [has_one A] (a : A) : A := add a one
+
+local attribute add1 bit0 bit1 [reducible]
+
+theorem add_comm_four [add_comm_semigroup A] (a b : A) : a + a + (b + b) = (a + b) + (a + b) :=
+sorry -- by simp
+
+theorem add_comm_middle [add_comm_semigroup A] (a b c : A) : a + b + c = a + c + b :=
+sorry -- by simp
+
+theorem bit0_add_bit0 [add_comm_semigroup A] (a b : A) : bit0 a + bit0 b = bit0 (a + b) :=
+sorry -- by simp
+
+theorem bit0_add_bit0_helper [add_comm_semigroup A] (a b t : A) (H : a + b = t) :
+        bit0 a + bit0 b = bit0 t :=
+sorry -- by rewrite -H; simp
+
+theorem bit1_add_bit0 [add_comm_semigroup A] [has_one A] (a b : A) :
+        bit1 a + bit0 b = bit1 (a + b) :=
+sorry -- by simp
+
+theorem bit1_add_bit0_helper [add_comm_semigroup A] [has_one A] (a b t : A)
+        (H : a + b = t) : bit1 a + bit0 b = bit1 t :=
+sorry -- by rewrite -H; simp
+
+theorem bit0_add_bit1 [add_comm_semigroup A] [has_one A] (a b : A) :
+        bit0 a + bit1 b = bit1 (a + b) :=
+sorry -- by simp
+
+theorem bit0_add_bit1_helper [add_comm_semigroup A] [has_one A] (a b t : A)
+        (H : a + b = t) : bit0 a + bit1 b = bit1 t :=
+sorry -- by rewrite -H; simp
+
+theorem bit1_add_bit1 [add_comm_semigroup A] [has_one A] (a b : A) :
+        bit1 a + bit1 b = bit0 (add1 (a + b)) :=
+sorry -- by simp
+
+theorem bit1_add_bit1_helper [add_comm_semigroup A] [has_one A] (a b t s: A)
+        (H : (a + b) = t) (H2 : add1 t = s) : bit1 a + bit1 b = bit0 s :=
+sorry -- by inst_simp
+
+theorem bin_add_zero [add_monoid A] (a : A) : a + zero = a :=
+sorry -- by simp
+
+theorem bin_zero_add [add_monoid A] (a : A) : zero + a = a :=
+sorry -- by simp
+
+theorem one_add_bit0 [add_comm_semigroup A] [has_one A] (a : A) : one + bit0 a = bit1 a :=
+sorry -- by simp
+
+theorem bit0_add_one [has_add A] [has_one A] (a : A) : bit0 a + one = bit1 a :=
+rfl
+
+theorem bit1_add_one [has_add A] [has_one A] (a : A) : bit1 a + one = add1 (bit1 a) :=
+rfl
+
+theorem bit1_add_one_helper [has_add A] [has_one A] (a t : A) (H : add1 (bit1 a) = t) :
+        bit1 a + one = t :=
+sorry -- by inst_simp
+
+theorem one_add_bit1 [add_comm_semigroup A] [has_one A] (a : A) : one + bit1 a = add1 (bit1 a) :=
+sorry -- by simp
+
+theorem one_add_bit1_helper [add_comm_semigroup A] [has_one A] (a t : A)
+        (H : add1 (bit1 a) = t) : one + bit1 a = t :=
+sorry -- by inst_simp
+
+theorem add1_bit0 [has_add A] [has_one A] (a : A) : add1 (bit0 a) = bit1 a :=
+rfl
+
+theorem add1_bit1 [add_comm_semigroup A] [has_one A] (a : A) :
+        add1 (bit1 a) = bit0 (add1 a) :=
+sorry -- by simp
+
+theorem add1_bit1_helper [add_comm_semigroup A] [has_one A] (a t : A) (H : add1 a = t) :
+        add1 (bit1 a) = bit0 t :=
+sorry -- by inst_simp
+
+theorem add1_one [has_add A] [has_one A] : add1 (one : A) = bit0 one :=
+rfl
+
+theorem add1_zero [add_monoid A] [has_one A] : add1 (zero : A) = one :=
+sorry -- by simp
+
+theorem one_add_one [has_add A] [has_one A] : (one : A) + one = bit0 one :=
+rfl
+
+theorem subst_into_sum [has_add A] (l r tl tr t : A) (prl : l = tl) (prr : r = tr)
+        (prt : tl + tr = t) : l + r = t :=
+sorry -- by simp
+
+theorem neg_zero_helper [add_group A] (a : A) (H : a = 0) : - a = 0 :=
+sorry -- by simp
+
+end norm_num
+
+attribute [simp]
+  zero_add add_zero one_mul mul_one
+
+attribute [simp]
+  neg_neg sub_eq_add_neg
+
+attribute [simp]
+  add.assoc add.comm add.left_comm
+  mul.left_comm mul.comm mul.assoc
+-/

algebra/group_power.lean

@@ -0,0 +1,176 @@
+/-
+Copyright (c) 2015 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Avigad, Robert Y. Lewis
+
+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 "gpow a i" for integer powers. The notation
+a^n is used for the first, but users can locally redefine it to gpow when needed.
+
+Note: power adopts the convention that 0^0=1.
+-/
+import data.nat.basic data.int.basic ..tools.auto.finish 
+
+universe u
+variable {α : Type u}
+
+class has_pow_nat (α : Type u) :=
+(pow_nat : α → nat → α)
+
+def pow_nat {α : Type u} [s : has_pow_nat α] : α → nat → α :=
+has_pow_nat.pow_nat
+
+infix ` ^ ` := pow_nat
+
+class has_pow_int (α : Type u) :=
+(pow_int : α → int → α)
+
+def pow_int {α : Type u} [s : has_pow_int α] : α → int → α :=
+has_pow_int.pow_int
+
+ /- monoid -/
+section monoid
+open nat
+
+variable [s : monoid α]
+include s
+
+def monoid.pow (a : α) : ℕ → α
+| 0     := 1
+| (n+1) := a * monoid.pow n
+
+instance monoid.has_pow_nat : has_pow_nat α :=
+has_pow_nat.mk monoid.pow
+
+@[simp] theorem pow_zero (a : α) : a^0 = 1 := rfl
+@[simp] theorem pow_succ (a : α) (n : ℕ) : a^(succ n) = a * a^n := rfl
+@[simp] theorem pow_one (a : α) : a^1 = a := mul_one _
+
+theorem pow_succ' (a : α) : ∀ (n : ℕ), a^(succ n) = (a^n) * a 
+| 0        := by simp 
+| (succ n) :=
+ suffices a * (a ^ n * a) = a * a ^ succ n, by simp [this],
+ by rw <-pow_succ'
+
+@[simp] theorem one_pow : ∀ n : ℕ, (1 : α)^n = (1:α)
+| 0        := rfl
+| (succ n) := by simp; rw one_pow
+
+theorem pow_add (a : α) : ∀ m n : ℕ, a^(m + n) = a^m * a^n 
+| m 0 := by simp
+| m (n+1) := by rw [add_succ, pow_succ', pow_succ', pow_add, mul_assoc]
+
+theorem pow_mul (a : α) (m : ℕ) : ∀ n, a^(m * n) = (a^m)^n
+| 0        := by simp
+| (succ n) := by rw [nat.mul_succ, pow_add, pow_succ', pow_mul]
+
+theorem pow_comm (a : α) (m n : ℕ)  : a^m * a^n = a^n * a^m :=
+by rw [←pow_add, ←pow_add, add_comm]
+
+end monoid
+
+/- commutative monoid -/
+
+section comm_monoid
+open nat
+variable [s : comm_monoid α]
+include s
+
+theorem mul_pow (a b : α) : ∀ n, (a * b)^n = a^n * b^n
+| 0        := by simp 
+| (succ n) := by simp; rw mul_pow
+
+end comm_monoid
+
+section group
+variable [s : group α]
+include s
+
+section nat
+open nat
+theorem inv_pow (a : α) : ∀n, (a⁻¹)^n = (a^n)⁻¹
+| 0        := by simp
+| (succ n) := by rw [pow_succ', _root_.pow_succ, mul_inv_rev, inv_pow] 
+
+theorem pow_sub (a : α) {m n : ℕ} (h : m ≥ n) : a^(m - n) = a^m * (a^n)⁻¹ :=
+have h1 : m - n + n = m, from nat.sub_add_cancel h,
+have h2 : a^(m - n) * a^n = a^m, by rw [←pow_add, h1],
+eq_mul_inv_of_mul_eq h2
+
+theorem pow_inv_comm (a : α) : ∀m n, (a⁻¹)^m * a^n = a^n * (a⁻¹)^m
+| 0 n               := by simp
+| m 0               := by simp
+| (succ m) (succ n) := calc
+  a⁻¹ ^ succ m * a ^ succ n = (a⁻¹ ^ m * a⁻¹) * (a * a^n) : by rw [pow_succ', _root_.pow_succ]
+                        ... = a⁻¹ ^ m * (a⁻¹ * a) * a^n : by simp
+                        ... = a⁻¹ ^ m * a^n : by simp
+                        ... = a ^ n * (a⁻¹)^m : by rw pow_inv_comm
+                        ... = a ^ n * (a * a⁻¹) * (a⁻¹)^m : by simp
+                        ... = (a^n * a) * (a⁻¹ * (a⁻¹)^m) : by simp only [mul_assoc]
+                        ... = a ^ succ n * a⁻¹ ^ succ m : by rw [pow_succ', _root_.pow_succ]; simp
+
+end nat
+
+open int
+
+
+def gpow (a : α) : ℤ → α
+| (of_nat n) := a^n
+| -[1+n]     := (a^(nat.succ n))⁻¹
+
+local attribute [ematch] le_of_lt
+open nat
+private lemma gpow_add_aux (a : α) (m n : nat) :
+  gpow a ((of_nat m) + -[1+n]) = gpow a (of_nat m) * gpow a (-[1+n]) :=
+or.elim (nat.lt_or_ge m (nat.succ n))
+ (assume : m < succ n,
+  have m ≤ n, from le_of_lt_succ this,
+  suffices gpow a -[1+ n-m] = (gpow a (of_nat m)) * (gpow a -[1+n]), by simp [*, of_nat_add_neg_succ_of_nat_of_lt],
+  suffices (a^(nat.succ (n - m)))⁻¹ = (gpow a (of_nat m)) * (gpow a -[1+n]), from this,
+  suffices (a^(nat.succ n - m))⁻¹ = (gpow a (of_nat m)) * (gpow a -[1+n]), by rw ←succ_sub; assumption,
+  by rw pow_sub; finish [gpow])
+ (assume : m ≥ succ n,
+  suffices gpow a (of_nat (m - succ n)) = (gpow a (of_nat m)) * (gpow a -[1+ n]), 
+    by rw [of_nat_add_neg_succ_of_nat_of_ge]; assumption,
+  suffices a ^ (m - succ n) = a^m * (a^succ n)⁻¹, from this,
+  by rw pow_sub; assumption)
+
+
+theorem gpow_add (a : α) : ∀i j : int, gpow a (i + j) = gpow a i * gpow a j
+| (of_nat m) (of_nat n) := pow_add _ _ _
+| (of_nat m) -[1+n]     := gpow_add_aux _ _ _
+| -[1+m]     (of_nat n) := begin rw [add_comm, gpow_add_aux], unfold gpow, rw [←inv_pow, pow_inv_comm] end
+| -[1+m]     -[1+n]     := 
+  suffices (a ^ (m + succ (succ n)))⁻¹ = (a ^ succ m)⁻¹ * (a ^ succ n)⁻¹, from this,
+  by rw [←succ_add_eq_succ_add, add_comm, pow_add, mul_inv_rev]
+
+
+theorem gpow_comm (a : α) (i j : ℤ) : gpow a i * gpow a j = gpow a j * gpow a i :=
+by rw [←gpow_add, ←gpow_add, add_comm]
+end group
+
+section ordered_ring
+open nat
+variable [s : linear_ordered_ring α]
+include s
+
+theorem pow_pos {a : α} (H : a > 0) : ∀ (n : ℕ), a ^ n > 0 
+| 0 := by simp; apply zero_lt_one
+| (succ n) := begin simp, apply mul_pos, assumption, apply pow_pos end
+
+theorem pow_ge_one_of_ge_one {a : α} (H : a ≥ 1) : ∀ (n : ℕ), a ^ n ≥ 1 
+| 0 := by simp; apply le_refl
+| (succ n) := 
+  begin 
+   simp, rw ←(one_mul (1 : α)), 
+   apply mul_le_mul, 
+   assumption,
+   apply pow_ge_one_of_ge_one,  
+   apply zero_le_one,
+   transitivity, apply zero_le_one, assumption
+  end
+
+end ordered_ring
+