digits question

Stream: new members

[Angela Li]

Hello! I'm trying to show

import data.nat.digits

lemma digits_le_9 (n : ℕ) : ∀ (d ∈ (digits 10 n)), d ≤ 9 := sorry

but I'm not really sure how to work with a list of arbitrary length.
digits_aux_def splits the list into n % b :: digits_aux b h (n / b) so long as 0 < n. I thought the n=0 case doesn't really matter since the list would be empty and so I could just show a digit is %b, but it still asks about the remainder of the list digits_aux b h (n / b).
Thanks.

[Kevin Buzzard]

I guess you do strong induction on n to prove that all the elements of digits_aux b h n are < n (for any b>=2)

[Angela Li]

Okay I shall try that!

[Kevin Buzzard]

import data.nat.digits

/-- The digits in the base b expansion of n are all less than b -/
lemma digits_lt_base (b : ℕ) (hb : 2 ≤ b) (n : ℕ) : ∀ d ∈ digits b n, d < b :=
begin
  cases b with b, linarith, cases b with b, linarith, clear hb,
  apply nat.strong_induction_on n,
  clear n,
  intro n,
  intro IH,
  intro d,
  intro hd,
  unfold digits at hd IH,
  have h := digits_aux_def (b+2) (by linarith) n,
  cases n with n,
  { cases hd}, -- base b+2 expansion of 0 has no digits
  replace h := h (nat.zero_lt_succ n),
  rw h at hd,
  cases hd,
  { -- zero'th digit
    rw hd,
    exact n.succ.mod_lt (by linarith),
  },
  apply IH _ _ d hd,
  apply nat.div_lt_self (nat.succ_pos _),
  linarith,
end

-- the base 10 digits of a number are all at most 9
lemma digits_le_9 (n : ℕ) : ∀ (d ∈ (digits 10 n)), d ≤ 9 :=
λ d hd, nat.le_of_lt_succ $ digits_lt_base 10 (by norm_num) n _ hd

@Angela Li

[Kevin Buzzard]

#3246

[Angela Li]

Hi. I am trying to show a number will have the same or less digits than a bigger number.

import data.nat.digits
lemma le_digits_len_le {b n m : ℕ} :  n ≤ m → (digits b n).length ≤ (digits b m).length := sorry

I have done cases twice to do it for base 0 and base 1, but I am stuck on base >= 2. I thought I could do induction or strong induction on c where m = n + c, but I got stuck. I'm not sure when to use strong induction vs induction (I kind of used it because I didn't know what else to do).
Thanks.

[Kevin Buzzard]

This is a great question!

[Kevin Buzzard]

You could also prove it was monotonic as a function of b

[Kevin Buzzard]

Why not prove that b^length n <= n and n < b^(1 + length n)?

[Kevin Buzzard]

warning : I might have made off by one errors.

[Angela Li]

I think I was trying to do that and decided to do this first because I got stuck haha.

[Kevin Buzzard]

I think you can do these by strong induction on n

[Alex J. Best]

If you can prove that (digits b n).length ≤ (digits b (n+1)).length first as a separate lemma then you could use that (inductively), to show n ≤ n+1 ≤ n + 2.... ≤ m - 1 ≤ m to that (digits b n).length ≤ (digits b (n+1)).length ≤ (digits b (n+2)).length ≤ ... ≤ (digits b m).length

[Reid Barton]

There seem to be some missing lemmas about digits: namely that it satisfies the hypotheses of the list in digits_of_digits

[Reid Barton]

they're also stated in the docstring for digits

[Reid Barton]

but as far as I can tell, not proven as lemmas

[Kevin Buzzard]

That's a good trick!

[Kevin Buzzard]

If you document it, they will come

[Angela Li]

(∀ (h : L ≠ list.nil), L.last h ≠ 0) Does this mean there's no leading 0s in the number? I don't really understand the definition of last.

[Kevin Buzzard]

Isn't it the first digit in the expansion (the way humans write it)

[Scott Morrison]

Sorry about the incompleteness of digits. I'll admit I wrote it thinking that the corresponding Freek problem was easy low-hanging fruit, but then got a bit bored of the subject before doing a thorough job.

This is a certainly a place where someone learning Lean could add lots of the useful lemmas in a pull request.

[Angela Li]

What's the Freek problem?
I think I will be exploring digits more bc I'm not sure if I can do what I want to do with happy numbers w/o more things about digits. Hopefully can contribute...

[Scott Morrison]

https://leanprover-community.github.io/100.html#85

[Kevin Buzzard]

@maintainers can @Angela Li have push access to non-master mathlib branches? She's written a couple of other lemmas which would be appropriate for data.nat.digits. Her github userid is snobbydragon. Thanks.

[Rob Lewis]

I just tried but it looks like someone beat me to it

[Bryan Gin-ge Chen]

Same. @Angela Li can visit https://github.com/leanprover-community/mathlib/invitations to accept.