rw tactic creates metavariable with no goal

Stream: lean4

[Ted Hwa]

Has anyone ever come across a situation where rw creates a metavariable, but no corresponding goal to fill it in? I have no #mwe yet (in the middle of a long argument). In my case, the metavariable corresponds to a missing proof.

The funny thing is, the proof still compiles with no errors. I think that's because the expression with the metavariable (let's call it foo ?m.123) is later used to match a goal foo pf where the pf is an actual proof, so Lean realizes it can fill in the metavariable with pf. But this doesn't explain the initial behavior, since there's no way Lean could have known that foo would be used in this way.

[Kevin Buzzard]

Lean can sometimes fill in proof metavariables by e.g. typeclass inference or finding them in the local context.

[Shreyas Srinivas]

rw doesn't create goals.

[Kevin Buzzard]

Oh sure it does

[Shreyas Srinivas]

It creates mvars, but not goals surely? Not ones it can't fill

[Kevin Buzzard]

Oh I don't know the difference between a metavariable and a goal

[Shreyas Srinivas]

A tactic could create a hole metavariable that it fills by looking for theorems or hypotheses

[Kevin Buzzard]

All I'm saying is that if h : P -> (A = B) then rw [h] might create a new goal P if the original goal is A

[Ted Hwa]

rw definitely creates additional goals for the mvars it can't fill.

[Shreyas Srinivas]

Never seen it happen. In fact I have had rw fail when it can't find some typeclass instance or argument which it could have thrown as a goal.

[Shreyas Srinivas]

But okay. TIL. Is there an example of this?

[Ted Hwa]

If it found them in the local context, shouldn't the value (or at least ... for a proof) show up in the infoview? Right now I see foo ?m.123 in the infoview.

[Shreyas Srinivas]

You could use extract_goal to help construct an mwe

[Kevin Buzzard]

variable (P : Prop) (A B : ℕ) (h : P → (A = B)) in
example : A = 0 := by
  rw [h]
  -- two goals B=0 and P