## Stream: general

### Topic: Underlying implementation and checking time

#### Li Yao'an (Oct 16 2020 at 06:58):

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 (Oct 16 2020 at 07:01):

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 (Oct 16 2020 at 07:02):

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

#### Mario Carneiro (Oct 16 2020 at 07:07):

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 (Oct 16 2020 at 07:09):

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

#### Mario Carneiro (Oct 16 2020 at 07:11):

It's possible that the kernel is doing the check

#### Mario Carneiro (Oct 16 2020 at 07:12):

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 (Oct 16 2020 at 07:17):

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

#### Mario Carneiro (Oct 16 2020 at 07:24):

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

#### Yury G. Kudryashov (Oct 16 2020 at 07:26):

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

#### Yury G. Kudryashov (Oct 16 2020 at 07:26):

Unfortunately, I have no MWE at hand.

#### Yury G. Kudryashov (Oct 16 2020 at 07:27):

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

#### Yury G. Kudryashov (Oct 16 2020 at 07:28):

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

#### Floris van Doorn (Oct 16 2020 at 19:30):

@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.

Last updated: May 16 2021 at 05:21 UTC