Advanced multiplication world final level

Stream: general

[Andrew Helwer]

Anyone have any small hints for the final level of advanced multiplication world that doesn't give away the full game? I'm at:
case mynat.succ
a b d : mynat,
hd : a ≠ 0 → a * b = a * d → b = d,
anz : a ≠ 0,
h : a * b = a * succ d
⊢ b = succ d

[Mario Carneiro]

unfold the definition of a * succ d , then use the inductive hypothesis and left cancellation of addition

[Andrew Helwer]

So use induction a second time?

[Kevin Buzzard]

This doesn't look good. Isn't hd useless?

[Kevin Buzzard]

We know a isn't zero, but we also know that ab isn't ad from h, so hd can never be used.

[Kevin Buzzard]

I'm really sorry about this final level -- nobody can do it ;-)

[Kevin Buzzard]

I usually ask students if they can prove it in maths rather than in Lean!

[Andrew Helwer]

No worries, it's nice to have a challenge! I definitely banged my head against the first level in advanced multiplication world for an hour before getting it - makes victory all the sweeter.

[Andrew Helwer]

I've started trying to follow this proof on math stackexchange: https://math.stackexchange.com/a/3219757/616655

[Andrew Helwer]

but then I get to "To say that m≠0 means that m=z+1 for some z" and I don't know how to introduce a new variable z

[Kevin Buzzard]

You can do cases m with z to do that.

[Andrew Helwer]

Ahhhh yeah that would do it. Also before that... I have a * b \ne 0 and a \ne 0 but don't think I have a theorem to get to b \ne 0

[Andrew Helwer]

I suppose I could look up how to introduce & prove new theorems mid-proof

[Kevin Buzzard]

But I am concerned that the state that your game is problematic because you will need induction at some point and your hd is useless. I think your hd needs to be beefed up to have a "for all b" in . I don't think you can finish from here, whatever a 2 point answer on stackexchange says

[Andrew Helwer]

Well I did try a double induction strategy at one point and after much finangling managed to change ab = ac => b = c to ba = ca => b = c lol. But perhaps I will try the induction again from the top without adding a "revert ha" at the beginning

[Andrew Helwer]

huh... actually that probably would have worked because then I could just use mul_comm and the inductive hypothesis? I will try this!

[Andrew Helwer]

All right I throw in the towel... does anyone have a proof of this? Would love to go over it line by line.

[Alex J. Best]

Credit : I copied this (with some light edits) from the solutions, but I won't link to them unless you ask for it as I don't want to spoil any fun ;):

  revert b,
  induction c with d hd,
  { intro b,
    rw mul_zero,
    intro h,
    cases (eq_zero_or_eq_zero_of_mul_eq_zero a b h),
      exfalso,
      apply ha,
      assumption,
    assumption,
  },
  { intros b hb,
    cases b with c,
    { rw mul_zero at hb,
      rw mul_succ at hb,
      exfalso,
      apply ha,
      rw eq_comm at hb,
      apply add_left_eq_zero (a * d) a hb,
    },
    { congr, -- c = d -> succ c = succ d
      apply hd,
      rw mul_succ at hb,
      rw mul_succ at hb,
      apply add_right_cancel (a*c) a (a*d) hb
    }
  }

[Andrew Helwer]

lol what is this revert b thing

[Alex J. Best]

revert is the opposite of intro, it turns a statement with given variable into a forall

[Alex J. Best]

I think it is listed under the tactics box on the left in natural number game.

[Andrew Helwer]

Oh sure, I've just never seen it used in this specific way... still going through the proof

[Andrew Helwer]

Huh I was actually very close, except for the use of "revert b" (which effect I still don't understand on the proof - makes the inductive hypothesis nicer?) and the use of case instead of a second induction

[Andrew Helwer]

Okay yeah this is very strange. Don't know why "revert b" has the effect that it does on the inductive hypothesis, can anyone explain? Thanks for the proof btw!

[Patrick Massot]

Without revert, b is fixed in the whole inductive proof.

[Patrick Massot]

(Note I don't even know what you want to prove, I can only tell what revert is doing to inductive proofs).

[Andrew Helwer]

so it looks like without "revert b", "cases b with e" rewrites our inductive hypothesis to "hd : a * succ e = a * d → succ e = d"
whereaswith "revert b" it's rewritten to "∀ (b : mynat), a * b = a * d → b = d" which we can actually use to solve the proof

[Andrew Helwer]

trying to wrap my head around when I'd want to put a universally-quantified variable in the inductive hypothesis vs not

[Patrick Massot]

Can someone post the goal of this proof?

[Andrew Helwer]

theorem mul_left_cancel (a b c : mynat) (ha : a ≠ 0) : a * b = a * c → b = c :=

[Patrick Massot]

so it looks like without "revert b", "cases b with e"

This is a typo, right? If you revert b you cannot case on b.

[Andrew Helwer]

This cases is nested within an induction, here's my (horribly formatted) proof:
revert b,
induction c with d hd,

intros b h,
rw mul_zero at h,
rw mul_eq_zero_iff at h,
cases h with p q,
exfalso,
apply ha,
exact p,
exact q,

intros b h,
cases b with e,
rw mul_zero at h,
symmetry at h,
exfalso,
apply ha,
rw mul_eq_zero_iff at h,
cases h with p q,
exact p,
exfalso,
apply succ_ne_zero d,
exact q,
rw succ_eq_succ_iff,
apply hd,
rw mul_succ a e at h,
rw mul_succ a d at h,
rw add_right_cancel_iff at h,
exact h,

[Patrick Massot]

The first two lines of the proof are revert b, induction c with d hd,. Here it should be very easy to compare the induction hypothesis you get with or without the revert. Clearly the one you get after revert is stronger.

[Andrew Helwer]

I guess what I want to get at is what exactly is this doing and in what circumstances would I want to do this (reverting a variable declaration is a new technique in this natural numbers game tutorial)

[Scott Morrison]

It's just a matter of whether you've fixing a value for b before you do the induction or not.

[Patrick Massot]

By the way, I don't know if this is explained in the natural number game, but the recommended way of doing those first two lines is induction c with d hd generalizing b, which does the intro afterwards (but this may be too much magic if you already have difficulties here).

[Scott Morrison]

intro b effectively says "let b be some particular value", and revert b says: actually, let's make life harder, by proving this for all values of b

[Alex J. Best]

I don't think generalizing works in natural number game?

[Marc Huisinga]

Andrew Helwer said:

trying to wrap my head around when I'd want to put a universally-quantified variable in the inductive hypothesis vs not

it depends! sometimes proving a more general statement is easier. in fact, for some inductive proofs you need to generalize to entirely different statements in order to be able to prove them comfortably (i.e. generalizing in a way that is trickier than just using revert).
if you have a bunch of universal quantifiers at the beginning of your statement, revert is just the same thing as shuffling around the order of those quantifiers, usually in a way that yields the strongest induction hypothesis when you introduce the variable you want to induct on.