what is LT in `LT.lt.not_lt`?

Stream: new members

[rzeta0]

What does the LT in LT.lt.not_lt mean?

I read this as a namespace similar to the Nat namespace under which several lemmas related to natural numbers reside.

What namespace is LT?

[Junyan Xu]

It's a notation typeclass, in particular a structure.
docs#LT.lt is a projection of the structure.

[Niels Voss]

It is a namespace, as you guessed, but it was automatically generated when the typeclass LT was defined. So LT is both a namespace and a typeclass. (Technically, namespaces aren't "generated", since they are basically just a prefix for an identifier, but in any case the lt was automatically added to the LT namespace)

[rzeta0]

What's a type class?

Is it things like LinearOrdered ? If so, what properties define an object in the type class LT ?

This is far outside my comfort zone so feel free to tell me to ignore this question for now.

The reason I pursued it is because the naming convention for lemmas isn't as intuitive or predicable as I had hoped.

[Niels Voss]

Type classes are a bit of a complicated subject. Semi-formally, a typeclass is a structure or inductive type that is allowed to appear in [] brackets as arguments to a def,lemma,theorem,etc. and is allowed to appear as the type of an instance definition. Don't worry if that didn't make sense right now.

Typeclasses basically serve the same role as interfaces from Java and C#, or traits in Rust. You can read about them in #tpil

For your specific problem, basically note that mathematicians didn't want to have to reprove the same theorem for Nat and Int and Real if the theorem only used the < symbol. So the same theorem in Mathlib might work for Nat and some other types. So instead of Nat.le_trans, the theorem might just be named le_trans.

[Kyle Miller]

docs#LT shows that it is a type with an lt function.

docs#LinearOrder shows that not only does it have lt, but 15 other fields as well.

[Kyle Miller]

(Fun fact @Niels Voss, namespaces actually do have some reality, and an LT namespace is created at some point. I think Lean keeps track of namespaces for resolving names and giving completions. docs#Lean.Environment.registerNamespace)

[Niels Voss]

Oh that's interesting, I didn't know that. This is usually not relevant to the end-user though, right?

[Kyle Miller]

I think it's pretty much just an optimization, so that Lean can consult a list of all the namespaces without needing to traverse the complete set of all declarations to compute it.

[Jireh Loreaux]

rzeta0 said:

The reason I pursued it is because the naming convention for lemmas isn't as intuitive or predicable as I had hoped.

@rzeta0 please note: the name of this lemma is special. It is not meant to be as natural as you might expect, it's explicitly useful for dot notation. In particular, if you have h : a < b, then you can write h.not_lt for a proof of ¬ b < a.

In fact, if you look at docs#LT.lt.not_lt, you'll see that this is an alias for the lemma with the proper name: docs#lt_asymm.

[Jireh Loreaux]

There's also docs#not_lt_of_lt, which is yet another alias of lt_asymm.

[Johan Commelin]

@rzeta0 Maybe the following also helps to explain the name.

variable (a b : Nat)

#check a < b -- a < b : Prop

set_option pp.notation false

#check a < b -- LT.lt a b : Prop

So a < b doesn't really fit into the low-level way that Lean thinks about the world: functions applied to other things by juxtaposition, like f x.
It does fit into a higher-level way that Lean understands, by using a notation system that allows infix operators. So at some point a < b was introduced as notation for LT.lt a b, and the latter is an ordinary function application again.

So if you have h : a < b, then under the hood that means h : LT.lt a b. And therefore you can use dot-notation:

• lemmas with names of the form LT.lt.foobar
• that take an argument (hyp : x < y)
• can be can be called as `h.foobar
• and will have h passed as the argument hyp.

Just like if you have

def Nat.factorial (n : Nat) : Nat := sorry

Whenever you have a k : Nat floating around, you can call k.factorial. Because Lean will inspect the type of k, and find that it is Nat. So then it looks for Nat.factorial, and passes k as the first argument of type Nat.

If you write h.not_lt then Lean inspects the type of h, finds that it has type LT.lt a b, and therefore looks for a lemma called LT.lt.not_lt. Then passes h as the first argument of type LT.lt _ _ to that lemma.

[Mario Carneiro]

Kyle Miller said:

I think it's pretty much just an optimization, so that Lean can consult a list of all the namespaces without needing to traverse the complete set of all declarations to compute it.

not just an optimization, it impacts how open resolves, as well as whether it will error

[Mario Carneiro]

def bar.X := 1

namespace A

section
open foo -- unknown namespace 'foo'
open bar -- resolves to _root_.bar
#check X -- ok
end

namespace foo  end foo
namespace bar  end bar

section
open foo -- ok
open bar -- resolves to A.bar
#check X -- fail
end