Zulip Chat Archive

Stream: new members

Topic: can you limit rewrite tactic

Andrew Parr (Jan 31 2021 at 20:24):

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 :=
  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,

-- Trying to convert the above 'calc mode' proof to 'tatic mode'
example : a ⁻¹ ⁻¹ = a :=
  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

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 (Jan 31 2021 at 20:25):


Kevin Buzzard (Jan 31 2021 at 20:26):

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 (Jan 31 2021 at 20:27):

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 (Jan 31 2021 at 20:38):

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.

Last updated: Dec 20 2023 at 11:08 UTC