giving a value a name, for `induction`

Stream: Is there code for X?

[David Renshaw]

import Mathlib.Data.Nat.Digits
import Mathlib.Data.Nat.Parity

theorem Nat.digits_add'
    (b : ℕ) (hb : 1 < b) (x y : ℕ) (hxb : x < b) (hx0 : x ≠ 0) :
    Nat.digits b (x * b ^ (Nat.digits b y).length + y) =
      Nat.digits b y ++ [x] := by

  -- I want to do induction on the list `Nat.digits b y`. These
  -- next two lines are to give that value a name. Is there
  -- a nicer way to accomplish this?
  have hd : ∃ ds, ds = Nat.digits b y := exists_eq
  obtain ⟨ds, hd⟩ := hd

  revert x y
  induction ds with
  | nil => sorry
  | cons d ds ih => sorry

[David Renshaw]

I find myself doing this dance often:

1. construct a trivial existential
2. immediately unpack it

The point is that I need the value to have a name so that I can do induction with it.
Is there a better way to do this?

[Alex J. Best]

You can do induction Nat.digits b y with, is that what you are asking for?

[David Renshaw]

That fails because of the revert x y line.

[David Renshaw]

y is no longer in context there

[Alex J. Best]

Ah sorry, does

  induction Nat.digits b y generalizing x y with

get you what you want? (maybe I should think about whats actually needed to prove this..)

[David Renshaw]

for what it's worth, the complete proof is here: https://github.com/dwrensha/math-puzzles-in-lean4/blob/3a2c6843f13d53e45edbd553045e78c512b1664f/MathPuzzles/Usa2003Q1.lean#L21-L53

[David Renshaw]

I'm just trying to clean it up before maybe PR'ing it to mathlib

[David Renshaw]

when I try induction Nat.digits b y generalizing x y with, I end up unable to prove the nil branch, because I need y to be zero and that information has now been lost

[Alex J. Best]

-- lemma for mathlib?
theorem Nat.digits_add'
    (b : ℕ) (hb : 1 < b) (x y : ℕ) (hxb : x < b) (hx0 : x ≠ 0) :
    Nat.digits b (x * b ^ (Nat.digits b y).length + y) =
      Nat.digits b y ++ [x] := by
  induction' hy : Nat.digits b y generalizing x y hxb hx0
  case nil =>
    have hyy : y = 0 := Nat.digits_eq_nil_iff_eq_zero.mp hy
    rw[hyy]
    simp
    exact Nat.digits_of_lt b x hx0 hxb
  case cons d ds ih =>
    rw[List.length_cons, Nat.pow_succ, List.cons_append]
    have hyp : 0 < y := by
       by_contra H
       replace H : y = 0 := Nat.eq_zero_of_nonpos y H
       rw[H] at hy
       simp at hy
    have h3 := Nat.digits_def' hb hyp
    have hdd := hy.symm
    rw[h3] at hdd
    have h4 : d = y % b := by aesop
    have h5 : ds = Nat.digits b (y/b) := by aesop
    have h2 := ih x (y/b) hxb hx0 h5.symm
    rw[h5] at h2
    have h6 : 0 < x * (b ^ List.length ds * b) + y := by positivity
    rw[Nat.digits_def' hb h6]
    rw[←Nat.mul_assoc]

    congr
    · rw[Nat.add_mod, Nat.mul_mod_left, zero_add, Nat.mod_mod]
      exact h4.symm
    · rw[h5,← h2]
      congr
      have hbz : 0 < b := Nat.zero_lt_one.trans hb
      rw[Nat.add_div hbz]
      have h6: ¬ (b ≤ y % b) := Nat.not_le.mpr (Nat.mod_lt y hbz)
      simp[h6]
      rw[Nat.mul_div_left _ hbz]

[Alex J. Best]

I'm not sure that the default induction tactic supports this, but you can use induction' instead which has a slightly different syntax

[Bhavik Mehta]

This isn't quite what you were looking for but this can be proved much more simply:

theorem Nat.digits_add'
    (b : ℕ) (hb : 1 < b) (x y : ℕ) (hxb : x < b) (hx0 : x ≠ 0) :
    Nat.digits b (x * b ^ (Nat.digits b y).length + y) =
      Nat.digits b y ++ [x] := by
  have : x * b ^ (Nat.digits b y).length + y = ofDigits b (Nat.digits b y ++ [x])
  · simp [ofDigits_append, ofDigits_digits, add_comm, mul_comm]
  rw [this, digits_ofDigits _ hb]
  · simpa [forall_and, or_imp, hxb] using fun _ => digits_lt_base hb
  · simpa

[David Renshaw]

wow!

[David Renshaw]

I opened a PR for a slight generalization of this theorem:
https://github.com/leanprover-community/mathlib4/pull/6999