feat(data/nat/digits): add norm_digits tactic (#4452)

This adds a basic tactic for normalizing expressions of the form `nat.digits a b = l`. As requested on Zulip: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/simplifying.20nat.2Edigits/near/212152395

Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

src/data/nat/digits.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison, Shing Tak Lam
+Authors: Scott Morrison, Shing Tak Lam, Mario Carneiro
 -/
 import data.int.modeq
 import tactic.interval_cases
@@ -15,6 +15,9 @@ and reconstructing numbers from their digits.
 
 We also prove some divisibility tests based on digits, in particular completing
 Theorem #85 from https://www.cs.ru.nl/~freek/100/.
+
+A basic `norm_digits` tactic is also provided for proving goals of the form
+`nat.digits a b = l` where `a` and `b` are numerals.
 -/
 
 namespace nat
@@ -74,13 +77,23 @@ end
 
 @[simp] lemma digits_zero_succ (n : ℕ) : digits 0 (n.succ) = [n+1] := rfl
 
+theorem digits_zero_succ' : ∀ {n : ℕ} (w : 0 < n), digits 0 n = [n]
+| 0 h := absurd h dec_trivial
+| (n+1) _ := rfl
+
 @[simp] lemma digits_one (n : ℕ) : digits 1 n = list.repeat 1 n := rfl
 
 @[simp] lemma digits_one_succ (n : ℕ) : digits 1 (n + 1) = 1 :: digits 1 n := rfl
 
 @[simp] lemma digits_add_two_add_one (b n : ℕ) :
   digits (b+2) (n+1) = (((n+1) % (b+2)) :: digits (b+2) ((n+1) / (b+2))) := rfl
 
+theorem digits_def' : ∀ {b : ℕ} (h : 2 ≤ b) {n : ℕ} (w : 0 < n),
+  digits b n = n % b :: digits b (n/b)
+| 0 h := absurd h dec_trivial
+| 1 h := absurd h dec_trivial
+| (b+2) h := digits_aux_def _ _
+
 @[simp]
 lemma digits_of_lt (b x : ℕ) (w₁ : 0 < x) (w₂ : x < b) : digits b x = [x] :=
 begin
@@ -544,4 +557,100 @@ begin
   exact t,
 end
 
+/-! ### `norm_digits` tactic -/
+
+namespace norm_digits
+
+theorem digits_succ
+  (b n m r l)
+  (e : r + b * m = n)
+  (hr : r < b)
+  (h : nat.digits b m = l ∧ 2 ≤ b ∧ 0 < m) :
+  nat.digits b n = r :: l ∧ 2 ≤ b ∧ 0 < n :=
+begin
+  rcases h with ⟨h, b2, m0⟩,
+  have b0 : 0 < b := by linarith,
+  have n0 : 0 < n := by linarith [mul_pos b0 m0],
+  refine ⟨_, b2, n0⟩,
+  obtain ⟨rfl, rfl⟩ := (nat.div_mod_unique b0).2 ⟨e, hr⟩,
+  subst h, exact nat.digits_def' b2 n0,
+end
+
+theorem digits_one
+  (b n) (n0 : 0 < n) (nb : n < b) :
+  nat.digits b n = [n] ∧ 2 ≤ b ∧ 0 < n :=
+begin
+  have b2 : 2 ≤ b := by linarith,
+  refine ⟨_, b2, n0⟩,
+  rw [nat.digits_def' b2 n0, nat.mod_eq_of_lt nb,
+    (nat.div_eq_zero_iff (by linarith : 0 < b)).2 nb, nat.digits_zero],
+end
+
+open tactic
+
+/-- Helper function for the `norm_digits` tactic. -/
+meta def eval_aux (eb : expr) (b : ℕ) :
+  expr → ℕ → instance_cache → tactic (instance_cache × expr × expr)
+| en n ic := do
+  let m := n / b,
+  let r := n % b,
+  (ic, er) ← ic.of_nat r,
+  (ic, pr) ← norm_num.prove_lt_nat ic er eb,
+  if m = 0 then do
+    (_, pn0) ← norm_num.prove_pos ic en,
+    return (ic, `([%%en] : list nat), `(digits_one %%eb %%en %%pn0 %%pr))
+  else do
+    em ← expr.of_nat `(ℕ) m,
+    (_, pe) ← norm_num.derive `(%%er + %%eb * %%em : ℕ),
+    (ic, el, p) ← eval_aux em m ic,
+    return (ic, `(@list.cons ℕ %%er %%el),
+      `(digits_succ %%eb %%en %%em %%er %%el %%pe %%pr %%p))
+
+/-- Helper function for the `norm_digits` tactic. -/
+meta def eval : expr → ℕ → expr → ℕ → tactic (expr × expr)
+| eb b en 0 := return (`([] : list ℕ), `(nat.digits_zero %%eb))
+| eb 0 en n := do
+  ic ← mk_instance_cache `(ℕ),
+  (_, pn0) ← norm_num.prove_pos ic en,
+  return (`([%%en] : list ℕ), `(@nat.digits_zero_succ' %%en %%pn0))
+| eb 1 en n := do
+  ic ← mk_instance_cache `(ℕ),
+  (_, pn0) ← norm_num.prove_pos ic en,
+  s ← simp_lemmas.add_simp simp_lemmas.mk `list.repeat,
+  (rhs, p2) ← simplify s [] `(list.repeat 1 %%en),
+  p ← mk_eq_trans `(nat.digits_one %%en) p2,
+  return (rhs, p)
+| eb b en n := do
+  ic ← mk_instance_cache `(ℕ),
+  (_, l, p) ← eval_aux eb b en n ic,
+  p ← mk_app ``and.left [p],
+  return (l, p)
+
+end norm_digits
+
+open tactic
+
+/--
+A tactic for normalizing expressions of the form `nat.digits a b = l` where
+`a` and `b` are numerals.
+
+```
+example : nat.digits 10 123 = [3,2,1] := by norm_digits
+```
+-/
+meta def norm_digits : tactic unit :=
+do `(nat.digits %%eb %%en = %%el') ← target,
+  b ← expr.to_nat eb,
+  n ← expr.to_nat en,
+  (el, p) ← nat.norm_digits.eval eb b en n,
+  unify el el',
+  exact p
+
+run_cmd add_interactive [``norm_digits]
+
+add_tactic_doc
+{ name        := "norm_digits",
+  category    := doc_category.tactic,
+  decl_names  := [`tactic.interactive.norm_digits],
+  tags        := ["arithmetic", "decision procedure"] }
 end nat

test/norm_digits.lean

@@ -0,0 +1,12 @@
+import data.nat.digits
+
+example : nat.digits 0 0 = [] := by norm_digits
+example : nat.digits 1 0 = [] := by norm_digits
+example : nat.digits 2 0 = [] := by norm_digits
+example : nat.digits 10 0 = [] := by norm_digits
+example : nat.digits 0 1 = [1] := by norm_digits
+example : nat.digits 0 1000 = [1000] := by norm_digits
+example : nat.digits 1 10 = [1, 1, 1, 1, 1, 1, 1, 1, 1, 1] := by norm_digits
+example : nat.digits 2 65536 = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1] := by norm_digits
+example : nat.digits 3 30000000 = [0, 1, 0, 1, 2, 0, 1, 1, 0, 0, 1, 1, 2, 0, 0, 2] := by norm_digits
+example : nat.digits 10 1234567 = [7, 6, 5, 4, 3, 2, 1] := by norm_digits