feat(data/nat/digits): digits_len (#11187)

Via a new `data.nat.log` import.
Also unprivate `digits_eq_cons_digits_div`.

The file needs a refactor to make the names more mathlib-like,
otherwise I would have named it `length_digits`.

src/data/nat/digits.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Shing Tak Lam, Mario Carneiro
 -/
 import data.int.modeq
+import data.nat.log
 import data.list.indexes
 import tactic.interval_cases
 import tactic.linarith
@@ -290,7 +291,7 @@ end
 lemma digits_ne_nil_iff_ne_zero {b n : ℕ} : digits b n ≠ [] ↔ n ≠ 0 :=
 not_congr digits_eq_nil_iff_eq_zero
 
-private lemma digits_last_aux {b n : ℕ} (h : 2 ≤ b) (w : 0 < n) :
+lemma digits_eq_cons_digits_div {b n : ℕ} (h : 2 ≤ b) (w : 0 < n) :
   digits b n = ((n % b) :: digits b (n / b)) :=
 begin
   rcases b with _|_|b,
@@ -306,7 +307,7 @@ lemma digits_last {b : ℕ} (m : ℕ) (h : 2 ≤ b) (p q) :
 begin
   by_cases hm : m = 0,
   { simp [hm], },
-  simp only [digits_last_aux h (nat.pos_of_ne_zero hm)],
+  simp only [digits_eq_cons_digits_div h (nat.pos_of_ne_zero hm)],
   rw list.last_cons,
 end
 
@@ -317,6 +318,23 @@ function.left_inverse.injective (of_digits_digits b)
   b.digits n = b.digits m ↔ n = m :=
 (digits.injective b).eq_iff
 
+lemma digits_len (b n : ℕ) (hb : 2 ≤ b) (hn : 0 < n) :
+  (b.digits n).length = b.log n + 1 :=
+begin
+  induction n using nat.strong_induction_on with n IH,
+  rw [digits_eq_cons_digits_div hb hn, list.length],
+  cases (n / b).eq_zero_or_pos with h h,
+  { have posb : 0 < b := zero_lt_two.trans_le hb,
+    simp [h, log_eq_zero_iff, ←nat.div_eq_zero_iff posb] },
+  { have hb' : 1 < b := one_lt_two.trans_le hb,
+    have : n / b < n := div_lt_self hn hb',
+    rw [IH _ this h, log_div_base, tsub_add_cancel_of_le],
+    rw [succ_le_iff],
+    refine log_pos hb' _,
+    contrapose! h,
+    rw div_eq_of_lt h }
+end
+
 lemma last_digit_ne_zero (b : ℕ) {m : ℕ} (hm : m ≠ 0) :
   (digits b m).last (digits_ne_nil_iff_ne_zero.mpr hm) ≠ 0 :=
 begin
@@ -404,25 +422,14 @@ by rw [of_digits_append, of_digits_digits, of_digits_digits]
 
 lemma digits_len_le_digits_len_succ (b n : ℕ) : (digits b n).length ≤ (digits b (n + 1)).length :=
 begin
-  cases b,
-  { -- base 0
-    cases n; simp },
-  { cases b,
-    { -- base 1
-      simp },
-    { -- base >= 2
-      apply nat.strong_induction_on n,
-      clear n,
-      intros n IH,
-      cases n,
-      { simp },
-      { rw [digits_add_two_add_one, digits_add_two_add_one],
-        by_cases hdvd : (b.succ.succ) ∣ (n.succ+1),
-        { rw [nat.succ_div_of_dvd hdvd, list.length_cons, list.length_cons, nat.succ_le_succ_iff],
-          apply IH,
-          exact nat.div_lt_self (by linarith) (by linarith) },
-        { rw nat.succ_div_of_not_dvd hdvd,
-          refl } } } }
+  rcases n.eq_zero_or_pos with rfl|hn,
+  { simp },
+  cases lt_or_le b 2 with hb hb,
+  { rcases b with _|_|b,
+    { simp [digits_zero_succ', hn] },
+    { simp, },
+    { simpa [succ_lt_succ_iff] using hb } },
+  simpa [digits_len, hb, hn] using log_le_log_of_le (le_succ _)
 end
 
 lemma le_digits_len_le (b n m : ℕ) (h : n ≤ m) : (digits b n).length ≤ (digits b m).length :=