rewrite tactic failed, lemma lhs is a metavariable

Stream: new members

[Jiekai]

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]

because rw is stupid

[Mario Carneiro]

try rw b_ih_h.symm

[Jiekai]

Worked! so many tricks

[Jiekai]

What's the difference between symm and ← ?

[Kevin Buzzard]

In theory, nothing

[Kevin Buzzard]

I am surprised the arrow didn't work

[Mario Carneiro]

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]

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

[Mario Carneiro]

both could be fixed in lean 3.8

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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

[Amaury Hayat]

Hi all ! Is this point still a problem ? I am asking because I had this type of issue for the first time today and only with the rule mul_mul_div: when I try to use

example (x y : real)(h: x≠ 0)(h1: y=1):y*x*(1/x) = 1:=
begin
  rwa ←mul_mul_div _ h,
end

this does not work and gives the message "rewrite tactic failed, lemma lhs is a metavariable" while when I try

example (x y : real)(h: x≠ 0)(h1: y=1):y*x*(1/x) = 1:=
begin
  rwa ←mul_mul_div y h,
end

it works. Since all other basic rules that I tried in the last months worked well I was wondering whether this is a general issue with rw / I am doing something wrong in this example / this only concerns mul_mul_div (and maybe a few others that I haven't tried) for some reason ?

[Kyle Miller]

This is curious -- it shouldn't matter that the LHS is a metavariable since you're rewriting in the reverse direction.

Here's a workaround:

example (x y : ℚ)(h: x≠ 0)(h1: y=1):y*x*(1/x) = 1:=
begin
  rwa (mul_mul_div _ h).symm,
end

[Yaël Dillies]

Is this a faulty check in rw? That is, it checks whether there are metavariables in the LHS before it actually knows which side of the equality is the LHS?

[Amaury Hayat]

Thanks for the answer :) Yes, this is curious, and also I tried many basic rules and never had that before...

[Yaël Dillies]

@Mario Carneiro are you aware of this?

[Reid Barton]

Is it the case in general that rw never works if you provide _ arguments? (assuming they can't somehow be inferred before looking at the rewrite target)

[Yaël Dillies]

No, I definitely made that work before.

[Mario Carneiro]

Yes, I was aware of this and find it mildly amusing

[Mario Carneiro]

I'm not even sure the check is all that useful, rw can totally work even if the pattern is a metavariable

[Mario Carneiro]

it should just match the first subterm which matches the type

[Mario Carneiro]

Oh, I even say as much earlier in this thread

[Kyle Miller]

It looks like it might be an easy fix: this if block should move two lines up. (Or, if the LHS check is not actually useful, the two lines above could be deleted.)

[Kyle Miller]

I tried removing the LHS check to see what would happen, and it looks like it's there to give a nicer error message.

example (x : ℕ) (h : ∀ (z : ℕ), z = z + 1) : x = x + 1 :=
begin
  rw h,
/-
14:3: rewrite tactic failed, did not find instance of the pattern in the target expression
  ?m_1
-/
end

According to a docstring for the pattern matching algorithm (kabstract): "We detect subterms equivalent to \c t using key-matching.
That is, only perform is_def_eq tests when the head symbol of substerm is equivalent to head symbol of \c t."

[Kyle Miller]

But backwards rewriting with LHS metavariables works great:

theorem nat.mul_div_left' (n : ℕ) {m : ℕ} (H : 0 < m) : n = n * m / m :=
by rwa nat.mul_div_left

example (x y : ℕ) (h : 0 < x) (h1 : y = 1) : y * x / x = 1:=
begin
  rwa ← nat.mul_div_left' _ h,
end

[Kyle Miller]

lean#690

[Eric Wieser]

The current behavior encourages us to write lemmas with the simpler dude on the RHS, right?

[Eric Wieser]

Not that that should mean we leave it broken, but docs#mul_mul_div looks backwards to me