What's the meaning of `_root_` in lean?

Stream: new members

[Michael Novak]

I'm learning about the proof of the Schroeder-Bernstein Theorem from the math in lean textbook and in some part the expression _root_ is used, but there isn't any explanation about it. What exactly does it mean?

[Chris Bailey]

There's an explanation and some examples in the lean reference in section 6.1, for some reason the exact link to the section is broken: https://lean-lang.org/doc/reference/latest/

"There is a root namespace, ordinarily denoted by simply omitting a namespace. It can be explicitly indicated by beginning a name with _root_. This can be necessary in contexts where a name would otherwise be interpreted relative to an ambient namespace (e.g. from a section scope) or local scope."

[Michael Novak]

I'm not sure I fully I understand it exactly. Maybe you could explain me how and why it's used in the proof of injectivity (theorem sb_injective) here: https://leanprover-community.github.io/mathematics_in_lean/C04_Sets_and_Functions.html#the-schroder-bernstein-theorem ?
In particular, why not prove by contradiction using the by_contra tactic instead of these two lines:

apply _root_.not_imp_self.mp
 intro (x₂nA : x₂ ∉ A)

?

[Chris Bailey]

If the Decidable namespace was open for some reason, _root_.not_imp_self is the way to get the root one instead of Decidable.not_imp_self. I don't know that the second part of the question is related, who knows why.

[Michael Novak]

The Classical namespace is open

[Chris Bailey]

I just checked my local copy of MIL, Decidable is indeed open. If you run #print not_imp_self above that theorem you get the decidable version.

[Michael Novak]

are Classical and Decidable the same thing?

[Michael Novak]

In the begging of the file the following lines appear:

open Set
open Function

noncomputable section
open Classical

[Michael Novak]

Anyway, I think I understand it now. Thank you very much!

[Chris Bailey]

It seems Decidable is opened by the prelude these days example

Also the root one is in the root namespace but it's defined in Mathlib.Logic.Basic

[Michael Novak]

what is the prelude?

[Chris Bailey]

The stuff you get without having to ask for it, without having to import anything. Think Nat, List, String.

[Michael Novak]

O.k., I understnad. Thanks!

[Kenny Lau]

Michael Novak said:

are Classical and Decidable the same thing?

they are in fact opposite :upside_down: classical logic assumes p or not p freely, and decidable does not assume it at all and you have to prove every instance constructively (i.e. by feeding a program to decide)

[Michael Novak]

O.k, thanks you! Hopefully I'll learn more in detail about decidability in lean and related ideas. Is it covered in more detail in either MIL, Theorem proving in Lean or Functional programming in Lean? (These are the texts I'm learning from).

[Kenny Lau]

@Michael Novak mathlib as a whole has decided long ago to ignore decidability and use classical because it's mainly about proving theorems in maths and not about computing (but as a result it does have other ways to help computing, the main one being norm_num)