slow proofs

Stream: general

[Yury G. Kudryashov]

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]

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]

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

[Simon Hudon]

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]

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]

Is it possible to trace unfolding of definitions?

[Yury G. Kudryashov]

I don't see any definitions to unfold here.

[Joe]

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]

I think this should fix it.

[Joe]

Lean cannot find the function d in dist_le_tsum_of_dist_le_of_tendsto

[Yury G. Kudryashov]

Thanks @Joe!

[Joe]

No problem.

[Yury G. Kudryashov]

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

[Jesse Michael Han]

try enabling the profiler

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Simon Hudon]

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