Tips for writing nicer code

Stream: mathlib4

[Gareth Ma]

I proved this thing here. It's just simplifying some asymptotic expressions $\sqrt{\frac{\log N}{\log(c + o(1))}} = (1 + o(1)\sqrt{\frac{\log N}{\log c}}$. As you can see, the proof is a bit weird and quite unlike Mathlib proofs, as it is very "linear". It's basically a calc proof but with have : (replace) instead. Is that okay, or is there a better way to write this?

[Kim Morrison]

4 lemmas, and then a 4 lines proof!

[Gareth Ma]

... true. Thanks...

[Kim Morrison]

It's not always possible to separate a long proof into smaller pieces. But usually it is, and the effort is usually worth it. I wish Mathlib did a lot more of this!

[Johan Commelin]

Scott Morrison Are you thinking of specific examples? Mathlib already encourages that style and does it quite a lot, no?

[Kim Morrison]

Yes, sorry, my message maybe misrepresented things. It's a lot better than it used to be.

One example that comes to mind is one of my own, at src#colimitLimitToLimitColimit_surjective

[Kim Morrison]

Surely that could be broken into smaller lemmas.

[Kim Morrison]

That example is also an interesting one because the number of heartbeats used is wildly nondeterministic. :-(

[Damiano Testa]

Surely the solution is a linter that throws and error when a proof spans more than 8 lines. :lol:

[Kevin Buzzard]

We already have the Gouezel linter (one of my favourite linters), which ensures that proofs which are longer than about 25 lines get commented. But it usually only runs in analysis/topology/geometry.

[Gareth Ma]

Okay but say now I want to break my proof down into lemmas, then since each lemma/step depends on the previous one, I will have to write

lemma aux {c : ℝ} (hc : 1 < c) (f : ℕ → ℝ) (hf : f =o[atTop] (fun _ ↦ 1 : ℕ → ℝ))
  (h : ∃ g : ℕ → ℝ, g =o[atTop] (fun _ ↦ 1 : ℕ → ℝ) ∧
    (fun N : ℕ ↦ sqrt (log N / log (c + f N)))
      =ᶠ[atTop] (fun N : ℕ ↦ sqrt (log N / (log c + log (1 + g N))))) :
  ∃ g : ℕ → ℝ, g =o[atTop] (fun _ ↦ 1 : ℕ → ℝ) ∧
    (fun N : ℕ ↦ sqrt (log N / log (c + f N)))
      =ᶠ[atTop] (fun N : ℕ ↦ sqrt (log N / (log c + g N))) := by
  sorry

4 times :thinking:

[Gareth Ma]

Oh actually no, I'm stupid. h is just aux0 hc f hf or whatever.