Can this proof be shortened?

Stream: new members

[Ching-Tsun Chou]

Just for fun, I proved a simple proposition from a blog post by Terence Tao:
https://terrytao.wordpress.com/2023/12/05/a-slightly-longer-lean-4-proof-tour/
My proof differs from Tao's in that it uses an invariant (h4 in the proof) to obviate the need to talk about summations. But I am not very satisfied by how much code I had to prove basically trivial properties. For example, the calc seems to contain way too many steps. Is there a shorter proof?

import mathlib

example (a D : ℕ → ℝ) (h1 : Antitone a) (h2 : ∀ k, D k ≥ 0)
    (h3 : ∀ k, a k ≤ D k - D (k + 1)) : a k ≤ D 0 / (k + 1) := by
  suffices h4 : (k + 1) * a k ≤ D 0 - D (k + 1) by
    have h5 : (↑k + 1) * a k ≤ D 0 := by have := h2 (k + 1) ; bound
    have h6 : 0 < k + (1 : ℝ) := by bound
    exact (le_div_iff₀' h6).mpr h5
  induction' k with k h_ind <;> simp
  · exact h3 0
  calc
    (↑k + 1 + 1) * a (k + 1) = (↑k + 1) * a (k + 1) + 1 * a (k + 1) := by ring
    _ = (↑k + 1) * a (k + 1) + a (k + 1) := by field_simp
    _ ≤ (↑k + 1) * a k + a (k + 1) := by bound
    _ ≤ D 0 - D (k + 1) + a (k + 1) := by bound
    _ ≤ D 0 - D (k + 1) + D (k + 1) - D (k + 1 + 1) := by have := h3 (k + 1) ; bound
    _ ≤ D 0 - D (k + 1 + 1) := by field_simp

By the way, the above was inspired by a PVS proof I saw. It uses the same invariant, but then PVS basically grinds out all the details with only some high-level human directions. Very impressive.

[Bjørn Kjos-Hanssen]

Yes, the number of calc steps can be reduced:

import Mathlib

example (a D : ℕ → ℝ) (h₁ : Antitone a) (h₂ : ∀ k, D k ≥ 0)
    (h₃ : ∀ k, a k ≤ D k - D (k + 1)) : a k ≤ D 0 / (k + 1) := by
  have : (k + 1) * a k ≤ D 0 - D (k + 1) := by
    induction' k with k h_ind <;> simp
    · exact h₃ 0
    calc _ = (↑k + 1) * a (k + 1) + a (k + 1) := by ring
         _ ≤ (↑k + 1) * a k + a (k + 1) := by bound
         _ ≤ _ := by specialize h₃ (k+1); bound
  apply (le_div_iff₀' (by bound)).mpr
  specialize h₂ (k + 1)
  bound

[Ching-Tsun Chou]

Thanks! I have to say that field_simp had behaved as I thought. Since ℝ is a field, I had thought that the first calc step could be solved by field_simp and was surprised that it couldn't.

[Damiano Testa]

Ching-Tsun Chou said:

Is there a shorter proof?

A "shortest proof" of any provable result exists, but it is almost never observed.

[Damiano Testa]

So, the answer to "Is there a shorter proof" is invariably "Yes".

[Ching-Tsun Chou]

That's why I asked the question. (;-)