Largest binder depth in mathlib

Stream: general

[Mario Carneiro]

I got curious about this question because metamath has a soft limit on the number of simultaneous bound variables because it uses letters of the alphabet and there are only 26 of those (notwithstanding some extensions to add primes in some user mathboxes). MM0 also has a variable limit of 55 with the current verifier design (because this bit-packs nicely), although there is an extension point in case more are needed in the future. (Technically, both metamath and MM0 support more variables than this but these are for "true" variables, that can appear in binders, rather than "local constants" which are fixed through the proof.)

Lean is a bit more binder-hungry than metamath because it uses binders for have, for example - is there some huge proof out there with 50+ variables?

Here's a metaprogram to find out:

#eval do
  env ← tactic.get_env,
  (env.fold (pure (`nat, 0)) $ λ d r, do
    (n, m) ← r,
    let m2 := d.value.fold 0 (λ _, max),
    pure $ if m2 > m then
      (d.to_name, m2) else
      (n, m)) >>= tactic.trace

What would you guess?

Results

On core lean, it outputs (widget.widget.component._mut_.with_state_0.inj_eq, 54). That means that there is a point somewhere in widget.widget.component._mut_.with_state_0.inj_eq that is under 54 nested binders (this is not counting all binders in the proof term, only the ones that all have to exist in the same context).

If you run this on mathlib, you get (linear_ordered_field.no_confusion_type, 134). I'm kind of surprised that it's not some big manual proof with a lot of haves like I predicted - instead it is just the crazy unpacking involved in docs#linear_ordered_field (which is an old_structure with 55 fields), and then doubled tripled because no_confusion_type needs to talk about two values of type linear_ordered_field unpacked into their components. (There is a third binder per field in no_confusion_type because it has an equality for each pair of fields that were unpacked.)