diff --git a/Fad.lean b/Fad.lean index 3db5ac3..65669a6 100644 --- a/Fad.lean +++ b/Fad.lean @@ -9,6 +9,8 @@ import Fad.«Chapter1-Ex» import Fad.Chapter2 import Fad.«Chapter2-Ex» +import Fad.«Chapter2-Query» +import Fad.«Chapter2-Amortized» import Fad.Chapter3 import Fad.«Chapter3-Ex» 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/Chapter10.lean b/Fad/Chapter10.lean new file mode 100644 index 0000000..851d4ff --- /dev/null +++ b/Fad/Chapter10.lean @@ -0,0 +1,1110 @@ + +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 + +/-- 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 [LinearOrder b] + (r : a → a → Prop) + (cost : a → b) + (xs ys : List a) + (hmono : ∀ x y, r x y → cost x ≤ cost y) + (h : ThinBy r xs ys) : + 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*} [LinearOrder β] + (r : a → a → Prop) (cost : a → β) + (hmono : ∀ x y, cost x ≤ cost y → r x y) : + ∀ (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`. -/ +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 + 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 (exercises): + + * 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. +-/ + +-- ## 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₁ + +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]` + 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 +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. -/ + +-- 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 + +/-! 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⟩ + · -- 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 + + +/-! ### 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₁) + +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] + +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] + 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] + simp only [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₁ + +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 diff --git a/Fad/Chapter13.lean b/Fad/Chapter13.lean index ec76540..548c52e 100644 --- a/Fad/Chapter13.lean +++ b/Fad/Chapter13.lean @@ -1,6 +1,9 @@ import Fad.Chapter1 +import Fad.Chapter10 +import Fad.API namespace Chapter13 + open Chapter1 (scanr₀) @@ -11,18 +14,125 @@ 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) + +-- #eval fib₀ 10 +-- #eval fib₀T 10 +-- The complexity is exponential +-- #eval [5, 10, 15, 20].map fun n => (n, (fib₀T n).time) + +--Litaral translation of tab and fib1 -def tab (f : Nat → Int) (lo hi : Nat) : Array Int := +def tabAntigo (f : Nat → Int) (lo hi : Nat) : Array Int := (List.range (hi - lo + 1)).map (fun i => f (lo + i)) |>.toArray -def fib₁ (n : Nat) : Int := +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 := tab a 0 n + 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" + +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" + + +-- 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) @@ -32,15 +142,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 @@ -49,8 +195,23 @@ 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 +--#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 @@ -66,14 +227,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 diff --git a/Fad/Chapter2-Amortized.lean b/Fad/Chapter2-Amortized.lean new file mode 100644 index 0000000..86ce39a --- /dev/null +++ b/Fad/Chapter2-Amortized.lean @@ -0,0 +1,339 @@ +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 + + +/-! # 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 diff --git a/Fad/Chapter2-Query.lean b/Fad/Chapter2-Query.lean new file mode 100644 index 0000000..8787cfb --- /dev/null +++ b/Fad/Chapter2-Query.lean @@ -0,0 +1,226 @@ +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 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 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. +-/ + +set_option autoImplicit false + +open Cslib (FreeM) + +namespace Chapter2Query + +/-! ## `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 +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 + +/-- 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 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* 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 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] + +/-- 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 `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 [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 *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 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 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) → FreeM (ConcatOp a) (List a) + | [] => pure [] + | xs :: xss => do + let ys ← concat₁ xss + 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 → FreeM (ConcatOp a) (List a) + | [], acc => pure acc + | xs :: xss, acc => do + let acc' ← FreeM.lift (ConcatOp.app acc xs) + concat₂ xss acc' + +/-- 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).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) + 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 + +/-- 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).cost concatOracle concatWeight : 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).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 + 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`/`.queriesOn` return the cost. -/ + +-- `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 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]]).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/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 diff --git a/README.md b/README.md index e33e6fa..06c8cc2 100644 --- a/README.md +++ b/README.md @@ -109,11 +109,11 @@ Along the way, readers gain experience not only in algorithm design, but also in 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 @@ -134,7 +134,7 @@ Along the way, readers gain experience not only in algorithm design, but also in 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 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