tactic at a target

Stream: Berkeley Lean Seminar

[Zachary Stier]

In Multiplication World level 9, we prove a*(b*c)=b*(a*c). I wanted to do rw mul_comm, rw mul_assoc, rw mul_comm, with the final rewrite applied to the parenthesized multiplication on the LHS (since beforehand we have b*(c*a)). Is this possible? I managed to prove it using induction but this seemed unnecessary.

[Kyle Miller]

You should be able to do rw mul_comm b c

[Patrick Lutz]

I think there's also a way to enter only the left hand side of a goal and use rewrites there, but I can't remember how to do it

[Zachary Stier]

Kyle Miller said:

You should be able to do rw mul_comm b c

Yes, this works, thanks!

[Kyle Miller]

My understanding is that mul_comm is a two-argument function, and giving it b and c causes it to be a concrete instance of commutativity. rw mul_comm b might have worked, too, since it partially applies the function with b.

[Jalex Stark]

Patrick Lutz said:

I think there's also a way to enter only the left hand side of a goal and use rewrites there, but I can't remember how to do it

I think conv and maybe conv_lhs are relevant keywords

[Jalex Stark]

Yes, the example on this docs page about conv is almost exactly the example zach brought up:
https://leanprover-community.github.io/extras/conv.html

[Jalex Stark]

example (a b c : ℕ) : a * (b * c) = a * (c * b) :=
begin
conv in (b*c) {rw mul_comm,},
end

[Zachary Stier]

Jalex Stark said:

Yes, the example on this docs page about conv is almost exactly the example zach brought up:
https://leanprover-community.github.io/extras/conv.html

Oh awesome, thanks! This looks like a very useful/general way to resolve these kinds of proofs.

[Jalex Stark]

once you take off the training wheels of the natural number game, the right way to deal with chaining commutativity and associativity is to apply the ring tactic

[Jalex Stark]

ring at h will do something like "apply commutativity, associativity, and distributivity until the expression is in normal form"

[Jalex Stark]

(also, hi! nice to see you here :slight_smile: )