Why my IDE is getting slow during this proof?

Stream: new members

[Hyunwoo Lee]

I try to prove some lemma in ODE theory. It's bit complicated but proof is not that long(~60 lines)

However, while proof state looks quite small, it takes 5~10 seconds to update infoview for every tactic and I can't keep writing more. It takes 5 seconds even when just adding new line in existing proof.

Because I fail to generate minimal reproducing example, I attach the whole problematic proof.

import Mathlib

section local_flow

lemma closedBall_in_openSet
  {T : Type} [MetricSpace T] {S : Set T} (hS : IsOpen S) {s : T} (hs : s ∈ S) :
    ∃ r >0, Metric.closedBall s r ⊆ S := by
    have ⟨ball, hunif ,hball⟩ := isOpen_iff_ball_subset.mp hS s hs
    obtain ⟨ε, hεpos, hεsubset⟩ := Metric.mem_uniformity_dist.mp hunif
    have hBU : Metric.ball s ε ⊆ UniformSpace.ball s ball := by {
      intros t ht
      apply hεsubset;rw [dist_comm];apply ht
    }
    have hball : Metric.ball s ε ⊆ S := by {
      apply subset_trans
      · apply hBU
      · apply hball
    }
    exists ε/2;constructor
    · aesop
    apply subset_trans (b:= Metric.ball s ε)
    · apply Metric.closedBall_subset_ball;linarith
    · aesop

def local_uniform_lipschitz_vector_field (T : Set ℝ) {X : Type} [MetricSpace X]
(S : Set X) (f : ℝ -> X -> X) (s : X) (t₀ : ℝ) : Prop :=
∃ (r_t r_s : NNReal), ∃ K,
  (Metric.closedBall t₀ r_t ⊆ T) ∧
  (Metric.closedBall s r_s ⊆ S) ∧
  ∀t ∈ (Metric.closedBall t₀ r_t), LipschitzOnWith K (f t) (Metric.closedBall s r_s)

lemma weak_PL_implies_IsPL
  {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
  [LocallyCompactSpace E] [SigmaCompactSpace E]
  {S : Set E} {tmin tmax : ℝ}
  (t₀ : Set.Icc tmin tmax) (hS : IsOpen S) (F : ℝ -> E -> E)
  (time_continity : ∀ s ∈ S, ContinuousOn (fun t => F t s) (Set.Icc tmin tmax))
  (locally_lipschitz : ∀ s ∈ S, local_uniform_lipschitz_vector_field (Set.Icc tmin tmax) S F s t₀)
  :∀s ∈ S, ∃(tm tM : ℝ), ∃(tt : Set.Icc tm tM), ∃ a r L K, IsPicardLindelof F tt s a r L K := by {
    intro s hs
    -- Because S is Open, we can find closed ball (cball s a) in S
    have ⟨a,ha,hcball⟩  := closedBall_in_openSet hS hs
    obtain ⟨r_t, r_s , K, ht,hr,hlip⟩  := locally_lipschitz s hs

    -- Because fun t => F t s is continuos for s and
    -- closed interval is compact, there's maximum L by exterm value thm
    obtain ⟨ M, F_Bounded ⟩: ∃ L, ∀t ∈ (Set.Icc tmin tmax),  ‖F t s‖ ≤ L := by sorry

    set L := Max.max (K * a + M) 0
    obtain L_pos : 0 ≤ L := by aesop

    exists (t₀ - (r_t : ℝ))
    exists (t₀ + (r_t : ℝ))
    set tt : ℝ := (t₀ : ℝ)
    obtain htmp : tt ∈ Set.Icc (t₀ - (r_t : ℝ)) (t₀ + (r_t : ℝ)) := by aesop
    exists ⟨tt,htmp⟩

    exists r_s, r_t, ⟨L,L_pos⟩, K
    constructor
    {
      intros _t _ht;apply hlip
      simp only [Metric.mem_closedBall, Real.dist_eq, abs_le];simp at _ht
      constructor;(all_goals linarith)
    }
    {
      intros x hx
      obtain H : x ∈ S := by aesop
      sorry
    }
    {
      sorry
    }
    {
      sorry
    }
  }

end local_flow

In the above example, when I try to replace sorry by some tactics, it takes unusual delay to update infoview on the right.

It seems that the part after constructor is the reason. When I quote the constructor part and replace it with sorry, there's no speed issue.

Could you give me an advice if it's possible to avoid such problem? I expect Lean can support this kinds of proof and there must be my mistake in using Lean. Also, please point out if there's problem in my code.

Thank you in advance.

+)
My environement

