Error in proving add_comm in MIL chapter 7 Ring3

Stream: new members

[Shanghe Chen]

Hi why it reports an error in line 96?

[Shanghe Chen]

0484D00B-27DC-40D9-8DBC-C892EBB8E2F1.png

[Shanghe Chen]

I checked the left and the right is the same. Should I add a rfl to it?

[Shanghe Chen]

Quite late in my timezone hence now I am stop debugging it and off the computer :smiling_face: Btw is there any tactic for rw but with the reverse direction? Lots of rw <- seems a little annoying

[Patrick Massot]

You will have a much higher hope of getting an answer if you post copy-pastable code instead of a screenshot.

[Shanghe Chen]

Sorry for the fuzzy screenshot.

[Shanghe Chen]

A minimal MWE is the following, trying to prove a+b = 1*(a+b):

namespace Ex1

set_option autoImplicit true
example [Ring R] (a b : R): (a+b) = 1 * (a+b) := by
  nth_rewrite 1 [←one_mul (a+b)]
  rfl
end Ex1

[Shanghe Chen]

I remembered that the rfl is unnecessary, but if I removed it, I got an error:

-- unsolved goals
-- R: Type ?u.3301
-- inst✝: Ring R
-- ab: R
-- ⊢ 1 * (a + b) = 1 * (a + b)

[Matt Diamond]

why do you think rfl is unnecessary? you're using nth_rewrite, not nth_rw

[Shanghe Chen]

Oh I dont know there is a tactic called nth_rw, that should be the tactic I want to use before :blush:

[Shanghe Chen]

Let me check the difference between them :tada:

[Shanghe Chen]

Btw is there any tactic like rw but use the reverse direction by default, the following example have lots of <-. It's kind of a little annoying

example {G : Type} [Group G] {a b c : G} (h : a * b = a * c) : b = c := by
  rw [← one_mul b, ← one_mul c, ← mul_left_inv a, mul_assoc, mul_assoc, h]

[Shanghe Chen]

Yeah change nth_rewrite to nth_rw the rfl is unnecessarily now. Thank you very much Matt :tada:

[Patrick Massot]

Why don’t you simply rewrite in h?

[Shanghe Chen]

I am reading MIL Chapter 7 and it’s quite often only using rw. Yeah it should be cleaner if rewritten h rather than the goal. I will try this. Thank you for the kindly advice:smiling_face:

[Timo Carlin-Burns]

Patrick, do you mind elaborating? This is version of the proof with rw ... at h which comes to mind, but I wouldn't say it's simpler

import Mathlib.Tactic

example {G : Type} [Group G] {a b c : G} (h : a * b = a * c) : b = c := by
  apply_fun (a⁻¹ * ·) at h
  rwa [inv_mul_cancel_left, inv_mul_cancel_left] at h

-- It seems simpler *not* to rewrite in h:
example {G : Type} [Group G] {a b c : G} (h : a * b = a * c) : b = c := by
  rw [← inv_mul_cancel_left a b, h, inv_mul_cancel_left a c]

[Patrick Massot]

I was really commenting on the fact that Coriver was complaining about needing a lot of right to left rewrites to bring the goal to h. I was suggesting to rather rewrite from left to right in h until you get the goal. Actually the solution I wrote in MIL is doing both: simpa [mul_assoc₃] using congr_arg (· * a⁻¹) h (part of what this section is teaching is the importance of tagging relevant lemmas with simp as you go). Also note that your solution use Mathlib’s group whereas the context in MIL is a custom definition of group. If you use Mathlib then you can just as well do a single rewrite using the lemma you need to prove…