chore: add highlights for v4.24 release notes

[viol37]

This PR adds highlights section to Lean v4.24 release notes.

[nomeata]

Thanks!

I think these may also deserve highlighting:

• #9927 implements extended induction-inspired syntax for mvcgen, allowing optional using invariants and with sections.

Here is an example to beef it up a bit:

theorem nodup_correct (h : nodup l = r) : r = true ↔ l.Nodup := by
  unfold nodup at h
  apply Id.of_wp_run_eq h; clear h
  mvcgen
  invariants
  · Invariant.withEarlyReturn
      (onReturn := fun ret seen => ⌜ret = false ∧ ¬l.Nodup⌝)
      (onContinue := fun xs seen =>
        ⌜(∀ x, x ∈ seen ↔ x ∈ xs.prefix) ∧ xs.prefix.Nodup⌝)
  with grind

(or maybe @sgraf812 prefers a different example to show-case this feature)

And maybe we could highlight this, saying “As an example for our continuous improvements to performance:

#10249 speeds up auto-completion by a factor of ~3.5x through various performance improvements in the language server.

[nomeata]

I am not sure if these frontends are actually interesting (they are tactic shorthands).

It’s more interesting to see which new abilities grind has, as in your next point. Maybe just focus on ac, and add an example or two, maybe

example (a b c : Nat) : max a (max b c) = max (max b 0) (max a c) := by
  grind only

[sgraf812]

Here is an example to beef it up a bit:

Good example. Here's related beef (leanprover/lean4#10566) for users to learn that syntax:

info: Try this:
  invariants
    ·
      Invariant.withEarlyReturn (onReturn := fun r letMuts => ⌜l.Nodup ∧ (r = true ↔ l.Nodup)⌝)
        (onContinue := fun xs letMuts => ⌜xs.prefix = [] ∧ letMuts = ∅ ∨ xs.suffix = [] ∧ l.Nodup⌝)
-/
#guard_msgs (info) in
theorem nodup_correct (h : nodup l = r) : r = true ↔ l.Nodup := by
  unfold nodup at h
  apply Id.of_wp_run_eq h; clear h
  mvcgen
  invariants?

Given the formatting mishap here, maybe it's better to stick with

def mySum (l : Array Nat) : Nat := Id.run do
  let mut out := 0
  for i in l do
    out := out + i
  return out

theorem mySum_correct (h : mySum l = x) : x = l.sum := by
  unfold mySum at h
  apply Id.of_wp_run_eq h
  mvcgen
  invariants
  · ⇓⟨xs, out⟩ => ⌜xs.prefix.sum = out⌝
  with grind

/--
info: Try this:
  invariants
    · ⇓⟨xs, letMuts⟩ => ⌜xs.prefix = [] ∧ letMuts = 0 ∨ xs.suffix = [] ∧ letMuts = l.sum⌝
-/
#guard_msgs (info) in
theorem mySum_correct_suggestion (h : mySum l = x) : x = l.sum := by
  unfold mySum at h
  apply Id.of_wp_run_eq h
  mvcgen
  invariants?
  all_goals admit

[github-actions]

Preview for this PR is ready! 🎉 (also as a proofreading version). built with commit 7537909.

[viol37]

Thank you for the suggestions! I've made the changes; let me know if there's anything else I can do.

As for the mvcgen highlight, I went with the nodup example, because I think I cannot use invariants? yet. I am guessing, mySum example will be useful for the next highlights.