Fully qualified identifiers, and possible "aliases"?

Stream: new members

[Isak Colboubrani]

If I can successfully run #check <name> or #print <name>, does that mean <name> is the unique, fully qualified identifier for that theorem/declaration?

Consider the examples below (Polynomial.X_pow_sub_C_ne_zero and mul_assoc):

Once I’ve verified that #check Polynomial.X_pow_sub_C_ne_zero and #print Polynomial.X_pow_sub_C_ne_zero works, can I be sure there are no other aliases or shorter names for that same theorem (unless, of course, the theorem has been duplicated under a different name)?

Is Polynomial.X_pow_sub_C_ne_zero itself the fully qualified name—independent of its location (Mathlib.Algebra.Polynomial.Degree.Operations)?

And how does this apply to more "global" declarations like mul_assoc? What is the fully qualified name for mul_assoc?

#mwe:

import Mathlib

#print Polynomial.X_pow_sub_C_ne_zero
#check Polynomial.X_pow_sub_C_ne_zero
-- import Mathlib.Algebra.Polynomial.Degree.Operations"

#print mul_assoc
#check mul_assoc
-- import Mathlib.Algebra.Group.Defs"

[Kyle Miller]

Isak Colboubrani said:

If I can successfully run #check <name> or #print <name>, does that mean <name> is the unique, fully qualified identifier for that theorem/declaration?

No, that is not the case.

1. You might have open commands that make it possible to refer to a declaration by a shorter name.
2. There might be aliases, created using the export command.

Simple counterexample:

#check toString

open Nat
#check succ

[Kyle Miller]

Both #check <name> and #print <name> will also succeed even if <name> is ambiguous. They print all interpretations.

[Kyle Miller]

I believe both #check and #print will print the fully-qualified names.

You can always hover over the declaration name to be sure. I think that gives the fully qualified name.

[Kyle Miller]

Isak Colboubrani said:

What is the fully qualified name for mul_assoc?

mul_assoc

[Isak Colboubrani]

Thanks @Kyle Miller!

Great point about open—I hadn’t considered that, but it makes perfect sense.

So generally, to find a declaration’s fully qualified name, can I just take the first identifier in the #check <name> output and ignore the trailing universe annotation (.{u})?

In this example, I would treat Polynomial.X_pow_sub_C_ne_zero as the fully qualified name:

import Mathlib
open Polynomial
#check X_pow_sub_C_ne_zero
-- Polynomial.X_pow_sub_C_ne_zero.{u} {R : Type u} [Ring R]
#check Polynomial.X_pow_sub_C_ne_zero
-- Polynomial.X_pow_sub_C_ne_zero.{u} {R : Type u} [Ring R]

Also, what do the these 32 universe-specific variants mean?

import Mathlib
#check Polynomial.X_pow_sub_C_ne_zero.{0}
-- X_pow_sub_C_ne_zero : 0 < ?m.4 → ∀ (a : ?m.1), X ^ ?m.4 - C a ≠ 0
#check Polynomial.X_pow_sub_C_ne_zero.{1}
-- X_pow_sub_C_ne_zero : 0 < ?m.1973 → ∀ (a : ?m.1970), X ^ ?m.1973 - C a ≠ 0
#check Polynomial.X_pow_sub_C_ne_zero.{2}
-- X_pow_sub_C_ne_zero : 0 < ?m.3942 → ∀ (a : ?m.3939), X ^ ?m.3942 - C a ≠ 0
#check Polynomial.X_pow_sub_C_ne_zero.{32}
-- X_pow_sub_C_ne_zero : 0 < ?m.5911 → ∀ (a : ?m.5908), X ^ ?m.5911 - C a ≠ 0

I naïvely assumed one of them would simply display the same output as for #check Polynomial.X_pow_sub_C_ne_zero, but they all seem to contain ?m.xxx placeholders. What’s happening here?

[Kyle Miller]

can I just take the first identifier in the #check <name> output

Kyle Miller said:

I believe both #check and #print will print the fully-qualified names.

Emphasis here on "believe". To be sure, you'll have to dig into the source code yourself.

[Kyle Miller]

Also, what do the these 32 universe-specific variants mean?

I am puzzled by your motivation here. Do you expect the different instantiations of the universe parameters to be fundamentally different from one another?

In any case, take a look at the source for #check. You'll see why there's different behavior when you give it something that's not an identifier.

[Isak Colboubrani]

Kyle Miller said:

Also, what do the these 32 universe-specific variants mean?

I am puzzled by your motivation here. Do you expect the different instantiations of the universe parameters to be fundamentally different from one another?

Quite the opposite—I assumed they were exactly the same, so I naïvely expected identical output for #check Polynomial.X_pow_sub_C_ne_zero and #check Polynomial.X_pow_sub_C_ne_zero.{n} for any $n \in \{0, 1, …, 31, 32\}$. (And if that wasn't the case I expected at least one of them to have exactly the same output as #check Polynomial.X_pow_sub_C_ne_zero: namely the one at the declaration’s original, lowest universe level.)

