Zulip Chat Archive

Stream: new members

Topic: Problem with rewrite tactic


view this post on Zulip Syx Pek (May 22 2020 at 12:54):

Hello there, I am working through the proof that left identity and left inverse implies a group from
https://leanprover-community.github.io/mathematics_in_lean/

theorem mul_right_inv (a : G) : a * a⁻¹ = 1 :=
begin
    have h₁ : (a⁻¹) * (a⁻¹)⁻¹ = (a⁻¹) * a, sorry,
    have h₂ : (a⁻¹)⁻¹ = a, sorry,
    calc a * a⁻¹
        = (a⁻¹)⁻¹ * (a⁻¹)          : by rw  h₂
    ... = 1                        : by rw mul_left_inv
end

But I face some difficulty. I don't see why line 6 fails.

view this post on Zulip Jason KY. (May 22 2020 at 12:57):

The left arrow means you want to rewrite using h₂ from a to (a⁻¹)⁻¹. Using just rw h₂ works fine!

view this post on Zulip Jason KY. (May 22 2020 at 12:58):

theorem mul_right_inv (a : G) : a * a⁻¹ = 1 :=
begin
    have h₁ : (a⁻¹) * (a⁻¹)⁻¹ = (a⁻¹) * a, sorry,
    have h₂ : (a⁻¹)⁻¹ = a, sorry,
    calc a * a⁻¹
        = (a⁻¹)⁻¹ * (a⁻¹)          : by rw h₂
    ... = 1                        : by rw mul_left_inv
end

view this post on Zulip Syx Pek (May 22 2020 at 13:02):

I see. But why doesn't the approach I suggested would fail. It says in the documentation, that it rewrites only the first copy of it, but it seems to rewrite all copies?

view this post on Zulip Bhavik Mehta (May 22 2020 at 13:05):

Out of interest where did you read that it rewrites only the first copy?

view this post on Zulip Jason KY. (May 22 2020 at 13:06):

In my experience it normally rewrites every instance :/

view this post on Zulip Bhavik Mehta (May 22 2020 at 13:06):

I think that it'll rewrite all copies of the first instance it finds, if that makes sense. That is, if you do rw add_comm and your term has a bunch of a + b and c + d, it'll change all of the a+b to b+a but none of the c+d

view this post on Zulip Syx Pek (May 22 2020 at 13:09):

It says "Sometimes the left-hand side of an identity can match more than one subterm in the pattern, in which case the rewrite tactic chooses the first match it finds when traversing the term. If that is not the one you want, you can use additional arguments to specify the appropriate subterm." on https://leanprover.github.io/theorem_proving_in_lean/tactics.html

view this post on Zulip Bhavik Mehta (May 22 2020 at 13:10):

Yeah, so seemingly it chooses the first match and applies that one as much as it can

view this post on Zulip Reid Barton (May 22 2020 at 13:11):

Yes, it is a confusing description of a confusing behavior

view this post on Zulip Scott Morrison (May 22 2020 at 14:43):

There is also nth_rewrite if you want control over this. (As well as the occs configuration argument for rw, which is even more confusingly specified.)

view this post on Zulip Scott Morrison (May 22 2020 at 14:43):

But usually conv to zoom into the place you're interested in is clearer and more maintainable.


Last updated: May 09 2021 at 18:17 UTC