From 4403d6feacd6492b9c3b05fb5a0f87ce137023a5 Mon Sep 17 00:00:00 2001 From: Eric Date: Mon, 14 Sep 2026 00:20:31 -0300 Subject: [PATCH 1/3] fix the exercise 5.13 --- Fad/Chapter5-Ex.lean | 63 ++++++++++++++++++++++++++++++++++++++------ 1 file changed, 55 insertions(+), 8 deletions(-) diff --git a/Fad/Chapter5-Ex.lean b/Fad/Chapter5-Ex.lean index c4cf086..d77b0db 100644 --- a/Fad/Chapter5-Ex.lean +++ b/Fad/Chapter5-Ex.lean @@ -263,13 +263,6 @@ def split [Inhabited a] [LE a] [DecidableRel (α := a) (· ≤ ·)] else (acc.1, x :: acc.2.2, acc.2.1) xs.foldr op (x, [], []) -/-- Nn `split₁` the `where` makes `op` visible from outside. - In `split`, `let` is defined only in the second equation of - the pattern match. `let rec` would make `op` also visible. - - If `op` is not visible, in the `split_left_le` we would need - `lift_lets ; intro op` -/ - def split₁ [Inhabited a] [LE a] [DecidableRel (α := a) (· ≤ ·)] : List a → (a × List a × List a) | [] => (default, [], []) @@ -280,9 +273,63 @@ def split₁ [Inhabited a] [LE a] [DecidableRel (α := a) (· ≤ ·)] then (x, acc.1 :: acc.2.2, acc.2.1) else (acc.1, x :: acc.2.2, acc.2.1) +/-- In `split₁` the `where` makes `op` visible from outside. + In `split`, `let` is defined only in the second equation of + the pattern match. `let rec` would make `op` also visible. + + Since `op` is not visible, we would need + `lift_lets ; intro op` in `split_left_le`-/ theorem split_left_le [Inhabited a] [LE a] [DecidableRel (α := a) (· ≤ ·)] - (xs : List a) : (split₁ xs).2.1.length ≤ xs.length := by sorry + (xs : List a) : (split xs).2.1.length ≤ xs.length := by + cases xs with + | nil => + simp [split] + | cons x xs => + unfold split + lift_lets; intro op + simp + have h : (xs.foldr op (x, [], [])).2.1.length + + (xs.foldr op (x, [], [])).2.2.length = xs.length := by + induction xs with + | nil => + simp + | cons y ys ih => + simp + by_cases h : y ≤ (List.foldr op (x, [], []) ys).1 + all_goals + simp [op, h] + linarith + omega +/-- + On the other hand, since `op` is visible, we can define the + lemma `split₁_lengths` to provide a better abstraction + for `split₁_left_le`. +-/ + +lemma split₁_lengths [Inhabited a] [LE a] [DecidableRel (α := a) (· ≤ ·)] + (xs : List a) (x : a) : + (xs.foldr split₁.op (x, [], [])).2.1.length + + (xs.foldr split₁.op (x, [], [])).2.2.length = xs.length := by + induction xs with + | nil => + simp + | cons y ys ih => + simp + by_cases h : y ≤ (List.foldr split₁.op (x, [], []) ys).1 + all_goals + simp [split₁.op, h] + linarith + +theorem split₁_left_le [Inhabited a] [LE a] [DecidableRel (α := a) (· ≤ ·)] + (xs : List a) : (split₁ xs).2.1.length ≤ xs.length := by + cases xs with + | nil => + simp [split₁] + | cons x xs => + simp [split₁] + have h := split₁_lengths xs x + omega partial def mkHeap [Inhabited a] [LE a] [DecidableRel (α := a) (· ≤ ·)] : List a → Tree a From 63370d29adb8a7c68a7c7dd95fdd9a4a7abba454 Mon Sep 17 00:00:00 2001 From: Eric Date: Mon, 14 Sep 2026 01:32:23 -0300 Subject: [PATCH 2/3] add termination of mkHeap in the exercise 5.13 --- Fad/Chapter5-Ex.lean | 31 ++++++++++++++++++++++++++++++- 1 file changed, 30 insertions(+), 1 deletion(-) diff --git a/Fad/Chapter5-Ex.lean b/Fad/Chapter5-Ex.lean index d77b0db..8142021 100644 --- a/Fad/Chapter5-Ex.lean +++ b/Fad/Chapter5-Ex.lean @@ -331,12 +331,41 @@ theorem split₁_left_le [Inhabited a] [LE a] [DecidableRel (α := a) (· ≤ · have h := split₁_lengths xs x omega -partial def mkHeap [Inhabited a] [LE a] [DecidableRel (α := a) (· ≤ ·)] +/-- For `mkHeap` termination. Again, it would be shorter with `split₁` -/ +lemma split_parts_length [Inhabited a] [LE a] [DecidableRel (α := a) (· ≤ ·)] + (xs : List a) (h : xs ≠ []) : + (split xs).2.1.length + (split xs).2.2.length = xs.length - 1 := by + cases xs with + | nil => contradiction + | cons x xs => + unfold split + lift_lets + intro op + simp + have h : + (xs.foldr op (x, [], [])).2.1.length + + (xs.foldr op (x, [], [])).2.2.length = xs.length := by + induction xs with + | nil => simp + | cons y ys ih => + simp_all + by_cases h : y ≤ (List.foldr op (x, [], []) ys).1 <;> + simp [op, h] <;> + linarith + omega + +def mkHeap [Inhabited a] [LE a] [DecidableRel (α := a) (· ≤ ·)] : List a → Tree a | [] => Tree.null | x :: xs => let p := split (x :: xs) Tree.node p.1 (mkHeap p.2.1) (mkHeap p.2.2) +termination_by xs => xs.length +decreasing_by + all_goals + have h := split_parts_length (x::xs) (by simp) + simp_all + omega end Heapsort From 8cd1b7e288155f22814adbcb34a7432f2954af1c Mon Sep 17 00:00:00 2001 From: Eric Date: Wed, 16 Sep 2026 10:26:40 -0300 Subject: [PATCH 3/3] Use Where version of split --- Fad/Chapter5-Ex.lean | 98 +++++++------------------------------------- 1 file changed, 15 insertions(+), 83 deletions(-) diff --git a/Fad/Chapter5-Ex.lean b/Fad/Chapter5-Ex.lean index 8142021..1f6ab64 100644 --- a/Fad/Chapter5-Ex.lean +++ b/Fad/Chapter5-Ex.lean @@ -254,16 +254,6 @@ def sortOn₃ [Ord b] (f : a → b) : List a → List a := namespace Heapsort def split [Inhabited a] [LE a] [DecidableRel (α := a) (· ≤ ·)] - : List a → (a × List a × List a) - | [] => (default, [], []) - | x :: xs => - 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) - xs.foldr op (x, [], []) - -def split₁ [Inhabited a] [LE a] [DecidableRel (α := a) (· ≤ ·)] : List a → (a × List a × List a) | [] => (default, [], []) | x :: xs => @@ -273,85 +263,27 @@ def split₁ [Inhabited a] [LE a] [DecidableRel (α := a) (· ≤ ·)] then (x, acc.1 :: acc.2.2, acc.2.1) else (acc.1, x :: acc.2.2, acc.2.1) -/-- In `split₁` the `where` makes `op` visible from outside. - In `split`, `let` is defined only in the second equation of - the pattern match. `let rec` would make `op` also visible. - - Since `op` is not visible, we would need - `lift_lets ; intro op` in `split_left_le`-/ - -theorem split_left_le [Inhabited a] [LE a] [DecidableRel (α := a) (· ≤ ·)] - (xs : List a) : (split xs).2.1.length ≤ xs.length := by - cases xs with - | nil => - simp [split] - | cons x xs => - unfold split - lift_lets; intro op - simp - have h : (xs.foldr op (x, [], [])).2.1.length + - (xs.foldr op (x, [], [])).2.2.length = xs.length := by - induction xs with - | nil => - simp - | cons y ys ih => - simp - by_cases h : y ≤ (List.foldr op (x, [], []) ys).1 - all_goals - simp [op, h] - linarith - omega -/-- - On the other hand, since `op` is visible, we can define the - lemma `split₁_lengths` to provide a better abstraction - for `split₁_left_le`. --/ - -lemma split₁_lengths [Inhabited a] [LE a] [DecidableRel (α := a) (· ≤ ·)] +theorem split_lengths [Inhabited a] [LE a] [DecidableRel (α := a) (· ≤ ·)] (xs : List a) (x : a) : - (xs.foldr split₁.op (x, [], [])).2.1.length + - (xs.foldr split₁.op (x, [], [])).2.2.length = xs.length := by + (split (x::xs)).2.1.length + (split (x::xs)).2.2.length = xs.length := by + simp_all [split] induction xs with - | nil => - simp + | nil => trivial | cons y ys ih => - simp - by_cases h : y ≤ (List.foldr split₁.op (x, [], []) ys).1 + by_cases h : y ≤ (List.foldr split.op (x, [], []) ys).1 all_goals - simp [split₁.op, h] + simp [split.op, h] linarith -theorem split₁_left_le [Inhabited a] [LE a] [DecidableRel (α := a) (· ≤ ·)] - (xs : List a) : (split₁ xs).2.1.length ≤ xs.length := by - cases xs with - | nil => - simp [split₁] - | cons x xs => - simp [split₁] - have h := split₁_lengths xs x - omega - -/-- For `mkHeap` termination. Again, it would be shorter with `split₁` -/ -lemma split_parts_length [Inhabited a] [LE a] [DecidableRel (α := a) (· ≤ ·)] - (xs : List a) (h : xs ≠ []) : - (split xs).2.1.length + (split xs).2.2.length = xs.length - 1 := by +theorem split_left_le [Inhabited a] [LE a] [DecidableRel (α := a) (· ≤ ·)] + (xs : List a) : (split xs).2.1.length ≤ xs.length := by + simp [split] cases xs with - | nil => contradiction + | nil => trivial | cons x xs => - unfold split - lift_lets - intro op + have h := split_lengths xs x + rw [split] at h simp - have h : - (xs.foldr op (x, [], [])).2.1.length + - (xs.foldr op (x, [], [])).2.2.length = xs.length := by - induction xs with - | nil => simp - | cons y ys ih => - simp_all - by_cases h : y ≤ (List.foldr op (x, [], []) ys).1 <;> - simp [op, h] <;> - linarith omega def mkHeap [Inhabited a] [LE a] [DecidableRel (α := a) (· ≤ ·)] @@ -363,9 +295,9 @@ def mkHeap [Inhabited a] [LE a] [DecidableRel (α := a) (· ≤ ·)] termination_by xs => xs.length decreasing_by all_goals - have h := split_parts_length (x::xs) (by simp) - simp_all - omega + have h := split_lengths xs x + simp + linarith end Heapsort