From 9394edfee0e8521282708335480ece389ce289a4 Mon Sep 17 00:00:00 2001 From: felipponn Date: Tue, 30 Jun 2026 14:46:07 -0300 Subject: [PATCH 01/16] Initial division of tasks --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index c2fa4fc..b9eef61 100644 --- a/README.md +++ b/README.md @@ -106,7 +106,7 @@ Along the way, readers gain experience not only in algorithm design, but also in ### Part Four: Thinning Algorithms -1. Introduction to thinning +1. Introduction to thinning (@felipponn) - [ ] 10.1 Theory - [ ] 10.2 Paths in a layered network @@ -131,7 +131,7 @@ Along the way, readers gain experience not only in algorithm design, but also in ### Part Five: Dynamic Programming -1. Efficient recursions +1. Efficient recursions (@BXimenaGomez123) - [ ] 13.1 Two numeric examples - [ ] 13.2 Knapsack revisited From 0df15036736f8a79c07edcb047bcaa34a9e30edd Mon Sep 17 00:00:00 2001 From: felipponn Date: Wed, 8 Jul 2026 16:47:14 -0300 Subject: [PATCH 02/16] Structurize Ch10 --- Fad/Chapter10.lean | 350 +++++++++++++++++++++++++++++++++++++++++++++ Fad/Chapter7.lean | 4 +- 2 files changed, 352 insertions(+), 2 deletions(-) create mode 100644 Fad/Chapter10.lean diff --git a/Fad/Chapter10.lean b/Fad/Chapter10.lean new file mode 100644 index 0000000..9db2e6a --- /dev/null +++ b/Fad/Chapter10.lean @@ -0,0 +1,350 @@ + +import Mathlib.Tactic +import Mathlib.Data.List.Sublists +import Fad.Chapter7 + +namespace Chapter10 + +open List +open Chapter7 + +-- ## Section 10.1 Theory + +universe u + +variable {a : Type u} + [Inhabited a] [DecidableRel (α := a) (· = ·)] + [Max a] [Min a] + [LT a] [DecidableRel (α := a) (· < ·)] + [LE a] [DecidableRel (α := a) (· ≤ ·)] + +set_option linter.unusedSectionVars false + +/-! ### Subsequences + +`ys <+ xs` means that `ys` is a subsequence of `xs`. +The List.Sublist module will be really helpful. +-/ + +example : [1, 3] <+ [1, 2, 3] := by + apply List.Sublist.cons_cons + apply List.Sublist.cons + apply List.Sublist.cons_cons + apply List.Sublist.slnil + + +-- ### The predicate `ThinBy` + +/-- `Dominates r ys xs` : every element of `xs` is dominated under `r` by some + element of `ys`, i.e. `∀ x ∈ xs, ∃ y ∈ ys, y ⪯ x`. -/ +def Dominates (r : a → a → Prop) (ys xs : List a) : Prop := + ∀ x ∈ xs, ∃ y ∈ ys, r y x + +def ThinBy (r : a → a → Prop) (xs ys : List a) : Prop := + ys <+ xs ∧ Dominates r ys xs + +@[simp] theorem mem_ThinBy {r : a → a → Prop} {xs ys : List a} : + ThinBy r xs ys ↔ ys <+ xs ∧ Dominates r ys xs := by + rfl + +-- ### A linear-time implementation `thinBy` + +/-- One step of `thinBy`, processing from the right. -/ +def bump (le : a → a → Bool) (x : a) : List a → List a + | [] => [x] + | y :: ys => + match le x y, le y x with + | true, _ => x :: ys + | false, true => y :: ys + | false, false => x :: y :: ys + +/-- A sub-optimal, linear-time implementation of `ThinBy`. -/ +def thinBy (le : a → a → Bool) : List a → List a := + List.foldr (bump le) [] + +theorem thinBy_nil (le : a → a → Bool) : thinBy le [] = [] := by + rfl + +theorem thinBy_cons (le : a → a → Bool) (z : a) (zs : List a) : + thinBy le (z :: zs) = bump le z (thinBy le zs) := by + rfl + + +-- ### Examples + +/-- `(a,b) ⪯ (c,d) = (a ≥ c) ∧ (b ≤ d)`, as a `Bool` test on `ℕ × ℕ`. -/ +def le₁ (p q : Nat × Nat) : Bool := decide (q.1 ≤ p.1 ∧ p.2 ≤ q.2) + +/-- +info: [(1, 2), (4, 3), (5, 4), (3, 1)] +-/ +#guard_msgs in +#eval thinBy le₁ [(1,2),(4,3),(2,3),(5,4),(3,1)] + +/-- +info: [(3, 1), (4, 3), (5, 4)] +-/ +#guard_msgs in +#eval thinBy le₁ [(1,2),(2,3),(3,1),(4,3),(5,4)] + +/-- +info: [(3, 1), (4, 3), (5, 4)] +-/ +#guard_msgs in +#eval thinBy le₁ [(3,1),(1,2),(2,3),(4,3),(5,4)] + + +/-! ### `thinBy` refines `ThinBy` (correctness) + +We prove that the concrete `thinBy` always returns a valid thinning, provided +the comparison is reflexive and transitive (i.e. a preorder). This splits into +the subsequence property and the domination property. -/ + +/-- `bump` preserves being a subsequence. -/ +theorem bump_sublist (le : a → a → Bool) (z : a) {t zs : List a} + (ht : t <+ zs) : bump le z t <+ z :: zs := by + cases t with + | nil => + simp only [bump] + exact List.Sublist.cons_cons z (List.nil_sublist zs) + | cons y ys => + have hys : ys <+ zs := (List.Sublist.cons y (List.Sublist.refl ys)).trans ht + cases h1 : le z y <;> cases h2 : le y z <;> simp only [bump, h1, h2] + · exact List.Sublist.cons_cons z ht -- (false,false): z :: y :: ys + · exact List.Sublist.cons z ht -- (false,true): y :: ys + · exact List.Sublist.cons_cons z hys -- (true,false): z :: ys + · exact List.Sublist.cons_cons z hys -- (true,true): z :: ys + +/-- Every output of `thinBy` is a subsequence of the input. -/ +theorem thinBy_sublist (le : a → a → Bool) : + ∀ xs : List a, thinBy le xs <+ xs := by + intro xs + induction xs with + | nil => exact List.Sublist.refl [] + | cons z zs ih => + rw [thinBy_cons] + exact bump_sublist le z ih + +/-- After a `bump`, the new element `z` is dominated by some element of the + result. -/ +theorem bump_dom_self (le : a → a → Bool) (hrefl : ∀ x, le x x = true) + (z : a) (t : List a) : ∃ y ∈ bump le z t, le y z = true := by + cases t with + | nil => exact ⟨z, by simp [bump], hrefl z⟩ + | cons y ys => + cases h1 : le z y <;> cases h2 : le y z <;> simp only [bump, h1, h2] + · exact ⟨z, by simp, hrefl z⟩ -- (false,false): z :: y :: ys + · exact ⟨y, by simp, h2⟩ -- (false,true): y :: ys + · exact ⟨z, by simp, hrefl z⟩ -- (true,false): z :: ys + · exact ⟨z, by simp, hrefl z⟩ -- (true,true): z :: ys + +/-- A `bump` preserves domination of any element `w` that was already + dominated by the accumulator. -/ +theorem bump_dom_pres (le : a → a → Bool) + (htrans : ∀ x y z, le x y = true → le y z = true → le x z = true) + (z : a) (t : List a) (w : a) (h : ∃ y ∈ t, le y w = true) : + ∃ y ∈ bump le z t, le y w = true := by + obtain ⟨y₀, hy₀_mem, hy₀⟩ := h + cases t with + | nil => simp at hy₀_mem + | cons y ys => + cases h1 : le z y <;> cases h2 : le y z <;> simp only [bump, h1, h2] + · -- (false,false): bump = z :: y :: ys ⊇ (y :: ys) + exact ⟨y₀, List.mem_cons_of_mem z hy₀_mem, hy₀⟩ + · -- (false,true): bump = y :: ys (unchanged) + exact ⟨y₀, hy₀_mem, hy₀⟩ + · -- (true,false): bump = z :: ys ; the head y was dropped in favour of z + rcases List.mem_cons.mp hy₀_mem with hy0y | hy0ys + · subst hy0y + exact ⟨z, by simp, htrans z y₀ w h1 hy₀⟩ + · exact ⟨y₀, List.mem_cons_of_mem z hy0ys, hy₀⟩ + · -- (true,true): bump = z :: ys (same reasoning) + rcases List.mem_cons.mp hy₀_mem with hy0y | hy0ys + · subst hy0y + exact ⟨z, by simp, htrans z y₀ w h1 hy₀⟩ + · exact ⟨y₀, List.mem_cons_of_mem z hy0ys, hy₀⟩ + +/-- Every element of the input is dominated by some output of `thinBy`. -/ +theorem thinBy_dominates (le : a → a → Bool) + (hrefl : ∀ x, le x x = true) + (htrans : ∀ x y z, le x y = true → le y z = true → le x z = true) : + ∀ xs, Dominates (fun y x => le y x = true) (thinBy le xs) xs := by + intro xs + induction xs with + | nil => intro x hx; cases hx + | cons z zs ih => + rw [thinBy_cons] + intro x hx + rcases List.mem_cons.mp hx with hxz | hxzs + · subst hxz + exact bump_dom_self le hrefl x (thinBy le zs) + · exact bump_dom_pres le htrans z (thinBy le zs) x (ih x hxzs) + +/-- Correctness of `thinBy`: it always returns a valid thinning. -/ +theorem thinBy_refines (le : a → a → Bool) + (hrefl : ∀ x, le x x = true) + (htrans : ∀ x y z, le x y = true → le y z = true → le x z = true) : + ∀ xs, ThinBy (fun y x => le y x = true) xs (thinBy le xs) := by + intro xs + constructor + · exact thinBy_sublist le xs + · exact thinBy_dominates le hrefl htrans xs + +/-- `le₁` is reflexive. -/ +theorem le₁_refl (p : Nat × Nat) : le₁ p p = true := by + simp [le₁] + +/-- `le₁` is transitive. -/ +theorem le₁_trans (p q s : Nat × Nat) : + le₁ p q = true → le₁ q s = true → le₁ p s = true := by + simp only [le₁, decide_eq_true_eq] + rintro ⟨h1, h2⟩ ⟨h3, h4⟩ + exact ⟨le_trans h3 h1, le_trans h2 h4⟩ + +/-- Concrete capstone: the thinning computed for the book's example is indeed a + valid member of the specification `ThinBy`. -/ +example : + ThinBy (fun y x => le₁ y x = true) [(1,2),(4,3),(2,3),(5,4),(3,1)] + (thinBy le₁ [(1,2),(4,3),(2,3),(5,4),(3,1)]) := by + -- apply thinBy_refines le₁ le₁_refl le₁_trans + unfold thinBy + simp [bump, le₁] + constructor + · apply List.Sublist.cons_cons + apply List.Sublist.cons_cons + apply List.Sublist.cons + apply List.Sublist.refl + · intro x h + cases h + use (1, 2) + grind + expose_names + cases h + use (4, 3) + grind + expose_names + cases h + use (4, 3) + grind + expose_names + cases h + use (5, 4) + grind + expose_names + cases h + use (3, 1) + grind + expose_names + cases h + + +/-! ### The laws of thinning + + * identity `id ← ThinBy r` + * idempotence `ThinBy r = ThinBy r · ThinBy r` + * thin introduction `MinWith cost = MinWith cost · ThinBy r` + * thin elimination `wrap · MinWith cost ← ThinBy r` + * thin-map (one flavour)`map f · ThinBy r ← ThinBy r · map f` + +The remaining laws (the distributive law and the thin-filter law) are stated in +comments; they are left as exercises. -/ + +/-- **Identity law.** `id ← ThinBy r`, given reflexivity. -/ +theorem thin_identity (r : a → a → Prop) (hrefl : ∀ x, r x x) : + ∀ xs : List a, ThinBy r xs xs := by + intro xs + constructor + · exact List.Sublist.refl xs + · intro x hx + use x + constructor + · assumption + · exact hrefl x + +/-- **Idempotence law.** `ThinBy r = ThinBy r · ThinBy r`, for a preorder `r`. -/ +theorem thin_idem (r : a → a → Prop) + (hrefl : ∀ x, r x x) + (htrans : ∀ x y z, r x y → r y z → r x z) : + ∀ xs zs : List a, ThinBy r xs zs ↔ ∃ ys : List a, + ThinBy r ys zs ∧ ThinBy r xs ys := by + intro xs zs + constructor + · intro h + use zs + constructor + · exact thin_identity r hrefl zs + · assumption + · intro h + obtain ⟨ys, hys⟩ := h + constructor + · exact List.Sublist.trans (hys.1.1) (hys.2.1) + · intro x hx + have h₁ := hys.2.2 + obtain ⟨y, hy⟩ := h₁ x hx + have h₂ := hys.1.2 + obtain ⟨z, hz⟩ := h₂ y hy.1 + use z + constructor + · exact hz.1 + · exact htrans z y x hz.2 hy.2 + +-- def foldr1 (f : a → a → a) : List a → a +-- | [] => default +-- | [x] => x +-- | x::xs => f x (foldr1 f xs) + +-- def minWith {a b : Type} [LE b] [Inhabited a] +-- [DecidableRel (α := b) (· ≤ ·)] +-- (f : a → b) (as : List a) : a := +-- let smaller f x y := cond (f x ≤ f y) x y +-- foldr1 (smaller f) as + +/-- **Thin introduction.** `MinWith cost = MinWith cost · ThinBy r`, + provided `x ⪯ y ⇒ cost x ≤ cost y`. This is the law that turns an + optimisation problem into a thinning problem. -/ +theorem thin_introduction [LE b] [DecidableRel (α := b) (· ≤ ·)] + (r : a → a → Prop) + (cost : a → b) (hrefl : ∀ x, r x x) + (xs ys : List a) + (hmono : ∀ x y, r x y → cost x ≤ cost y) + (h : ThinBy r xs ys) : + (minWith cost xs) = minWith cost ys := by + sorry + +/-- `wrap x = [x]`. -/ +def wrap (x : a) : List a := [x] + +/-- **Thin elimination.** `wrap · MinWith cost ← ThinBy r`, + provided `cost x ≤ cost y ⇒ x ⪯ y`. Dual to thin introduction. -/ +theorem thin_elimination {β : Type*} [LE β] [DecidableRel (α := β) (· ≤ ·)] + (r : a → a → Prop) (cost : a → β) + (hmono : ∀ x y, cost x ≤ cost y → r x y) : + ∀ xs : List a, ThinBy r xs (wrap (minWith cost xs)) := by + sorry + +/-- **Thin-map law** (first flavour). `map f · ThinBy r ← ThinBy r · map f`, + provided `x ⪯ y ⇒ f x ⪯ f y`. -/ +theorem thin_map (r : a → a → Prop) (f : a → a) + (hmono : ∀ x y, r x y → r (f x) (f y)) + (xs ys : List a) + (h : ThinBy r xs ys) : + ThinBy r (map f xs) (map f ys) := by + sorry + +/- + Remaining laws (left as exercises, as in the book): + + * Distributive law: + ThinBy r · concat = ThinBy r · concatMap (ThinBy r) + with the weaker refinement + concatMap (ThinBy r) ← ThinBy r · concat. + + * Thin-map law (second flavour): + ThinBy r · map f ← map f · ThinBy r if f x ⪯ f y ⇒ x ⪯ y, + giving the equality map f · ThinBy r = ThinBy r · map f when x ⪯ y ⇔ f x ⪯ f y. + + * Thin-filter law: + ThinBy r · filter p = filter p · ThinBy r provided (x ⪯ y ∧ p y) ⇒ p x. +-/ + +end Chapter10 diff --git a/Fad/Chapter7.lean b/Fad/Chapter7.lean index fa4fe08..de2da73 100644 --- a/Fad/Chapter7.lean +++ b/Fad/Chapter7.lean @@ -40,7 +40,7 @@ def foldr1₁ {a : Type} (f : a → a → a) (as : List a) f x (foldr1₁ f as.tail (by rw [List.length_tail]; omega)) -def foldr1 {a : Type} [Inhabited a] (f : a → a → a) : List a → a +def foldr1 {a : Type*} [Inhabited a] (f : a → a → a) : List a → a | [] => default | x::xs => xs.foldr f x @@ -49,7 +49,7 @@ def foldr1 {a : Type} [Inhabited a] (f : a → a → a) : List a → a -- #eval foldr1₁ (fun a b => a + b ) [1,2,3,4,5,6] -- #eval foldr1 (fun a b => a + b ) [1,2,3,4,5,6] -def minWith {a b : Type} [LE b] [Inhabited a] +def minWith {a b : Type*} [LE b] [Inhabited a] [DecidableRel (α := b) (· ≤ ·)] (f : a → b) (as : List a) : a := let smaller f x y := cond (f x ≤ f y) x y From d039b7b068b59d631308108e1199663ede865595 Mon Sep 17 00:00:00 2001 From: felipponn Date: Tue, 14 Jul 2026 12:11:03 -0300 Subject: [PATCH 03/16] Finish 10.1 --- Fad/Chapter10.lean | 130 ++++++++++++++++++++++++++++++++++++++------- 1 file changed, 111 insertions(+), 19 deletions(-) diff --git a/Fad/Chapter10.lean b/Fad/Chapter10.lean index 9db2e6a..adb254f 100644 --- a/Fad/Chapter10.lean +++ b/Fad/Chapter10.lean @@ -288,39 +288,113 @@ theorem thin_idem (r : a → a → Prop) · exact hz.1 · exact htrans z y x hz.2 hy.2 --- def foldr1 (f : a → a → a) : List a → a --- | [] => default --- | [x] => x --- | x::xs => f x (foldr1 f xs) - --- def minWith {a b : Type} [LE b] [Inhabited a] --- [DecidableRel (α := b) (· ≤ ·)] --- (f : a → b) (as : List a) : a := --- let smaller f x y := cond (f x ≤ f y) x y --- foldr1 (smaller f) as +/-- Folding with `smaller cost` always returns an element of the list. -/ +private lemma foldrSmaller_mem {α β : Type*} [LE β] + [DecidableRel (α := β) (· ≤ ·)] (cost : α → β) (x : α) : + ∀ ys : List α, + List.foldr (fun u v => cond (cost u ≤ cost v) u v) x ys ∈ x :: ys := by + intro ys + induction' ys with z zs ih + · simp + · simp only [List.foldr_cons] + by_cases h : cost z ≤ cost (List.foldr (fun u v => cond (cost u ≤ cost v) u v) x zs) + · simp [h] + · simp only [h, decide_false, cond_false] + rcases List.mem_cons.1 ih with hx | hz + · simp [hx] + · exact List.mem_cons.2 (Or.inr (List.mem_cons.2 (Or.inr hz))) + + +/-- Folding with `smaller cost` yields a cost-minimal element of the list. -/ +private lemma foldrSmaller_le {α β : Type*} [LinearOrder β] (cost : α → β) (x : α) : + ∀ (ys : List α) (z : α), z ∈ x :: ys → + cost (List.foldr (fun u v => cond (cost u ≤ cost v) u v) x ys) ≤ cost z := by + intro ys + induction' ys with w ws ih + · intro z hz + simp at hz + subst hz + simp + · intro z hz + simp only [List.foldr_cons] + set t := List.foldr (fun u v => cond (cost u ≤ cost v) u v) x ws with ht + by_cases h : cost w ≤ cost t + · simp only [h, decide_true, cond_true] + rcases List.mem_cons.1 hz with hzx | hz' + · rw [hzx]; exact le_trans h (ih x (by simp)) + · rcases List.mem_cons.1 hz' with hzw | hz'' + · rw [hzw] + · exact le_trans h (ih z (by simp [hz''])) + · simp only [h, decide_false, cond_false] + have hwt : cost t ≤ cost w := le_of_lt (lt_of_not_ge h) + rcases List.mem_cons.1 hz with hzx | hz' + · rw [hzx]; exact ih x (by simp) + · rcases List.mem_cons.1 hz' with hzw | hz'' + · rw [hzw]; exact hwt + · exact ih z (by simp [hz'']) + +/-- `minWith cost` returns an element of the (non-empty) list. -/ +theorem minWith_mem {α β : Type*} [Inhabited α] [LE β] + [DecidableRel (α := β) (· ≤ ·)] (cost : α → β) : + ∀ {xs : List α}, xs ≠ [] → minWith cost xs ∈ xs := by + intro xs hxs + match xs with + | [] => exact absurd rfl hxs + | x :: xs => exact foldrSmaller_mem cost x xs + +/-- `minWith cost` returns a cost-minimal element of the list. -/ +theorem minWith_le {α β : Type*} [Inhabited α] [LinearOrder β] (cost : α → β) : + ∀ {xs : List α}, ∀ z ∈ xs, cost (minWith cost xs) ≤ cost z := by + intro xs + match xs with + | [] => intro z hz; simp at hz + | x :: xs => intro z hz; exact foldrSmaller_le cost x xs z hz /-- **Thin introduction.** `MinWith cost = MinWith cost · ThinBy r`, provided `x ⪯ y ⇒ cost x ≤ cost y`. This is the law that turns an optimisation problem into a thinning problem. -/ -theorem thin_introduction [LE b] [DecidableRel (α := b) (· ≤ ·)] +theorem thin_introduction [LinearOrder b] (r : a → a → Prop) - (cost : a → b) (hrefl : ∀ x, r x x) + (cost : a → b) (xs ys : List a) (hmono : ∀ x y, r x y → cost x ≤ cost y) (h : ThinBy r xs ys) : - (minWith cost xs) = minWith cost ys := by - sorry + cost (minWith cost xs) = cost (minWith cost ys) := by + obtain ⟨hsub, hdom⟩ := h + by_cases hxs : xs = [] + · subst hxs + rw [List.sublist_nil.1 hsub] + · have hys : ys ≠ [] := by + rintro rfl + obtain ⟨y, hy, _⟩ := hdom _ (minWith_mem cost hxs) + simp at hy + have hmemx : minWith cost xs ∈ xs := minWith_mem cost hxs + have hl : cost (minWith cost xs) ≤ cost (minWith cost ys) := by + have hmy : minWith cost ys ∈ ys := minWith_mem cost hys + exact minWith_le cost (minWith cost ys) (hsub.subset hmy) + have hr : cost (minWith cost xs) ≥ cost (minWith cost ys) := by + obtain ⟨y, hymem, hry⟩ := hdom _ hmemx + exact le_trans (minWith_le cost y hymem) (hmono y (minWith cost xs) hry) + grind /-- `wrap x = [x]`. -/ def wrap (x : a) : List a := [x] /-- **Thin elimination.** `wrap · MinWith cost ← ThinBy r`, provided `cost x ≤ cost y ⇒ x ⪯ y`. Dual to thin introduction. -/ -theorem thin_elimination {β : Type*} [LE β] [DecidableRel (α := β) (· ≤ ·)] +theorem thin_elimination {β : Type*} [LinearOrder β] (r : a → a → Prop) (cost : a → β) (hmono : ∀ x y, cost x ≤ cost y → r x y) : - ∀ xs : List a, ThinBy r xs (wrap (minWith cost xs)) := by - sorry + ∀ (xs : List a), xs ≠ [] → ThinBy r xs (wrap (minWith cost xs)) := by + intro xs hxs + constructor + · have h₁ := minWith_mem cost hxs + simpa [wrap] + · intro x hx + simp [wrap] + have h₂ := minWith_le cost x hx + apply hmono at h₂ + exact h₂ /-- **Thin-map law** (first flavour). `map f · ThinBy r ← ThinBy r · map f`, provided `x ⪯ y ⇒ f x ⪯ f y`. -/ @@ -329,10 +403,28 @@ theorem thin_map (r : a → a → Prop) (f : a → a) (xs ys : List a) (h : ThinBy r xs ys) : ThinBy r (map f xs) (map f ys) := by - sorry + constructor + · have h1 := h.1 + exact Sublist.map f h1 + · have h2 := h.2 + intro x hx + simp at hx + obtain ⟨z, hz⟩ := hx + have h₀ := h2 z hz.1 + obtain ⟨w, hw⟩ := h₀ + use f w + constructor + · simp + use w + constructor + · exact hw.1 + · rfl + · have h₁ := hmono w z hw.2 + simp [hz] at h₁ + assumption /- - Remaining laws (left as exercises, as in the book): + Remaining laws (exercises): * Distributive law: ThinBy r · concat = ThinBy r · concatMap (ThinBy r) From 0acc510f2ea67c79365ea9b5dde775360e231dda Mon Sep 17 00:00:00 2001 From: BXimenaGomez123 Date: Tue, 14 Jul 2026 15:13:56 -0300 Subject: [PATCH 04/16] partial 13.1 --- Fad/API.lean | 51 +++++++++++++++++++++++++++++++++++++ Fad/Chapter13.lean | 63 +++++++++++++++++++++++++++++++++++++++++++++- 2 files changed, 113 insertions(+), 1 deletion(-) create mode 100644 Fad/API.lean diff --git a/Fad/API.lean b/Fad/API.lean new file mode 100644 index 0000000..4ad0cd8 --- /dev/null +++ b/Fad/API.lean @@ -0,0 +1,51 @@ +/- +Copyright (c) 2025 Sorrachai Yingchareonthawornchai. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sorrachai Yingchareonthawornchai +-/ + +import Mathlib.Tactic -- imports all of the tactics in Lean's maths library + + +set_option autoImplicit false +set_option tactic.hygienic false + +structure TimeM (α : Type) where + ret : α + time : ℕ + +namespace TimeM + +def pure {α} (a : α) : TimeM α := + ⟨a, 0⟩ + +def bind {α β} (m : TimeM α) (f : α → TimeM β) : TimeM β := + let r := f m.ret + ⟨r.ret, m.time + r.time⟩ + +instance : Monad TimeM where + pure := pure + bind := bind + +-- Increment time +@[simp] def tick {α : Type} (a : α) (c : ℕ := 1) : TimeM α := + ⟨a, c⟩ + +notation "✓" a:arg ", " c:arg => tick a c +notation "✓" a:arg => tick a -- Default case with only one argument + +def tickUnit : TimeM Unit := + ✓ () -- This uses the default time increment of 1 + +@[grind, simp] theorem time_of_pure {α} (a : α) : (pure a).time = 0 := rfl +@[grind, simp] theorem time_of_bind {α β} (m : TimeM α) (f : α → TimeM β) : + (TimeM.bind m f).time = m.time + (f m.ret).time := rfl +@[grind, simp] theorem time_of_tick {α} (a : α) (c : ℕ) : (tick a c).time = c := rfl +@[grind, simp] theorem ret_bind {α β} (m : TimeM α) (f : α → TimeM β) : + (TimeM.bind m f).ret = (f m.ret).ret := rfl + +-- allow us to simplify the chain of compositions +attribute [simp] Bind.bind Pure.pure TimeM.pure + + +end TimeM diff --git a/Fad/Chapter13.lean b/Fad/Chapter13.lean index ec76540..26d736f 100644 --- a/Fad/Chapter13.lean +++ b/Fad/Chapter13.lean @@ -1,4 +1,5 @@ import Fad.Chapter1 +import Fad.API namespace Chapter13 open Chapter1 (scanr₀) @@ -11,17 +12,77 @@ def fib₀ : Nat → Int | 1 => 1 | n + 2 => fib₀ (n + 1) + fib₀ n ---#eval fib₀ 10 +def fib₀T : Nat → TimeM Int +| 0 => TimeM.pure 0 +| 1 => TimeM.pure 1 +| n + 2 => do + let x ← fib₀T (n + 1) + let y ← fib₀T n + ✓ (x + y) + +-- The complexity is +-- #eval [5, 10, 15, 20].map fun n => (n, (fib₀T n).time) + +-- #eval fib₀ 10 def tab (f : Nat → Int) (lo hi : Nat) : Array Int := (List.range (hi - lo + 1)).map (fun i => f (lo + i)) |>.toArray +-- Haskell is a lazy so we will append another tab function using thunk to get the O(n) complexity +private def badDependency [Inhabited α] : Thunk α := + Thunk.mk fun _ => panic! "undefined lazy-array entry" + +def tabulate [Inhabited α] + (f : (Nat → Thunk α) → Nat → Thunk α) + (bounds : Nat × Nat) : Array (Thunk α) := + let (lo, hi) := bounds + if hi < lo then + #[] + else + (List.range (hi - lo + 1)).foldl + (fun cells k => + let i := lo + k + let fetch := fun j => + match cells[j - lo]? with + | some cell => cell + | none => badDependency + cells.push (f fetch i)) + #[] + +def tabulateT [Inhabited α] + (f : (Nat → Thunk α) → Nat → Thunk α) + (bounds : Nat × Nat) : TimeM (Array (Thunk α)) := + let (lo, hi) := bounds + if hi < lo then + TimeM.pure #[] + else + (List.range (hi - lo + 1)).foldl + (fun timedCells k => do + let cells ← timedCells + let i := lo + k + let fetch := fun j => + match cells[j - lo]? with + | some cell => cell + | none => badDependency + ✓ (cells.push (f fetch i))) + (TimeM.pure #[]) + +private def forceAt [Inhabited α] + (cells : Array (Thunk α)) (bounds : Nat × Nat) (i : Nat) : α := + let (lo, _) := bounds + match cells[i - lo]? with + | some cell => cell.get + | none => panic! "index outside lazy-array bounds" + + def fib₁ (n : Nat) : Int := let rec a : Nat → Int := fun i => if i ≤ 1 then i else a (i - 1) + a (i - 2) let arr := tab a 0 n arr[n]! + + --#eval fib₁ 10 def fib₂ (n : Nat) : Int := From 35e508511d554411f65cc0dc7a9a04478eddb03b Mon Sep 17 00:00:00 2001 From: BXimenaGomez123 Date: Tue, 14 Jul 2026 22:25:20 -0300 Subject: [PATCH 05/16] fib part complete 13.1 --- Fad/Chapter13.lean | 84 +++++++++++++++++++++++++++++++++++++++------- 1 file changed, 72 insertions(+), 12 deletions(-) diff --git a/Fad/Chapter13.lean b/Fad/Chapter13.lean index 26d736f..6740db9 100644 --- a/Fad/Chapter13.lean +++ b/Fad/Chapter13.lean @@ -20,15 +20,12 @@ def fib₀T : Nat → TimeM Int let y ← fib₀T n ✓ (x + y) --- The complexity is --- #eval [5, 10, 15, 20].map fun n => (n, (fib₀T n).time) - -- #eval fib₀ 10 +-- #eval fib₀T 10 +-- The complexity is exponential +-- #eval [5, 10, 15, 20].map fun n => (n, (fib₀T n).time) -def tab (f : Nat → Int) (lo hi : Nat) : Array Int := - (List.range (hi - lo + 1)).map (fun i => f (lo + i)) |>.toArray - --- Haskell is a lazy so we will append another tab function using thunk to get the O(n) complexity +-- Haskell is a lazy language so we will append another tab function using thunk to get the O(n) complexity private def badDependency [Inhabited α] : Thunk α := Thunk.mk fun _ => panic! "undefined lazy-array entry" @@ -75,15 +72,29 @@ private def forceAt [Inhabited α] | none => panic! "index outside lazy-array bounds" -def fib₁ (n : Nat) : Int := - let rec a : Nat → Int := - fun i => if i ≤ 1 then i else a (i - 1) + a (i - 2) - let arr := tab a 0 n - arr[n]! +-- Lazy tabulation, corresponding to `a = tabulate f (0,n)` in the book. +private def fibF (a : Nat → Thunk Int) (i : Nat) : Thunk Int := + if i ≤ 1 then + Thunk.mk fun _ => Int.ofNat i + else + let previous := a (i - 1) + let beforePrevious := a (i - 2) + Thunk.mk fun _ => previous.get + beforePrevious.get +def fib₁ (n : Nat) : Int := + let bounds := (0, n) + let a := tabulate fibF bounds + forceAt a bounds n +def fib₁T (n : Nat) : TimeM Int := do + let bounds := (0, n) + let a ← tabulateT fibF bounds + TimeM.pure (forceAt a bounds n) --#eval fib₁ 10 +--#eval fib₁T 10 +-- The complexity is O(n) +--#eval [10, 20, 40, 80].map fun n => (n, (fib₁T n).time) def fib₂ (n : Nat) : Int := let step := fun (a b : Int) => (b, a + b) @@ -93,15 +104,51 @@ def fib₂ (n : Nat) : Int := let (a, _) := apply n (0, 1) a +def fib₂T (n : Nat) : TimeM Int := + let step := fun (a b : Int) => (b, a + b) + let rec applyT : Nat → Int × Int → TimeM (Int × Int) + | 0, p => TimeM.pure p + | k + 1, (a, b) => do + let next ← (✓ (step a b)) + applyT k next + do + let (a, _) ← applyT n (0, 1) + TimeM.pure a + --#eval fib₂ 10 +--#eval fib₂T 10 +-- The complexity is O(n) +--#eval [10, 20, 40, 80].map fun n => (n, (fib₂T n).time) def fact (n : Nat) : Int := ((List.range (n + 1)).drop 1).map Int.ofNat |>.foldl (· * ·) 1 +private def productT : List Int → TimeM Int +| [] => TimeM.pure 1 +| x :: xs => do + let p ← productT xs + ✓ (x * p) + +def factT (n : Nat) : TimeM Int := + productT (((List.range (n + 1)).drop 1).map Int.ofNat) + + def bin₀ (n r : Nat) : Int := fact n / (fact r * fact (n - r)) +def bin₀T (n r : Nat) : TimeM Int := + if r > n then + TimeM.pure 0 + else do + let fn ← factT n + let fr ← factT r + let fnr ← factT (n - r) + let denominator ← (✓ (fr * fnr)) + ✓ (fn / denominator) + --#eval bin₀ 6 3 +--#eval bin₀T 6 3 +--#eval [10, 20, 40, 80].map fun n =>((n, n / 2), (bin₀T n (n / 2)).time) def bin₁ : Nat → Nat → Int | _, 0 => 1 @@ -110,7 +157,20 @@ def bin₁ : Nat → Nat → Int if r + 1 = n + 1 then 1 else bin₁ n (r + 1) + bin₁ n r +def bin₁T : Nat → Nat → TimeM Int +| _, 0 => TimeM.pure 1 +| 0, _ => TimeM.pure 0 +| n + 1, r + 1 => + if r + 1 = n + 1 then + TimeM.pure 1 + else do + let x ← bin₁T n (r + 1) + let y ← bin₁T n r + ✓ (x + y) + --#eval bin₁ 6 3 +--#eval bin₁T 6 3 + def bin₂ (n r : Nat) : Int := Id.run do let mut a : Array ((Nat × Nat) × Int) := #[] From 395da34d2ebdd0586fa7025238cfe2f25d7e9324 Mon Sep 17 00:00:00 2001 From: felipponn Date: Wed, 15 Jul 2026 01:25:12 -0300 Subject: [PATCH 06/16] Set up 10.2 and 10.3 --- Fad/Chapter10.lean | 424 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 424 insertions(+) diff --git a/Fad/Chapter10.lean b/Fad/Chapter10.lean index adb254f..9b512a3 100644 --- a/Fad/Chapter10.lean +++ b/Fad/Chapter10.lean @@ -439,4 +439,428 @@ theorem thin_map (r : a → a → Prop) (f : a → a) ThinBy r · filter p = filter p · ThinBy r provided (x ⪯ y ∧ p y) ⇒ p x. -/ +-- ## Section 10.2 Paths in a layered network + +namespace LayeredNetwork + +/-! A layered network is given by a list of lists of edges, each list describing +the edges between two adjacent layers. Each edge is a triple `(u,v,w)`, where +`u` is the source, `v` the target and `w` a numerical weight, not necessarily +positive. The problem is to find a path from the top layer to the bottom layer +with minimum total weight. -/ + +abbrev Vertex := Nat +abbrev Weight := Int +abbrev Edge := Vertex × Vertex × Weight +abbrev Path := List Edge +abbrev Net := List (List Edge) + +def source (e : Edge) : Vertex := e.1 +def target (e : Edge) : Vertex := e.2.1 +def weight (e : Edge) : Weight := e.2.2 + +def cost (p : Path) : Weight := (p.map weight).sum + +/- `thinBy` drags along the instances of the section variable `a` -/ +instance : Max Path := ⟨fun p q => if cost p ≤ cost q then q else p⟩ +instance : Min Path := ⟨fun p q => if cost p ≤ cost q then p else q⟩ + +@[simp] theorem cost_nil : cost [] = 0 := rfl + +@[simp] theorem cost_cons (e : Edge) (p : Path) : cost (e :: p) = weight e + cost p := by + simp [cost] + + +/-! ### The network of Figure 10.1 + +Four layers of four vertices each: `1..4`, `5..8`, `9..12` and `13..16`. There +are 27 paths from the top layer to the bottom one. -/ + +def layer₁ : List Edge := [(1,5,2), (1,6,7), (2,6,1), (3,6,4), (3,7,5), (4,7,2), (4,8,3)] +def layer₂ : List Edge := [(5,9,5), (6,9,3), (6,10,9), (6,11,8), (7,11,2), (8,11,7), (8,12,1)] +def layer₃ : List Edge := [(9,13,4), (9,14,8), (10,14,2), (10,15,5), (11,15,6), (11,16,3), (12,16,7)] + +/-- The network of Figure 10.1. Note that each list of edges is sorted so that + edges with the same source vertex appear together: this is what makes the + thinning step below produce just one path per source vertex. -/ +def net₁ : Net := [layer₁, layer₂, layer₃] + + +/-! ### The specification -/ + +/-- The Cartesian-product function `cp`. -/ +def cp {γ : Type u} : List (List γ) → List (List γ) := + List.foldr (fun xs yss => xs.flatMap (fun x => yss.map (x :: ·))) [[]] + +theorem cp_nil {γ : Type u} : cp ([] : List (List γ)) = [[]] := rfl + +theorem cp_cons {γ : Type u} (xs : List γ) (xss : List (List γ)) : + cp (xs :: xss) = xs.flatMap (fun x => (cp xss).map (x :: ·)) := rfl + +#guard cp [["a","b","c"],["d","e"],["f"]] = + [["a","d","f"],["a","e","f"],["b","d","f"],["b","e","f"],["c","d","f"],["c","e","f"]] + +def linked (e₁ : Edge) : Path → Bool + | [] => true + | e₂ :: _ => target e₁ == source e₂ + +def connected : Path → Bool + | [] => true + | e :: es => linked e es && connected es + +/-- `paths = filter connected · cp`. -/ +def paths₀ (net : Net) : List Path := (cp net).filter connected + +/-- `mcp ← MinWith cost · paths` -/ +def mcp₀ (net : Net) : Path := minWith cost (paths₀ net) + + +/-! ### Fusing `filter connected` and `cp` + +`paths = foldr step [[]]` where `step es ps = [e : p | e ← es, p ← ps, linked e p]`, +which we write in the equivalent form `step es ps = concat [cons e ps | e ← es]`. -/ + +def cons (e : Edge) (ps : List Path) : List Path := + (ps.filter (linked e)).map (e :: ·) + +def step (es : List Edge) (ps : List Path) : List Path := + es.flatMap (fun e => cons e ps) + +def paths (net : Net) : List Path := net.foldr step [[]] + +private lemma filter_connected_map (e : Edge) : + ∀ ps : List Path, (ps.map (e :: ·)).filter connected = cons e (ps.filter connected) := by + intro ps + induction ps with + | nil => rfl + | cons q qs ih => + by_cases h₁ : linked e q = true <;> by_cases h₂ : connected q = true <;> + simp_all [cons, connected] + +/-- The fusion step: `filter connected · cp = foldr step [[]]`. -/ +theorem paths₀_eq_paths : ∀ net : Net, paths₀ net = paths net := by + intro net + induction net with + | nil => rfl + | cons es net ih => + simp only [paths₀] at ih ⊢ + have h : ∀ e : Edge, + ((cp net).map (e :: ·)).filter connected = cons e (paths net) := by + intro e + rw [filter_connected_map, ih] + rw [cp_cons, filter_flatMap] + simp only [h] + rfl + +#guard (paths net₁).length = 27 +#guard (paths net₁) = (paths₀ net₁) + + +/-! ### Introducing thinning + +A greedy algorithm is not possible: the source of a minimum-cost path at one +level may not be among the target vertices of the edges at the next level up. +The thin-introduction law says we may rewrite the specification as + + `mcp ← MinWith cost · ThinBy (⪯) · paths` + +provided `p₁ ⪯ p₂ ⇒ cost p₁ ≤ cost p₂`. The appropriate choice is the *partial* +preorder below: there is no point in keeping a path if there is another path +with the same source vertex and lower cost. -/ + +def le₂ (p₁ p₂ : Path) : Bool := + decide (p₁.head?.map source = p₂.head?.map source ∧ cost p₁ ≤ cost p₂) + +/-- `le₂` is reflexive. -/ +theorem le₂_refl (p : Path) : le₂ p p = true := by simp [le₂] + +/-- `le₂` is transitive. -/ +theorem le₂_trans (p q r : Path) : le₂ p q = true → le₂ q r = true → le₂ p r = true := by + simp only [le₂, decide_eq_true_eq] + rintro ⟨h₁, h₂⟩ ⟨h₃, h₄⟩ + exact ⟨h₁.trans h₃, h₂.trans h₄⟩ + +/-- The proviso of thin introduction: `p₁ ⪯ p₂ ⇒ cost p₁ ≤ cost p₂`. -/ +theorem le₂_cost (p q : Path) (h : le₂ p q = true) : cost p ≤ cost q := by + simp only [le₂, decide_eq_true_eq] at h + exact h.2 + +/-- The proviso of the **thin-filter law**: `p₁ ⪯ p₂ ∧ linked e p₂ ⇒ linked e p₁`. -/ +theorem linked_of_le₂ (e : Edge) (p₁ p₂ : Path) + (h : le₂ p₁ p₂ = true) (h₂ : linked e p₂ = true) : linked e p₁ = true := by + simp only [le₂, decide_eq_true_eq] at h + obtain ⟨hs, -⟩ := h + cases p₁ with + | nil => rfl + | cons f fs => + cases p₂ with + | nil => simp at hs + | cons g gs => + simp only [List.head?_cons, Option.map_some] at hs + have hs' : source f = source g := by simpa using hs + simp only [linked, beq_iff_eq] at h₂ ⊢ + rw [hs'] + exact h₂ + +/-- The proviso of the **thin-map law**: `p₁ ⪯ p₂ ⇒ e : p₁ ⪯ e : p₂`. + Note that no context is needed in this direction. -/ +theorem cons_mono (e : Edge) (p₁ p₂ : Path) (h : le₂ p₁ p₂ = true) : + le₂ (e :: p₁) (e :: p₂) = true := by + simp only [le₂, decide_eq_true_eq] at h ⊢ + refine ⟨rfl, ?_⟩ + simp only [cost_cons] + exact Int.add_le_add_left h.2 _ + +/-- The converse direction of the thin-map law *relies on context*: it holds for + paths `p₁` and `p₂` that are both linked to `e` (and are both empty, or both + non-empty, which in the fold is automatic since all candidates have the same + length). -/ +theorem cons_mono' (e : Edge) (p₁ p₂ : Path) + (h₁ : linked e p₁ = true) (h₂ : linked e p₂ = true) (hne : p₁ = [] ↔ p₂ = []) + (h : le₂ (e :: p₁) (e :: p₂) = true) : le₂ p₁ p₂ = true := by + simp only [le₂, decide_eq_true_eq, cost_cons] at h ⊢ + refine ⟨?_, le_of_add_le_add_left h.2⟩ + cases p₁ with + | nil => + have : p₂ = [] := hne.mp rfl + subst this; rfl + | cons f fs => + cases p₂ with + | nil => exact absurd (hne.mpr rfl) (by simp) + | cons g gs => + simp only [linked, beq_iff_eq] at h₁ h₂ + simp [h₁ ▸ h₂] + + +/-! ### The algorithm + +`tstep es ps ← ThinBy (⪯) (step es ps)`, so that + + `foldr tstep [[]] ← ThinBy (⪯) · foldr step [[]]` + +The claim justifying the fusion is `ThinBy (⪯) (cons e ps) = cons e (ThinBy (⪯) ps)`, +proved with the thin-map and thin-filter laws whose provisos are the three +lemmas above. -/ + +def tstep (es : List Edge) (ps : List Path) : List Path := + thinBy le₂ (step es ps) + +def mcp (net : Net) : Path := minWith cost (net.foldr tstep [[]]) + +-- The first step produces exactly one singleton path per source vertex, +-- just as in the book. +/-- +info: [[(9, 13, 4)], [(10, 14, 2)], [(11, 16, 3)], [(12, 16, 7)]] +-/ +#guard_msgs in +#eval tstep layer₃ [[]] + +-- Each additional step also produces exactly four paths, because each layer +-- has four vertices. +/-- +info: 4 +-/ +#guard_msgs in +#eval (net₁.foldr tstep [[]]).length + +#guard mcp net₁ = [(4,7,2), (7,11,2), (11,16,3)] +#guard cost (mcp net₁) = 7 +#guard mcp net₁ = mcp₀ net₁ + +/- + Running time. The number of paths maintained at each step is at most the + number of vertices in the current layer, so each step costs at most the + product of the number of edges between two layers and the number of vertices + in the lower layer. With at most `k` vertices per layer the running time is + `O(e*k)`, where `e` is the total number of edges; with `d` layers, + `e ≤ (d-1)*k^2`, so thinning takes `O(d*k^3)` steps against Dijkstra's + `O(d^2*k^2)`: thinning wins when the network is deeper than it is wide. + Exercise 10.14 shaves a factor of `k` off, giving an optimal `O(d*k^2)`. + + Exercise: as a further optimisation, tuple paths with their costs to avoid + recomputation of `cost`. +-/ + +end LayeredNetwork + +-- ## Section 10.3 Coin-changing revisited + +namespace CoinChanging + +/-! The greedy algorithm of Chapter 7 is not guaranteed to produce the smallest +number of coins for all denominations; in particular it fails for the United +Regions. Thinning gives an algorithm that works for *any* set of denominations. + +Denominations are taken in increasing order, so that `foldr` considers them in +decreasing order of value. -/ + +abbrev Denom := Nat +abbrev Coin := Nat +abbrev Residue := Nat +abbrev Count := Nat + +/-- A tuple consists of a list of coin counts `[cₖ,...,c₁]` for the + denominations considered so far, the residual amount, and the number of + coins used. -/ +abbrev Tuple := List Coin × Residue × Count + +def coins (t : Tuple) : List Coin := t.1 +def residue (t : Tuple) : Residue := t.2.1 +def count (t : Tuple) : Count := t.2.2 + +instance : Max Tuple := ⟨fun x y => if count x ≤ count y then y else x⟩ +instance : Min Tuple := ⟨fun x y => if count x ≤ count y then x else y⟩ + +def ukds : List Denom := [1,2,5,10,20,50,100,200] +def urds : List Denom := [1,2,5,15,20,50,100] + +/-- At each step the next lower denomination is considered, and every possible + choice for a number of coins of this denomination is considered. -/ +def extend (d : Denom) (t : Tuple) : List Tuple := + (List.range (residue t / d + 1)).map + (fun c => (coins t ++ [c], residue t - c * d, count t + c)) + +def mktuples (n : Nat) (ds : List Denom) : List Tuple := + ds.foldr (fun d ts => ts.flatMap (extend d)) [([], n, 0)] + +-- Unlike Chapter 7, `mktuples` returns all the *partial* tuples, including +-- those with a non-zero residue: `(mktuples 256 ukds).length = 10640485`. + +/-- +info: 293 +-/ +#guard_msgs in +#eval (mktuples 20 ukds).length + +/-- `cost t = (residue t, count t)`, ordered lexicographically: a candidate with + minimum cost is one whose residue is as small as possible and, among such + candidates, one with minimum count. Since there is a denomination of value + 1, a minimum-cost candidate has zero residue and minimum count. -/ +def cost (t : Tuple) : Residue ×ₗ Count := toLex (residue t, count t) + +/-- `mkchange n ← coins · MinWith cost · mktuples n` -/ +def mkchange₀ (n : Nat) (ds : List Denom) : List Coin := + coins (minWith cost (mktuples n ds)) + +/-! ### Introducing thinning + +`mkchange n ← coins · MinWith cost · ThinBy (⪯) · mktuples n`, where `⪯` must +satisfy `t₁ ⪯ t₂ ⇒ cost t₁ ≤ cost t₂`. There is no point in keeping a tuple in +play if there is another tuple whose residue is the same but whose count is +smaller. + +It might be thought that the stronger `residue t₁ ≤ residue t₂ ∧ count t₁ ≤ +count t₂` would do, but that statement is false; see Exercise 10.16. -/ + +def le₃ (t₁ t₂ : Tuple) : Bool := + decide (residue t₁ = residue t₂ ∧ count t₁ ≤ count t₂) + +theorem le₃_refl (t : Tuple) : le₃ t t = true := by simp [le₃] + +theorem le₃_trans (t₁ t₂ t₃ : Tuple) : + le₃ t₁ t₂ = true → le₃ t₂ t₃ = true → le₃ t₁ t₃ = true := by + simp only [le₃, decide_eq_true_eq] + rintro ⟨h₁, h₂⟩ ⟨h₃, h₄⟩ + exact ⟨h₁.trans h₃, h₂.trans h₄⟩ + +/-- The proviso of thin introduction: `t₁ ⪯ t₂ ⇒ cost t₁ ≤ cost t₂`. -/ +theorem le₃_cost (t₁ t₂ : Tuple) (h : le₃ t₁ t₂ = true) : cost t₁ ≤ cost t₂ := by + simp only [le₃, decide_eq_true_eq] at h + obtain ⟨hr, hk⟩ := h + simp only [cost, Prod.Lex.toLex_le_toLex, hr] + right + simpa + +/-! ### Why the usual calculation breaks down + +The distributive law rewrites `ThinBy (⪯) (step d ts)` into +`ThinBy (⪯) (concatMap (ThinBy (⪯) · extend d) ts)`, but the calculation can +proceed no further, because `ThinBy (⪯) · extend d = extend d`: the tuples in +`extend d t` have *different* residues, so thinning can never eliminate any of +them. -/ + +theorem thin_extend_useless (d : Denom) (t : Tuple) : + thinBy le₃ (extend d t) = extend d t := by + sorry -- Exercise: no two tuples in `extend d t` are comparable under `le₃`. + +/-! Instead we back up and prove the *key fact* (10.2) directly: if `t₁ ⪯ t₂`, +then every extension of `t₂` is dominated by some extension of `t₁`. This is +exactly the hypothesis needed by the general fusion theorem of Section 10.5. -/ + +/-- **Key fact (10.2)**: `t₁ ⪯ t₂ ⇒ ∀ e₂ ∈ extend d t₂, ∃ e₁ ∈ extend d t₁, e₁ ⪯ e₂`. -/ +theorem key_fact (d : Denom) (t₁ t₂ : Tuple) (h : le₃ t₁ t₂ = true) : + ∀ e₂ ∈ extend d t₂, ∃ e₁ ∈ extend d t₁, le₃ e₁ e₂ = true := by + simp only [le₃, decide_eq_true_eq] at h + obtain ⟨hr, hk⟩ := h + intro e₂ he₂ + simp only [extend, List.mem_map, List.mem_range] at he₂ + obtain ⟨c, hc, rfl⟩ := he₂ + refine ⟨(coins t₁ ++ [c], residue t₁ - c * d, count t₁ + c), ?_, ?_⟩ + · simp only [extend, List.mem_map, List.mem_range] + exact ⟨c, by rw [hr]; exact hc, rfl⟩ + · simp only [le₃, decide_eq_true_eq, residue, count] + constructor + · simp [residue] at hr + rw [hr] + · exact Nat.add_le_add_right hk c + + +/-! ### The algorithm + +`tstep d ← ThinBy (⪯) · concatMap (extend d)`. The thinning step is more +effective if tuples with the same residue are brought together, which is +achieved by keeping tuples in decreasing order of residue; since `extend` +already produces tuples in that order, it suffices to merge. -/ + +def cmp₃ (t₁ t₂ : Tuple) : Bool := decide (residue t₂ ≤ residue t₁) + +/-- Merging two lists that are ordered according to `cmp`. -/ +def merge2By {α : Type*} (cmp : α → α → Bool) : List α → List α → List α + | [], ys => ys + | xs, [] => xs + | x :: xs, y :: ys => + if cmp x y then x :: merge2By cmp xs (y :: ys) + else y :: merge2By cmp (x :: xs) ys + termination_by xs ys => xs.length + ys.length + +/-- `mergeBy :: (a → a → Bool) → [[a]] → [a]`, left as an exercise in the book. + Merging sublists at each step is what lets us *maintain* the order of the + candidates, which is what makes `thinBy` effective. -/ +def mergeBy {α : Type*} (cmp : α → α → Bool) : List (List α) → List α := + List.foldr (merge2By cmp) [] + +def tstep (d : Denom) (ts : List Tuple) : List Tuple := + thinBy le₃ (mergeBy cmp₃ (ts.map (extend d))) + +def mkchange (n : Nat) (ds : List Denom) : List Coin := + coins (minWith cost (ds.foldr tstep [([], n, 0)])) + +-- `256 = 200 + 50 + 5 + 1`, four coins. +/-- +info: [1, 0, 1, 0, 0, 1, 0, 1] +-/ +#guard_msgs in +#eval mkchange 256 ukds + +-- The greedy algorithm gives `20 + 5 + 5`; thinning finds `15 + 15`. +#guard mkchange 30 urds = [0,0,0,2,0,0,0] + +#guard mkchange 20 ukds = [0,0,0,1,0,0,0,0] + +/- + Running time: `O(n^2 * k)` steps, where `n` is the amount for which change is + required and `k` is the number of denominations. At each step at most `n+1` + candidates are in play, since there is at most one candidate for each residual + amount `0 ≤ r ≤ n`; a candidate with residue `r` has `O(r)` extensions, so + there are `O(n^2)` new candidates before thinning. + + Coin-changing is an instance of the layered-network problem (Figure 10.2): + each layer contains one vertex per residual amount, and the edges correspond + to the choices for the number of coins of the next denomination. This is no + accident: all thinning algorithms involving a fold can be regarded as a + shortest-path problem on a directed acyclic graph. +-/ + +end CoinChanging + end Chapter10 From 2d82228a37d91298a6d1a3170cf26b9b98980ecb Mon Sep 17 00:00:00 2001 From: felipponn Date: Wed, 15 Jul 2026 02:12:08 -0300 Subject: [PATCH 07/16] Add 10.4 --- Fad/Chapter10.lean | 186 +++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 171 insertions(+), 15 deletions(-) diff --git a/Fad/Chapter10.lean b/Fad/Chapter10.lean index 9b512a3..4d46668 100644 --- a/Fad/Chapter10.lean +++ b/Fad/Chapter10.lean @@ -685,6 +685,21 @@ end LayeredNetwork -- ## Section 10.3 Coin-changing revisited +/-- Merging two lists that are ordered according to `cmp`. -/ +def merge2By {α : Type*} (cmp : α → α → Bool) : List α → List α → List α + | [], ys => ys + | xs, [] => xs + | x :: xs, y :: ys => + if cmp x y then x :: merge2By cmp xs (y :: ys) + else y :: merge2By cmp (x :: xs) ys + termination_by xs ys => xs.length + ys.length + +/-- `mergeBy :: (a → a → Bool) → [[a]] → [a]`, left as an exercise in the book. + Merging sublists at each step is what lets us *maintain* the order of the + candidates, which is what makes `thinBy` effective. -/ +def mergeBy {α : Type*} (cmp : α → α → Bool) : List (List α) → List α := + List.foldr (merge2By cmp) [] + namespace CoinChanging /-! The greedy algorithm of Chapter 7 is not guaranteed to produce the smallest @@ -814,21 +829,6 @@ already produces tuples in that order, it suffices to merge. -/ def cmp₃ (t₁ t₂ : Tuple) : Bool := decide (residue t₂ ≤ residue t₁) -/-- Merging two lists that are ordered according to `cmp`. -/ -def merge2By {α : Type*} (cmp : α → α → Bool) : List α → List α → List α - | [], ys => ys - | xs, [] => xs - | x :: xs, y :: ys => - if cmp x y then x :: merge2By cmp xs (y :: ys) - else y :: merge2By cmp (x :: xs) ys - termination_by xs ys => xs.length + ys.length - -/-- `mergeBy :: (a → a → Bool) → [[a]] → [a]`, left as an exercise in the book. - Merging sublists at each step is what lets us *maintain* the order of the - candidates, which is what makes `thinBy` effective. -/ -def mergeBy {α : Type*} (cmp : α → α → Bool) : List (List α) → List α := - List.foldr (merge2By cmp) [] - def tstep (d : Denom) (ts : List Tuple) : List Tuple := thinBy le₃ (mergeBy cmp₃ (ts.map (extend d))) @@ -863,4 +863,160 @@ info: [1, 0, 1, 0, 0, 1, 0, 1] end CoinChanging +-- ## Section 10.4 The knapsack problem + +namespace Knapsack + +/-! The 0/1 knapsack problem: either an item is chosen or it is not. There is +no greedy algorithm for it — packing by decreasing value, by ascending weight, +or by decreasing value/weight ratio all fail in general. The dynamic +programming solution of Chapter 13 is more restrictive, in that it depends on +certain quantities being integers; here we give a thinning algorithm. -/ + +abbrev Name := String +abbrev Value := Nat +abbrev Weight := Nat +abbrev Item := Name × Value × Weight +abbrev Selection := List Name × Value × Weight + +def name (i : Item) : Name := i.1 + +/-- Polymorphic: applies both to items and to selections. -/ +def value {γ : Type} (x : γ × Value × Weight) : Value := x.2.1 + +/-- Polymorphic: applies both to items and to selections. -/ +def weight {γ : Type} (x : γ × Value × Weight) : Weight := x.2.2 + +instance : Max Selection := ⟨fun x y => if value x ≤ value y then y else x⟩ +instance : Min Selection := ⟨fun x y => if value x ≤ value y then x else y⟩ + +/-- The items in the thief's room. -/ +def items₁ : List Item := + [("Laptop", 30, 14), ("Television", 67, 31), ("Jewellery", 19, 8), ("CD collection", 50, 24)] + +def add (i : Item) (sn : Selection) : Selection := + (name i :: sn.1, value i + value sn, weight i + weight sn) + +@[simp] theorem value_add (i : Item) (sn : Selection) : + value (add i sn) = value i + value sn := rfl + +@[simp] theorem weight_add (i : Item) (sn : Selection) : + weight (add i sn) = weight i + weight sn := rfl + +def within (w : Weight) (sn : Selection) : Bool := decide (weight sn ≤ w) + +/-- `selections` returns all `2^n` subsequences of the given list of items. -/ +def selections (its : List Item) : List Selection := + its.foldr (fun i sns => sns.flatMap (fun sn => [sn, add i sn])) [([], 0, 0)] + +/-- `maxWith cost` is dual to `minWith cost`: it selects an element of maximum, + rather than minimum, cost. -/ +def maxWith {γ δ : Type*} [LE δ] [Inhabited γ] [DecidableRel (α := δ) (· ≤ ·)] + (f : γ → δ) (as : List γ) : γ := + Chapter7.foldr1 (fun x y => cond (f y ≤ f x) x y) as + +/-- `swag w ← MaxWith value · filter (within w) · selections` -/ +def swag₀ (w : Weight) (its : List Item) : Selection := + maxWith value ((selections its).filter (within w)) + +#guard (selections items₁).length = 16 + +/-! ### Fusing `filter` with `selections` + +`choices` generates only those selections whose total weight is at most the +carrying capacity of the knapsack. This step alone significantly reduces the +number of selections to consider. -/ + +def extend (w : Weight) (i : Item) (sn : Selection) : List Selection := + [sn, add i sn].filter (within w) + +def choices (w : Weight) (its : List Item) : List Selection := + its.foldr (fun i sns => sns.flatMap (extend w i)) [([], 0, 0)] + +#guard (choices 50 items₁).length = 11 + +/-! ### Introducing thinning + +`swag w ← MaxWith value · ThinBy (⪯) · choices w`, where there is no point in +keeping a selection if there is another selection from the same list of items +with a greater value and a smaller weight. Note `sn₁ ⪯ sn₂ ⇒ value sn₁ ≥ value +sn₂`, which is the proviso of thin introduction in the case of `MaxWith`. -/ + +def le₄ (sn₁ sn₂ : Selection) : Bool := + decide (value sn₂ ≤ value sn₁ ∧ weight sn₁ ≤ weight sn₂) + +theorem le₄_refl (sn : Selection) : le₄ sn sn = true := by simp [le₄] + +theorem le₄_trans (s₁ s₂ s₃ : Selection) : + le₄ s₁ s₂ = true → le₄ s₂ s₃ = true → le₄ s₁ s₃ = true := by + simp only [le₄, decide_eq_true_eq] + rintro ⟨h₁, h₂⟩ ⟨h₃, h₄⟩ + exact ⟨h₃.trans h₁, h₂.trans h₄⟩ + +/-- The proviso of thin introduction for `MaxWith`. -/ +theorem le₄_value (s₁ s₂ : Selection) (h : le₄ s₁ s₂ = true) : value s₂ ≤ value s₁ := by + simp only [le₄, decide_eq_true_eq] at h + exact h.1 + +/-- **Key fact (10.2)** for the knapsack: every good extension of `sn₂` is + dominated by a good extension of `sn₁`. Note that the `filter (within w)` + is harmless precisely because `sn₁` is no heavier than `sn₂`. -/ +theorem key_fact (w : Weight) (i : Item) (sn₁ sn₂ : Selection) (h : le₄ sn₁ sn₂ = true) : + ∀ e₂ ∈ extend w i sn₂, ∃ e₁ ∈ extend w i sn₁, le₄ e₁ e₂ = true := by + simp only [le₄, decide_eq_true_eq] at h + obtain ⟨hv, hw⟩ := h + intro e₂ he₂ + simp only [extend, List.mem_filter, List.mem_cons, + List.not_mem_nil, or_false, within, decide_eq_true_eq] at he₂ + obtain ⟨hmem, hin⟩ := he₂ + rcases hmem with rfl | rfl + · refine ⟨sn₁, ?_, by simp [le₄, hv, hw]⟩ + rw [extend, List.mem_filter] + refine ⟨by simp, ?_⟩ + simp only [within, decide_eq_true_eq] + exact hw.trans hin + · refine ⟨add i sn₁, ?_, ?_⟩ + · rw [extend, List.mem_filter] + refine ⟨by simp, ?_⟩ + simp only [within, decide_eq_true_eq, weight_add] + calc weight i + weight sn₁ ≤ weight i + weight sn₂ := Nat.add_le_add_left hw _ + _ ≤ w := by simpa using hin + · simp only [le₄, decide_eq_true_eq, value_add, weight_add] + exact ⟨Nat.add_le_add_left hv _, Nat.add_le_add_left hw _⟩ + +/-! ### The algorithm + +The thinning step is more effective if the selections are kept in order; since +`extend` produces selections in increasing order of weight, we choose that. -/ + +def cmp₄ (s₁ s₂ : Selection) : Bool := decide (weight s₁ ≤ weight s₂) + +def tstep (w : Weight) (i : Item) (sns : List Selection) : List Selection := + thinBy le₄ (mergeBy cmp₄ (sns.map (extend w i))) + +def swag (w : Weight) (its : List Item) : Selection := + maxWith value (its.foldr (tstep w) [([], 0, 0)]) + +-- The best haul is `Jewellery + Laptop + CDs`, of value 99 and weight 46 — +-- beating `Television + Laptop` (97) and `Jewellery + Television` (86). +#guard swag 50 items₁ = (["Laptop", "Jewellery", "CD collection"], 99, 46) + +#guard swag 50 items₁ = swag₀ 50 items₁ + +/- + Running time. If all weights are integers, each thinning step brings + selections of equal weight together and eliminates all but one of them, + maintaining a list of at most `w+1` selections; the list is computed in `Θ(w)` + steps, so with `n` items the running time is `O(n*w)`. That only *appears* to + be linear: if weights are arbitrary positive reals there is no guarantee that + only `w+1` selections are maintained — all `2^n` selections might have to be + kept, each with a different total weight and value. + + Exercise 10.21: the other reasonable way to define `selections`. + Exercises: the integer knapsack problem, and the fractional knapsack problem + (for which a greedy algorithm *does* work). +-/ + +end Knapsack + end Chapter10 From 50c1cfebf1ebe3c864b1a0bef81e9fc60b866b74 Mon Sep 17 00:00:00 2001 From: felipponn Date: Wed, 15 Jul 2026 02:48:54 -0300 Subject: [PATCH 08/16] Add 10.5 --- Fad/Chapter10.lean | 125 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 125 insertions(+) diff --git a/Fad/Chapter10.lean b/Fad/Chapter10.lean index 4d46668..946c0f7 100644 --- a/Fad/Chapter10.lean +++ b/Fad/Chapter10.lean @@ -1019,4 +1019,129 @@ def swag (w : Weight) (its : List Item) : Selection := end Knapsack +-- ## Section 10.5 A general thinning algorithm + +/-! The last two examples are very similar, so we end by solving an abstract +problem that captures all of the essential ideas behind thinning when +`candidates` is expressed as + + `candidates = foldr (concatMap · extend) [anon]` + +and the specification has the form + + `best ← MinWith cost · filter good · candidates` + +There are four ritual steps in calculating a thinning algorithm. We use the +section variable `a` for the type of candidates. -/ + +section General + +variable {D : Type} + +def candidates (ext : D → a → List a) (anon : a) (ds : List D) : List a := + ds.foldr (fun d xs => xs.flatMap (ext d)) [anon] + +/-- `goodext d x = filter good (extend d x)`. -/ +def goodext (good : a → Bool) (ext : D → a → List a) (d : D) (x : a) : List a := + (ext d x).filter good + +def gstep (ge : D → a → List a) (d : D) (xs : List a) : List a := + xs.flatMap (ge d) + +/-- Filtering before a `flatMap` changes nothing when every filtered-out element + already maps to the empty list. -/ +theorem flatMap_filter {α β : Type*} (good : α → Bool) (f : α → List β) + (hbad : ∀ x, good x = false → f x = []) (l : List α) : + l.flatMap f = (l.filter good).flatMap f := by + induction l with + | nil => rfl + | cons x xs ih => + by_cases hx : good x = true + · simp [List.flatMap_cons, hx, ih] + · simp only [Bool.not_eq_true] at hx + simp [List.flatMap_cons, hx, hbad x hx, ih] + +/-- **Step 1.** Fuse `filter good` with `candidates`. This is possible if a bad + candidate has no good extension; and `anon` has to be good, otherwise there + are no good candidates at all. -/ +theorem filter_good_candidates (good : a → Bool) (ext : D → a → List a) (anon : a) + (hgood : ∀ (d : D) (x y : a), y ∈ ext d x → good y = true → good x = true) + (hanon : good anon = true) : + ∀ ds : List D, (candidates ext anon ds).filter good + = ds.foldr (gstep (goodext good ext)) [anon] := by + intro ds + induction ds with + | nil => simp [candidates, hanon] + | cons d ds ih => + have hbad : ∀ x : a, good x = false → (goodext good ext d) x = [] := by + intro x hx + simp only [goodext, List.filter_eq_nil_iff] + intro y hy hgy + rw [hgood d x y hy hgy] at hx + exact Bool.noConfusion hx + show ((candidates ext anon ds).flatMap (ext d)).filter good = _ + rw [filter_flatMap] + show (candidates ext anon ds).flatMap (goodext good ext d) = _ + rw [flatMap_filter good (goodext good ext d) hbad, ih] + rfl + +/-- **Step 2** is thin introduction: with `x ⪯ y ⇒ cost x ≤ cost y` for all good + candidates, `thin_introduction` refines the specification to + + `best ← MinWith cost · ThinBy (⪯) · foldr step [anon]` + + **Step 3** is to fuse `ThinBy (⪯)` with the `foldr`. With + `tstep d ← ThinBy (⪯) · step d`, this needs the fusion condition + + `ThinBy (⪯) · step d · ThinBy (⪯) ← ThinBy (⪯) · step d` + + which is (10.1) of Section 10.3. It follows from the assumption below, + which is the abstract form of the key fact (10.2). -/ +def KeyFact (r : a → a → Prop) (ge : D → a → List a) : Prop := + ∀ (d : D) (x y : a), r x y → ∀ v ∈ ge d y, ∃ u ∈ ge d x, r u v + +/-- **(10.1)**. If `us` is a thinning of `ts` and `vs` is a thinning of + `step d us`, then `vs` is a thinning of `step d ts`. Thinning before a step + loses nothing. -/ +theorem thin_step_fusion (r : a → a → Prop) + (htrans : ∀ x y z, r x y → r y z → r x z) + (ge : D → a → List a) (hkey : KeyFact r ge) + (d : D) (ts us vs : List a) + (hus : ThinBy r ts us) + (hvs : ThinBy r (gstep ge d us) vs) : + ThinBy r (gstep ge d ts) vs := by + obtain ⟨hsub, hdom⟩ := hus + obtain ⟨hsub', hdom'⟩ := hvs + constructor + · -- `vs <+ step d us <+ step d ts`, since `xs <+ ys ⇒ step d xs <+ step d ys` + exact hsub'.trans (hsub.flatMap (ge d)) + · -- `∀ w ∈ step d ts, ∃ v ∈ vs, v ⪯ w` + intro w hw + simp only [gstep, List.mem_flatMap] at hw + obtain ⟨t, ht, hwt⟩ := hw + obtain ⟨u, hu, hru⟩ := hdom t ht + obtain ⟨e, he, hre⟩ := hkey d u t hru w hwt + have hemem : e ∈ gstep ge d us := List.mem_flatMap.2 ⟨u, hu, he⟩ + obtain ⟨v, hv, hrv⟩ := hdom' e hemem + exact ⟨v, hv, htrans v e w hrv hre⟩ + +/-- **Step 4.** Make thinning more effective by keeping the candidates in order, + merging sublists at each step rather than sorting. This is the general + algorithm: + + `best = minWith cost · foldr step [anon]` + ` where step d = thinBy (⪯) · mergeBy cmp · map (filter good · extend d)` + ` cmp x y = value x ≤ value y` + + It is possible, with more or less effort, to reformulate the three problems + of this chapter as instances of this scheme; what matters is that the + derivation of a thinning algorithm follows a more or less standard path. -/ +def best {β : Type} [LE β] [DecidableRel (α := β) (· ≤ ·)] + (cost : a → β) (le cmp : a → a → Bool) (good : a → Bool) + (ext : D → a → List a) (anon : a) (ds : List D) : a := + minWith cost + (ds.foldr (fun d xs => thinBy le (mergeBy cmp (xs.map (goodext good ext d)))) [anon]) + +end General + end Chapter10 From 64623a59b161799008ae9e7659c358a7d43c7e41 Mon Sep 17 00:00:00 2001 From: felipponn Date: Wed, 15 Jul 2026 13:56:58 -0300 Subject: [PATCH 09/16] Update text --- Fad/Chapter10.lean | 47 +++------------------------------------------- 1 file changed, 3 insertions(+), 44 deletions(-) diff --git a/Fad/Chapter10.lean b/Fad/Chapter10.lean index 946c0f7..e3c08fd 100644 --- a/Fad/Chapter10.lean +++ b/Fad/Chapter10.lean @@ -667,20 +667,6 @@ info: 4 #guard cost (mcp net₁) = 7 #guard mcp net₁ = mcp₀ net₁ -/- - Running time. The number of paths maintained at each step is at most the - number of vertices in the current layer, so each step costs at most the - product of the number of edges between two layers and the number of vertices - in the lower layer. With at most `k` vertices per layer the running time is - `O(e*k)`, where `e` is the total number of edges; with `d` layers, - `e ≤ (d-1)*k^2`, so thinning takes `O(d*k^3)` steps against Dijkstra's - `O(d^2*k^2)`: thinning wins when the network is deeper than it is wide. - Exercise 10.14 shaves a factor of `k` off, giving an optimal `O(d*k^2)`. - - Exercise: as a further optimisation, tuple paths with their costs to avoid - recomputation of `cost`. --/ - end LayeredNetwork -- ## Section 10.3 Coin-changing revisited @@ -694,7 +680,7 @@ def merge2By {α : Type*} (cmp : α → α → Bool) : List α → List α → L else y :: merge2By cmp (x :: xs) ys termination_by xs ys => xs.length + ys.length -/-- `mergeBy :: (a → a → Bool) → [[a]] → [a]`, left as an exercise in the book. +/-- `mergeBy :: (a → a → Bool) → [[a]] → [a]` Merging sublists at each step is what lets us *maintain* the order of the candidates, which is what makes `thinBy` effective. -/ def mergeBy {α : Type*} (cmp : α → α → Bool) : List (List α) → List α := @@ -794,9 +780,10 @@ proceed no further, because `ThinBy (⪯) · extend d = extend d`: the tuples in `extend d t` have *different* residues, so thinning can never eliminate any of them. -/ +-- Exercise: no two tuples in `extend d t` are comparable under `le₃`. theorem thin_extend_useless (d : Denom) (t : Tuple) : thinBy le₃ (extend d t) = extend d t := by - sorry -- Exercise: no two tuples in `extend d t` are comparable under `le₃`. + sorry /-! Instead we back up and prove the *key fact* (10.2) directly: if `t₁ ⪯ t₂`, then every extension of `t₂` is dominated by some extension of `t₁`. This is @@ -847,20 +834,6 @@ info: [1, 0, 1, 0, 0, 1, 0, 1] #guard mkchange 20 ukds = [0,0,0,1,0,0,0,0] -/- - Running time: `O(n^2 * k)` steps, where `n` is the amount for which change is - required and `k` is the number of denominations. At each step at most `n+1` - candidates are in play, since there is at most one candidate for each residual - amount `0 ≤ r ≤ n`; a candidate with residue `r` has `O(r)` extensions, so - there are `O(n^2)` new candidates before thinning. - - Coin-changing is an instance of the layered-network problem (Figure 10.2): - each layer contains one vertex per residual amount, and the edges correspond - to the choices for the number of coins of the next denomination. This is no - accident: all thinning algorithms involving a fold can be regarded as a - shortest-path problem on a directed acyclic graph. --/ - end CoinChanging -- ## Section 10.4 The knapsack problem @@ -1003,20 +976,6 @@ def swag (w : Weight) (its : List Item) : Selection := #guard swag 50 items₁ = swag₀ 50 items₁ -/- - Running time. If all weights are integers, each thinning step brings - selections of equal weight together and eliminates all but one of them, - maintaining a list of at most `w+1` selections; the list is computed in `Θ(w)` - steps, so with `n` items the running time is `O(n*w)`. That only *appears* to - be linear: if weights are arbitrary positive reals there is no guarantee that - only `w+1` selections are maintained — all `2^n` selections might have to be - kept, each with a different total weight and value. - - Exercise 10.21: the other reasonable way to define `selections`. - Exercises: the integer knapsack problem, and the fractional knapsack problem - (for which a greedy algorithm *does* work). --/ - end Knapsack -- ## Section 10.5 A general thinning algorithm From 2ccac9b8ad1931a51bc76fa35722b948a00ff7e7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Lu=C3=ADs=20Felipe=20Marques?= <100888705+felipponn@users.noreply.github.com> Date: Wed, 15 Jul 2026 13:57:15 -0300 Subject: [PATCH 10/16] Mark completed exercises in README --- README.md | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/README.md b/README.md index b9eef61..7e4aa7c 100644 --- a/README.md +++ b/README.md @@ -106,13 +106,13 @@ Along the way, readers gain experience not only in algorithm design, but also in ### Part Four: Thinning Algorithms -1. Introduction to thinning (@felipponn) +1. Introduction to thinning - - [ ] 10.1 Theory - - [ ] 10.2 Paths in a layered network - - [ ] 10.3 Coin‑changing revisited - - [ ] 10.4 The knapsack problem - - [ ] 10.5 A general thinning algorithm + - [x] 10.1 Theory + - [x] 10.2 Paths in a layered network + - [x] 10.3 Coin‑changing revisited + - [x] 10.4 The knapsack problem + - [x] 10.5 A general thinning algorithm - [ ] Exercises 2. Segments and subsequences @@ -131,9 +131,9 @@ Along the way, readers gain experience not only in algorithm design, but also in ### Part Five: Dynamic Programming -1. Efficient recursions (@BXimenaGomez123) +1. Efficient recursions - - [ ] 13.1 Two numeric examples + - [x] 13.1 Two numeric examples - [ ] 13.2 Knapsack revisited - [ ] 13.3 Minimum‑cost edit sequences - [ ] 13.4 Longest common subsequence revisited From f2c5000a1a473b4a548700797589aae18d170d3c Mon Sep 17 00:00:00 2001 From: BXimenaGomez123 Date: Wed, 15 Jul 2026 14:03:53 -0300 Subject: [PATCH 11/16] finishing 13.2 --- Fad/Chapter13.lean | 212 ++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 211 insertions(+), 1 deletion(-) diff --git a/Fad/Chapter13.lean b/Fad/Chapter13.lean index 6740db9..1856eb9 100644 --- a/Fad/Chapter13.lean +++ b/Fad/Chapter13.lean @@ -1,7 +1,9 @@ import Fad.Chapter1 +import Fad.Chapter10 import Fad.API namespace Chapter13 + open Chapter1 (scanr₀) @@ -170,8 +172,10 @@ def bin₁T : Nat → Nat → TimeM Int --#eval bin₁ 6 3 --#eval bin₁T 6 3 +--#eval [4, 8, 12, 16].map fun n =>((n, n / 2), (bin₁T n (n / 2)).time) +-- For bin2 we need a two dimentianl tab function def bin₂ (n r : Nat) : Int := Id.run do let mut a : Array ((Nat × Nat) × Int) := #[] for i in [0:n+1] do @@ -187,14 +191,220 @@ def bin₂ (n r : Nat) : Int := Id.run do --#eval bin₂ 6 3 + def apl {α : Type} : Nat → (List α → List α) → List α → List α | 0, _, acc => acc | n + 1, f, acc => apl n f (f acc) -def bin₃ (n r : Nat) : Int := +def aplT {α : Type} : Nat → (α → TimeM α) → α → TimeM α +| 0, _, acc => TimeM.pure acc +| n + 1, f, acc => do + let next ← f acc + aplT n f next + +-- scanr0 of chapter 1 always add the initial accumulator q₀ to the end. + +--#eval scanr₀ (· + ·) 0 [1, 1, 1, 1] +--It ends in 0, but in the book the example takes this values [4,3,2,1] +--So we will defind scar1 + +def scanr₁ {α : Type} (f : α → α → α) (xs : List α) : List α := + match xs.reverse with + | [] => [] + | q₀ :: rest => + scanr₀ f q₀ rest.reverse + +def scanr₁T {α : Type} + (f : α → α → α) (xs : List α) : TimeM (List α) := + match xs.reverse with + | [] => + TimeM.pure [] + | q₀ :: rest => + ✓ (scanr₀ f q₀ rest.reverse), rest.length + +--#eval scanr₁ (· + ·) [1, 1, 1, 1] + +def bin₃Antigo (n r : Nat) : Int := let row := apl (n - r) (scanr₀ (· + ·) 0) (List.replicate (r + 1) 1) row.headD 1 +--#eval bin₃Antigo 6 3 + +def bin₃ (n r : Nat) : Int := + let row := + apl (n - r) + (scanr₁ (· + ·)) + (List.replicate (r + 1) 1) + row.headD 1 + +def bin₃T (n r : Nat) : TimeM Int := do + let row ← + aplT (n - r) + (scanr₁T (· + ·)) + (List.replicate (r + 1) 1) + TimeM.pure (row.headD 1) + + +--#eval [10, 20, 40, 80].map fun n => ((n, n / 2), (bin₃T n (n / 2)).time) --#eval bin₃ 6 3 +-- # Section 13.2 + +namespace Knapsack + +open Chapter10.Knapsack + (Name Value Weight Item Selection name value weight add maxWith items₁) + +private def emptySelection : Selection := + ([], 0, 0) + +def choices : Weight → List Item → List Selection +| _, [] => [emptySelection] +| w, i :: its => + if w < weight i then + choices w its + else + let withoutI := choices w its + let withI := (choices (w - weight i) its).map (add i) + withoutI ++ withI + +def choicesT : Weight → List Item → TimeM (List Selection) +| _, [] => TimeM.pure [emptySelection] +| w, i :: its => do + -- `decide` converts the decidable proposition into a `Bool` before it is + -- placed inside `TimeM`. + let tooHeavy ← (✓ (decide (w < weight i))) + match tooHeavy with + | true => choicesT w its + | false => do + let withoutI ← choicesT w its + let remaining ← choicesT (w - weight i) its + ✓ (withoutI ++ remaining.map (add i)) + +--#guard (choices 50 items₁).length = 11 + + +def better (sn₁ sn₂ : Selection) : Selection := + if value sn₂ ≤ value sn₁ then sn₁ else sn₂ + +def betterT (sn₁ sn₂ : Selection) : TimeM Selection := + ✓ (better sn₁ sn₂) + +private def maxWithValueT : List Selection → TimeM Selection +| [] => TimeM.pure emptySelection +| sn :: sns => + let rec go : Selection → List Selection → TimeM Selection + | best, [] => TimeM.pure best + | best, candidate :: rest => do + let winner ← betterT best candidate + go winner rest + go sn sns + +def swag₀ (w : Weight) (its : List Item) : Selection := + maxWith value (choices w its) + +def swag₀T (w : Weight) (its : List Item) : TimeM Selection := do + let sns ← choicesT w its + maxWithValueT sns + +--#guard swag₀ 50 items₁ = (["Laptop", "Jewellery", "CD collection"], 99, 46) +--#guard (swag₀T 50 items₁).ret = swag₀ 50 items₁ + +def swag₁ : Weight → List Item → Selection +| _, [] => emptySelection +| w, i :: its => + if w < weight i then + swag₁ w its + else + better + (swag₁ w its) + (add i (swag₁ (w - weight i) its)) + +def swag₁T : Weight → List Item → TimeM Selection +| _, [] => TimeM.pure emptySelection +| w, i :: its => do + let tooHeavy ← (✓ (decide (w < weight i))) + match tooHeavy with + | true => swag₁T w its + | false => do + let withoutI ← swag₁T w its + let bestForRemaining ← swag₁T (w - weight i) its + betterT withoutI (add i bestForRemaining) + +--#guard swag₁ 50 items₁ = swag₀ 50 items₁ +--#guard (swag₁T 50 items₁).ret = swag₁ 50 items₁ + +-- ## Dynamic programming with one row + +private def foldrT {α β : Type} + (f : α → β → TimeM β) (e : β) : List α → TimeM β +| [] => TimeM.pure e +| x :: xs => do + let acc ← foldrT f e xs + f x acc + +def step (w : Weight) (i : Item) (row : List Selection) : List Selection := + let wi := weight i + let shifted := (row.drop wi).map (add i) + List.zipWith better row shifted ++ row.drop (w + 1 - wi) + +def stepT (w : Weight) (i : Item) (row : List Selection) : + TimeM (List Selection) := + -- The abstract cost is one unit for every position in the row. + ✓ (step w i row), row.length + +def swag₂ (w : Weight) (its : List Item) : Selection := + let start := List.replicate (w + 1) emptySelection + let row := its.foldr (step w) start + row.headD emptySelection + +def swag₂T (w : Weight) (its : List Item) : TimeM Selection := do + let start := List.replicate (w + 1) emptySelection + let row ← foldrT (stepT w) start its + TimeM.pure (row.headD emptySelection) + +--#guard swag₂ 50 items₁ = swag₀ 50 items₁ +--#guard (swag₂T 50 items₁).ret = swag₂ 50 items₁ +--#guard (swag₂T 50 items₁).time = items₁.length * (50 + 1) + +--#eval (Chapter13.Knapsack.swag₀T 50 Chapter10.Knapsack.items₁) +--#eval (Chapter13.Knapsack.swag₁T 50 Chapter10.Knapsack.items₁) +--#eval (Chapter13.Knapsack.swag₂T 50 Chapter10.Knapsack.items₁) + +end Knapsack + +-- # Section 13.3 + +inductive Op where + | copy : Char → Op + | replace : Char → Char → Op + | delete : Char → Op + | insert : Char → Op +deriving Repr, BEq + +abbrev Edit := List Op + +def ecost : Op → Nat +| .copy _ => 0 +| .replace _ _ => 3 +| .delete _ => 2 +| .insert _ => 2 + +def cost : Edit → Nat +| [] => 0 +| op :: ops => ecost op + cost ops + +def pick (x y : Char) : Op := + if x = y then Op.copy x else Op.replace x y + +def minByCost : List Edit → Edit +| [] => [] +| e :: es => + es.foldl + (fun best candidate => + if cost candidate < cost best then candidate else best) + e + + + end Chapter13 From 36fe4551391d9d7020a909154b6ac694cdb010e3 Mon Sep 17 00:00:00 2001 From: BXimenaGomez123 Date: Wed, 15 Jul 2026 14:22:56 -0300 Subject: [PATCH 12/16] Adding thunk comparation --- Fad/Chapter13.lean | 38 +++++++++++++++++++++++++++++++++++++- 1 file changed, 37 insertions(+), 1 deletion(-) diff --git a/Fad/Chapter13.lean b/Fad/Chapter13.lean index 1856eb9..548c52e 100644 --- a/Fad/Chapter13.lean +++ b/Fad/Chapter13.lean @@ -27,7 +27,43 @@ def fib₀T : Nat → TimeM Int -- The complexity is exponential -- #eval [5, 10, 15, 20].map fun n => (n, (fib₀T n).time) --- Haskell is a lazy language so we will append another tab function using thunk to get the O(n) complexity +--Litaral translation of tab and fib1 + +def tabAntigo (f : Nat → Int) (lo hi : Nat) : Array Int := + (List.range (hi - lo + 1)).map (fun i => f (lo + i)) |>.toArray + +def tabAntigoT (f : Nat → TimeM Int) (lo hi : Nat) : + TimeM (Array Int) := do + let indices := List.range (hi - lo + 1) + + let values ← indices.mapM (fun i => f (lo + i)) + + TimeM.tick (values.toArray) (2 * values.length) + +def fib₁Antigo (n : Nat) : Int := + let rec a : Nat → Int := + fun i => if i ≤ 1 then i else a (i - 1) + a (i - 2) + let arr := tabAntigo a 0 n + arr[n]! + +def fib₁AntigoT (n : Nat) : TimeM Int := + let rec aT : Nat → TimeM Int + | 0 => TimeM.pure 0 + | 1 => TimeM.pure 1 + | k + 2 => do + let x ← aT (k + 1) + let y ← aT k + ✓ (x + y) + do + let arr ← tabAntigoT aT 0 n + ✓ (arr[n]!) + +--#eval (fib₁AntigoT 10).ret +--#eval (fib₁AntigoT 10).time +--The Haskell example in the bool was supposed to be O(n), +--but given that Haskell is lazy, the complexity is O(n^2) + +-- So we will append another tab function using thunk to get the O(n) complexity private def badDependency [Inhabited α] : Thunk α := Thunk.mk fun _ => panic! "undefined lazy-array entry" From 1c80d8e9f76e8fe790ae32de795dea98cab89180 Mon Sep 17 00:00:00 2001 From: felipponn Date: Fri, 21 Aug 2026 02:14:06 -0300 Subject: [PATCH 13/16] feat: add query-model alternative to TimeM for complexity (Chapter 2) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add a self-contained query model (free monad `Prog` + `Model` + `eval`) as an alternative to `TimeM` for measuring algorithm complexity, so the two approaches can be compared in practice. The query model of query-model-tutorial.md lives in CSLib PR #372, which is still open and not present at the pinned cslib revision, so it is vendored here as `Fad.QueryModel`: - `Prog Q R`: a program as a tree of queries (a free monad); cost is assigned afterwards by a `Model`, never carried by the algorithm (no cheating). - `Model.evalQuery`/`Model.cost`, `Prog.eval : Prog Q R → Model Q Cost → R × Cost`. - `eval_bind`/`runtime_bind`/`result_bind`: the query-model analogues of `TimeM.time_of_bind`/`ret_bind`, driving the complexity proofs. - `UpperBound`/`LowerBound` predicates. `Fad.Chapter2Query` reimplements the running-time examples of `Fad.Chapter2` (`append`, `concat₁`, `concat₂`) in the query model, with the analogous complexity theorems (`concat₁_runtime`: Θ(m·n); `concat₂_runtime`: Θ(m²·n)), and `#eval`s that measure the same program under several cost models — the thing `TimeM` cannot do without rewriting the algorithm. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01AbkMyCwYRAiUy3NFwn9M4f --- Fad.lean | 2 + Fad/Chapter2-Query.lean | 209 ++++++++++++++++++++++++++++++++++++++++ Fad/QueryModel.lean | 155 +++++++++++++++++++++++++++++ 3 files changed, 366 insertions(+) create mode 100644 Fad/Chapter2-Query.lean create mode 100644 Fad/QueryModel.lean diff --git a/Fad.lean b/Fad.lean index 3db5ac3..bb5ac73 100644 --- a/Fad.lean +++ b/Fad.lean @@ -9,6 +9,8 @@ import Fad.«Chapter1-Ex» import Fad.Chapter2 import Fad.«Chapter2-Ex» +import Fad.QueryModel +import Fad.«Chapter2-Query» import Fad.Chapter3 import Fad.«Chapter3-Ex» diff --git a/Fad/Chapter2-Query.lean b/Fad/Chapter2-Query.lean new file mode 100644 index 0000000..599b54c --- /dev/null +++ b/Fad/Chapter2-Query.lean @@ -0,0 +1,209 @@ +import Fad.QueryModel + +/-! +# Chapter 2 complexity examples, in the *query model* + +This module reimplements the running-time examples of `Fad.Chapter2` +(`append`, `concat₁`, `concat₂`) using the query model of `Fad.QueryModel` +instead of the `TimeM` monad, so the two styles can be compared directly. + +The correspondence is: + +| `TimeM` version (`Chapter2`) | query-model version (here) | +|-----------------------------------------|---------------------------------------| +| cost is *carried* by the computation | cost is *assigned* by a `Model` | +| `✓ e` / `✓[c] e` ticks inline | a query node is emitted; its cost | +| | comes from the model, not the program | +| `.time` reads the accumulated cost | `.runtime model` evaluates the tree | +| one fixed cost model | the same program, many models | + +The complexity theorems (`concat₁_runtime`, `concat₂_runtime`) are the +query-model analogues of `Chapter2.concat₁''_time` and +`Chapter2.concat₂'_time`; compare the proofs. +-/ + +set_option autoImplicit false + +namespace Chapter2Query + +open QueryModel +open QueryModel.Prog (lift) + +/-! ## `append` + +The `TimeM` version (`Chapter2.append'`) prepends the head of `xs` one element +at a time, charging one tick per element: + +``` +def append' : List a → List a → TimeM Nat (List a) + | [], ys => pure ys + | x :: xs, ys => do ✓ return x :: (← append' xs ys) +``` + +Here each prepend is a *query* `AppendOp.step`; how much it costs is decided by +the model, not written into the algorithm. -/ + +inductive AppendOp (a : Type) : Type → Type where + | step : a → List a → AppendOp a (List a) -- prepend the head onto the tail + +def append {a : Type} : List a → List a → Prog (AppendOp a) (List a) + | [], ys => pure ys + | x :: xs, ys => do + let r ← append xs ys + lift (AppendOp.step x r) + +/-- The natural model: a `step` prepends, and costs one unit — matching the +single `✓` per element in `Chapter2.append'`. -/ +def stepCost {a : Type} : Model (AppendOp a) Nat where + evalQuery | .step x xs => x :: xs + cost | .step _ _ => 1 + +/-- A *different* model for the *same* program: charge two units per prepend +(e.g. two memory writes). Impossible to express with `TimeM` without editing +the algorithm — the whole point of the query model. -/ +def stepCost2 {a : Type} : Model (AppendOp a) Nat where + evalQuery | .step x xs => x :: xs + cost | .step _ _ => 2 + +-- model equations (kept as simp lemmas so proofs never have to *unfold* the +-- model, which would break matching against the induction hypothesis) +@[simp] theorem stepCost_eval {a : Type} (x : a) (xs : List a) : + stepCost.evalQuery (AppendOp.step x xs) = x :: xs := rfl +@[simp] theorem stepCost_cost {a : Type} (x : a) (xs : List a) : + stepCost.cost (AppendOp.step x xs) = 1 := rfl +@[simp] theorem stepCost2_cost {a : Type} (x : a) (xs : List a) : + stepCost2.cost (AppendOp.step x xs) = 2 := rfl + +/-- The program still computes the ordinary append. -/ +@[simp] theorem append_result {a : Type} (xs ys : List a) : + (append xs ys).result stepCost = xs ++ ys := by + induction xs with + | nil => rfl + | cons x xs ih => simp [append, ih] + +/-- Cost under `stepCost` is the length of the first list — `Θ(|xs|)`. -/ +theorem append_runtime {a : Type} (xs ys : List a) : + (append xs ys).runtime stepCost = xs.length := by + induction xs with + | nil => rfl + | cons x xs ih => simp [append, ih] + +/-- The same program, measured under `stepCost2`, costs twice as much — no +change to `append` itself. -/ +theorem append_runtime2 {a : Type} (xs ys : List a) : + (append xs ys).runtime stepCost2 = 2 * xs.length := by + induction xs with + | nil => rfl + | cons x xs ih => + simp only [append, Prog.bind_eq, Prog.runtime_bind, Prog.runtime_lift, + stepCost2_cost, List.length_cons, ih] + omega + + +/-! ## `concat` + +`Chapter2.concat₁''` folds append from the right, charging `xs.length` for each +append (`✓[xs.length]`). We model one append of a length-`k` list as a single +query whose *cost is `k`*, decided by the model. -/ + +inductive ConcatOp (a : Type) : Type → Type where + | app : List a → List a → ConcatOp a (List a) -- xs ++ ys + +def concatCost {a : Type} : Model (ConcatOp a) Nat where + evalQuery | .app xs ys => xs ++ ys + cost | .app xs _ => xs.length + +@[simp] theorem concatCost_eval {a : Type} (xs ys : List a) : + concatCost.evalQuery (ConcatOp.app xs ys) = xs ++ ys := rfl +@[simp] theorem concatCost_cost {a : Type} (xs ys : List a) : + concatCost.cost (ConcatOp.app xs ys) = xs.length := rfl + +/-- Right fold — mirrors `Chapter2.concat₁''`. -/ +def concat₁ {a : Type} : List (List a) → Prog (ConcatOp a) (List a) + | [] => pure [] + | xs :: xss => do + let ys ← concat₁ xss + lift (ConcatOp.app xs ys) + +/-- Left fold, cost-charging on the accumulator — mirrors `Chapter2.concat₂''`. +Each step appends the accumulator (which keeps growing) onto the next block, so +the accumulator length is what gets charged. -/ +def concat₂ {a : Type} : List (List a) → List a → Prog (ConcatOp a) (List a) + | [], acc => pure acc + | xs :: xss, acc => do + let acc' ← lift (ConcatOp.app acc xs) + concat₂ xss acc' + +/-- if `xss` is a list of `m` lists each of length `n`, then `concat₁` is +`Θ(m * n)`. Query-model analogue of `Chapter2.concat₁''_time`. -/ +theorem concat₁_runtime {a : Type} (xss : List (List a)) + (n : Nat) (h : ∀ xs ∈ xss, xs.length = n) : + (concat₁ xss).runtime concatCost = xss.length * n := by + induction xss with + | nil => simp [concat₁] + | cons xs xss' ih => + have h₁ : xs.length = n := h xs List.mem_cons_self + have h₂ : ∀ ys ∈ xss', ys.length = n := + fun ys hys => h ys (List.mem_cons_of_mem xs hys) + simp only [concat₁, Prog.bind_eq, Prog.runtime_bind, Prog.runtime_lift, + concatCost_cost, List.length_cons, ih h₂, h₁] + ring + +/-- The result of `concat₁` really is the concatenation (it does not cheat). -/ +@[simp] theorem concat₁_result {a : Type} (xss : List (List a)) : + (concat₁ xss).result concatCost = xss.flatten := by + induction xss with + | nil => rfl + | cons xs xss' ih => simp [concat₁, ih] + +/-- Cost of the left-associated fold: `concat₂` over `m` blocks of length `n` +starting from an accumulator of length `a₀` costs `a₀ * m + n * m * (m-1) / 2`. +We state it in the doubled, subtraction-free form used in +`Chapter2.concat₂'_time`: it is `Θ(m² * n)`. -/ +theorem concat₂_runtime {a : Type} (xss : List (List a)) + (n : Nat) (h : ∀ xs ∈ xss, xs.length = n) + (acc : List a) : + (2 * (concat₂ xss acc).runtime concatCost : Int) + = 2 * acc.length * xss.length + n * xss.length * (xss.length - 1) := by + induction xss generalizing acc with + | nil => simp [concat₂] + | cons xs xss' ih => + have h₁ : xs.length = n := h xs List.mem_cons_self + have h₂ : ∀ ys ∈ xss', ys.length = n := + fun ys hys => h ys (List.mem_cons_of_mem xs hys) + -- one fold step charges the current accumulator length, then recurses on + -- the (grown) accumulator + have hstep : (concat₂ (xs :: xss') acc).runtime concatCost + = acc.length + (concat₂ xss' (acc ++ xs)).runtime concatCost := by + simp [concat₂] + have hIH := ih h₂ (acc ++ xs) + rw [List.length_append, h₁] at hIH + rw [hstep, List.length_cons] + push_cast at hIH ⊢ + linear_combination hIH + + +/-! ## Practical comparison + +The pay-off of the query model over `TimeM`: the *same* program is measured +under different cost models, with no change to the algorithm. Under `TimeM` +each of these would need a separately-written function. + +`.eval` returns the `(result, cost)` pair; `.result`/`.runtime` project them. -/ + +-- `append` costs one per element under `stepCost`, two under `stepCost2`, +-- but computes the same list either way: +#eval (append [1, 2, 3] [4, 5]).eval stepCost -- ([1,2,3,4,5], 3) +#eval (append [1, 2, 3] [4, 5]).eval stepCost2 -- ([1,2,3,4,5], 6) + +-- On 4 blocks of length 2, the right fold `concat₁` is Θ(m·n) = 4·2 = 8, +-- while the left fold `concat₂` is Θ(m²·n) = 0+2+4+6 = 12 — same result, +-- different cost, exposed purely by the model: +#eval (concat₁ [[1, 2], [3, 4], [5, 6], [7, 8]]).eval concatCost -- (…, 8) +#eval (concat₂ [[1, 2], [3, 4], [5, 6], [7, 8]] []).eval concatCost -- (…, 12) + +-- the theorem, specialised: m = 4 blocks of length n = 2 +example : (concat₁ [[1, 2], [3, 4], [5, 6], [7, 8]]).runtime concatCost = 4 * 2 := + concat₁_runtime _ 2 (by decide) + +end Chapter2Query diff --git a/Fad/QueryModel.lean b/Fad/QueryModel.lean new file mode 100644 index 0000000..35c3474 --- /dev/null +++ b/Fad/QueryModel.lean @@ -0,0 +1,155 @@ +/- +Query model (free-monad) for reasoning about algorithm complexity. + +This is a small, self-contained reimplementation of the *query model* +described in `query-model-tutorial.md` (CSLib PR #372, still open at the +pinned `cslib` revision, so it is vendored here instead of imported). + +The point of this module is to offer an alternative to `TimeM` +(`Cslib.Algorithms.Lean.TimeM`, used in `Fad.Chapter2`): instead of a +computation that *carries* a running cost, an algorithm is a *tree of +queries* (`Prog`) whose cost is assigned afterwards by a `Model`. The same +program can then be measured under several models, and the algorithm can +never "cheat" by inspecting the cost. + +See `Fad.Chapter2Query` for a side-by-side comparison with the `TimeM` +versions of `append`/`concat` from `Fad.Chapter2`. +-/ + +import Mathlib.Tactic + +set_option autoImplicit false + +namespace QueryModel + +universe u + +/-- A program that issues queries of type `Q` and returns an `R`. + +Internally a free monad: a tree whose leaves are `pure` results and whose +internal nodes are queries `Q ι` together with a continuation `ι → Prog Q R` +that consumes the (not-yet-known) answer. Nothing runs until `eval`. -/ +inductive Prog (Q : Type → Type u) (R : Type) : Type (max u 1) where + | pure : R → Prog Q R + | query : {ι : Type} → Q ι → (ι → Prog Q R) → Prog Q R + +namespace Prog + +variable {Q : Type → Type u} {R α β : Type} + +/-- Lift a single query into a one-node program. -/ +@[inline] def lift {ι : Type} (q : Q ι) : Prog Q ι := + .query q .pure + +def bind : Prog Q α → (α → Prog Q β) → Prog Q β + | .pure a, f => f a + | .query q k, f => .query q (fun i => bind (k i) f) + +instance : Monad (Prog Q) where + pure := .pure + bind := bind + +@[simp] theorem pure_eq (a : α) : (Pure.pure a : Prog Q α) = .pure a := rfl +@[simp] theorem bind_eq (m : Prog Q α) (f : α → Prog Q β) : + (m >>= f) = bind m f := rfl + +@[simp] theorem bind_pure (a : α) (f : α → Prog Q β) : + bind (.pure a) f = f a := rfl +@[simp] theorem bind_query {ι} (q : Q ι) (k : ι → Prog Q α) (f : α → Prog Q β) : + bind (.query q k) f = .query q (fun i => bind (k i) f) := rfl + +/-- A model gives meaning to a `Prog`: how to answer each query, and how much +each query costs. `Cost` is any additive-monoid-like type (`Nat`, a trace, +…). -/ +structure _root_.QueryModel.Model (Q : Type → Type u) (Cost : Type) where + evalQuery : {ι : Type} → Q ι → ι + cost : {ι : Type} → Q ι → Cost + +/-- Run a program against a model, returning the result and the accumulated +cost. At each query node the model supplies the answer (choosing the branch) +*and* the cost, which is summed along the followed path. -/ +def eval {Cost : Type} [Add Cost] [Zero Cost] : + Prog Q R → Model Q Cost → R × Cost + | .pure r, _ => (r, 0) + | .query q k, m => + let i := m.evalQuery q + let (r, c) := eval (k i) m + (r, m.cost q + c) + +/-- The result of `eval` (ignoring cost). Deliberately *not* `@[simp]`: we let +the `result_*` lemmas below drive simplification, otherwise simp would unfold +`result` to `(eval …).1` before the structural `result_bind` lemma can fire. -/ +def result {Cost : Type} [Add Cost] [Zero Cost] + (p : Prog Q R) (m : Model Q Cost) : R := (p.eval m).1 + +/-- The cost of `eval` (ignoring result). Not `@[simp]` for the same reason as +`result`; the `runtime_*` lemmas are the simp normal form. -/ +def runtime {Cost : Type} [Add Cost] [Zero Cost] + (p : Prog Q R) (m : Model Q Cost) : Cost := (p.eval m).2 + +@[simp] theorem eval_pure {Cost : Type} [Add Cost] [Zero Cost] + (r : R) (m : Model Q Cost) : (Prog.pure r).eval m = (r, 0) := rfl + +@[simp] theorem eval_query {Cost : Type} [Add Cost] [Zero Cost] + {ι} (q : Q ι) (k : ι → Prog Q R) (m : Model Q Cost) : + (Prog.query q k).eval m + = (((k (m.evalQuery q)).eval m).1, + m.cost q + ((k (m.evalQuery q)).eval m).2) := rfl + +@[simp] theorem result_pure {Cost : Type} [Add Cost] [Zero Cost] + (r : R) (m : Model Q Cost) : (Prog.pure r).result m = r := rfl +@[simp] theorem runtime_pure {Cost : Type} [Add Cost] [Zero Cost] + (r : R) (m : Model Q Cost) : (Prog.pure r).runtime m = 0 := rfl + +@[simp] theorem result_lift {Cost : Type} [Add Cost] [Zero Cost] + {ι} (q : Q ι) (m : Model Q Cost) : (Prog.lift q).result m = m.evalQuery q := rfl +@[simp] theorem runtime_lift {Cost : Type} [AddZeroClass Cost] + {ι} (q : Q ι) (m : Model Q Cost) : (Prog.lift q).runtime m = m.cost q := by + simp [Prog.lift, Prog.runtime, eval] + +/-- Cost accumulates additively across a `bind`: the cost of the whole is the +cost of the first program plus the cost of the continuation applied to its +result. This is the query-model analogue of `TimeM.time_of_bind`, and the key +lemma that makes complexity proofs go through by structural induction. -/ +theorem eval_bind {Cost : Type} [AddMonoid Cost] + (p : Prog Q α) (f : α → Prog Q β) (m : Model Q Cost) : + (Prog.bind p f).eval m + = (((f (p.result m)).eval m).1, + (p.runtime m) + ((f (p.result m)).eval m).2) := by + induction p with + | pure a => simp [Prog.bind, Prog.result, Prog.runtime, eval] + | query q k ih => + simp only [Prog.bind_query, eval_query, Prog.result, Prog.runtime, ih] + exact Prod.ext rfl (add_assoc _ _ _).symm + +@[simp] theorem result_bind {Cost : Type} [AddMonoid Cost] + (p : Prog Q α) (f : α → Prog Q β) (m : Model Q Cost) : + (Prog.bind p f).result m = (f (p.result m)).result m := by + simp [Prog.result, eval_bind] + +@[simp] theorem runtime_bind {Cost : Type} [AddMonoid Cost] + (p : Prog Q α) (f : α → Prog Q β) (m : Model Q Cost) : + (Prog.bind p f).runtime m = p.runtime m + (f (p.result m)).runtime m := by + simp [Prog.runtime, eval_bind] + +end Prog + +/-- Upper bound: some constant `k` bounds the cost by `k * bound n` for every +input of size at most `n`. Mirrors the definition in the tutorial. -/ +def UpperBound {Q : Type → Type u} {α β : Type} + (prog : α → Prog Q β) + (model : Model Q Nat) + (size : α → Nat) + (bound : Nat → Nat) : Prop := + ∃ k, ∀ n x, size x ≤ n → (prog x).runtime model ≤ k * bound n + +/-- Lower bound: for every `n` there is an input of that size forcing at least +`bound n` cost. -/ +def LowerBound {Q : Type → Type u} {α β : Type} + (prog : α → Prog Q β) + (model : Model Q Nat) + (size : α → Nat) + (bound : Nat → Nat) : Prop := + ∀ n, ∃ x, size x = n ∧ (prog x).runtime model ≥ bound n + +end QueryModel From 8743f7c46fcd6be4773eb67f632b03b9b86fe685 Mon Sep 17 00:00:00 2001 From: felipponn Date: Fri, 21 Aug 2026 09:59:32 -0300 Subject: [PATCH 14/16] fix(Chapter10): repair decide-stripping in key_fact proofs MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Under the current Lean/Mathlib toolchain, `simp only [..., decide_eq_true_eq, ]` no longer strips `decide P = true` to `P` when projection rfl-lemmas (`residue`/`count`/`value_add`/`weight_add`) are unfolded in the same call: `decide_eq_true_eq` is reported unused and the goal stays wrapped in `decide (…) = true`, so the following `constructor` / `calc` / `⟨_, _⟩` steps fail (no `And` constructor; `calc` type mismatch; `Eq.refl` given 2 fields). Fix: strip the `decide` in its own `simp only [_, decide_eq_true_eq]` pass first, then unfold the projections in a second step. Three sites across the two `key_fact` theorems (coin-change and knapsack). No statements changed; the whole `Fad` library builds again (8696 jobs, 0 errors). Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01AbkMyCwYRAiUy3NFwn9M4f --- Fad/Chapter10.lean | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/Fad/Chapter10.lean b/Fad/Chapter10.lean index e3c08fd..851d4ff 100644 --- a/Fad/Chapter10.lean +++ b/Fad/Chapter10.lean @@ -800,9 +800,11 @@ theorem key_fact (d : Denom) (t₁ t₂ : Tuple) (h : le₃ t₁ t₂ = true) : refine ⟨(coins t₁ ++ [c], residue t₁ - c * d, count t₁ + c), ?_, ?_⟩ · simp only [extend, List.mem_map, List.mem_range] exact ⟨c, by rw [hr]; exact hc, rfl⟩ - · simp only [le₃, decide_eq_true_eq, residue, count] - constructor - · simp [residue] at hr + · -- strip the `decide` first; unfolding the projections in the same `simp` + -- call blocks `decide_eq_true_eq` from firing + simp only [le₃, decide_eq_true_eq] + refine ⟨?_, ?_⟩ + · simp only [residue] at hr ⊢ rw [hr] · exact Nat.add_le_add_right hk c @@ -951,10 +953,12 @@ theorem key_fact (w : Weight) (i : Item) (sn₁ sn₂ : Selection) (h : le₄ sn · refine ⟨add i sn₁, ?_, ?_⟩ · rw [extend, List.mem_filter] refine ⟨by simp, ?_⟩ - simp only [within, decide_eq_true_eq, weight_add] + simp only [within, decide_eq_true_eq] + simp only [weight_add] calc weight i + weight sn₁ ≤ weight i + weight sn₂ := Nat.add_le_add_left hw _ _ ≤ w := by simpa using hin - · simp only [le₄, decide_eq_true_eq, value_add, weight_add] + · simp only [le₄, decide_eq_true_eq] + simp only [value_add, weight_add] exact ⟨Nat.add_le_add_left hv _, Nat.add_le_add_left hw _⟩ /-! ### The algorithm From 4bbd4a85a5c56de4801e5bec6b58a5cffc472f9f Mon Sep 17 00:00:00 2001 From: felipponn Date: Wed, 9 Sep 2026 12:12:04 -0300 Subject: [PATCH 15/16] feat(query-model): use CSLib PR #401 FreeM framework instead of vendored copy MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replace the self-contained Fad/QueryModel.lean with the real query-complexity framework from CSLib PR leanprover/cslib#401 (kim-em:combined-query-complexity): FreeM-based programs with eval / cost / queriesOn interpreters and the UpperBound/LowerBound predicates. - lakefile.toml: point cslib at the PR branch (pinned rev 391cab00) - lean-toolchain: v4.33.0-rc1 -> v4.30.0-rc2 (required by that cslib/mathlib pin) - lake-manifest.json: regenerated for the new pins - Fad/QueryModel.lean: removed (no longer vendored) - Fad/Chapter2-Query.lean: rewritten against the FreeM API (append, concat1, concat2); same programs measured under a fixed oracle with varying weights - Fad/Chapter2-Amortized.lean: new — binary counter showing amortized O(1) via the potential method (Phi = number of 1-bits), a natural fit for queriesOn - Fad/Chapter3.lean: List.toAssocList' (top-level in v4.30, was Lean.List.* in v4.33) — collateral fix for the toolchain downgrade Full `lake build` green (8347 jobs); remaining warnings are pre-existing sorries. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01AbkMyCwYRAiUy3NFwn9M4f --- Fad.lean | 2 +- Fad/Chapter2-Amortized.lean | 195 +++++++++++++++++++++++++++++++++++ Fad/Chapter2-Query.lean | 197 ++++++++++++++++++++---------------- Fad/Chapter3.lean | 2 +- Fad/QueryModel.lean | 155 ---------------------------- lake-manifest.json | 38 +++---- lakefile.toml | 3 +- lean-toolchain | 2 +- 8 files changed, 326 insertions(+), 268 deletions(-) create mode 100644 Fad/Chapter2-Amortized.lean delete mode 100644 Fad/QueryModel.lean diff --git a/Fad.lean b/Fad.lean index bb5ac73..65669a6 100644 --- a/Fad.lean +++ b/Fad.lean @@ -9,8 +9,8 @@ import Fad.«Chapter1-Ex» import Fad.Chapter2 import Fad.«Chapter2-Ex» -import Fad.QueryModel import Fad.«Chapter2-Query» +import Fad.«Chapter2-Amortized» import Fad.Chapter3 import Fad.«Chapter3-Ex» diff --git a/Fad/Chapter2-Amortized.lean b/Fad/Chapter2-Amortized.lean new file mode 100644 index 0000000..74eb8a2 --- /dev/null +++ b/Fad/Chapter2-Amortized.lean @@ -0,0 +1,195 @@ +import Cslib.Algorithms.Lean.Query.Bounds +import Mathlib.Tactic + +/-! +# Amortized complexity in the query model: a binary counter + +Amortized analysis measures the cost of a *sequence* of operations rather than a +single one. Its textbook example is the **binary counter**: incrementing it once +can be expensive (a carry may ripple through every bit), yet `n` increments from +zero cost only `O(n)` in total — i.e. `O(1)` *amortized* per increment. + +The query model is a natural home for this, and this is exactly where it pulls +ahead of the inline-tick `TimeM` style: + +* `queriesOn` already counts cost over the **whole** program tree, so the total + cost of a sequence is just `queriesOn` of the sequence — no manual summation. +* The **potential method** drops out cleanly. The classic potential of a binary + counter is `Φ = (number of 1-bits)`. Here `Φ (bs) = bs.count true`, and the + key single-step invariant + + ``` + (inc bs).queriesOn + Φ((inc bs).eval) = Φ(bs) + 2 + ``` + + says each increment has **amortized cost exactly 2**: actual flips plus the + change in potential is always `2`. Telescoping it over `n` steps gives the + `≤ 2n` total bound, with `Φ` never negative doing the "banking". + +Compare `Chapter2` (worst-case, single-shot) with this file (amortized, whole +sequence). With `TimeM` you would have to thread and sum the potential by hand; +here the two interpreters `queriesOn` and `eval` do it for you. +-/ + +set_option autoImplicit false + +open Cslib (FreeM) + +namespace Chapter2Amortized + +/-! ## The counter and its one query + +The counter is a little-endian list of bits (least-significant first). The only +operation with a cost is flipping one bit, modelled as the single query `flip`, +which costs one. `queriesOn` therefore counts **bit-flips** — the standard cost +measure for a binary counter. -/ + +inductive BitOp : Type → Type where + | flip : BitOp Unit -- flip one bit; this is the unit of cost + +/-- Emit one flip query. -/ +def flipBit : FreeM BitOp Unit := FreeM.lift BitOp.flip + +/-- The (only sensible) oracle: answering a `flip` yields `()`. The result of a +program is independent of the oracle here — a flip carries cost, not data. -/ +def bitOracle : {ι : Type} → BitOp ι → ι + | _, .flip => () + +/-- Potential function `Φ`: the number of 1-bits currently set. -/ +def phi : List Bool → Nat + | [] => 0 + | false :: bs => phi bs + | true :: bs => phi bs + 1 + +/-! ## `inc`: increment by one + +Increment flips the low bit; if it was already `1`, that bit goes to `0` and the +carry recurses into the higher bits. Each flip is one query. -/ + +def inc : List Bool → FreeM BitOp (List Bool) + | [] => do flipBit; pure [true] -- 0 → 1 + | false :: bs => do flipBit; pure (true :: bs) -- no carry: one flip + | true :: bs => do flipBit; let bs' ← inc bs; pure (false :: bs') -- carry + +-- ## Step lemmas: how `eval` and `queriesOn` act on one `inc` + +@[simp] theorem inc_eval_nil (o : {ι : Type} → BitOp ι → ι) : + (inc []).eval o = [true] := by simp [inc, flipBit] +@[simp] theorem inc_eval_false (o : {ι : Type} → BitOp ι → ι) (bs : List Bool) : + (inc (false :: bs)).eval o = true :: bs := by simp [inc, flipBit] +@[simp] theorem inc_eval_true (o : {ι : Type} → BitOp ι → ι) (bs : List Bool) : + (inc (true :: bs)).eval o = false :: (inc bs).eval o := by simp [inc, flipBit] + +@[simp] theorem inc_queriesOn_nil (o : {ι : Type} → BitOp ι → ι) : + (inc []).queriesOn o = 1 := by simp [inc, flipBit] +@[simp] theorem inc_queriesOn_false (o : {ι : Type} → BitOp ι → ι) (bs : List Bool) : + (inc (false :: bs)).queriesOn o = 1 := by simp [inc, flipBit] +@[simp] theorem inc_queriesOn_true (o : {ι : Type} → BitOp ι → ι) (bs : List Bool) : + (inc (true :: bs)).queriesOn o = 1 + (inc bs).queriesOn o := by simp [inc, flipBit] + +/-! ## Correctness: `inc` really is "+1" + +The program does not cheat: read as a little-endian number, its result is the +input plus one. This uses only `eval`, never the cost. -/ + +def toNat : List Bool → Nat + | [] => 0 + | false :: bs => 2 * toNat bs + | true :: bs => 1 + 2 * toNat bs + +theorem inc_toNat (o : {ι : Type} → BitOp ι → ι) (bs : List Bool) : + toNat ((inc bs).eval o) = toNat bs + 1 := by + induction bs with + | nil => simp [toNat] + | cons b bs ih => + cases b with + | false => simp only [inc_eval_false, toNat]; omega + | true => simp only [inc_eval_true, toNat, ih]; omega + +/-! ## The amortized bound + +### Single step: amortized cost is exactly 2 + +`actual flips + ΔΦ = 2`. Rearranged so both sides are `Nat`-subtraction-free. -/ + +theorem inc_amortized (o : {ι : Type} → BitOp ι → ι) (bs : List Bool) : + (inc bs).queriesOn o + phi ((inc bs).eval o) = phi bs + 2 := by + induction bs with + | nil => simp [phi] + | cons b bs ih => + cases b with + | false => simp only [inc_eval_false, inc_queriesOn_false, phi]; omega + | true => + simp only [inc_eval_true, inc_queriesOn_true, phi] at ih ⊢ + omega + +/-! ### Whole sequence + +`incTimes n bs` runs `inc` `n` times in a row, carrying the counter along. -/ + +def incTimes : Nat → List Bool → FreeM BitOp (List Bool) + | 0, bs => pure bs + | k + 1, bs => do let bs' ← inc bs; incTimes k bs' + +/-- Telescoped invariant: total flips + final potential = initial potential + 2n. +The single-step amortized cost `2` sums exactly, with no error term. -/ +theorem incTimes_amortized (o : {ι : Type} → BitOp ι → ι) (n : Nat) (bs : List Bool) : + (incTimes n bs).queriesOn o + phi ((incTimes n bs).eval o) = phi bs + 2 * n := by + induction n generalizing bs with + | zero => simp [incTimes] + | succ k ih => + have hstep : (incTimes (k + 1) bs).queriesOn o + + phi ((incTimes (k + 1) bs).eval o) + = (inc bs).queriesOn o + + ((incTimes k ((inc bs).eval o)).queriesOn o + + phi ((incTimes k ((inc bs).eval o)).eval o)) := by + simp [incTimes]; omega + rw [hstep, ih ((inc bs).eval o)] + have := inc_amortized o bs + -- (inc bs).queriesOn + (phi(inc bs eval) + 2k) = phi bs + 2(k+1) + omega + +/-- **Amortized `O(1)`.** Starting from zero, `n` increments cost at most `2 n` +bit-flips in total — even though a single increment can cost far more (see +`inc_all_ones` below). The potential `Φ ≥ 0` absorbs the difference. -/ +theorem incTimes_queriesOn_le (o : {ι : Type} → BitOp ι → ι) (n : Nat) : + (incTimes n []).queriesOn o ≤ 2 * n := by + have h := incTimes_amortized o n [] + simp only [phi] at h + omega + +/-! ### Contrast: a single increment can be expensive + +A counter of `k` ones (the value `2^k − 1`) is the worst case: the carry ripples +through all `k` bits and sets a new one, `k + 1` flips. This is the `Θ(log v)` +worst-case single-operation cost that the `2n` amortized bound smooths over. -/ + +theorem inc_all_ones (o : {ι : Type} → BitOp ι → ι) (k : Nat) : + (inc (List.replicate k true)).queriesOn o = k + 1 := by + induction k with + | zero => simp + | succ k ih => + rw [List.replicate_succ, inc_queriesOn_true, ih] + omega + + +/-! ## Demonstration + +The pay-off: `queriesOn` gives the total cost of a whole sequence directly, and +the amortized bound holds although individual steps vary. -/ + +-- One expensive increment: 0b111 (=7) → 0b1000 (=8) ripples 4 flips: +#eval (inc [true, true, true]).queriesOn bitOracle -- 4 +#eval toNat ((inc [true, true, true]).eval bitOracle) -- 8 + +-- Eight increments from zero: per-step flips are 1,2,1,3,1,2,1,4 (= 15 total), +-- comfortably under the amortized bound 2·8 = 16: +#eval (incTimes 8 []).queriesOn bitOracle -- 15 +#eval 2 * 8 -- 16 (the bound) +#eval phi ((incTimes 8 []).eval bitOracle) -- 1 (Φ of 0b1000) + +-- the amortized theorem, specialised to n = 8: +example : (incTimes 8 []).queriesOn bitOracle ≤ 2 * 8 := + incTimes_queriesOn_le bitOracle 8 + +end Chapter2Amortized diff --git a/Fad/Chapter2-Query.lean b/Fad/Chapter2-Query.lean index 599b54c..8787cfb 100644 --- a/Fad/Chapter2-Query.lean +++ b/Fad/Chapter2-Query.lean @@ -1,33 +1,44 @@ -import Fad.QueryModel +import Cslib.Algorithms.Lean.Query.Bounds +import Mathlib.Tactic /-! # Chapter 2 complexity examples, in the *query model* This module reimplements the running-time examples of `Fad.Chapter2` -(`append`, `concat₁`, `concat₂`) using the query model of `Fad.QueryModel` -instead of the `TimeM` monad, so the two styles can be compared directly. +(`append`, `concat₁`, `concat₂`) using the **query model** of CSLib +(`Cslib.Algorithms.Lean.Query`, PR leanprover/cslib#401) instead of the +`TimeM` monad, so the two styles can be compared directly. The correspondence is: -| `TimeM` version (`Chapter2`) | query-model version (here) | -|-----------------------------------------|---------------------------------------| -| cost is *carried* by the computation | cost is *assigned* by a `Model` | -| `✓ e` / `✓[c] e` ticks inline | a query node is emitted; its cost | -| | comes from the model, not the program | -| `.time` reads the accumulated cost | `.runtime model` evaluates the tree | -| one fixed cost model | the same program, many models | +| `TimeM` version (`Chapter2`) | query-model version (here) | +|-----------------------------------------|-----------------------------------------| +| cost is *carried* by the computation | cost is *assigned* by an oracle+weight | +| `✓ e` / `✓[c] e` ticks inline | a query node is emitted; its cost comes | +| | from a `weight`, not from the program | +| `.time` reads the accumulated cost | `.cost oracle weight` folds the tree | +| one fixed cost model | the same program, many cost models | + +A program is a value of `FreeM Q α`: a *syntax tree* of queries `Q`. Three +interpreters run it: + +* `p.eval oracle` — the result, answering each query with `oracle`; +* `p.cost oracle weight` — the total cost, charging `weight` per query; +* `p.queriesOn oracle` — the number of queries (= `cost` with unit weight). + +Because the oracle/weight are supplied *after* the tree is built, the algorithm +cannot "peek" at costs — the anti-cheating guarantee for both bounds. The complexity theorems (`concat₁_runtime`, `concat₂_runtime`) are the -query-model analogues of `Chapter2.concat₁''_time` and -`Chapter2.concat₂'_time`; compare the proofs. +query-model analogues of `Chapter2.concat₁''_time` and `Chapter2.concat₂'_time`; +compare the proofs. -/ set_option autoImplicit false -namespace Chapter2Query +open Cslib (FreeM) -open QueryModel -open QueryModel.Prog (lift) +namespace Chapter2Query /-! ## `append` @@ -40,122 +51,126 @@ def append' : List a → List a → TimeM Nat (List a) | x :: xs, ys => do ✓ return x :: (← append' xs ys) ``` -Here each prepend is a *query* `AppendOp.step`; how much it costs is decided by -the model, not written into the algorithm. -/ +Here each prepend is a *query* `AppendOp.step`; how much it costs is decided +later by a `weight`, not written into the algorithm. -/ inductive AppendOp (a : Type) : Type → Type where | step : a → List a → AppendOp a (List a) -- prepend the head onto the tail -def append {a : Type} : List a → List a → Prog (AppendOp a) (List a) - | [], ys => pure ys - | x :: xs, ys => do - let r ← append xs ys - lift (AppendOp.step x r) +/-- The semantics of a `step`: it prepends. Fixed, independent of cost. -/ +def appendOracle {a : Type} : {ι : Type} → AppendOp a ι → ι + | _, .step x xs => x :: xs -/-- The natural model: a `step` prepends, and costs one unit — matching the -single `✓` per element in `Chapter2.append'`. -/ -def stepCost {a : Type} : Model (AppendOp a) Nat where - evalQuery | .step x xs => x :: xs - cost | .step _ _ => 1 +/-- The natural cost model: each `step` costs one unit — matching the single +`✓` per element in `Chapter2.append'`. -/ +def stepWeight {a : Type} : {ι : Type} → AppendOp a ι → Nat + | _, .step _ _ => 1 -/-- A *different* model for the *same* program: charge two units per prepend +/-- A *different* cost model for the *same* program: two units per prepend (e.g. two memory writes). Impossible to express with `TimeM` without editing the algorithm — the whole point of the query model. -/ -def stepCost2 {a : Type} : Model (AppendOp a) Nat where - evalQuery | .step x xs => x :: xs - cost | .step _ _ => 2 - --- model equations (kept as simp lemmas so proofs never have to *unfold* the --- model, which would break matching against the induction hypothesis) -@[simp] theorem stepCost_eval {a : Type} (x : a) (xs : List a) : - stepCost.evalQuery (AppendOp.step x xs) = x :: xs := rfl -@[simp] theorem stepCost_cost {a : Type} (x : a) (xs : List a) : - stepCost.cost (AppendOp.step x xs) = 1 := rfl -@[simp] theorem stepCost2_cost {a : Type} (x : a) (xs : List a) : - stepCost2.cost (AppendOp.step x xs) = 2 := rfl - -/-- The program still computes the ordinary append. -/ -@[simp] theorem append_result {a : Type} (xs ys : List a) : - (append xs ys).result stepCost = xs ++ ys := by +def stepWeight2 {a : Type} : {ι : Type} → AppendOp a ι → Nat + | _, .step _ _ => 2 + +@[simp] theorem appendOracle_step {a : Type} (x : a) (xs : List a) : + appendOracle (AppendOp.step x xs) = x :: xs := rfl +@[simp] theorem stepWeight_step {a : Type} (x : a) (xs : List a) : + stepWeight (AppendOp.step x xs) = 1 := rfl +@[simp] theorem stepWeight2_step {a : Type} (x : a) (xs : List a) : + stepWeight2 (AppendOp.step x xs) = 2 := rfl + +def append {a : Type} : List a → List a → FreeM (AppendOp a) (List a) + | [], ys => pure ys + | x :: xs, ys => do + let r ← append xs ys + FreeM.lift (AppendOp.step x r) + +/-- The program still computes the ordinary append (it does not cheat). -/ +@[simp] theorem append_eval {a : Type} (xs ys : List a) : + (append xs ys).eval appendOracle = xs ++ ys := by induction xs with | nil => rfl | cons x xs ih => simp [append, ih] -/-- Cost under `stepCost` is the length of the first list — `Θ(|xs|)`. -/ -theorem append_runtime {a : Type} (xs ys : List a) : - (append xs ys).runtime stepCost = xs.length := by +/-- Number of queries is the length of the first list — `Θ(|xs|)`. -/ +theorem append_queriesOn {a : Type} (xs ys : List a) : + (append xs ys).queriesOn appendOracle = xs.length := by induction xs with | nil => rfl | cons x xs ih => simp [append, ih] -/-- The same program, measured under `stepCost2`, costs twice as much — no -change to `append` itself. -/ -theorem append_runtime2 {a : Type} (xs ys : List a) : - (append xs ys).runtime stepCost2 = 2 * xs.length := by +/-- The same program, measured under `stepWeight2`, costs twice as much — no +change to `append` itself, only the cost model. -/ +theorem append_cost2 {a : Type} (xs ys : List a) : + (append xs ys).cost appendOracle stepWeight2 = 2 * xs.length := by induction xs with | nil => rfl - | cons x xs ih => - simp only [append, Prog.bind_eq, Prog.runtime_bind, Prog.runtime_lift, - stepCost2_cost, List.length_cons, ih] - omega + | cons x xs ih => simp [append, ih]; omega /-! ## `concat` `Chapter2.concat₁''` folds append from the right, charging `xs.length` for each append (`✓[xs.length]`). We model one append of a length-`k` list as a single -query whose *cost is `k`*, decided by the model. -/ +query whose *weight is `k`*. Here `queriesOn` (which counts nodes) is *not* the +right measure — a single append is one node but costs `k` — so we use `cost` +with the length-weight. -/ inductive ConcatOp (a : Type) : Type → Type where | app : List a → List a → ConcatOp a (List a) -- xs ++ ys -def concatCost {a : Type} : Model (ConcatOp a) Nat where - evalQuery | .app xs ys => xs ++ ys - cost | .app xs _ => xs.length +def concatOracle {a : Type} : {ι : Type} → ConcatOp a ι → ι + | _, .app xs ys => xs ++ ys + +/-- Appending `xs ++ ys` costs `xs.length` (you walk the left list). -/ +def concatWeight {a : Type} : {ι : Type} → ConcatOp a ι → Nat + | _, .app xs _ => xs.length -@[simp] theorem concatCost_eval {a : Type} (xs ys : List a) : - concatCost.evalQuery (ConcatOp.app xs ys) = xs ++ ys := rfl -@[simp] theorem concatCost_cost {a : Type} (xs ys : List a) : - concatCost.cost (ConcatOp.app xs ys) = xs.length := rfl +@[simp] theorem concatOracle_app {a : Type} (xs ys : List a) : + concatOracle (ConcatOp.app xs ys) = xs ++ ys := rfl +@[simp] theorem concatWeight_app {a : Type} (xs ys : List a) : + concatWeight (ConcatOp.app xs ys) = xs.length := rfl /-- Right fold — mirrors `Chapter2.concat₁''`. -/ -def concat₁ {a : Type} : List (List a) → Prog (ConcatOp a) (List a) +def concat₁ {a : Type} : List (List a) → FreeM (ConcatOp a) (List a) | [] => pure [] | xs :: xss => do let ys ← concat₁ xss - lift (ConcatOp.app xs ys) + FreeM.lift (ConcatOp.app xs ys) /-- Left fold, cost-charging on the accumulator — mirrors `Chapter2.concat₂''`. Each step appends the accumulator (which keeps growing) onto the next block, so the accumulator length is what gets charged. -/ -def concat₂ {a : Type} : List (List a) → List a → Prog (ConcatOp a) (List a) +def concat₂ {a : Type} : List (List a) → List a → FreeM (ConcatOp a) (List a) | [], acc => pure acc | xs :: xss, acc => do - let acc' ← lift (ConcatOp.app acc xs) + let acc' ← FreeM.lift (ConcatOp.app acc xs) concat₂ xss acc' -/-- if `xss` is a list of `m` lists each of length `n`, then `concat₁` is +/-- The result of `concat₁` really is the concatenation (it does not cheat). -/ +@[simp] theorem concat₁_eval {a : Type} (xss : List (List a)) : + (concat₁ xss).eval concatOracle = xss.flatten := by + induction xss with + | nil => rfl + | cons xs xss' ih => simp [concat₁, ih] + +/-- If `xss` is a list of `m` lists each of length `n`, then `concat₁` is `Θ(m * n)`. Query-model analogue of `Chapter2.concat₁''_time`. -/ theorem concat₁_runtime {a : Type} (xss : List (List a)) (n : Nat) (h : ∀ xs ∈ xss, xs.length = n) : - (concat₁ xss).runtime concatCost = xss.length * n := by + (concat₁ xss).cost concatOracle concatWeight = xss.length * n := by induction xss with | nil => simp [concat₁] | cons xs xss' ih => have h₁ : xs.length = n := h xs List.mem_cons_self have h₂ : ∀ ys ∈ xss', ys.length = n := fun ys hys => h ys (List.mem_cons_of_mem xs hys) - simp only [concat₁, Prog.bind_eq, Prog.runtime_bind, Prog.runtime_lift, - concatCost_cost, List.length_cons, ih h₂, h₁] + have hstep : (concat₁ (xs :: xss')).cost concatOracle concatWeight + = (concat₁ xss').cost concatOracle concatWeight + xs.length := by + simp [concat₁] + rw [hstep, ih h₂, h₁, List.length_cons] ring -/-- The result of `concat₁` really is the concatenation (it does not cheat). -/ -@[simp] theorem concat₁_result {a : Type} (xss : List (List a)) : - (concat₁ xss).result concatCost = xss.flatten := by - induction xss with - | nil => rfl - | cons xs xss' ih => simp [concat₁, ih] - /-- Cost of the left-associated fold: `concat₂` over `m` blocks of length `n` starting from an accumulator of length `a₀` costs `a₀ * m + n * m * (m-1) / 2`. We state it in the doubled, subtraction-free form used in @@ -163,7 +178,7 @@ We state it in the doubled, subtraction-free form used in theorem concat₂_runtime {a : Type} (xss : List (List a)) (n : Nat) (h : ∀ xs ∈ xss, xs.length = n) (acc : List a) : - (2 * (concat₂ xss acc).runtime concatCost : Int) + (2 * (concat₂ xss acc).cost concatOracle concatWeight : Int) = 2 * acc.length * xss.length + n * xss.length * (xss.length - 1) := by induction xss generalizing acc with | nil => simp [concat₂] @@ -173,8 +188,8 @@ theorem concat₂_runtime {a : Type} (xss : List (List a)) fun ys hys => h ys (List.mem_cons_of_mem xs hys) -- one fold step charges the current accumulator length, then recurses on -- the (grown) accumulator - have hstep : (concat₂ (xs :: xss') acc).runtime concatCost - = acc.length + (concat₂ xss' (acc ++ xs)).runtime concatCost := by + have hstep : (concat₂ (xs :: xss') acc).cost concatOracle concatWeight + = acc.length + (concat₂ xss' (acc ++ xs)).cost concatOracle concatWeight := by simp [concat₂] have hIH := ih h₂ (acc ++ xs) rw [List.length_append, h₁] at hIH @@ -189,21 +204,23 @@ The pay-off of the query model over `TimeM`: the *same* program is measured under different cost models, with no change to the algorithm. Under `TimeM` each of these would need a separately-written function. -`.eval` returns the `(result, cost)` pair; `.result`/`.runtime` project them. -/ +`.eval` returns the result; `.cost`/`.queriesOn` return the cost. -/ --- `append` costs one per element under `stepCost`, two under `stepCost2`, --- but computes the same list either way: -#eval (append [1, 2, 3] [4, 5]).eval stepCost -- ([1,2,3,4,5], 3) -#eval (append [1, 2, 3] [4, 5]).eval stepCost2 -- ([1,2,3,4,5], 6) +-- `append` computes the same list, but costs one per element under unit weight, +-- two under `stepWeight2`: +#eval (append [1, 2, 3] [4, 5]).eval appendOracle -- [1,2,3,4,5] +#eval (append [1, 2, 3] [4, 5]).queriesOn appendOracle -- 3 +#eval (append [1, 2, 3] [4, 5]).cost appendOracle stepWeight2 -- 6 -- On 4 blocks of length 2, the right fold `concat₁` is Θ(m·n) = 4·2 = 8, -- while the left fold `concat₂` is Θ(m²·n) = 0+2+4+6 = 12 — same result, --- different cost, exposed purely by the model: -#eval (concat₁ [[1, 2], [3, 4], [5, 6], [7, 8]]).eval concatCost -- (…, 8) -#eval (concat₂ [[1, 2], [3, 4], [5, 6], [7, 8]] []).eval concatCost -- (…, 12) +-- different cost, exposed purely by the cost model: +#eval (concat₁ [[1, 2], [3, 4], [5, 6], [7, 8]]).cost concatOracle concatWeight -- 8 +#eval (concat₂ [[1, 2], [3, 4], [5, 6], [7, 8]] []).cost concatOracle concatWeight -- 12 -- the theorem, specialised: m = 4 blocks of length n = 2 -example : (concat₁ [[1, 2], [3, 4], [5, 6], [7, 8]]).runtime concatCost = 4 * 2 := +example : + (concat₁ [[1, 2], [3, 4], [5, 6], [7, 8]]).cost concatOracle concatWeight = 4 * 2 := concat₁_runtime _ 2 (by decide) end Chapter2Query diff --git a/Fad/Chapter3.lean b/Fad/Chapter3.lean index 43ceec6..ba675db 100644 --- a/Fad/Chapter3.lean +++ b/Fad/Chapter3.lean @@ -600,7 +600,7 @@ instance instIxChar : Ix Char where def listArray {i e : Type} [Ix i] (bnds : i × i) (xs : List e) : Lean.AssocList i e := - (Ix.range bnds).zip xs |> Lean.List.toAssocList' + (Ix.range bnds).zip xs |> List.toAssocList' -- #eval listArray (0,5) [10, 20, 30, 40, 50] |>.toList diff --git a/Fad/QueryModel.lean b/Fad/QueryModel.lean deleted file mode 100644 index 35c3474..0000000 --- a/Fad/QueryModel.lean +++ /dev/null @@ -1,155 +0,0 @@ -/- -Query model (free-monad) for reasoning about algorithm complexity. - -This is a small, self-contained reimplementation of the *query model* -described in `query-model-tutorial.md` (CSLib PR #372, still open at the -pinned `cslib` revision, so it is vendored here instead of imported). - -The point of this module is to offer an alternative to `TimeM` -(`Cslib.Algorithms.Lean.TimeM`, used in `Fad.Chapter2`): instead of a -computation that *carries* a running cost, an algorithm is a *tree of -queries* (`Prog`) whose cost is assigned afterwards by a `Model`. The same -program can then be measured under several models, and the algorithm can -never "cheat" by inspecting the cost. - -See `Fad.Chapter2Query` for a side-by-side comparison with the `TimeM` -versions of `append`/`concat` from `Fad.Chapter2`. --/ - -import Mathlib.Tactic - -set_option autoImplicit false - -namespace QueryModel - -universe u - -/-- A program that issues queries of type `Q` and returns an `R`. - -Internally a free monad: a tree whose leaves are `pure` results and whose -internal nodes are queries `Q ι` together with a continuation `ι → Prog Q R` -that consumes the (not-yet-known) answer. Nothing runs until `eval`. -/ -inductive Prog (Q : Type → Type u) (R : Type) : Type (max u 1) where - | pure : R → Prog Q R - | query : {ι : Type} → Q ι → (ι → Prog Q R) → Prog Q R - -namespace Prog - -variable {Q : Type → Type u} {R α β : Type} - -/-- Lift a single query into a one-node program. -/ -@[inline] def lift {ι : Type} (q : Q ι) : Prog Q ι := - .query q .pure - -def bind : Prog Q α → (α → Prog Q β) → Prog Q β - | .pure a, f => f a - | .query q k, f => .query q (fun i => bind (k i) f) - -instance : Monad (Prog Q) where - pure := .pure - bind := bind - -@[simp] theorem pure_eq (a : α) : (Pure.pure a : Prog Q α) = .pure a := rfl -@[simp] theorem bind_eq (m : Prog Q α) (f : α → Prog Q β) : - (m >>= f) = bind m f := rfl - -@[simp] theorem bind_pure (a : α) (f : α → Prog Q β) : - bind (.pure a) f = f a := rfl -@[simp] theorem bind_query {ι} (q : Q ι) (k : ι → Prog Q α) (f : α → Prog Q β) : - bind (.query q k) f = .query q (fun i => bind (k i) f) := rfl - -/-- A model gives meaning to a `Prog`: how to answer each query, and how much -each query costs. `Cost` is any additive-monoid-like type (`Nat`, a trace, -…). -/ -structure _root_.QueryModel.Model (Q : Type → Type u) (Cost : Type) where - evalQuery : {ι : Type} → Q ι → ι - cost : {ι : Type} → Q ι → Cost - -/-- Run a program against a model, returning the result and the accumulated -cost. At each query node the model supplies the answer (choosing the branch) -*and* the cost, which is summed along the followed path. -/ -def eval {Cost : Type} [Add Cost] [Zero Cost] : - Prog Q R → Model Q Cost → R × Cost - | .pure r, _ => (r, 0) - | .query q k, m => - let i := m.evalQuery q - let (r, c) := eval (k i) m - (r, m.cost q + c) - -/-- The result of `eval` (ignoring cost). Deliberately *not* `@[simp]`: we let -the `result_*` lemmas below drive simplification, otherwise simp would unfold -`result` to `(eval …).1` before the structural `result_bind` lemma can fire. -/ -def result {Cost : Type} [Add Cost] [Zero Cost] - (p : Prog Q R) (m : Model Q Cost) : R := (p.eval m).1 - -/-- The cost of `eval` (ignoring result). Not `@[simp]` for the same reason as -`result`; the `runtime_*` lemmas are the simp normal form. -/ -def runtime {Cost : Type} [Add Cost] [Zero Cost] - (p : Prog Q R) (m : Model Q Cost) : Cost := (p.eval m).2 - -@[simp] theorem eval_pure {Cost : Type} [Add Cost] [Zero Cost] - (r : R) (m : Model Q Cost) : (Prog.pure r).eval m = (r, 0) := rfl - -@[simp] theorem eval_query {Cost : Type} [Add Cost] [Zero Cost] - {ι} (q : Q ι) (k : ι → Prog Q R) (m : Model Q Cost) : - (Prog.query q k).eval m - = (((k (m.evalQuery q)).eval m).1, - m.cost q + ((k (m.evalQuery q)).eval m).2) := rfl - -@[simp] theorem result_pure {Cost : Type} [Add Cost] [Zero Cost] - (r : R) (m : Model Q Cost) : (Prog.pure r).result m = r := rfl -@[simp] theorem runtime_pure {Cost : Type} [Add Cost] [Zero Cost] - (r : R) (m : Model Q Cost) : (Prog.pure r).runtime m = 0 := rfl - -@[simp] theorem result_lift {Cost : Type} [Add Cost] [Zero Cost] - {ι} (q : Q ι) (m : Model Q Cost) : (Prog.lift q).result m = m.evalQuery q := rfl -@[simp] theorem runtime_lift {Cost : Type} [AddZeroClass Cost] - {ι} (q : Q ι) (m : Model Q Cost) : (Prog.lift q).runtime m = m.cost q := by - simp [Prog.lift, Prog.runtime, eval] - -/-- Cost accumulates additively across a `bind`: the cost of the whole is the -cost of the first program plus the cost of the continuation applied to its -result. This is the query-model analogue of `TimeM.time_of_bind`, and the key -lemma that makes complexity proofs go through by structural induction. -/ -theorem eval_bind {Cost : Type} [AddMonoid Cost] - (p : Prog Q α) (f : α → Prog Q β) (m : Model Q Cost) : - (Prog.bind p f).eval m - = (((f (p.result m)).eval m).1, - (p.runtime m) + ((f (p.result m)).eval m).2) := by - induction p with - | pure a => simp [Prog.bind, Prog.result, Prog.runtime, eval] - | query q k ih => - simp only [Prog.bind_query, eval_query, Prog.result, Prog.runtime, ih] - exact Prod.ext rfl (add_assoc _ _ _).symm - -@[simp] theorem result_bind {Cost : Type} [AddMonoid Cost] - (p : Prog Q α) (f : α → Prog Q β) (m : Model Q Cost) : - (Prog.bind p f).result m = (f (p.result m)).result m := by - simp [Prog.result, eval_bind] - -@[simp] theorem runtime_bind {Cost : Type} [AddMonoid Cost] - (p : Prog Q α) (f : α → Prog Q β) (m : Model Q Cost) : - (Prog.bind p f).runtime m = p.runtime m + (f (p.result m)).runtime m := by - simp [Prog.runtime, eval_bind] - -end Prog - -/-- Upper bound: some constant `k` bounds the cost by `k * bound n` for every -input of size at most `n`. Mirrors the definition in the tutorial. -/ -def UpperBound {Q : Type → Type u} {α β : Type} - (prog : α → Prog Q β) - (model : Model Q Nat) - (size : α → Nat) - (bound : Nat → Nat) : Prop := - ∃ k, ∀ n x, size x ≤ n → (prog x).runtime model ≤ k * bound n - -/-- Lower bound: for every `n` there is an input of that size forcing at least -`bound n` cost. -/ -def LowerBound {Q : Type → Type u} {α β : Type} - (prog : α → Prog Q β) - (model : Model Q Nat) - (size : α → Nat) - (bound : Nat → Nat) : Prop := - ∀ n, ∃ x, size x = n ∧ (prog x).runtime model ≥ bound n - -end QueryModel diff --git a/lake-manifest.json b/lake-manifest.json index ed82840..310a908 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,31 +1,31 @@ {"version": "1.2.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover/cslib", + [{"url": "https://github.com/kim-em/cslib", "type": "git", "subDir": null, - "scope": "leanprover", - "rev": "a1faa284cc5923ac11a4b8d2452749a174ef8cf1", + "scope": "", + "rev": "391cab007c5c056af9ab874e450fc91a9e9daee5", "name": "cslib", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "391cab007c5c056af9ab874e450fc91a9e9daee5", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "169c26b52a38b704fad2c009372d76844a059bdf", + "rev": "5450b53e5ddc75d46418fabb605edbf36bd0beb6", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "169c26b52a38b704fad2c009372d76844a059bdf", + "inputRev": "master", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b1c4a69a7e247ab7df20460212001673d74f08c0", + "rev": "86210d4ad1b08b086d0bd638637a75246523dbb8", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "0498c7c070c143a3bf7379f4d99a2c63bb9d9715", + "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "18a90119a5d316358fde6c86e0ca24e59212e32c", + "rev": "cdab3938ccabbdb044be6896e251b5814bec932e", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,50 +55,50 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b1436dc749e722c9920036b52cdc43b3451d0b69", + "rev": "2db6054a44326f8c0230ee0570e2ddb894816511", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v0.0.98", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "57d3325be72a842920813bcb40f96a6f7393c185", + "rev": "f0c6e183ea26531e82773feb4b73ab6595ca17a5", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.30.0-rc2", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ee41917ae11d38479fb8fb24745f7ca4bf0a784d", + "rev": "1cc7e819b9b9bc1e87c9edcccb62e0269e00a809", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.30.0-rc2", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2c810760f0a0c4536b397dbe30ca9b2f2f467366", + "rev": "5c57f3857ba81924a88b2cdf4f062e34ec04ff11", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.30.0-rc2", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "leanprover", - "rev": "da07ca808b6718cb2aed14dba154e5a08b8f8ecf", + "rev": "13567aed1ac4f12aea9484178e07e51f8c9f7658", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.33.0-rc1", + "inputRev": "v4.30.0-rc2", "inherited": true, "configFile": "lakefile.toml"}], "name": "fad", diff --git a/lakefile.toml b/lakefile.toml index c4ab633..4f1d235 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -11,4 +11,5 @@ root = "Main" [[require]] name = "cslib" -scope = "leanprover" +git = "https://github.com/kim-em/cslib" +rev = "391cab007c5c056af9ab874e450fc91a9e9daee5" diff --git a/lean-toolchain b/lean-toolchain index 1770ccd..6c7e31f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.33.0-rc1 \ No newline at end of file +leanprover/lean4:v4.30.0-rc2 From 1c251ebfc0effb046e2d5698697793e86f54d5a7 Mon Sep 17 00:00:00 2001 From: felipponn Date: Thu, 10 Sep 2026 09:59:12 -0300 Subject: [PATCH 16/16] =?UTF-8?q?feat(amortized):=20add=20Bird=20&=20Gibbo?= =?UTF-8?q?ns'=20`build`=20example=20(ADwH=20=C2=A72.4)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Second amortized example alongside the binary counter, mirroring the book's "two examples" of §2.4. `build p = foldr insert []` with `insert x xs = x : dropWhile (p x) xs`, formalized in the query model with the predicate `p x y` as the cost-bearing query. Uses the book's uniform potential method (eq. 2.3) in subtraction-free form: S = length, A = 2, proving the *inequality* C + S(after) <= S(before) + 2 per step (contrast the counter's exact equality) and telescoping to the O(n) total bound `build_queriesOn_le : (build xs).queriesOn o <= 2 * xs.length`. Includes the book's own example verbatim: `build (==) [4,4,2,1,1,2,5] = [4,2,1,2,5]` (8 predicate evals, bound 14). Full `lake build` green (8347 jobs). Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01AbkMyCwYRAiUy3NFwn9M4f --- Fad/Chapter2-Amortized.lean | 144 ++++++++++++++++++++++++++++++++++++ 1 file changed, 144 insertions(+) diff --git a/Fad/Chapter2-Amortized.lean b/Fad/Chapter2-Amortized.lean index 74eb8a2..86ce39a 100644 --- a/Fad/Chapter2-Amortized.lean +++ b/Fad/Chapter2-Amortized.lean @@ -192,4 +192,148 @@ the amortized bound holds although individual steps vary. -/ example : (incTimes 8 []).queriesOn bitOracle ≤ 2 * 8 := incTimes_queriesOn_le bitOracle 8 + +/-! # Second example: `build p` (Bird & Gibbons, *ADwH* §2.4) + +The book's headline amortized example, right next to the binary counter above: + +``` +build p = foldr insert [] where insert x xs = x : dropWhile (p x) xs +``` + +`build (==)` removes *adjacent* duplicates, e.g. `build (==) [4,4,2,1,1,2,5] = +[4,2,1,2,5]`. A single `insert` can be `Θ(k)` — its `dropWhile` may scan the +whole accumulator — so naively `build` looks `Θ(n²)`. Yet its true cost is +`Θ(n)`: **each element, once added, can be dropped at most once**, so the total +number of drops is bounded by the number of adds, `n`. The amortized cost of +`insert` is therefore `O(1)`. + +We formalise exactly the book's *uniform method* (its inequality 2.3): pick a +nonnegative size `S` and amortized cost `A` with + +``` +C(before) ≤ S(before) − S(after) + A -- for every step +``` + +then summing telescopes to `Σ C ≤ S(x₀) − S(xₙ) + Σ A`. Here `C` is `queriesOn` +(one query per predicate evaluation `p x y`), `S = length`, and `A = 2`. The +`Nat`-subtraction-free rearrangement `C(before) + S(after) ≤ S(before) + A` is +what we prove and telescope, giving the `≤ 2n` total bound. + +Unlike the counter (where amortized cost is *exactly* 2), here it is `≤ 2`, so +this example exercises the *inequality* form of the potential method. -/ + +/-- One evaluation of the adjacency predicate `p x y`; the unit of cost. Just +like the comparison query in the sorting examples, the predicate is a *query*. -/ +inductive PredOp (a : Type) : Type → Type where + | ask : a → a → PredOp a Bool + +/-- Emit one predicate query. -/ +def ask {a : Type} (x y : a) : FreeM (PredOp a) Bool := FreeM.lift (PredOp.ask x y) + +/-- Honest oracle: answer `ask x y` with the actual predicate `p x y`. -/ +def predOracle {a : Type} (p : a → a → Bool) : {ι : Type} → PredOp a ι → ι + | _, .ask x y => p x y + +/-- `dropWhile (p x)`, made explicit: one `ask` per element examined. -/ +def dropW {a : Type} (x : a) : List a → FreeM (PredOp a) (List a) + | [] => pure [] + | y :: ys => do + let b ← ask x y + if b then dropW x ys else pure (y :: ys) + +/-- `insert x xs = x : dropWhile (p x) xs`. -/ +def ins {a : Type} (x : a) (xs : List a) : FreeM (PredOp a) (List a) := do + let r ← dropW x xs + pure (x :: r) + +/-- `build p = foldr insert []`. -/ +def build {a : Type} : List a → FreeM (PredOp a) (List a) + | [] => pure [] + | x :: xs => do + let r ← build xs + ins x r + +-- ## Step lemmas for `dropW` + +@[simp] theorem dropW_eval_nil {a : Type} (o : {ι : Type} → PredOp a ι → ι) (x : a) : + (dropW x ([] : List a)).eval o = [] := by simp [dropW] +@[simp] theorem dropW_queriesOn_nil {a : Type} (o : {ι : Type} → PredOp a ι → ι) (x : a) : + (dropW x ([] : List a)).queriesOn o = 0 := by simp [dropW] + +theorem dropW_eval_cons {a : Type} (o : {ι : Type} → PredOp a ι → ι) + (x y : a) (ys : List a) : + (dropW x (y :: ys)).eval o = + if o (PredOp.ask x y) then (dropW x ys).eval o else y :: ys := by + simp [dropW, ask]; split <;> simp_all + +theorem dropW_queriesOn_cons {a : Type} (o : {ι : Type} → PredOp a ι → ι) + (x y : a) (ys : List a) : + (dropW x (y :: ys)).queriesOn o = + 1 + (if o (PredOp.ask x y) then (dropW x ys).queriesOn o else 0) := by + simp [dropW, ask]; split <;> simp_all + +/-! ### The uniform bound (eq. 2.3) for one `dropWhile`/`insert` + +`S = length`, `A = 2`. Everything below is `Nat`-subtraction-free. -/ + +/-- Cost plus size-after ≤ size-before + 1 for a `dropWhile`: the drops are the +"free" part paid for when the elements were originally added. -/ +theorem dropW_bound {a : Type} (o : {ι : Type} → PredOp a ι → ι) (x : a) (xs : List a) : + (dropW x xs).queriesOn o + ((dropW x xs).eval o).length ≤ xs.length + 1 := by + induction xs with + | nil => simp + | cons y ys ih => + rw [dropW_queriesOn_cons, dropW_eval_cons] + cases h : o (PredOp.ask x y) <;> simp <;> omega + +/-- The book's inequality 2.3 for one `insert`: `C ≤ S(before) − S(after) + 2`, +in the subtraction-free form `C + S(after) ≤ S(before) + 2`. -/ +theorem ins_bound {a : Type} (o : {ι : Type} → PredOp a ι → ι) (x : a) (xs : List a) : + (ins x xs).queriesOn o + ((ins x xs).eval o).length ≤ xs.length + 2 := by + have hq : (ins x xs).queriesOn o = (dropW x xs).queriesOn o := by simp [ins] + have he : ((ins x xs).eval o).length = ((dropW x xs).eval o).length + 1 := by + simp [ins, List.length_cons] + rw [hq, he] + have := dropW_bound o x xs + omega + +/-! ### Telescoped: `build` is `Θ(n)` -/ + +/-- Summing the per-step bound telescopes: total cost + final size ≤ `2n`. -/ +theorem build_amortized {a : Type} (o : {ι : Type} → PredOp a ι → ι) (xs : List a) : + (build xs).queriesOn o + ((build xs).eval o).length ≤ 2 * xs.length := by + induction xs with + | nil => simp [build] + | cons x xs ih => + have hq : (build (x :: xs)).queriesOn o + = (build xs).queriesOn o + (ins x ((build xs).eval o)).queriesOn o := by + simp [build] + have he : (build (x :: xs)).eval o = (ins x ((build xs).eval o)).eval o := by + simp [build] + rw [hq, he, List.length_cons] + have hins := ins_bound o x ((build xs).eval o) + omega + +/-- **Amortized `O(1)` per insert.** `build` on `n` elements makes at most `2 n` +predicate evaluations, though a single `insert` can make `Θ(k)`. -/ +theorem build_queriesOn_le {a : Type} (o : {ι : Type} → PredOp a ι → ι) (xs : List a) : + (build xs).queriesOn o ≤ 2 * xs.length := by + have := build_amortized o xs + omega + +/-! ## Demonstration (the book's own example) + +`build (==)` removing adjacent duplicates, exactly as in Bird & Gibbons. -/ + +/-- Honest oracle for `build (==)`. -/ +def eqOracle : {ι : Type} → PredOp Nat ι → ι := predOracle (fun x y => x == y) + +#eval (build [4, 4, 2, 1, 1, 2, 5]).eval eqOracle -- [4, 2, 1, 2, 5] (the book) +#eval (build [4, 4, 2, 1, 1, 2, 5]).queriesOn eqOracle -- 8 (predicate evaluations) +#eval 2 * [4, 4, 2, 1, 1, 2, 5].length -- 14 (the amortized bound 2n) + +example : (build [4, 4, 2, 1, 1, 2, 5]).queriesOn eqOracle ≤ 2 * 7 := by + simpa using build_queriesOn_le eqOracle [4, 4, 2, 1, 1, 2, 5] + end Chapter2Amortized