(I'm a beginner here, but the expectation above comes from the following: my simple mental mode that each universe embeds into the next—everything in universe 0 also lives in universe 1, everything in universe 1 in universe 2, and so on up to universe 32. As far as I understand, Polynomial.X_pow_sub_C_ne_zero is a Prop and thus has it "home" in universe 0 (but can be found in universe 1-32 too!).)

[Kyle Miller]

Given your questions about exact implementations of tactics, I strongly recommend you investigate the implementation of #check.

[Kyle Miller]

and so on up to universe 32

There are infinitely many universe levels. Passing 32 simply triggers the "you probably don't mean this" error.

[Aaron Liu]

You can pass 31 + n to exceed it (for concrete n)

[Kyle Miller]

Isak Colboubrani said:

As far as I understand, Polynomial.X_pow_sub_C_ne_zero is a Prop and thus has it "home" in universe 0 (but can be found in universe 1-32 too!)

I'm not sure that's the right interpretation. Yes, this theorem has a type that is in Prop (a.k.a. Sort 0), but the domains of the foralls are types, and the theorem is parameterized so that those domains can come from various universe levels.

The Prop universe is "impredicative". The effect of impredicativity is that, despite the fact that the domains can lie in larger universes, the type is regardless still in Prop.

[Kyle Miller]

(You give me a :+1: @Aaron Liu, but there's a subtlety that I'm not sure about. I don't know if there are versions of type theory where the way impredicativity works is that the type is "actually" in the higher universe, but then there is a corresponding Prop that means "the type in that higher universe is inhabited." At least from within Lean's system it's "no, Polynomial.X_pow_sub_C_ne_zero is not found in any higher universes, it is only in Prop".)

[Aaron Liu]

Kyle Miller said:

(You give me a :+1: Aaron Liu, but there's a subtlety that I'm not sure about. I don't know if there are versions of type theory where the way impredicativity works is that the type is "actually" in the higher universe, but then there is a corresponding Prop that means "the type in that higher universe is inhabited." At least from within Lean's system it's "no, Polynomial.X_pow_sub_C_ne_zero is not found in any higher universes, it is only in Prop".)

What do you by "corresponding"? Is that a function?

[Isak Colboubrani]

Thanks, that’s really helpful—TIL!

I’m left wondering why Lean displays the fully elaborated signature for #check mul_assoc, but shows a ?m.1 placeholder when I force it to universe 0 by doing #check mul_assoc.{0}. Is that due to what you mentioned about the theorem being parameterized?

Is it that at level 0 Lean can no longer infer the parameters (G : Type u₁, [Semigroup G], etc.) when printing?

More specifically, I’m wondering whether this is merely a practical implementation choice, or if Lean "doesn’t have" the required information to print that at universe level 0 (from a theoretical perspective).

import Mathlib

#check mul_assoc
-- mul_assoc.{u_1} {G : Type u_1} [Semigroup G] (a b c : G) : a * b * c = a * (b * c)

#check mul_assoc.{0}
-- mul_assoc : ∀ (a b c : ?m.1), a * b * c = a * (b * c)

[Aaron Liu]

#check has special support for identifiers vs terms

[Aaron Liu]

So since mul_assoc is an identifier, it gets the special treatment. You can see what happens when you do #check (mul_assoc) is different.

[Isak Colboubrani]

Aaron Liu said:

You can pass 31 + n to exceed it (for concrete n)

Heh, nice trick @Aaron Liu! It seems to work for $n \le 32$, but the process can be repeated to reach arbitrarily high:

#check mul_assoc.{32+33}
-- fails: maximum universe level offset threshold (32) has been reached, …
#check mul_assoc.{32+32}
-- works
#check mul_assoc.{32+32+32+32+32+32+32+32+32+32}
-- works

[Edward van de Meent]

perhaps the following is to your satisfaction:

import Mathlib

#check mul_assoc
-- mul_assoc.{u_1} {G : Type u_1} [Semigroup G] (a b c : G) : a * b * c = a * (b * c)

#check (mul_assoc)
-- mul_assoc : ∀ (a b c : ?m.2), a * b * c = a * (b * c)

#check mul_assoc.{0}
-- mul_assoc : ∀ (a b c : ?m.288), a * b * c = a * (b * c)

[Aaron Liu]

Isak Colboubrani said:

Heh, nice trick Aaron Liu!

Of course you can also set_option maxUniverseOffset 999 and get up to 999 offsets.

[Edward van de Meent]

which is to say, there's nothing special about universe levels here, it's just that once you provide specific terms, the #check command needs to employ a different algorithm for displaying the type

[Kyle Miller]

Isak Colboubrani said:

I’m left wondering why Lean displays the fully elaborated signature for #check

I see you didn't follow up on my strong suggestion. Please read it — if there is anything you don't understand, please ask followup questions.

[Kyle Miller]

It's all a "go to definition" away