Zulip Chat Archive

Stream: new members

Topic: Help with rw

Daniel Vainsencher (Jun 03 2022 at 18:18):

Second day using lean, and a little confused.

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

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 (Jun 03 2022 at 18:20):

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 (Jun 03 2022 at 18:21):

Ah... thanks!

Daniel Vainsencher (Jun 03 2022 at 18:27):

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 :=
calc A=B : sorry
...   =C : sorry
...   =D : sorry,

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

Riccardo Brasca (Jun 03 2022 at 18:27):

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 (Jun 03 2022 at 18:28):

The example is just not precise

Daniel Vainsencher (Jun 03 2022 at 18:28):

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

Patrick Massot (Jun 03 2022 at 18:29):

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

Patrick Massot (Jun 03 2022 at 18:29):

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

will presumably work

Daniel Vainsencher (Jun 03 2022 at 18:40):

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 (Jun 03 2022 at 18:41):

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 (Jun 03 2022 at 18:47):

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

Kyle Miller (Jun 03 2022 at 18:54):

Seems like a good idea to me

Kyle Miller (Jun 03 2022 at 18:55):

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

have H : A = D,
{ calc A = B : _
  ...    = C : _
  ...    = D : _,
  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 (Jun 04 2022 at 16:06):

@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

Last updated: Dec 20 2023 at 11:08 UTC