## Stream: new members

### Topic: simplifying nat.digits

#### Kevin Lacker (Oct 02 2020 at 22:48):

Is there a way to automatically simplify the digits of a given number? like to simplify nat.digits 10 123 into [3, 2, 1]. it uses some digits_aux helper which seems to cause problems when i just simp

#### Bryan Gin-ge Chen (Oct 02 2020 at 23:04):

Is this what you want?

import data.nat.digits

example : nat.digits 10 123 = [3,2,1] :=
by norm_num


#### Kevin Lacker (Oct 02 2020 at 23:06):

hmm, close enough. I had (nat.digits 10 123) inside an expression, and i wanted it to simplify that

#### Kevin Lacker (Oct 02 2020 at 23:06):

is norm_num supposed to also simplify subexpressions? or just when (nat.digits 10 123) is the whole thing

#### Kevin Lacker (Oct 02 2020 at 23:07):

i guess to give specific code, i was attempting to prove (nat.digits 10 153846).head = 6 ∧ of_digits 10 ((nat.digits 10 153846).tail.concat 6) = 4 * 153846

#### Kevin Lacker (Oct 02 2020 at 23:08):

i got norm_num to do it, but only if i wrote some lemma to help break down (nat.digits 10 x) and passed in to norm_num

#### Kevin Lacker (Oct 02 2020 at 23:08):

but i feel like i am just making up random stuff and seeing if norm_num can then solve the problem, rather than intelligently crafting a solution

#### Bryan Gin-ge Chen (Oct 02 2020 at 23:17):

Yeah, I'm not sure what the best way is myself. I can't get norm_num to prove nat.digits 10 3846 = [6,4,8,3] (or anything else with more than 3 digits) at the moment.

It could be that we're missing some simp lemmas for nat.digits.

#### Kevin Lacker (Oct 02 2020 at 23:19):

ok. if I define this lemma:

lemma digit_recursion (n : ℕ) (h1 : n ≥ 1) :
(nat.digits 10 n) = (n % 10) :: (nat.digits 10 (n / 10)) :=
begin
have h2: (n - 1) + 1 = n, from nat.sub_add_cancel h1,
rw ← h2,
refl,
end


and pass it to norm_num, then it succeeds at simplifying. it seems to stumble because you have to rewrite 153846 as (153846 - 1) + 1 to apply the lemmas in the library, and i'm guessing that step is omitted because it isn't getting simpler. so maybe something like this should be in the digits lib

#### Bryan Gin-ge Chen (Oct 02 2020 at 23:22):

Yes, that seems like it should be in data/nat/digits (generalized to base b, of course).

#### Bryan Gin-ge Chen (Oct 02 2020 at 23:37):

Actually, that seems very close to digits_aux_def, so there should be some way to use that instead, though I'm not having any luck at the moment.

Edit: see below

#### Bryan Gin-ge Chen (Oct 02 2020 at 23:44):

import data.nat.digits

lemma aux : nat.digits 10 153846 = [6,4,8,3,5,1] := begin
norm_num [nat.digits, nat.digits_aux_def],
end

lemma aux' : [4, 8, 3, 5, 1, 6] = nat.digits 10 615384 := begin
norm_num [nat.digits, nat.digits_aux_def],
end

