[Merged by Bors] - refactor(library): decouple algebraic hierarchy from core lib

library/data/bitvec.lean

@@ -43,9 +43,9 @@ section shift
     begin
       by_cases (i ≤ n),
       { have h₁ := sub_le n i,
-        rw [min_eq_right h], rw [min_eq_left h₁, ← nat.add_sub_assoc h, add_comm, nat.add_sub_cancel] },
+        rw [min_eq_right h], rw [min_eq_left h₁, ← nat.add_sub_assoc h, nat.add_comm, nat.add_sub_cancel] },
       { have h₁ := le_of_not_ge h,
-        rw [min_eq_left h₁, sub_eq_zero_of_le h₁, zero_min, add_zero] }
+        rw [min_eq_left h₁, sub_eq_zero_of_le h₁, zero_min, nat.add_zero] }
     end $
     repeat fill (min n i) ++ₜ take (n-i) x
 
@@ -158,7 +158,9 @@ section conversion
   theorem bits_to_nat_to_list {n : ℕ} (x : bitvec n)
   : bitvec.to_nat x = bits_to_nat (vector.to_list x)  := rfl
 
-  local attribute [simp] add_comm add_assoc add_left_comm mul_comm mul_assoc mul_left_comm
+  local attribute [simp] nat.add_comm nat.add_assoc nat.add_left_comm nat.mul_comm nat.mul_assoc
+  local attribute [simp] nat.zero_add nat.add_zero nat.one_mul nat.mul_one nat.zero_mul nat.mul_zero
+  -- mul_left_comm
 
   theorem to_nat_append {m : ℕ} (xs : bitvec m) (b : bool)
   : bitvec.to_nat (xs ++ₜ b::nil) = bitvec.to_nat xs * 2 + bitvec.to_nat (b::nil) :=
@@ -189,15 +191,10 @@ section conversion
   theorem to_nat_of_nat {k n : ℕ}
   : bitvec.to_nat (bitvec.of_nat k n) = n % 2^k :=
   begin
-    induction k with k generalizing n,
+    induction k with k ih generalizing n,
     { unfold pow nat.pow, simp [nat.mod_one], refl },
     { have h : 0 < 2, { apply le_succ },
-      rw [ of_nat_succ
-         , to_nat_append
-         , k_ih
-         , bits_to_nat_to_bool
-         , mod_pow_succ h],
-      ac_refl, }
+      rw [of_nat_succ, to_nat_append, ih, bits_to_nat_to_bool, mod_pow_succ h, nat.mul_comm] }
   end
 
   protected def to_int : Π {n : nat}, bitvec n → int

library/data/rbtree/basic.lean

@@ -201,7 +201,7 @@ lemma depth_max' : ∀ {c n} {t : rbnode α}, is_red_black t c n → depth max t
 begin
   intros c n' t h,
   induction h,
-  case leaf_rb { simp [max, depth, upper] },
+  case leaf_rb { simp [max, depth, upper, nat.mul_zero] },
   case red_rb {
     suffices : succ (max (depth max h_l) (depth max h_r)) ≤ 2 * h_n + 1,
     { simp [depth, upper, *] at * },
@@ -211,7 +211,7 @@ begin
     have : depth max h_l ≤ 2*h_n + 1, from le_trans h_ih_rb_l (upper_le _ _),
     have : depth max h_r ≤ 2*h_n + 1, from le_trans h_ih_rb_r (upper_le _ _),
     suffices new : max (depth max h_l) (depth max h_r) + 1 ≤ 2 * h_n + 2*1,
-    { simp [depth, upper, succ_eq_add_one, left_distrib, *] at * },
+    { simp [depth, upper, succ_eq_add_one, nat.left_distrib, *] at * },
     apply succ_le_succ, apply max_le; assumption
   }
 end

library/data/stream.lean

@@ -42,14 +42,14 @@ theorem head_cons (a : α) (s : stream α) : head (a :: s) = a := rfl
 theorem tail_cons (a : α) (s : stream α) : tail (a :: s) = s := rfl
 
 theorem tail_drop (n : nat) (s : stream α) : tail (drop n s) = drop n (tail s) :=
-funext (λ i, begin unfold tail drop, simp [add_comm, add_left_comm] end)
+funext (λ i, begin unfold tail drop, simp [nat.add_comm, nat.add_left_comm] end)
 
 theorem nth_drop (n m : nat) (s : stream α) : nth n (drop m s) = nth (n+m) s := rfl
 
 theorem tail_eq_drop (s : stream α) : tail s = drop 1 s := rfl
 
 theorem drop_drop (n m : nat) (s : stream α) : drop n (drop m s) = drop (n+m) s :=
-funext (λ i, begin unfold drop, rw add_assoc end)
+funext (λ i, begin unfold drop, rw nat.add_assoc end)
 
 theorem nth_succ (n : nat) (s : stream α) : nth (succ n) s = nth n (tail s) := rfl
 

library/init/algebra/default.lean

@@ -4,5 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.algebra.group init.algebra.ordered_group init.algebra.ring init.algebra.ordered_ring
-import init.algebra.field init.algebra.ordered_field init.algebra.norm_num init.algebra.functions
+import init.algebra.functions