## Stream: general

### Topic: slow proofs

#### Yury G. Kudryashov (Dec 24 2019 at 01:03):

Hi, the following files have largest compile times as counted by running something like for f in $(find . -name *.lean); do time lean -j1 --profile$f; done after leanpkg build:

./src/data/complex/exponential.time!1:01.78
./src/data/polynomial.time!1:57.13
./src/data/real/ennreal.time!1:01.25
./src/group_theory/congruence.time!1:03.07
./src/linear_algebra/basic.time!1:58.68
./src/ring_theory/power_series.time!1:18.62
./src/topology/algebra/infinite_sum.time!1:37.40
./src/category_theory/limits/shapes/binary_products.time!2:04.08
./src/data/multiset.time!2:01.77
./src/analysis/complex/exponential.time!3:50.83


#### Yury G. Kudryashov (Dec 24 2019 at 01:03):

And the longest-running proof is

lemma dist_le_tsum_dist_of_tendsto [metric_space α] {f : ℕ → α}
(h : summable (λn, dist (f n) (f n.succ))) {a : α} (ha : tendsto f at_top (𝓝 a)) (n) :
dist (f n) a ≤ ∑ m, dist (f (n+m)) (f (n+m).succ) :=
dist_le_tsum_of_dist_le_of_tendsto (λ n:ℕ, dist (f n) (f n.succ))
(λ n:ℕ, le_refl (dist (f n) (f n.succ))) h ha n


in infinite_sum.lean.

#### Yury G. Kudryashov (Dec 24 2019 at 01:04):

Any idea what makes it so hard to elaborate this proof?

#### Simon Hudon (Dec 24 2019 at 01:07):

The two things I can think of are 1. how long is the path to the type class instances that it needs (and the number of candidates being considered) 2. and the amount of definition unfolding required to check that functions are applied to arguments of the right type.

#### Yury G. Kudryashov (Dec 24 2019 at 01:09):

lemma dist_le_tsum_of_dist_le_of_tendsto [metric_space α] {f : ℕ → α} (d : ℕ → ℝ)
(hf : ∀ n, dist (f n) (f n.succ) ≤ d n) (hd : summable d) {a : α} (ha : tendsto f at_top (𝓝 a))
(n : ℕ) :
dist (f n) a ≤ ∑ m, d (n + m) :=
_


#### Yury G. Kudryashov (Dec 24 2019 at 01:11):

Is it possible to trace unfolding of definitions?

#### Yury G. Kudryashov (Dec 24 2019 at 01:11):

I don't see any definitions to unfold here.

#### Joe (Dec 24 2019 at 01:14):

lemma dist_le_tsum_dist_of_tendsto [metric_space α] {f : ℕ → α}
(h : summable (λn, dist (f n) (f n.succ))) {a : α} (ha : tendsto f at_top (𝓝 a)) (n) :
dist (f n) a ≤ ∑ m, dist (f (n+m)) (f (n+m).succ) :=
show dist (f n) a ≤ ∑ m, (λx, dist (f x) (f x.succ)) (n + m), from
dist_le_tsum_of_dist_le_of_tendsto (λ n, dist (f n) (f n.succ)) (λ _, le_refl _) h ha n


#### Joe (Dec 24 2019 at 01:14):

I think this should fix it.

#### Joe (Dec 24 2019 at 01:15):

Lean cannot find the function d in dist_le_tsum_of_dist_le_of_tendsto

Thanks @Joe!

No problem.

#### Yury G. Kudryashov (Dec 24 2019 at 03:13):

Is there any way to understand which tactic in a long begin...end block slows down the elaboration?

#### Jesse Michael Han (Dec 24 2019 at 04:02):

try enabling the profiler

#### Yury G. Kudryashov (Dec 24 2019 at 04:06):

lean --profile --json reports ... took ... s once for each begin ... end block.

#### Yury G. Kudryashov (Dec 24 2019 at 04:06):

Or maybe more than once but each time it points to the position of end.

#### Simon Hudon (Dec 24 2019 at 04:08):

It might be more convenient if you use set_option profiler to turn it on

Last updated: May 14 2021 at 22:15 UTC