example : (nat.digits 10 153846).head = 6 ∧
nat.of_digits 10 ((nat.digits 10 153846).tail.concat 6) = 4 * 153846 :=
begin
split,
{ rw [aux, list.head], }, -- can also use  norm_num [nat.digits, nat.digits_aux_def],
{ norm_num [aux, aux', nat.of_digits_digits], }, -- not sure how to prove this cleanly without aux and aux'
end

-- basically the same as nat.digits_aux_def
lemma digit_recursion (n : ℕ) (h1 : n ≥ 1) :
(nat.digits 10 n) = (n % 10) :: (nat.digits 10 (n / 10)) :=
begin
apply nat.digits_aux_def,
linarith,
end


#### Kevin Lacker (Oct 03 2020 at 03:07):

interesting... so I ended up with:

lemma digit_recursion (n : ℕ) (h1 : n > 0) :
(nat.digits 10 n) = (n % 10) :: (nat.digits 10 (n / 10)) :=
begin
have h2: (n - 1) + 1 = n, from nat.sub_add_cancel h1,
rw ← h2,
refl,
end

example : (nat.digits 10 153846).head = 6 ∧ of_digits 10 ((nat.digits 10 153846).tail.concat 6) = 4 * 153846 :=
by norm_num [digit_recursion, of_digits]


So with digit_recursion the whole thing is handled by norm_num. I don't really know why digits_aux_def doesn't do this in conjunction with norm_num. Maybe the condition that 1 < 10 is complicated enough that norm_num doesn't automate a reduction that requires it?

#### Kevin Lacker (Oct 03 2020 at 03:10):

i'm not sure what to conclude, because it does seem convenient for norm_num to be able to handle this whole expression, yet it doesn't seem like something specific to base 10 belongs in the base library, yet it seems like without something 10-specific you essentially have to unpack the digits library and use lots of different nat.digits_aux_def, nat.of_digits_digits, etc lemmas

#### Kevin Lacker (Oct 03 2020 at 03:11):

I think the digits library has a bit of a problem - the core definition also works with base 0 and base 1, but those ways of having are basically totally different from the others, so all these theorems only work with a base > 1, which then causes trouble with things like, you can't say that simp should operate only for bases that are greater than 1, IIUC

#### Bryan Gin-ge Chen (Oct 03 2020 at 03:17):

Well, I wouldn't say that my attempt is anything near the final word on norm_num.

@Mario Carneiro any thoughts?

#### Mario Carneiro (Oct 03 2020 at 03:19):

you can do a lot better than this with a dedicated tactic/subcomponent of norm_num

#### Scott Morrison (Oct 03 2020 at 03:54):

I agree with Kevin's criticism of the digits library allowing base 0 and 1. That was a flat out mistake on my part. It's useless generality. If someone wants to change it I think that could be valuable!

#### Mario Carneiro (Oct 03 2020 at 03:56):

well those natural numbers aren't going away

#### Mario Carneiro (Oct 03 2020 at 03:57):

the only thing that should change is a tacit assumption that the other case doesn't matter

#### Johan Commelin (Oct 03 2020 at 04:05):

@Kevin Lacker I think maybe we want to know how to add and mul numbers written in base n. In other words

def digits.add (n : nat) (A B : list nat) := sorry

lemma digits_add (n i j : nat) :
digits n (i + j) = digits.add n (digits n i) (digits n j) := sorry


#### Mario Carneiro (Oct 03 2020 at 04:16):

It's a bit overkill but here's a relatively efficient digit prover:

import data.nat.digits

theorem nat.digits_def' : ∀ {b : ℕ} (h : 2 ≤ b) {n : ℕ} (w : 0 < n),
nat.digits b n = n % b :: nat.digits b (n/b)
| 0 h := absurd h dec_trivial
| 1 h := absurd h dec_trivial
| (b+2) h := nat.digits_aux_def _ _

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

meta def eval_digits_aux (eb : expr) (b : ℕ) : expr → ℕ → tactic (expr × expr)
| en n := do
let m := n / b,
let r := n % b,
ic ← mk_instance_cache (ℕ),
er ← expr.of_nat (ℕ) r,
(_, pr) ← norm_num.prove_lt_nat ic er eb,
if m = 0 then do
(_, pn0) ← norm_num.prove_pos ic en,
return (([%%en] : list nat), (digits_one %%eb %%en %%pn0 %%pr))
else do
em ← expr.of_nat (ℕ) m,
(_, pe) ← norm_num.derive (%%er + %%eb * %%em : ℕ),
(el, p) ← eval_digits_aux em m,
return ((@list.cons ℕ %%er %%el),
(digits_succ %%eb %%en %%em %%er %%el %%pe %%pr %%p))

meta def eval_digits (eb : expr) (b : ℕ) : expr → ℕ → tactic (expr × expr)
| en 0 := return (([] : list nat), (nat.digits_zero %%eb))
| en n := do
(l, p) ← eval_digits_aux eb b en n,
p ← mk_app and.left [p],
return (l, p)

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) ← eval_digits eb b en n,
unify el el',
exact p

example : nat.digits 10 123 = [3,2,1] := by norm_digits


#### Bryan Gin-ge Chen (Oct 03 2020 at 05:00):

will you PR it? :pray:

#### Kevin Lacker (Oct 03 2020 at 07:11):

wow, it is cool that you could create norm_digits! i will have to learn more about creating tactics, a lot of the stuff like meta def, the whole if...then construct, backticks, the %% operator, etc I did not recognize.

#### Patrick Massot (Oct 03 2020 at 08:25):

All this is explained in https://leanprover-community.github.io/extras/tactic_writing.html

PR'd as #4451.

#### Mario Carneiro (Oct 05 2020 at 22:39):

Also PR'd as #4452 :stuck_out_tongue:

#### Scott Morrison (Oct 05 2020 at 22:41):

I prefer what you did --- put the tactic in nat.digits directly.

#### Scott Morrison (Oct 05 2020 at 22:41):

I'll close mine, and copy across some doc-strings.

#### Mario Carneiro (Oct 05 2020 at 22:41):

I also fixed a thing where the tactic hangs if you try to normalize base 1

#### Mario Carneiro (Oct 05 2020 at 22:43):

The interface is still pretty primitive, so I've opted to leave it as a non-interactive tactic

#### Mario Carneiro (Oct 05 2020 at 22:43):

if it was integrated into norm_num it would be able to simplify nat.digits` expressions anywhere in the target, instead of assuming it is the lhs of the goal

#### Scott Morrison (Oct 05 2020 at 22:45):

Oh, didn't see you message. I added the interactive connectivity as a suggestion.

#### Mario Carneiro (Oct 05 2020 at 22:46):

eh it's fine, I guess that helps with documentation and the like

Last updated: May 16 2021 at 05:21 UTC