Having trouble with hiding

Stream: new members

[Kevin Cheung]

Lean complains about the following:

import Mathlib.Logic.Basic

open Classical hiding not_imp

example (p q : Prop): ¬ (p → q) ↔ p ∧ ¬ q := by
  rw [not_imp]

The error is in the last line:

Ambiguous term
  not_imp
Possible interpretations:
  _root_.not_imp : ¬(?m.2 → ?m.3) ↔ ?m.2 ∧ ¬?m.3

  Classical.not_imp : ¬(?m.2 → ?m.3) ↔ ?m.2 ∧ ¬?m.3

If I am already hiding Classical.not_imp, why is not_imp still ambiguous? In fact, the following works:

open Classical hiding not_imp

example (p q : Prop): ¬ (p → q) ↔ p ∧ ¬ q := by
  rw [not_imp]

Is it impossible to hide Classical.not_imp?

[Ruben Van de Velde]

Where is the _root_ one defined?

[Kevin Cheung]

I'm not sure. But I htink it is in Mathlib.Logic.Basic.

[Ruben Van de Velde]

Probably it's worth asking in #lean4 with the example without mathlib

[Ruben Van de Velde]

It's not exported, is it?

[Robin Arnez]

It is exported in Init.Classical but then mathlib defines it again in the root namespace

[Ruben Van de Velde]

Weird, #check not_imp just works and finds Classical.not_imp

[Ruben Van de Velde]

Probably we can just remove _root_.not_imp?

[Ruben Van de Velde]

Funnily, the export means you can use not_imp without qualification or open, but not _root_.not_imp

[Ruben Van de Velde]

#34625

[Robin Arnez]

Ruben Van de Velde schrieb:

Weird, #check not_imp just works and finds Classical.not_imp

Try #check (not_imp), #check <identifier> has special behavior

[Ruben Van de Velde]

Doesn't seem to change it on my side

[Robin Arnez]

Hmm?

import Mathlib.Logic.Basic

/-- info: Classical.not_imp {a b : Prop} : ¬(a → b) ↔ a ∧ ¬b -/
#guard_msgs in
#check not_imp

/--
error: Ambiguous term
  not_imp
Possible interpretations:
  _root_.not_imp : ¬(?m.1 → ?m.2) ↔ ?m.1 ∧ ¬?m.2
  ⏎
  Classical.not_imp : ¬(?m.1 → ?m.2) ↔ ?m.1 ∧ ¬?m.2
-/
#guard_msgs in
#check (not_imp)

[Ruben Van de Velde]

Huh

[Ruben Van de Velde]

Looks like I was trying in one of the three files that don't import Logic.Basic

[Kevin Cheung]

Ruben Van de Velde said:

#34625

Does this PR make the second example (quoted below) fail?

open Classical hiding not_imp

example (p q : Prop): ¬ (p → q) ↔ p ∧ ¬ q := by
  rw [not_imp]

[Kevin Cheung]

Robin Arnez said:

Try #check (not_imp), #check <identifier> has special behavior

Is there documentation on the difference in behaviour?

[Robin Arnez]

https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=hash-check