ambiguous not_imp

Stream: general

[Johan Commelin]

Together with @Pim Otte I stumbled upon

import Mathlib.Logic.Basic

variable (P Q : Prop) -- let `P` and `Q` be two logical statements

example : ¬ (P → Q) ↔ P := by
  rw [not_imp] -- ambiguous
  sorry

#check not_imp -- Classical.not_imp, no failure
#check Classical.not_imp -- Classical.not_imp
#check _root_.not_imp -- not_imp

[Johan Commelin]

docs#Classical.not_imp is in core. Should mathlib drop docs#not_imp ?

[Jireh Loreaux]

are you missing an open Classical in the code above?

[Jireh Loreaux]

I'm just confused as to how that rw could be ambiguous without it.

[Kyle Miller]

https://github.com/leanprover/lean4/blob/e9e858a4484905a0bfe97c4f05c3924ead02eed8/src/Init/Classical.lean#L169-L170

[Jireh Loreaux]

Why doesn't Lean complain when docs#not_imp is declared in Mathlib then? That seems like a bug.

[Jireh Loreaux]

But aside from this, yes, let's abolish docs#not_imp.

[Kyle Miller]

Exporting doesn't create new declarations, it just adds to a table of name synonyms used by name resolution. It's working as designed, but perhaps it could be considered to be a usability bug.

[Jireh Loreaux]

Yeah, it seems like when you add a declaration to the environment if there is a name synonym, then Lean should warn you.

[Jireh Loreaux]

Shall I create an issue?

[Kyle Miller]

Sure, seems reasonable. Maybe it could be a linter warning?

[Jireh Loreaux]

Does this constitute a bug report or an RFC?

[Kyle Miller]

Let's say a bug report since you're saying "this doesn't work how I expect it to". An RFC would be "here's a proposed solution". Its OK if a bug report has some discussion about possible solutions at the end.

[Jireh Loreaux]

lean4#5258

[Johan Commelin]

@Jireh Loreaux Thanks for turning this into a bug report!