OS : Ubutnu 24.04.1
IDE : Visual Studio Code 1.104.2
Lean4 version : v4.23.0-rc2
Mathlib4 : Latest

[Michael Rothgang]

Can you provide an #mwe? (Clicking on the link will tell you what this is.)

[Hyunwoo Lee]

I really want to. But as I mentioned, I cannot even guess what's the problem and fail to reproduce such phenomenon in the simpler one. If it's not a common problem, I will try to make a lot of experiment as I can and share the result later. I hope I can find minimal example.

[Michael Rothgang]

Sure. But right now, your code does not compile: what imports do you have?

[Michael Rothgang]

You can certainly tell us those, right?

[Hyunwoo Lee]

@Michael Rothgang Oh I see. Sorry. I change the the code in my original question. Hope it works

[Michael Rothgang]

Yes, now I open your code in the playground. I don't see any "obviously slow" parts, but can offer a few tweaks:

[Michael Rothgang]

• style: put spaces after comma and around colons; no superfluous spaces before parens. hypotheses by four spaces, but the proof by two.
• your proof that L is positive can just be by positivity (and you can even inline this, as L is used only once)
• I believe use is more common in mathlib, and you can combined subsequent use lines

With all these applies, the code looks like so

import Mathlib

set_option profiler true

section local_flow

lemma closedBall_in_openSet
  {T : Type} [MetricSpace T] {S : Set T} (hS : IsOpen S) {s : T} (hs : s ∈ S) :
    ∃ r >0, Metric.closedBall s r ⊆ S := by
    have ⟨ball, hunif ,hball⟩ := isOpen_iff_ball_subset.mp hS s hs
    obtain ⟨ε, hεpos, hεsubset⟩ := Metric.mem_uniformity_dist.mp hunif
    have hBU : Metric.ball s ε ⊆ UniformSpace.ball s ball := by {
      intros t ht
      apply hεsubset;rw [dist_comm];apply ht
    }
    have hball : Metric.ball s ε ⊆ S := by {
      apply subset_trans
      · apply hBU
      · apply hball
    }
    exists ε/2;constructor
    · aesop
    apply subset_trans (b:= Metric.ball s ε)
    · apply Metric.closedBall_subset_ball;linarith
    · aesop

def local_uniform_lipschitz_vector_field (T : Set ℝ) {X : Type} [MetricSpace X]
(S : Set X) (f : ℝ -> X -> X) (s : X) (t₀ : ℝ) : Prop :=
∃ (r_t r_s : NNReal), ∃ K,
  (Metric.closedBall t₀ r_t ⊆ T) ∧
  (Metric.closedBall s r_s ⊆ S) ∧
  ∀t ∈ (Metric.closedBall t₀ r_t), LipschitzOnWith K (f t) (Metric.closedBall s r_s)

set_option profiler.threshold 50

