NNG induction

Stream: new members

[Nir Paz]

I have the following code from the Natural number game:

lemma mul_add (t a b : mynat) : t * (a + b) = t * a + t * b :=
begin

induction b with b hb,
rw add_zero,
rw mul_zero,
rw add_zero,
refl,
rw succ_eq_add_one,
rw add_comm b,
rw ← add_assoc,
rw ← succ_eq_add_one,
rw hb,

end

My question is about the reason I can't use hb to simplify t * (succ a + b) . I know t * (succ a + b) isn't written exactly like hb, but the induction hypothesis isn't about a specific a, it says that for every t and a a certain equality holds, and I want to substitute succ a as the value for the variable named a. It feels mostly like a matter of naming variables.

[Notification Bot]

A message was moved here from #new members > Can't display a number wrapped in a structure by Johan Commelin.

[Johan Commelin]

@Nir Paz Hint: do revert a before the induction.

[Thomas Browning]

The induction hypothesis is not a statement about every t and a. It's only a statement about that specific t and a.

[Thomas Browning]

induction b with b hb generalizing t a is another way to generalize the induction hypothesis.

[Nir Paz]

Thanks!

[Arien Malec]

I struggled with this as well -- Lean is far more stubborn than you are. It will only use rw using statements that it knows are definitionally equal; that means that it won't use leaps of logic that make sense to you until you teach it.