simplifying nat.digits

Stream: new members

[Kevin Lacker]

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]

Is this what you want?

import data.nat.digits

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

[Kevin Lacker]

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

[Kevin Lacker]

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

[Kevin Lacker]

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]

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]

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]

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]

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]

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

[Bryan Gin-ge Chen]

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]

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]

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]

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]

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]

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

@Mario Carneiro any thoughts?

[Mario Carneiro]

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

[Scott Morrison]

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]

well those natural numbers aren't going away

[Mario Carneiro]

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

[Johan Commelin]

@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]

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]

will you PR it? :pray:

[Kevin Lacker]

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]

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

[Scott Morrison]

PR'd as #4451.

[Mario Carneiro]

Also PR'd as #4452 :stuck_out_tongue:

[Scott Morrison]

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

[Scott Morrison]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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