Underlying implementation and checking time

Stream: general

[Li Yao'an]

This is more of a curiosity than a practical concern.

Real numbers in Lean are constructed in some way to satisfy some axioms we desire about real numbers. I imagine the reals could be a quotient on sequences of rational numbers, which is a quotient on un-reduced fractions, which is constructed from two natural numbers.

I'm wondering if this complexity affects proof checking times, with the potential to blow up if we add a few more layers to it.

As an experiment, I wrote the following:

def Aut (α : Type) : Type := α → α
def Aut10 (α : Type) := Aut(Aut(Aut(Aut(Aut(Aut(Aut(Aut(Aut(Aut(α))))))))))
def constfn {α : Type} (a : α) : α → α := λ x, a

attribute [irreducible] def Aut20N := Aut10(Aut10(ℕ))

def Aut20N_constfn (a) := @constfn Aut20N a -- deterministic timeout

It looks like Lean times out because it needs to expand the type of Aut20N. Would this potentially be a practical issue with more complex mathematics?

[Mario Carneiro]

Yes, this can happen sometimes. Basically, we treat unfolding itself as an operation, and a proof should avoid doing too much of it

[Mario Carneiro]

by that logic Aut20N_constfn is a "large" proof, because it requires a lot of unfolding to typecheck

[Mario Carneiro]

That said, once you have put in the type ascriptions (or even before), there should not be a problem with your proof. But Aut20N is a "time bomb" in a sense because calling whnf on it causes a blowup, and many parts of lean are not as careful as they should be about this

def Aut (α : Type) : Type := α → α
def constfn {α : Type} (a : α) : α → α := λ x, a
attribute [irreducible] def Aut20N : Type := Aut^[20] ℕ

def Aut20N_constfn (a : Aut20N) : Aut20N → Aut20N :=
constfn a -- deterministic timeout

[Johan Commelin]

I'm confused. I thought that the attribute [irreducible] would prevent this...

[Mario Carneiro]

It's possible that the kernel is doing the check

[Mario Carneiro]

This actually comes up less than you would think, because usually when you introduce a new definition you replace the top level connective. The bad case is when it is a lot of work just to find out what the top level connective is

[Yury G. Kudryashov]

Is the fact that Lean sometimes fails to apply a lemma about λ _, a to (0 : α → β) somehow related to this?

[Mario Carneiro]

You mean even if you explicitly apply the lemma with refine?

[Yury G. Kudryashov]

I mean if I do a term mode proof, and use, e.g., measurable_const to prove measurable 0.

[Yury G. Kudryashov]

Unfortunately, I have no MWE at hand.

[Yury G. Kudryashov]

See, e.g., this for a non-minimal example.

[Yury G. Kudryashov]

Here it's about unifying continuous_const with coercion of 0 : linear_map _ _ _.

[Floris van Doorn]

@Yury G. Kudryashov I'm not sure if it's the same issue, but in your linked example @continuous_const _ _ _ _ (0 : F) works without convert.