## Stream: new members

### Topic: rewrite tactic failed, lemma lhs is a metavariable

#### Jiekai (Mar 29 2020 at 04:46):

Why is rw ← b_ih_h, here failing?

rewrite tactic failed, lemma lhs is a metavariable
state:
a b_n b_ih_w : mynat,
b_ih_h : b_n + succ b_ih_w = a
⊢ a = succ b_n + b_ih_w


#### Mario Carneiro (Mar 29 2020 at 04:47):

because rw is stupid

#### Mario Carneiro (Mar 29 2020 at 04:47):

try rw b_ih_h.symm

#### Jiekai (Mar 29 2020 at 04:49):

Worked! so many tricks

#### Jiekai (Mar 29 2020 at 04:52):

What's the difference between symm and  ← ?

#### Kevin Buzzard (Mar 29 2020 at 09:21):

In theory, nothing

#### Kevin Buzzard (Mar 29 2020 at 09:21):

I am surprised the arrow didn't work

#### Mario Carneiro (Mar 29 2020 at 11:12):

The reason is because the rewrite tactic is explicitly checking that the lhs is not a variable. The idea here is that if you rewrite with something that matches any term, you will not get a useful result. This check is wrong for two reasons: (1) the variable is not a metavariable, and even if it was that might still be a reasonable thing to do if the type of the variable is constraining enough; and (2) it's always the lhs, not the rhs, even if you use <-.

#### Patrick Massot (Mar 29 2020 at 11:13):

Isn't at least point 2) something that could change in Lean 3.8?

#### Mario Carneiro (Mar 29 2020 at 11:31):

both could be fixed in lean 3.8

#### Mario Carneiro (Mar 29 2020 at 11:32):

There is nothing wrong with the algorithm, there is just a check that throws an exception. Delete the check and everything else should work

#### Patrick Massot (Mar 29 2020 at 11:32):

I meant that point 2) sounds like a plain bug, whereas point 1) is debatable.

#### Mario Carneiro (Mar 29 2020 at 11:43):

I think that the part of 1) about not matching variables that are not metavariables / universally quantified variables is also a bug. For example in the example above, we are rewriting with an equality in the context, which can only match a, not anything else with the same type as a

#### Mario Carneiro (Mar 29 2020 at 11:44):

The only time the error is reasonable is if you are rewriting with \forall x, x = ..., so that the pattern can match any term

Last updated: May 13 2021 at 22:15 UTC