lemma weak_PL_implies_IsPL
    {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    [LocallyCompactSpace E] [SigmaCompactSpace E]
    {S : Set E} {tmin tmax : ℝ}
    (t₀ : Set.Icc tmin tmax) (hS : IsOpen S) (F : ℝ -> E -> E)
    (time_continity : ∀ s ∈ S, ContinuousOn (fun t => F t s) (Set.Icc tmin tmax))
    (locally_lipschitz : ∀ s ∈ S, local_uniform_lipschitz_vector_field (Set.Icc tmin tmax) S F s t₀) :
    ∀s ∈ S, ∃(tm tM : ℝ), ∃(tt : Set.Icc tm tM), ∃ a r L K, IsPicardLindelof F tt s a r L K := by {
  intro s hs
  -- Because S is open, we can find closed ball (cball s a) in S
  have ⟨a, ha, hcball⟩ := closedBall_in_openSet hS hs
  obtain ⟨r_t, r_s , K, ht, hr, hlip⟩  := locally_lipschitz s hs

  -- Because fun t => F t s is continuos for s and
  -- closed interval is compact, there's maximum L by exterm value thm
  obtain ⟨M, F_Bounded⟩ : ∃ L, ∀t ∈ (Set.Icc tmin tmax),  ‖F t s‖ ≤ L := by sorry
  use (t₀ - (r_t : ℝ)), (t₀ + (r_t : ℝ))
  set tt : ℝ := (t₀ : ℝ)
  obtain htmp : tt ∈ Set.Icc (t₀ - (r_t : ℝ)) (t₀ + (r_t : ℝ)) := by sorry--aesop
  use ⟨tt, htmp⟩, r_s, r_t, ⟨max (K * a + M) 0, by positivity⟩, K
  constructor
  {
    intros _t _ht;apply hlip
    simp only [Metric.mem_closedBall, Real.dist_eq, abs_le];simp at _ht
    constructor;(all_goals linarith)
  }
  {
    intros x hx
    obtain H : x ∈ S := by sorry--aesop
    sorry
  }
  {
    sorry
  }
  {
    sorry
  }
  }

end local_flow

[Michael Rothgang]

Now, your design of having t₀ be in a subtype of the real numbers (as opposed to a real number with a proof that it lies in the interval) certainly strikes me as slightly unusual. This could cause slowness (related to casting), but I also suspect that this might not be the nicest to work with. Have you tried it as just a real number?

[Hyunwoo Lee]

Wow, only with your simple change, it's getting significantly faster. Thank you so much!

You are right, using real number with additional constraint looks much more reasonable way. Even if it's not a reason of slowness, it makes proof dirty.

Thank you for the nice advice. I will compare the change and tell you if I find specific reason of slowness :)

[Michael Rothgang]

Perhaps the aesop was a bit slow. (In general, if there's a simpler tactic, that might also be faster.)

[Hyunwoo Lee]

After few experiment, I make a hypothesis as followings.

1. Whenever I write the tactic, Lean LSP run(?) the proof all over again.
2. If there exist several slow tactics, such as aesop, then every aesop run again every time I write the single tactic.
3. Even though single aesop takes managable time, run every aesop and find appropriate term for each hole every time the proof state is changed makes huge, intolerable delay.
4. So I need to avoid using aesop in the big proof, and separate the part using aesop to other lemma.

Does it make sense?

[Marc Huisinga]

Generally, Lean attempts to process proofs incrementally, so that only parts of the proof after the line you changed need to be re-processed. When querying the goal state, it can then provide it before the whole proof has finished. For example, in the following proof, you can see the proof states around intro before the sleep has completed, and the orange bars show that only the sleep is being processed:

example : True → True := by
  intro h
  sleep 5000

However, this incrementality is not yet supported for all tactic combinators and syntaxes, and it looks like it doesn't work for tactic blocks wrapped in { }:

example : True → True := by {
  intro h -- No goal state until `sleep` has completed
  sleep 5000
}

In your original proof, simply removing the curly brackets for the by will make your proof process incrementally, and you don't have to wait for the aesop further down in the file to see your goal state.

cc @Sebastian Ullrich

[Michael Rothgang]

Oh, I didn't know { } broke incrementality. That's useful information, thank you!

[Michael Rothgang]

Is that a mere oversight/easy to fix, or will this not happen in the foreseeable future?

[Michael Rothgang]

Surrounding proofs by curly brackets is useful for teaching: you get a clear error in all cases when a proof is not yet complete; currently, due to lean4#3555 you get a very confusing error if you have an empty tactic sequence.
I have taught myself to always start a proof with sorry, but that's just one more papercut that seems superfluous.

[Sebastian Ullrich]

I think lean#3555 getting fixed is more likely to happen near term

[Michael Rothgang]

To comment on the original message: splitting a large proof into independent pieces is good practice anyway - independently whether it makes your IDE respond faster.