fix(Chapter5-Ex): Complete the exercise 5.13

[derik713]

This PR:

• Completes the proof for the split_left_le theorem.
• Demonstrates the difference between using where vs. let for local functions.
• Updates mkHeap so it is no longer a partial function.

[Copilot]

🟢 Approval recommended

No unresolved blocking issues were identified.

Pull request overview

Completes Exercise 5.13 by proving split-length properties and making mkHeap terminating.

Changes:

• Proves split_left_le and related lemmas.
• Demonstrates where versus let.
• Replaces partial mkHeap with a terminating definition.

File summaries

File	Description
Fad/Chapter5-Ex.lean	Adds proofs and termination reasoning for heapsort helpers.

Review details

• Files reviewed: 1/1 changed files
• Comments generated: 0
• Review effort level: Lite

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[arademaker]

We will not keep both split and split₁ in the code. We will decide between let and where in a final split.

[arademaker]

From this comment, it seems split isn't ideal as written. We also don't need both ' split ' and ' split₁ ' here. So we need to decide whether to use where, let, or let rec. In the past, I thought where was not recommended, but I was wrong; I saw many uses of where in the Lean Std code. It seems we will be fine with let rec op, but I don't like adding rec when op isn't recursive. So we can keep split₁ by just renaming it to split or we can rewrite split to something like

def split {a} [Inhabited a] [LE a] [DecidableRel (α := a) (· ≤ ·)]
 (xs : List a) : (a × List a × List a) := 
 let op x acc :=
  if x ≤ acc.1
  then (x, acc.1 :: acc.2.2, acc.2.1)
  else (acc.1, x :: acc.2.2, acc.2.1)
 match xs with
 | []      => (default, [], [])
 | x :: xs => xs.foldr op (x, [], [])

It would be good to try both and report which one makes the proof of split_parts_length easier/shorter.

[derik713]

I opted for the where version because split_lengths (and the other theorems) become simpler once the auxiliary function is already named.