# Zulip Chat Archive

## 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: Aug 03 2023 at 10:10 UTC