Rewrite fails to disambiguate when only one option is valid

[b-mehta]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

Rewrite fails to disambiguate when only one option is valid

Context

theorem add_succ : true = true := rfl

open Nat

#check add_succ -- Nat.add_succ
#check (add_succ : true = true) -- _root_.add_succ

example (x y : Nat) : x + (y + 1) = (x + y) + 1 := by
  rw [add_succ]
  /-
  ambiguous, possible interpretations
  _root_.add_succ : true = true

  Nat.add_succ : ∀ (n m : Nat), n + succ m = succ (n + m)
  -/

Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/ambiguous.20rewrite.20when.20only.20one.20is.20valid. The equivalent in Lean 3 succeeds. Thanks to @kmill for minimising. This showed up in porting the exponential-ramsey project.

Steps to Reproduce

Code as above.

Expected behavior: The rewrite succeeds and closes the goal.

Actual behavior: The rewrite fails.

Versions

Lean (version 4.3.0-rc1, commit baa4b68, Release)
MacOS

Additional Information

None

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

NB: This happens with other tactics as well:

/--
error: ambiguous term, use fully qualified name, possible interpretations [_root_.add_succ, Nat.add_succ]
-/
#guard_msgs in
example (x y : Nat) : x + (y + 1) = (x + y) + 1 := by
  apply add_succ

Arguably it’s an issue with #check?

[Kha]

Arguably it’s an issue with #check?

Yes, that's #5873

[Kha]

@b-mehta Was this more of a porting gotcha or are you still interested in seeing this issue fixed?

[b-mehta]

I'm still interested in seeing this issue fixed, outside of being a regression from Lean 3:

1. It's confusing behaviour to beginners to see a rewrite fail with error mentioning "ambiguous", when there's not actually an ambiguity.
2. This came up in mathlib, see eg the linked PR above.
3. If I write a term in term-mode which has an ambiguity in name resolution, Lean is able (IIUC) to disambiguate in the case that the types are enough to figure it out. So it would be nice if the same were true in rewrites.

[b-mehta]

(deleting this comment because it was nonsense)

[nomeata]

So would you expect that all tactics to try all possible interpretations of a name, and silently use the first that happens to make progress? Or only some of them? Would simp use the first one that it can use, and ignore the others, or all of them?

[b-mehta]

So would you expect that all tactics to try all possible interpretations of a name, and silently use the first that happens to make progress?

No, but if there is exactly one interpretation which makes sense, I would expect the tactic to use that one, rather than failing with an error that there are multiple possible interpretations. If there are multiple interpretations which make sense, then an "ambiguous, possible interpretations" error is completely fine. The bug in this issue is specifically that rw [_root_.add_succ] fails, and rw [Nat.add_succ] succeeds despite Lean's error message saying that these are both possible. And as such, the rw [add_succ] should disambiguate to rw [Nat.add_succ]. If there are three name resolutions and two of them could be valid, then "ambiguous" would make complete sense.

I hope this makes it clearer what the expected behaviour here is! If nothing else, then I hope it is clear that "ambiguous, possible interpretations" is a poor error message given that not all the interpretations are actually possible.

[nomeata]

Thanks for the (heh) elaboration. My personal opinion is that I find the current behavior, with a clear phase separation between name resolution and tactic execution, more predictable and preferable. But I have noticed that I'm leaning towards more explicitness and less magic than seems to be idiomatic in at least mathlib, so I'll just let that stand and let others call this shot.

[nomeata]

And, to add, some more questions that this feature require raises:

Assuming that rewrite [foo] would succeed if foo resolves to multiple names, but exactly one of them can be rewritten with, how does that interact with tactic combinators.

• For example, rewrite [foo] <;> rfl – will that work if both foo’s can be rewritten with, but only in one case the the next step closes the goal?
• Would rw [foo] behave the same as rewrite [foo] <;> rfl, or differently?
• What about tac <;> rewrite [foo]. Does this work if there is a “globally unique” foo that this can be rewritten with, or can every branch make it's own decision? If the latter, what type and docstring is shown when hovering foo?

---

More generally, if in rewrite [foo] the foo can be understood as “bag of theorems, of which exactly one should may make sense”, then it seems prudent to make that a proper feature of its own, where a name can generally be a bag of theorems, and make good use of that in general. This is what Isabelle does – lemmas foo_or_bar = foo bar is a thing, and often useful. It seems odd if Lean effectively properly supported names-referring-to-sets-of-things, but then only expose it when name resolution is ambiguous due to namespaces.

Actually, we almost already have that feature, in a way, although the syntax is a bit weird:

open _root_ renaming Nat.le_of_lt → foo
open _root_ renaming Int.le_of_lt → foo
open _root_ renaming True.intro → foo

/--
error: ambiguous, possible interpretations ⏎
  True.intro : True
  ⏎
  @Int.le_of_lt : ∀ {a b : Int}, a < b → a ≤ b
  ⏎
  @Nat.le_of_lt : ∀ {n m : Nat}, n < m → n ≤ m
---
error: tactic 'rewrite' failed, equality or iff proof expected
  ?m.5
⊢ True
-/
#guard_msgs in
example : True := by rw [@foo]

