Rewriting the goal with metavariables duplicates goals

Stream: lean4

[Yann Herklotz]

It seems like rewriting a goal with uninstantiated metavariables leads to the goals associated with the metavariable to be duplicated. For example for the following theorem:

example : ∀ d g, d = g → exists x : Nat, x = d := by
  intros d g H1
  constructor
  rewrite [H1,←H1,H1,←H1,H1]
  -- rotate_left; exact g; rfl

We are left with 7 goals, and each additional rewrite adds another goal. However, if you do instantiate the metavariable, then all goals disappear as expected.

I was mainly wondering if this was expected, because we sometimes have a few metavariables that aren't resolved until the very end with a large context and perform rewrites, which seems to slow down the vscode window and maybe lean itself because it tries to display all the repeated contexts.

[Jovan Gerbscheid]

I have run into this as well, and I agree that it is a problem. I've made a fix for it here: lean4#4381

[Patrick Massot]

Jovan probably means lean4#4381

[Jovan Gerbscheid]

Oops, I keep forgetting to write lean4

[Patrick Massot]

It seems you also forget to include tests :wink:

[Jovan Gerbscheid]

I'll do that next :)

[Jovan Gerbscheid]

I've added a minimal test now

[Yann Herklotz]

Oh amazing thanks for the quick response, I'll try that out and see if it affects the performance of our proofs too.

[Notification Bot]

Yann Herklotz has marked this topic as resolved.

[Eric Wieser]

This issue seems to have returned for me, c.f. lean4#6407

[Jovan Gerbscheid]

The fix wasn't exhaustive: after the fix, rw only duplicates metavariables that appear in the rewrite rule. This fixes the original example where the rewrite rule is just a free variable. But when using a lemma like eq_comm, the metavariables from the goal will appear in eq_comm after unification. If you instead use @eq_comm, then the metavariable will not get duplicated

[Notification Bot]

Eric Wieser has marked this topic as unresolved.