How often is equality of types used in Mathlib?

Stream: general

[James E Hanson]

Roughly speaking, how often is equality of types actually used in Mathlib? I'm thinking about analyzing the use of universes in Mathlib (specifically trying to automatically optimize the consistency strength used by proofs) and I feel like this is going to be important for the approach I'm envisioning.

I know that it's possible to write a script in Lean that searches for this kind of thing, but I'm finding the documentation of the relevant libraries a little sparse.

[Ruben Van de Velde]

Should be (almost?) never

[James E Hanson]

That would be my guess, but is it actually never used even by tactics?

[Mirek Olšák]

What do you mean by "used"? Sometimes, casting is necessary.

[Aaron Liu]

for example rw uses docs#Eq.mpr

[Kyle Miller]

I wouldn't be surprised if congr/convert are responsible for a good number of type equalities.

[Mirek Olšák]

Of course, there are a lot of undecidable questions regarding type equalities, and I would expect mathlib definitions not depending on these undecidable questions.

[Aaron Liu]

equality of types is not evil when it's an equality of indices

[James E Hanson]

Mirek Olšák said:

What do you mean by "used"? Sometimes, casting is necessary.

I mean it in the broad sense of proof terms containing subterms of the form A = B : Prop or p : A = B.

[Mirek Olšák]

Then yes, casting can happen, and be important in dealing with dependent types. Why is it a problem? By the way, I was also thinking of analyzing the universes, @Mario Carneiro did a preliminary analysis of counting that there are at most 5 universes used, and than we were discussing how the analysis could be more careful.

[Kevin Buzzard]

Mirek do you want to remind us of the reason that some reasonable-looking statement about counting ended up using 5 universes? You gave us an explanation at LLL once right?

The reason I mention this is that it demonstrates how controlling universes in lean proofs might be a harder problem than one might initially think (well at least that was my take-home message from your presentation).

[Mirek Olšák]

It had a reasonable core of why like 1 extra universe pops up mathematically, and the remaining 4 were some technical (hard to explain) details.

[Kevin Buzzard]

Right but it might be the case that James would be interested in hearing this. I am very conscious of the fact that you worked out a bunch of stuff, told a room full of people in London and then this information didn't ever get written down (so it's only people like you and Mario that understand these subtleties).

[Kevin Buzzard]

I remember saying to Mario in about 2019 "presumably it's easy to take a Lean proof that ostensibly uses universes and run some analysis on it to verify that it could be translated into a ZFC proof" and Mario's response was something like "this is actually harder than you think" and I never really understood why at the time, but your LLL demo gave me a much clearer idea of how Lean just throws universes around.

[Mirek Olšák]

Sure, let me write here the "reasonable core"

[Kevin Buzzard]

old thread here #Type theory > Theory of Lean with n universes @ 💬 , older thread here #general > Highest universe in mathlib @ 💬

[Mirek Olšák]

• Nat.card is a function that takes a α : Type, and returns a Nat which is the number of the elements in case the given type is finite, or zero if it is infinite. Looks tame, right?
• However, it is defined as a function which first converts α to a Cardinal.{0}, and then compares this with ℵ₀. This already raises eyebrows a little, when you want to think of a Cardinal as an equivalence class on all sets. On the other hand, for analysis purposes, it would be also possible to just think of a Cardinal as a lightweight wrapper around Type, only with redefined = meaning ≃. So basic reasoning about cardinals can be translated into reasoning about types.
• However, when proving some basic facts about Nat.card, it is useful to know Cardinal.nat_lt_aleph0: that when we take a natural number, and convert to a cardinal, the resulting cardinal is smaller than aleph0. In the proof of this obvious fact, we change the goal ↑n < ℵ₀ to succ ↑n ≤ ℵ₀, where the succ is a cardinal successor.
• Why is a cardinal successor well defined? Standard set theory builds it through taking as all the ordinal types inside but that is not the most straightforward way in Lean. In Lean, we know that cardinals form a well-order, so we can take the class of all strictly bigger cardinals, and take the smallest one.
• How do we prove that every class of cardinals has a minimal element? Remember, Lean's cardinals are just types ordered with injective mappings, they are not by definition ordinals like in ZFC. But no problem, you might know a proof why every two sets are comparable: use Zorn's lemma to find a maximal matching between the two sets, and the smaller set is the one that ran out of elements. The same idea can be done as well on a class of cardinals, you take a maximal class-ary matching, and find the set which ran out of elements.
• This math is still inside Type 1, but quite nontrivially outside ZFC.