(And while you can write open _root_ renaming Nat.le_of_lt → Foo.foo, it doesn't actually add foo to namespace Foo in a way that you can open Foo.)

Anyways, it’s a big design space, and I’d prefer the simplicity of asking the use to be explicit which lemma they want to use.

[kmill]

I think that this doesn't need to have quite so profound of design consequences @nomeata. The question to me is just "should kabstract be considered to be part of elaboration or not"? We have at least a couple examples of it being within the scope of elaboration (the triangle operator and elabAsElim), so it doesn't seem impossible for the product of a rw theorem elaboration to be the theorem and the motive together. This should naturally handle disambiguation in the way Bhavik would want. Edit: When writing this I forgot that this disambiguation happens too early even in the elaborator to help rw disambiguate. The next paragraph should be OK though.

Similarly, for apply, if we made it into an app elaborator mode like we'd discussed once in a DM, that too would naturally handle disambiguation.

[nomeata]

We discussed this a bit further, and decided to leave things as they are. The error message is rather explicit and actionable, so I expect the status quote to be less confusing overall. Plus the unclear scope of “exactly one works” in the presence of tactic combinators.

(I acknowledge that the existing term-mode disambiguation muddies my argument a bit, but still.)

[b-mehta]

I see, so this is viewed as an acceptable regression from Lean 3 behaviour?

I don't view the error message as particularly clear in this case: it says there are multiple possible interpretations, not all of them are actually possible. Indeed, in the example in the OP, using _root_.add_succ is not possible. More generally, does this closure mean that when I see a message "possible interpretations" in the future, I should not take this as accurate?

The scope of "exactly one works" can be restricted to exactly the tactic which is throwing the error. Indeed, the behaviour here can be inferred from the Lean 3 version! Furthermore, this disambiguation is exactly how the term-mode disambiguation works, and how the exact tactic works:

theorem add_succ (_ _ : ℕ): true = true := rfl

open Nat

example (x y : Nat) : x + (y + 1) = (x + y) + 1 := by
  exact add_succ x y

In the future, should I continue to expect inconsistencies like this in elaboration?

[nomeata]

Maybe I am confused by what you mean, but isn’t_root_.add_succ is a possible interpretation of “add_succ” in this point? It’s an interpretation that happens to make rw fail, but so does rw [mul_succ].

Would you say that Nat.mul_succ is not an interpretation of mul_succ in rw [mul_succ] if that rewrite fails?

More generally, does this closure mean that when I see a message "possible interpretations" in the future, I should not take this as accurate?

I understand this message as “possible interpretations of the name”, which is accurate. It does not mean “possible interpretations of the name for which rewriting succeeds”.

to exactly the tactic which is throwing the error.

This is a concept I have qualms with. Many tactics are implemented by elaboration to other tactics. Do you mean “tactic that the user wrote” or “primitive tactic” (whatever that means).

Consider rewrite [thmA_or_thm_B, thm2], where thmA an resolve to thmA or thmB. Assume that both rewrite, but only if thmB was taken, thm2 can apply. Should this, under your design, succeeds as rewrite [thmB, thm2] would, or complain that thmA_or_thmB is ambiguous?

Or similar with rw – is the rfl inside that tactic included or not?

In the future, should I continue to expect inconsistencies like this in elaboration?

Yes, unfortunately. Note that

example (x y : Nat) : x + (y + 1) = (x + y) + 1 := by
  apply add_succ x y

also reports “ambiguous, possible interpretations”.

It seems that term elaboration can and will use type information to resolve ambiguities, and it’s not always clear how much type information is available in a given context. But it seems that’s consistent with other features, like dot notation.

[kmill]

@b-mehta I was just reading the Lean 3 source code, and I don't see anything that indicates that rw was aware of choice nodes. (In Lean 3, parsing and elaboration ambiguities could be represented using "choice nodes". In Lean 4, only parsing has choice nodes.) I also checked how type inference worked for choice nodes, and Lean 3 threw an error in that case, so there are also no features that could have made this disambiguation work that I can see.

Could you please verify that the Lean 3 rw was able to disambiguate in the way you're saying it did? It seems possible that this is all explainable by other differences, and it would be good to be completely sure that there was a disambiguation mechanism that rw was using before continuing the discussion in this direction.

[digama0]

As far as I am aware, lean 3 did not handle this situation any better than lean 4.

[b-mehta]

I understand this message as “possible interpretations of the name”, which is accurate. It does not mean “possible interpretations of the name for which rewriting succeeds”.

Hmm okay, this is convincing.

Could you please verify that the Lean 3 rw was able to disambiguate in the way you're saying it did?

Huh, looking at my older non-minimised example, the behaviour which I'd originally complained about seems to actually work fine now (and behaves similarly to Lean 3).

...and investigating further, the difference happened in minimisation! The example with pow_succ in the linked zulip thread (seemingly) didn't disambiguate correctly, but does now, and it's because of the protected tag on Nat.pow_succ. Whereas after changing to add_succ, where there's no protected on Nat.add_succ, the situation changes.
(Maybe this means Nat.add_succ should be protected, though?)

So I'm happy to consider this issue resolved. Thanks all!