Theorem: String.toNatAux_accumulates (One.lean)

State before:
s : List Char
accum : ℕ
⊢ toNatAux s accum = toNatAux s 0 + accum * 10 ^ List.length s
Tactic:
induction s generalizing accum with
| nil => unfold toNatAux; simp
| cons head tail ih =>
  unfold toNatAux
  rw [ih]
  conv => right; rw [ih]
  simp [Nat.succ_eq_add_one]
  ring
State after:
no goals

State before:
case nil
accum : ℕ
⊢ toNatAux [] accum = toNatAux [] 0 + accum * 10 ^ List.length []
Tactic:
unfold toNatAux
State after:
case nil
accum : ℕ
⊢ accum = 0 + accum * 10 ^ List.length []

State before:
case nil
accum : ℕ
⊢ accum = 0 + accum * 10 ^ List.length []
Tactic:
simp
State after:
no goals

State before:
case cons
head : Char
tail : List Char
ih : ∀ (accum : ℕ), toNatAux tail accum = toNatAux tail 0 + accum * 10 ^ List.length tail
accum : ℕ
⊢ toNatAux (head :: tail) accum = toNatAux (head :: tail) 0 + accum * 10 ^ List.length (head :: tail)
Tactic:
unfold toNatAux
State after:
case cons
head : Char
tail : List Char
ih : ∀ (accum : ℕ), toNatAux tail accum = toNatAux tail 0 + accum * 10 ^ List.length tail
accum : ℕ
⊢ toNatAux tail (accum * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) =
    toNatAux tail (0 * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) + accum * 10 ^ List.length (head :: tail)

State before:
case cons
head : Char
tail : List Char
ih : ∀ (accum : ℕ), toNatAux tail accum = toNatAux tail 0 + accum * 10 ^ List.length tail
accum : ℕ
⊢ toNatAux tail (accum * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) =
    toNatAux tail (0 * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) + accum * 10 ^ List.length (head :: tail)
Tactic:
rw [ih]
State after:
case cons
head : Char
tail : List Char
ih : ∀ (accum : ℕ), toNatAux tail accum = toNatAux tail 0 + accum * 10 ^ List.length tail
accum : ℕ
⊢ toNatAux tail 0 + (accum * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) * 10 ^ List.length tail =
    toNatAux tail (0 * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) + accum * 10 ^ List.length (head :: tail)

State before:
case cons
head : Char
tail : List Char
ih : ∀ (accum : ℕ), toNatAux tail accum = toNatAux tail 0 + accum * 10 ^ List.length tail
accum : ℕ
⊢ toNatAux tail 0 + (accum * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) * 10 ^ List.length tail =
    toNatAux tail (0 * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) + accum * 10 ^ List.length (head :: tail)
Tactic:
conv => right; rw [ih]
State after:
case cons
head : Char
tail : List Char
ih : ∀ (accum : ℕ), toNatAux tail accum = toNatAux tail 0 + accum * 10 ^ List.length tail
accum : ℕ
⊢ toNatAux tail 0 + (accum * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) * 10 ^ List.length tail =
    toNatAux tail 0 + (0 * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) * 10 ^ List.length tail +
      accum * 10 ^ List.length (head :: tail)

State before:
case cons
head : Char
tail : List Char
ih : ∀ (accum : ℕ), toNatAux tail accum = toNatAux tail 0 + accum * 10 ^ List.length tail
accum : ℕ
⊢ toNatAux tail 0 + (accum * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) * 10 ^ List.length tail =
    toNatAux tail 0 + (0 * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) * 10 ^ List.length tail +
      accum * 10 ^ List.length (head :: tail)
Tactic:
simp [Nat.succ_eq_add_one]
State after:
case cons
head : Char
tail : List Char
ih : ∀ (accum : ℕ), toNatAux tail accum = toNatAux tail 0 + accum * 10 ^ List.length tail
accum : ℕ
⊢ toNatAux tail 0 + (accum * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) * 10 ^ List.length tail =
    toNatAux tail 0 + (Char.toNat head - Char.toNat (Char.ofNat 48)) * 10 ^ List.length tail +
      accum * 10 ^ (List.length tail + 1)

State before:
case cons
head : Char
tail : List Char
ih : ∀ (accum : ℕ), toNatAux tail accum = toNatAux tail 0 + accum * 10 ^ List.length tail
accum : ℕ
⊢ toNatAux tail 0 + (accum * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) * 10 ^ List.length tail =
    toNatAux tail 0 + (Char.toNat head - Char.toNat (Char.ofNat 48)) * 10 ^ List.length tail +
      accum * 10 ^ (List.length tail + 1)
Tactic:
ring
State after:
no goals