Is it possible to complete MIL C02 S01 exercise as stated?

Stream: new members

[Dan Abramov]

Quoting MIL:

The following exercise is a little more challenging. You can use the theorems listed underneath.

example (a b : ℝ) : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by
  sorry

#check pow_two a
#check mul_sub a b c
#check add_mul a b c
#check add_sub a b c
#check sub_sub a b c
#check add_zero a

I've given it some time and I can't figure out how to complete it with just these theorems.

I've searched on this forum and found this existing thread by @Kate but both solutions given in the thread rely on theorems not in the list:

• @Julian Berman's relies on sub_add, sub_self, and sub_zero
• @Abraham Solomon's relies on mul_neg and add_neg_cancel

Is it actually possible to write it with the given list of theorems? If not, should MIL be amended?

[Dan Abramov]

Attempting to rectify in https://github.com/avigad/mathematics_in_lean_source/pull/279

[Kevin Buzzard]

yeah this is definitely proving tricky :-) Are you claiming that everyone can avoid mul_comm? How do you cancel a * b and b * a?

[Dan Abramov]

When solving, I took mul_comm for granted because it's used earlier in the text on this page. Technically this is true for sub_self too (although it was only used once so was easier to forget about). However, the rest of the candidates (sub_add, sub_zero, mul_neg or add_neg_cancel) were not used earlier.

In my proposed edit/solution in https://github.com/avigad/mathematics_in_lean_source/pull/279, I added sub_add and sub_self (because this one was only used once and is easy to forget). I didn't bother adding mul_comm there explicitly but can do.

[Kevin Buzzard]

I'm looking at the source (search for sub_sub in https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html) and my reading of it is "as well as the lemmas we mentioned above, such as mul_comm, you might also want to use these ones most of which we didn't mention yet"

[Dan Abramov]

Right, that matches my reading — but sub_add is not on that list (and also isn't mentioned earlier), and I couldn't figure out a way to progress without it.

[Dan Abramov]

Concretely, no matter what I was doing, I ended up getting stuck on something like a * a - a * b + a * b - ... and then saw no way to get rid of - a * b + a * b since I can't just change the order of these. I was hoping to use add_comm to somehow turn it into + a * b - a * b but the equivalence of - x and + (-x) is not yet established in the text so I wasn't sure how to do that either.

[Jeremy Avigad]

Thanks for the fixes. We will make a pass at revisions soon. It's possible that theorems were renamed since the exercise was first written, e.g. the old sub_sub might have been the reverse direction of sub_add or something like that. But anyhow it is an oversight that we didn't provide a solution.