[Mirek Olšák]

And then the other universe jumps:

• Lean.Data.AC.Variable which is used for some low-level automation in proofs (AC stands for associativity, commutativity) raises the universe level for no essential reason. It stores a datapoint of universe Sort u but itself it is of universe Type u = Sort (u+1). The technical reason is that it cannot be Sort 0 if the input is Sort 0, and the universe level max is not sufficiently flexible.
• Standard recursion uses more universe levels than one would expect. Consider for example a function defined by

def f : Nat → Type
| 0 => Int
| k+1 => (f k) → Prop

it is a little wild but looks definable in ZFC. The analysis would claim it uses up to Type 2 because if you #print f, you see it uses Nat.brecOn, and its first hidden argument is a motive := (fun x ↦ Type) which is of type ℕ → Type 1 which is of type Type 2.

[James E Hanson]

Mirek Olšák said:

• This math is still inside Type 1, but quite nontrivially outside ZFC.

Sure, but nothing in this argument as written needs the cardinality bound of Type and Type 1 to actually be inaccessible cardinals. The same proof would work verbatim if Type happened to be types of cardinality less than $\beth_{\omega}$ and Type 1 happened to be types of cardinality less than $\beth_{\omega+\omega}$, say.

[James E Hanson]

• Say that a 'small cardinal' is an equinumerosity class of elements of $V_{\omega+\omega}$.
• Cantor-Schröder-Bernstein shows that the injection pre-order lifts to a partial order on the small cardinals.
• Cantor's theorem regarding power sets shows that for any small cardinal there is a strictly larger small cardinal.
• You can similarly show that the set of small cardinals is well-ordered by the lift of the injection order, which together with the previous point shows that any small cardinal has a small cardinal successor.

[James E Hanson]

So I guess like I find 'nontrivially outside ZFC' a little bit debatable. It's only outside of ZFC if you're bad at set theory.

[Mario Carneiro]

I think the real question is not whether the theorem is provable (obviously it is), but rather whether the proof itself can be made to fit in ZFC

[Aaron Liu]

so you need to be good at set theory for it to work

[Aaron Liu]

I think that's nontrivial

[Mario Carneiro]

It's all well and good talking about kappa-small whatever, but unless you have a strategy for uniformly and automatically putting that in all the right places in the proof I don't see how you make it work

[Mario Carneiro]

and doing that is roughly what Mirek and I discussed

[James E Hanson]

Mario Carneiro said:

I think the real question is not whether the theorem is provable (obviously it is), but rather whether the proof itself can be made to fit in ZFC

I don't understand. I just sketched how to make that proof fit in ZFC.

[James E Hanson]

Or do you mean 'how to make it automatically fit in ZFC'?

[Mario Carneiro]

if you had to elaborate the proof again with different adjectives then it's a different proof, no?

[Mario Carneiro]

unless you actually mean the first sentence "The same proof would work verbatim if Type happened to be types of cardinality less than $\beth_{\omega}$ and Type 1 happened to be types of cardinality less than $\beth_{\omega+\omega}$, say." in which case I'm not sure what you mean by the bullets

[James E Hanson]

Okay so the actual automatic strategy I'm envisioning is this:

• Examine the relevant types to determine the most fine-grained assignment of universe levels that is compatible with the type checking. (In particular, you also give new universe level variables to types that are normally a fixed level (like Nat).)
• Look at what type formation operations are actually being used for each of those level variables.
• Ideally you'd then find that many of these universes only really need to be closed under some fairly small fragment of the standard type forming operations. (This is the most questionable part.)
• Then use this to convert the proof (in whatever specific language) to one that uses fewer full universes.

[Mario Carneiro]

why do you need the first bullet?

[Mario Carneiro]

otherwise yes I more or less agree on the strategy, and in this case I think you would want an answer which says that the proof ultimately only uses that Type 1 is closed under powerset. Unfortunately I think it will also need to have several dependent pi types in it so you will have to be careful to detect this if you don't want it to be required to be a regular cardinal

