Help with rw

Stream: new members

[Daniel Vainsencher]

Second day using lean, and a little confused.

example (a b : ℝ ) : a+a*b-a*b=a :=
begin
rw sub_self (a*b),
end

fails with

rewrite tactic failed, did not find instance of the pattern in the target expression
  a * b - a * b

which I found surprising. I'm following the tutorials, this came up as part of 01_equality_rewriting.lean example 0008. I'm sure there is workaround that doesn't use sub_self, I'm looking to understand why my expectation is wrong and learn more about how rw matches work.

[Yaël Dillies]

a+a*b-a*b means (a+a*b)-a*b. There's actually no a*b-a*b in there :smile: . You can use docs#add_sub_assoc to get there.

[Daniel Vainsencher]

Ah... thanks!

[Daniel Vainsencher]

Another question: in https://leanprover-community.github.io/extras/calc.html, the example code

example : A = D :=
calc A = B : sorry
...    = C : sorry
...    = D : sorry

does not work, I needed at least

example (A B C D : ℝ ) : A = D :=
begin
calc A=B : sorry
...   =C : sorry
...   =D : sorry,
end

to get it to work. Is the example simply not precise or is something deeper going on?

[Riccardo Brasca]

It's good to understand why rw sub_self (a*b) doesn't work here, but if you are wondering how can we possible do serious math if we have to write down all this associativity/commutativity/blahblah stuff, it's good to know that ring proves your result automatically.

[Riccardo Brasca]

The example is just not precise

[Daniel Vainsencher]

Thanks @Riccardo Brasca , the tutorial I'm doing does make that point.

[Patrick Massot]

It has nothing to do with begin/end, it's missing variables

[Patrick Massot]

example (A B C D : ℝ ) : A = D :=
calc A=B : sorry
...   =C : sorry
...   =D : sorry

will presumably work

[Daniel Vainsencher]

Thanks @Patrick Massot , that is helpful, that does work. I see that without the begin/end I also do not need the terminating ,. Is there a syntax reference I should be looking at?

[Yaël Dillies]

You never need the trailing comma. It's just a quirk of the infoview that you need it to see the Goals accomplished.

[Daniel Vainsencher]

Is a PR fixing the calc doc to Patrick's version a good idea?

[Kyle Miller]

Seems like a good idea to me

[Kyle Miller]

It might be worth making the tactic version right after it look more like

have H : A = D,
{ calc A = B : _
  ...    = C : _
  ...    = D : _,
  sorry,
  sorry,
  sorry }

as well. Or maybe also put it inside an example with a begin/end block to show how it might work? I'm not sure if the have is part of the tip or not.

[Daniel Vainsencher]

@Kyle Miller I am not as sure about the second example, it seems to assume context anyway, so I'm leaving that change off for now. Also changed wording some, PR at https://github.com/leanprover-community/leanprover-community.github.io/pull/268