can you limit rewrite tactic

Stream: new members

[Andrew Parr]

Hi I've not posted before so let me first introduce myself. I'm Andrew Parr and I'm currently studying for an MSc in Mathematics at the Open University part time and I'm also trying to learn lean.

I'm been looking at the excellent formalising-mathemtics by @Kevin Buzzard but am currently stuck on proving the lemma inv_inv in tatic mode (found in week_2\Part_A_groups.lean).

After struggling for a while to prove this in tactic mode I found I could prove it in calc mode. I then tried to convert this proof to tactic mode but fail because the rewrite tactic is rewriting both of the a terms. The following extract should help to clarify what I mean.

@[simp] lemma inv_inv : a ⁻¹ ⁻¹ = a :=
begin
  calc a⁻¹ ⁻¹ = 1 * a⁻¹ ⁻¹ : by rw one_mul -- after this we have a⁻¹⁻¹ = 1 * a⁻¹⁻¹
    ... = (a * a⁻¹) * a⁻¹ ⁻¹ : by rw mul_right_inv
    ... = a * (a⁻¹ * a⁻¹ ⁻¹) : by rw mul_assoc
    ... = a * 1 : by rw mul_right_inv
    ... = a : by rw mul_one,
end

-- Trying to convert the above 'calc mode' proof to 'tatic mode'
example : a ⁻¹ ⁻¹ = a :=
begin
  rw ← one_mul a, -- this does both sides giving (1 * a)⁻¹ ⁻¹ = 1 * a
  -- adding "at |-" to the above also doesn't help
  rw ← mul_right_inv a⁻¹, -- again this does both sides
  sorry,
end

Is there a way to tell the rw tactic to only work on the right hand side (or something). What I'm I missing here?

[Patrick Massot]

https://leanprover-community.github.io/extras/conv.html

[Kevin Buzzard]

Hi! You can tell the rw tactic to only work on the right hand side using the conv_rhs tactic. Try conv_rhs {rw ← one_mul a}.

[Kevin Buzzard]

You can also cheat and look at how I did it in the kb_solutions subdirectory which I uploaded after the workshop: https://github.com/ImperialCollegeLondon/formalising-mathematics/blob/master/src/week_2/kb_solutions/Part_A_groups_solutions.lean

[Andrew Parr]

Brilliant, thank you Patrick and Kevin. This is exactly what I was missing.
I did notice there were solutions for week_1, but didn't have them for week_2. I didn't think of doing another git pull.
I have them now.