[James E Hanson]

Well so set-theoretically, there's kind of two varieties of 'reasonably closed' cardinals. There's regular cardinals and there's strong limit cardinals. Strongly inaccessible cardinals are cardinals that are closed in both senses, but ZFC alone gives you plenty of cardinals that are one or the other.

The idea is that maybe in many specific places you only really need one or the other kind of closure and tying everything to the same $\mathbb{N}$-indexed hierarchy of universes makes those different kinds of requirements interact in a way that artificially requires inaccessible cardinals.

[James E Hanson]

Mario Carneiro said:

otherwise yes I more or less agree on the strategy, and in this case I think you would want an answer which says that the proof ultimately only uses that Type 1 is closed under powerset. Unfortunately I think it will also need to have several dependent pi types in it so you will have to be careful to detect this if you don't want it to be required to be a regular cardinal

What would be an example of one of the dependent pi types that shows up in this proof?

[Mario Carneiro]

the part that Mirek sketched is the main content of the proof, but there is a bunch of bureaucratic nonsense done to get to that point

[Mario Carneiro]

and when it comes to universe level counting the bureaucracy is as impactful if not more so than the "real content"

[James E Hanson]

Right, that makes sense.

What would you say is a minimally complicated proof in Mathlib in which this starts to happen noticeably? I would be interested in trying to look at it in detail.

[Mario Carneiro]

well Mirek's example uses not 1 universe but 5

[Mario Carneiro]

at most one has an interesting origin story

[Mario Carneiro]

the other are facepalm moments

[James E Hanson]

So would you already see this bureaucracy in action in, say, the proof that addition on the natural numbers is commutative?

[Mario Carneiro]

yes, I believe so

[Mario Carneiro]

you could try running the tool on Nat.add_comm

[James E Hanson]

I did. I saw something involving brecOn, which I think was mentioned in one of the previous threads.

[James E Hanson]

One thing I was confused about though before was that in some places you were saying that Mathlib only uses 3 universes and in others 5. I assume these are in different senses of 'use'?

[Mario Carneiro]

mathlib has changed between lean 3 and lean 4

[Mario Carneiro]

the discussion has spanned multiple years

[James E Hanson]

Ah I see.

[James E Hanson]

Is there a better way to look at proof terms in detail than to try to step through something like this?
image.png

[James E Hanson]

Specifically, this is the result of

set_option pp.all true

#reduce (proofs := true) (types := true) Nat.add_comm

[Mario Carneiro]

well you shouldn't reduce it in the first place, just look at the individual declarations

[James E Hanson]

What do you mean by that specifically?

[Mario Carneiro]

#print Nat.add_comm, #print Nat.below etc

[Mario Carneiro]

but without a tool telling you where to look you'll probably get lost anyway

[Mirek Olšák]

By the way, theoretically, I was also asking this question which could help making this "you are not using too large cardinalities" more rigorous. Unfortunatelly, I still don't know the answer, building a model out of somehow bounded functions is still trickier than I thought... #Type theory > Can ZFC model restricted Lean? @ 💬

[Mirek Olšák]

James E Hanson said:

Mirek Olšák said:

• This math is still inside Type 1, but quite nontrivially outside ZFC.

Sure, but nothing in this argument as written needs the cardinality bound of Type and Type 1 to actually be inaccessible cardinals. The same proof would work verbatim if Type happened to be types of cardinality less than $\beth_{\omega}$ and Type 1 happened to be types of cardinality less than $\beth_{\omega+\omega}$, say.

This is a little tricky statement what you mean by "needs the cardinality bound". You got the successor function on cardinals from some magic in Type 1 (or above due to the bureaucracy I mentioned next). If you then take a small set of Cardinal's in Type, and take a successor of each. As long as you don't have a control over how quickly the successor function grows, you have no guarantee that this image stays in Type.

[Mirek Olšák]

My plan would be to for start:

