Zulip Chat Archive

Stream: new members

Topic: can you limit rewrite tactic


view this post on Zulip 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 :=
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?

view this post on Zulip Patrick Massot (Jan 31 2021 at 20:25):

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

view this post on Zulip 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}.

view this post on Zulip 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

view this post on Zulip 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: May 18 2021 at 16:25 UTC