# Zulip Chat Archive

## 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

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

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