CODEWITHSUNDEEP
lean
alcorn
alcorn

Reputation: 1368

Why was the second inductive hypothesis not needed in this nested induction proof?

I'm working through the Natural Number game and I've completed a proof for mul_add. The proof looks like this:

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

begin

  induction b with B hB,

  -- b base case
  rw add_zero a,
  rw mul_zero t,
  rw add_zero (t*a),
  refl,

  induction a with A hA,

  -- a base case
  rw zero_add (succ B),
  rw mul_zero t,
  rw zero_add (t * succ B),
  refl,

  -- joint inductive step
  rw add_succ (succ A) B,
  rw mul_succ t (succ A + B),
  rw hB,
  rw add_assoc (t*succ A) (t*B) t,
  rw <- mul_succ t B,
  refl,

end

Why I did not need to use the inductive hypothesis hA in this proof? Intuitively it would seem that I should "use up" everything that is generated in the course of the proof. For reference, the two inductive hypotheses generated are

hA : t * (A + B) = t * A + t * B → t * (A + succ B) = t * A + t * succ B,
hB : t * (succ A + B) = t * succ A + t * B

Upvotes: 1

Views: 124

Answers (1)

Christopher Hughes
Christopher Hughes

Reputation: 1129

The second induction wasn't actually necessary in this proof. The proof you wrote for the succ case works without inducting on A first, just replacing every mention of succ A with a

This proof should work.

lemma mul_add (t a b : nat) : t * (a + b) = t * a + t * b :=

begin

  induction b with B hB,

  -- b base case
  rw add_zero a,
  rw mul_zero t,
  rw add_zero (t*a),
  refl,

  rw add_succ a B,
  rw mul_succ t (a + B),
  rw hB,
  rw add_assoc (t*a) (t*B) t,
  rw <- mul_succ t B,
  refl,

end

Sometimes it can happen that you need to case split on whether a natural number is zero or not, but without using your induction hypothesis, but this isn't one of those occasions.

Upvotes: 2

Related Questions