• give up on issues like the Zorn's lemma on class-ary matchings
• try to implement the straightforward interpreting Type as the class of all sets
• track which Type 1 objects are still representable with a ZFC (first order definable) class (Cardinal.{0}, Ordinal.{0}, bundled structures) -- ZFC can handle classes a little, you can quantify over them, separation & replacement uses class functions
• try to reduce terms when we would be getting higher. Often the reason for it is just infrastructure, for example typeclass inference, and ultimately doesn't need higher universes after reduction
• find the first moments where this jumps out of ZFC (my example of Zorn's lemma over class-ary matchings would be one of them)

[James E Hanson]

Mirek Olšák said:

As long as you don't have a control over how quickly the successor function grows,

Successor is bounded by power set. It's very easy to ensure that a set of cardinals is closed under successors.

[James E Hanson]

Mirek Olšák said:

• for example typeclass inference,

Is it easy to explain why typeclass inference introduces universes?

[Mirek Olšák]

James E Hanson said:

Mirek Olšák said:

As long as you don't have a control over how quickly the successor function grows,

Successor is bounded by power set. It's very easy to ensure that a set of cardinals is closed under successors.

You know this. An analysis tool that just looked over some magic with Zorn's lemma over class-ary matchings will not make this deduction.

[Mirek Olšák]

Just to be clear, I am not arguing that math in Lean cannot be done with ZFC, I think almost all of it can (maybe except some niches, for example if someone formalized the consistency in ZFC...) I was trying to explain why checking this automatically is hard.

[Mirek Olšák]

James E Hanson said:

Mirek Olšák said:

• for example typeclass inference,

Is it easy to explain why typeclass inference introduces universes?

First, I need to emphasise that "introduces universes" is not a well defined concept, only a vague idea of "we are somehow using more than ZFC allows". Type theory doesn't match with set theory exactly, in particular has these infinitely many axioms which mimic some second-order functions but not others, so no matter what I write, you could object a bit.

But let me try. Let's say we understand how to model Ordinal.{0} in ZFC. Ordinals are partially ordered, which is realized with the typeclass instance

#check (Ordinal.partialOrder : PartialOrder Ordinal)

A partial order is a structure containing among others

class PartialOrder.{u} (α : Type u) where
  le : α → α → Prop
  lt : α → α → Prop
  ...

So we first use PartialOrder.mk.{1} : (α → α → Prop) → (α → α → Prop) → ... to build such instance,
and then look inside it again with LE.le to interpret what it means when we write o1 < o2 for two ordinals o1, o2. For example the PartialOrder.mk.{1} is not even a class function, it takes class functions as arguments, and wraps them into one object. Mario was suggesting that maybe we could have a type system above ZFC to take care of these but I am not exactly sure what it should be, and it might be easier to just try to reduce (so we can see what happens in practice).

[Mario Carneiro]

I think James is suggesting to take Ordinal.{0} to be the set of ordinals in $\beth_\omega$

[Mirek Olšák]

I don't know exactly which constructions in mathlib escape the $V_{\omega+\omega}$ model, certainly Cardinal.beth.

[Mario Carneiro]

the important one is Cardinal.ord

[Aaron Liu]

inductive types?

[Mirek Olšák]

Also, when I say I believe Lean's math can be done within ZFC, it implies that it can be also done within some $V_{\alpha}$ because then it is done only using finitely many axioms, and finitely many axioms of ZFC fit inside some $V_{\alpha}$. The difficulty is to ensure automatically it is the case.

[Mirek Olšák]

Aaron Liu said:

inductive types?

Sure, forall type too. But I meant the specific examples.

[James E Hanson]

Mirek Olšák said:

I don't know exactly which constructions in mathlib escape the $V_{\omega+\omega}$ model, certainly Cardinal.beth.

In general I'm imagining something a little bit more dynamic than picking cardinal bounds manually, something analogous to how you prove the reflection theorem.

[Mirek Olšák]

Yes, then the only issue is when the function is coming from a higher universe, like the cardinal successor function constructed via Zorn's lemma in Type 1.

[James E Hanson]

Sure but that could live in something like $V_{\omega_1}$.

[Mirek Olšák]

In theory, you could do wild things in the higher universe, for example you could take a natural number $n$, and return the smallest $\alpha$ such that $V_{\alpha}$ is a partial model of ZFC satisfying the first $n$ instances of replacement... You could even construct a wordly cardinal in Type 0.

[James E Hanson]

@Mario Carneiro Do you have a script that can list the definitions of inductive types that are actually used in a theorem? I think I saw something like that in ZFCWithoutInductives.lean.

[James E Hanson]

Mirek Olšák said:

In theory, you could do wild things in the higher universe, for example you could take a natural number $n$, and return the smallest $\alpha$ such that $V_{\alpha}$ is a partial model of ZFC satisfying the first $n$ instances of replacement... You could even construct a wordly cardinal in Type 0.

Sure, I understand that Type 0 is comparable to the category of sets smaller than an inaccessible cardinal and that you can reflect things down from higher Type n's into Type 0, but the question is whether you can tell by inspection that certain proofs really aren't using that much power.

[Mirek Olšák]

Then, the inspection would have to get some understanding of what the Zorn's lemma trick defining successor is doing, otherwise it cannot distinguish it from the "evil" functions such as this one.

[James E Hanson]

Why do you think the Zorn's lemma thing is so difficult specifically?

[James E Hanson]

Also, to be honest, I really wouldn't use the word 'evil' to describe those things.

[Mirek Olšák]

Ok, sorry :slight_smile: , I should write non-ZFC.

[James E Hanson]

Mirek Olšák said:

for example you could take a natural number $n$, and return the smallest $\alpha$ such that $V_{\alpha}$ is a partial model of ZFC satisfying the first $n$ instances of replacement...

But this is a definable function in ZFC. It's just not provably total.

[Mirek Olšák]

My guess is that seeing what the Zorn lemma constructed is a ZFC-definable, or at least ZFC-bounded function is nontrivial unless we actually understand deeply that it is building a successor. But at the same time, I would say it is not a priority for start.

[Mirek Olšák]

For example, I was asking in the other thread if we could guarantee that functions are limited if we rectrict recursion, and disallow unique choice (I would still like to have a definite answer). But that Zorn's lemma thing uses choice to build the outcome...

[James E Hanson]

Global choice is conservative over ZFC though.

[James E Hanson]

(Depending on how you formalize it precisely.)

[Mario Carneiro]

James E Hanson said:

Mario Carneiro Do you have a script that can list the definitions of inductive types that are actually used in a theorem? I think I saw something like that in ZFCWithoutInductives.lean.

https://github.com/leanprover-community/mathlib4/blob/945082d8fc6abb2fb927bc80cce35c44902d442c/Counterexamples/ZFCWithoutInductives.lean#L1192-L1222

[Mirek Olšák]

I mean unique choice, which is a concept that ZFC is not very familiar with -- that any function-like relation can be turned into a function (that can be then used for replacement). ZFC uses function-like relations for replacement directly, but Lean distinguishes functions and function-like relations.

[James E Hanson]

I know what unique choice is.

[James E Hanson]

I'm saying that the class Zorn argument can maybe be done with global choice.

[Mirek Olšák]

Ah, you are answering a different question then, sorry.

[Mirek Olšák]

That might be true actually that the Zorn lemma argument doesn't need unique choice...

[Mirek Olšák]

I think it is not obvious from the argument itself that it is choosing something limited

[Mirek Olšák]

Of course it is obvious in retrospect because the constructions shows that anything with a strictly larger size is bigger or equal than the successor. But it doesn't start with taking something limited, and building the successor below.

[Snir Broshi]

I just found out that docs#cast exists, and is used for equality of types, e.g.
https://github.com/leanprover-community/mathlib4/blob/9739946deb29b3252628071c8ed4072b1ddbfbfb/Mathlib/Topology/MetricSpace/Gluing.lean#L311-L312

[James E Hanson]

I've realized that I should have asked a more specific question, which is 'how often is equality of types used where the two types in question aren't part of a single indexed family of types?'

Casting in this kind of context sometimes seems unavoidable, but on the other extreme, the type Nat = Rat certainly never occurs in Mathlib.

[Aaron Liu]

James E Hanson said:

I've realized that I should have asked a more specific question, which is 'how often is equality of types used where the two types in question aren't part of a single indexed family of types?'

I would hope something like "only when both are Props or one is a free variable or...", since otherwise you can't really do anything with it.