CLRS-Lean
Chapters 1–35 · CLRS Fourth Edition
Chapter 27. Online Algorithms

Chapter 27 — Online Algorithms

CLRS, fourth edition · Lean 4 formalization

The proofs below use the models and assumptions described in the scope and implementation notes.

Imports

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

27.1. Waiting for an Elevator

This section formalizes the rent-or-buy (ski rental) problem that opens CLRS §27.1 on online algorithms. You can rent the equipment for r per day or buy it for a one-time cost p, without knowing how many days you will need it. An online algorithm must choose rent-or-buy as the days arrive; the offline optimum knows the total number of days in advance. The elevator scenario of the section — wait for the elevator (renting, one time unit at a time) and if it does not come by time S - E, take the stairs (buying at cost S) — is the same problem with r = 1 and p scaled by the elevator ride time E.

Main results:

Definition SkiRental.rentThenBuyCost: the cost of the deterministic strategy that rents for the first a days and buys on day a+1 if the trip outlasts it.
Definition SkiRental.optCost: the optimal offline cost, min (T*r) p.
Definition SkiRental.IsCompetitive: a strategy is c-competitive when its cost is at most c times the optimal offline cost on every input.
Theorem SkiRental.rentThenBuy_two_competitive (Theorem 27.1, upper bound): any strategy that rents a days with a*r < p ≤ (a+1)*r — rent strictly less than the break-even point, buy no later than the day renting overtakes buying — is 2-competitive.
Definition SkiRental.Strategy and SkiRental.onlineCost: the general causal model of a deterministic online strategy (its first buy day, or never).
Theorem SkiRental.rentThenBuy_lower_bound / SkiRental.skiRental_lower_bound (Theorem 27.1, lower bound): no deterministic strategy beats 2 - r/p.
Definition Elevator.cost and Elevator.optCost: the elevator instance.
Theorem Elevator.elevator_two_competitive: the "wait S - E then take the stairs" strategy is 2-competitive.
Theorem Elevator.elevator_lower_bound: no deterministic wait beats 2 - E/S.
Lemma Elevator.elevator_worst_case_ratio: when the elevator comes late the cost is exactly (2 - E/S) * S, the competitive ratio stated in CLRS §27.1.

The model is deliberately thin: costs are real numbers, the input is the total number of days T : ℕ, and a deterministic online strategy is its first buy day (a "rent a days then buy" threshold, or none for "never buy"), which is the general causal model — an online strategy decides rent-or-buy day by day without seeing the future, and buying is irreversible. The deterministic lower bound 2 - r/p (and its elevator form 2 - E/S) is formalized as an adversarial construction: for every strategy there is a finite input on which it pays at least 2 - r/p times the offline optimum.

Notation conventions used in this section:

r : the daily rental cost
p : the one-time purchase cost
a : the number of days a strategy rents before buying
T : the total number of days (the input, unknown to the online algorithm)
E : the elevator ride time
S : the time the stairs take
w : the number of seconds a strategy waits before taking the stairs

              noncomputable sectionnamespace CLRSnamespace SkiRental

The cost of the deterministic online strategy that rents for the first a days and, if the trip lasts longer than a days, buys on day a+1, on an input of T days: it pays T * r (renting every day) when T ≤ a, and a * r + p (renting a days then buying) otherwise. r is the per-day rental cost and p the one-time purchase cost (CLRS §27.1).

def rentThenBuyCost (r p : ℝ) (a T : ℕ) : ℝ :=
  if T ≤ a then (T : ℝ) * r else (a : ℝ) * r + p

The optimal offline cost for a trip of T days: rent every day (cost T * r) or buy once (cost p), whichever is cheaper. The offline optimum knows T in advance.

def optCost (r p : ℝ) (T : ℕ) : ℝ :=
  min ((T : ℝ) * r) p

A deterministic strategy a is c-competitive when, on every input T, its cost is at most c times the optimal offline cost.

def IsCompetitive (r p c : ℝ) (a : ℕ) : Prop :=
  ∀ T : ℕ, rentThenBuyCost r p a T ≤ c * optCost r p T

On a trip short enough that renting every day is no more than buying, the offline optimum is to rent every day.


lemma optCost_eq_rent (r p : ℝ) (T : ℕ) (h : (T : ℝ) * r ≤ p) :
    optCost r p T = (T : ℝ) * r := by
  rw [optCost]
  exact min_eq_left h

On a trip long enough that buying costs no more than renting every day, the offline optimum is to buy.


lemma optCost_eq_buy (r p : ℝ) (T : ℕ) (h : p ≤ (T : ℝ) * r) :
    optCost r p T = p := by
  rw [optCost]
  exact min_eq_right h

A short trip's cost under the rent-a-then-buy strategy is pure renting.


lemma rentThenBuyCost_short (r p : ℝ) (a T : ℕ) (h : T ≤ a) :
    rentThenBuyCost r p a T = (T : ℝ) * r := by
  rw [rentThenBuyCost]
  exact if_pos h

A long trip's cost under the rent-a-then-buy strategy is renting a days and then buying.


lemma rentThenBuyCost_long (r p : ℝ) (a T : ℕ) (h : ¬ T ≤ a) :
    rentThenBuyCost r p a T = (a : ℝ) * r + p := by
  rw [rentThenBuyCost]
  exact if_neg h

Theorem 27.1 (rent-or-buy is 2-competitive), upper bound. Let r > 0 be the daily rental cost and p > 0 the purchase cost. A strategy that rents for a days with a * r < p ≤ (a + 1) * r — renting strictly less than the break-even point, and buying no later than the day renting overtakes buying — is 2-competitive: whatever the number of days T, it pays at most twice the optimal offline cost. (CLRS §27.1 shows the strategy that waits S - E seconds before taking the stairs is exactly this with competitive ratio 2 - E/S.)

set_option linter.unusedVariables false in


theorem rentThenBuy_two_competitive (r p : ℝ) {a : ℕ} (hr : 0 < r) (hp : 0 < p)
    (hlt : (a : ℝ) * r < p) (hge : p ≤ ((a + 1 : ℕ) : ℝ) * r) :
    IsCompetitive r p 2 a := by
  intro T
  by_cases hT : T ≤ a
  · -- Short trip: the strategy rents every day, exactly the optimum.
    have hcost : rentThenBuyCost r p a T = (T : ℝ) * r :=
      rentThenBuyCost_short r p a T hT
    have hTle : (T : ℝ) ≤ (a : ℝ) := by exact_mod_cast hT
    have hTrp : (T : ℝ) * r ≤ p := by
      calc
        (T : ℝ) * r ≤ (a : ℝ) * r := mul_le_mul_of_nonneg_right hTle (le_of_lt hr)
        _ ≤ p := le_of_lt hlt
    have hopt : optCost r p T = (T : ℝ) * r := optCost_eq_rent r p T hTrp
    rw [hcost, hopt]
    have hnn : 0 ≤ (T : ℝ) * r := mul_nonneg (Nat.cast_nonneg T) (le_of_lt hr)
    nlinarith
  · -- Long trip: the strategy rents `a` days then buys, and the optimum buys.
    have haT : a < T := Nat.lt_of_not_ge hT
    have hcost : rentThenBuyCost r p a T = (a : ℝ) * r + p :=
      rentThenBuyCost_long r p a T hT
    have hTge : ((a + 1 : ℕ) : ℝ) ≤ (T : ℝ) := by exact_mod_cast (Nat.succ_le_of_lt haT)
    have hTrp : p ≤ (T : ℝ) * r :=
      le_trans hge (mul_le_mul_of_nonneg_right hTge (le_of_lt hr))
    have hopt : optCost r p T = p := optCost_eq_buy r p T hTrp
    rw [hcost, hopt]
    have hle : (a : ℝ) * r ≤ p := le_of_lt hlt
    nlinarith

Deterministic lower bound

A deterministic online strategy for ski rental is its first buy day: it rents days 0 .. a-1 and buys on day a if the trip lasts that long, or none if it never buys. This is the general causal model — an online strategy must decide rent-or-buy day by day without seeing the future, and buying is irreversible, so the whole strategy is determined by this one threshold.

abbrev Strategy := Option ℕ

The cost of running a deterministic strategy s on a trip of T days: the threshold strategy rents then buys, and the never-buy strategy rents every day.

def onlineCost (r p : ℝ) (s : Strategy) (T : ℕ) : ℝ :=
  match s with
  | none => (T : ℝ) * r
  | some a => rentThenBuyCost r p a T

Theorem 27.1 (deterministic lower bound), threshold form. For r > 0 and p > 0, no rent-a-then-buy threshold strategy beats competitive ratio 2 - r/p: for every a there is an input T on which it pays at least (2 - r/p) times the optimal offline cost.


theorem rentThenBuy_lower_bound (r p : ℝ) (hr : 0 < r) (hp : 0 < p) (a : ℕ) :
    ∃ T : ℕ, 0 < T ∧ 0 < optCost r p T ∧
      (2 - r / p) * optCost r p T ≤ rentThenBuyCost r p a T := by
  refine ⟨a + 1, by omega, ?_, ?_⟩
  · exact lt_min (mul_pos (by positivity) hr) hp
  have ha0 : 0 ≤ (a : ℝ) := Nat.cast_nonneg a
  have hcost : rentThenBuyCost r p a (a + 1) = (a : ℝ) * r + p := by
    apply rentThenBuyCost_long
    intro h
    omega
  rw [hcost]
  have hcast : ((a + 1 : ℕ) : ℝ) = (a : ℝ) + 1 := by norm_num
  by_cases hle : ((a + 1 : ℕ) : ℝ) * r ≤ p
  · -- Buy early: the optimum is to rent every day; the strategy buys too soon.
    have hopt : optCost r p (a + 1) = ((a + 1 : ℕ) : ℝ) * r := optCost_eq_rent r p (a + 1 : ℕ) hle
    rw [hopt]
    rw [hcast]
    have hrp : r ≤ p := by
      have h1 : r ≤ ((a : ℝ) + 1) * r := by nlinarith [ha0]
      exact le_trans h1 (by rw [← hcast]; exact hle)
    have hprod : 0 ≤ (p - r) * (p - ((a : ℝ) + 1) * r) := by
      exact mul_nonneg (sub_nonneg.mpr hrp) (sub_nonneg.mpr (by rw [← hcast]; exact hle))
    have hid : p * ((a : ℝ) * r + p - (2 - r / p) * ((a : ℝ) + 1) * r) =
        (p - r) * (p - ((a : ℝ) + 1) * r) := by
      field_simp [ne_of_gt hp]
      ring
    have hnn : 0 ≤ p * ((a : ℝ) * r + p - (2 - r / p) * ((a : ℝ) + 1) * r) := by
      rw [hid]
      exact hprod
    nlinarith
  · -- Buy at or after break-even: the optimum is to buy; the strategy rents first.
    have hopt : optCost r p (a + 1) = p := optCost_eq_buy r p (a + 1 : ℕ) (le_of_not_ge hle)
    rw [hopt]
    have hge : p ≤ ((a : ℝ) + 1) * r := by rw [← hcast]; exact le_of_not_ge hle
    field_simp [ne_of_gt hp]
    nlinarith [hr, hp, hge, ha0]

Theorem 27.1 (deterministic lower bound). For r > 0 and p > 0, no deterministic online strategy beats competitive ratio 2 - r/p: for every strategy there is an input T on which it pays at least (2 - r/p) times the optimal offline cost.


theorem skiRental_lower_bound (r p : ℝ) (hr : 0 < r) (hp : 0 < p) (s : Strategy) :
    ∃ T : ℕ, 0 < T ∧ 0 < optCost r p T ∧
      (2 - r / p) * optCost r p T ≤ onlineCost r p s T := by
  cases s with
  | none =>
      -- The strategy never buys, so on a long trip it pays `T * r` while the
      -- optimum is `p`; pick `T` large enough that `2 * p - r ≤ T * r`.
      obtain ⟨T, hT⟩ := exists_nat_gt (2 * p / r : ℝ)
      have hTpos : 0 < T := by
        have hq : 0 < 2 * p / r := div_pos (by positivity) hr
        have ht : (0 : ℝ) < T := hq.trans hT
        exact_mod_cast ht
      refine ⟨T, hTpos, lt_min (mul_pos (by exact_mod_cast hTpos) hr) hp, ?_⟩
      simp [onlineCost]
      have hmul : (2 * p / r) * r < (T : ℝ) * r := mul_lt_mul_of_pos_right hT hr
      have h2p : (2 * p / r) * r = 2 * p := by field_simp [ne_of_gt hr]
      have hTr : 2 * p - r ≤ (T : ℝ) * r := by nlinarith
      have hp_opt : p ≤ (T : ℝ) * r := by nlinarith
      have hopt : optCost r p T = p := optCost_eq_buy r p T hp_opt
      rw [hopt]
      have hgoal : (2 - r / p) * p = 2 * p - r := by field_simp [ne_of_gt hp]
      rw [hgoal]
      exact hTr
  | some a =>
      simp [onlineCost]
      exact rentThenBuy_lower_bound r p hr hp a

Strictly smaller ratios fail on a positive-cost finite input.

theorem skiRental_not_competitive_below (r p c : ℝ) (hr : 0 < r) (hp : 0 < p)
    (s : Strategy) (hc : c < 2 - r / p) :
    ∃ T : ℕ, 0 < T ∧ c * optCost r p T < onlineCost r p s T := by
  obtain ⟨T,hT,hpos,hbound⟩ := skiRental_lower_bound r p hr hp s
  exact ⟨T,hT,(mul_lt_mul_of_pos_right hc hpos).trans_le hbound⟩

end SkiRentalnamespace Elevator

The cost of the online strategy that waits w seconds and then, if the elevator has not arrived, takes the stairs, on the input where the elevator arrives after t seconds. If it arrives in time (t ≤ w) the cost is t + E; otherwise the elevator is treated as having never arrived and the cost is w + S. E is the elevator ride time and S the stairs time (CLRS §27.1).

def cost (E S w t : ℝ) : ℝ :=
  if t ≤ w then t + E else w + S

The optimal offline cost when the elevator arrives after t seconds: take the elevator (waiting t and riding E) or take the stairs immediately (cost S), whichever is cheaper.

def optCost (E S t : ℝ) : ℝ :=
  min (t + E) S

Elevator corollary of Theorem 27.1. With elevator ride time E ≥ 0 and stairs time S > 0, the strategy that waits S - E seconds and then takes the stairs is 2-competitive: whatever the arrival time t ≥ 0, it pays at most twice the optimal offline cost.

set_option linter.unusedVariables false in


theorem elevator_two_competitive (E S : ℝ) (hE : 0 ≤ E) (hS : 0 < S) :
    ∀ t : ℝ, 0 ≤ t → cost E S (S - E) t ≤ 2 * optCost E S t := by
  intro t ht0
  by_cases ht : t ≤ S - E
  · -- The elevator comes in time: the strategy is optimal.
    have hcost : cost E S (S - E) t = t + E := by
      simp [cost, ht]
    have hle : t + E ≤ S := by
      nlinarith
    have hopt : optCost E S t = t + E := by
      rw [optCost]
      exact min_eq_left hle
    rw [hcost, hopt]
    have hnn : 0 ≤ t + E := by
      nlinarith [ht0, hE]
    nlinarith
  · -- The elevator comes late (or never): the strategy takes the stairs.
    have hcost : cost E S (S - E) t = (S - E) + S := by
      simp [cost, ht]
    have hgt : S < t + E := by
      nlinarith
    have hopt : optCost E S t = S := by
      rw [optCost]
      exact min_eq_right (le_of_lt hgt)
    rw [hcost, hopt]
    nlinarith [hS, hE]

Worst-case cost ratio. When the elevator comes after the wait time, the "wait S - E then take the stairs" strategy pays exactly (2 - E/S) * S, so its competitive ratio on that input is 2 - E/S, matching the value stated in CLRS §27.1. For 0 < E < S the ratio lies strictly between 1 and 2 (the second conjunct).

lemma elevator_worst_case_ratio (E S : ℝ) (hE : 0 < E) (hS : 0 < S) :
    (S - E) + S = (2 - E / S) * S ∧ (2 - E / S) < 2 := by
  constructor
  · field_simp [ne_of_gt hS]
    ring
  · have hpos : 0 < E / S := div_pos hE hS
    linarith

Elevator lower bound (corollary of the deterministic bound). For 0 < E < S, no deterministic wait threshold w beats competitive ratio 2 - E/S: for every w ≥ 0 there is an arrival time t ≥ 0 on which the strategy pays at least (2 - E/S) times the optimal offline cost. Combined with elevator_two_competitive, the "wait S - E then stairs" strategy is exactly optimal.


theorem elevator_lower_bound (E S : ℝ) (hE : 0 < E) (hS : 0 < S) (hES : E < S)
    (w : ℝ) (hw0 : 0 ≤ w) :
    ∃ t : ℝ, 0 ≤ t ∧ (2 - E / S) * optCost E S t ≤ cost E S w t := by
  have hdiv : E / S < 1 := (div_lt_one hS).mpr hES
  have hden : 0 < 2 - E / S := by nlinarith
  have hden2 : 2 - E / S ≠ 0 := ne_of_gt hden
  have hpos : 0 < S * 2 - E := by nlinarith [hES, hS]
  have hpos2 : S * 2 - E ≠ 0 := ne_of_gt hpos
  by_cases hw : w < S - E
  · -- Too eager: the elevator arrives exactly at the adversarial boundary.
    let t : ℝ := (w + S) / (2 - E / S) - E
    refine ⟨t, ?_, ?_⟩
    · dsimp [t]
      field_simp [hden2, hpos2, ne_of_gt hS]
      nlinarith [hE, hS, hw0, sq_nonneg (S - E)]
    · have hgt : w < t := by
        dsimp [t]
        field_simp [hden2, hpos2, ne_of_gt hS]
        nlinarith [hw, hES, hS]
      have hcost : cost E S w t = w + S := by
        rw [cost, if_neg (show ¬ t ≤ w by intro htle; nlinarith [hgt])]
      rw [hcost]
      have hleS : t + E ≤ S := by
        dsimp [t]
        field_simp [hden2, hpos2, ne_of_gt hS]
        nlinarith [hw, hES, hS]
      have hopt : optCost E S t = t + E := by
        rw [optCost]
        exact min_eq_left hleS
      rw [hopt]
      have hmain : (2 - E / S) * (t + E) = w + S := by
        dsimp [t]
        rw [sub_add_cancel]
        exact mul_div_cancel₀ (w + S) hden2
      rw [hmain]
  · -- Patient enough: the elevator arrives after the wait is abandoned.
    refine ⟨w + 1, ?_, ?_⟩
    · nlinarith [hw0]
    · have hle : S - E ≤ w := le_of_not_gt hw
      have hcost : cost E S w (w + 1) = w + S := by
        rw [cost, if_neg (show ¬ w + 1 ≤ w by nlinarith)]
      rw [hcost]
      have hopt : optCost E S (w + 1) = S := by
        rw [optCost]
        apply min_eq_right
        nlinarith [hle]
      rw [hopt]
      have hmain : (2 - E / S) * S = 2 * S - E := by
        field_simp [ne_of_gt hS]
      rw [hmain]
      exact (by nlinarith [hle] : 2 * S - E ≤ w + S)

end Elevatorend CLRS

Imports

import Mathlib.Data.List.Basic
import Mathlib.Tactic

27.2. Maintaining a Search List

This section formalizes the list-update problem that CLRS §27.2 uses to introduce amortized competitive analysis of online algorithms. A list of distinct keys must serve a sequence of requests; servicing a request costs the position of the requested key (scanning from the front). An online list-update strategy may rearrange its list after each request, paying for the rearrangement, while the offline optimum knows the whole request sequence in advance. MOVE-TO-FRONT — after each request, move the requested key to the front — is the classic deterministic strategy, and CLRS §27.2 proves it is 4-competitive by the potential method.

Main results:

Definition SearchList.before: strict order (a before b) in a list.
Definition SearchList.position: the 0-based position of a key in a list.
Definition SearchList.invDist: the inversion distance between two lists.
Definition SearchList.moveToFront: move a key to the front of a list.
Definition SearchList.potential: the potential function 2 * invDist.
Lemma SearchList.invDist_moveToFront_add_pos: the phase-1 potential change.
Lemma SearchList.invDist_triangle: the triangle inequality for invDist.
Theorem SearchList.mtf_step_four_competitive: the per-request amortized bound that drives the potential argument.
Theorem SearchList.mtf_four_competitive (Theorem 27.2): MOVE-TO-FRONT is 4-competitive against any list-update strategy.

The core theorem uses equality of resident key sets via toFinset, not List.Perm or a no-duplicates invariant. Its counters remain defined on lists with duplicate keys, but then distinct preceding keys need not equal physical indices, and inversion counts are not minimum adjacent-swap costs. The textbook list interpretation requires distinct-key lists preserved as permutations. Requests must lie in the list. The competing strategy is a function List α → α → List α; arbitrary offline traces or auxiliary strategy state are not represented by this interface. Initial potential is zero when both strategies start from the same list.

Notation conventions used in this section:

L : the list maintained by MOVE-TO-FRONT
M : the list maintained by the competing strategy
σ : the request sequence
x : the current request
A : a list-update strategy

              namespace CLRSnamespace SearchListvariable {α : Type} [DecidableEq α]

a is strictly before b in the list L (both elements present).

def before (a b : α) (L : List α) : Prop :=
  b ∈ L ∧ a ∈ L.takeWhile (fun c => decide (c ≠ b))

Membership in before is decidable for DecidableEq α.

instance before_decidable (a b : α) (L : List α) : Decidable (before a b L) :=
  inferInstanceAs (Decidable (b ∈ L ∧ a ∈ L.takeWhile (fun c => decide (c ≠ b))))

Number of distinct keys strictly before the first occurrence of x. This is its 0-based index only for a duplicate-free list containing the key.

def position (x : α) (L : List α) : ℕ :=
  (L.toFinset.filter (fun y => before y x L)).card

Inversion distance: the number of unordered element pairs whose relative order differs between the two lists. The minimum adjacent-swap interpretation requires duplicate-free permutations; equal key sets alone do not suffice.

def invDist (L₁ L₂ : List α) : ℕ :=
  (L₁.toFinset.sum fun a =>
    (L₁.toFinset.filter (fun b => before a b L₁ ∧ before b a L₂)).card)

The cost of servicing one request x by scanning from the front: the 1-based position.

def scanCost (x : α) (L : List α) : ℕ := position x L + 1

The cost of servicing one request x with MOVE-TO-FRONT: scanning to the position and then swapping x to the front (2·position + 1).

def mtfCost (x : α) (L : List α) : ℕ := 2 * position x L + 1

Move-to-front: after accessing x, bring it to the front of the list.

def moveToFront (x : α) (L : List α) : List α := x :: L.erase x

A list-update strategy: given the current list and the request, the next list.

abbrev Strategy (α : Type) [DecidableEq α] := List α → α → List α

Potential function: twice the inversion distance between the two lists.

def potential (L₁ L₂ : List α) : ℕ := 2 * invDist L₁ L₂

Cost of a general strategy processing request x from list L to list L': the scan cost plus the inversion distance of the rearrangement.

def strategyCost (x : α) (L L' : List α) : ℕ := scanCost x L + invDist L L'

Total cost of MOVE-TO-FRONT over a request sequence.

def mtfTotalCost : List α → List α → ℕ
  | [], _ => 0
  | x :: σ, L => mtfCost x L + mtfTotalCost σ (moveToFront x L)

Total cost of a strategy over a request sequence.

def strategyTotalCost (A : Strategy α) : List α → List α → ℕ
  | [], _ => 0
  | x :: σ, L => strategyCost x L (A L x) + strategyTotalCost A σ (A L x)

Final list after running MOVE-TO-FRONT over a request sequence.

def mtfRun : List α → List α → List α
  | [], L => L
  | x :: σ, L => mtfRun σ (moveToFront x L)

Final list after running a strategy over a request sequence.

def strategyRun (A : Strategy α) : List α → List α → List α
  | [], L => L
  | x :: σ, L => strategyRun A σ (A L x)

Recursion rule for before.

-- ========== basic lemmas about `before` ==========


lemma before_cons (a b x : α) (L : List α) :
    before a b (x :: L) ↔ x ≠ b ∧ b ∈ L ∧ (a = x ∨ before a b L) := by
  constructor
  · intro h
    rcases h with ⟨hb, ha⟩
    have hxb : x ≠ b := by
      intro hx
      subst x
      simp at ha
    have hbL : b ∈ L := by
      rcases (List.mem_cons.mp hb) with hb' | hb''
      · exact (hxb hb'.symm).elim
      · exact hb''
    have hxneq : decide (x ≠ b) = true := decide_eq_true hxb
    refine ⟨hxb, hbL, ?_⟩
    · unfold List.takeWhile at ha
      rw [hxneq] at ha
      rw [List.mem_cons] at ha
      rcases ha with ha | hat
      · exact Or.inl ha
      · exact Or.inr ⟨hbL, hat⟩
  · intro h
    rcases h with ⟨hxb, hbL, hdisj⟩
    have hxneq : decide (x ≠ b) = true := decide_eq_true hxb
    have hbcons : b ∈ x :: L := by
      rw [List.mem_cons]
      exact Or.inr hbL
    rcases hdisj with ha | hab
    · subst a
      unfold before
      constructor
      · exact hbcons
      · unfold List.takeWhile
        rw [hxneq]
        exact (List.mem_cons_self : x ∈ x :: (L.takeWhile (fun c => decide (c ≠ b))))
    · unfold before
      constructor
      · exact hbcons
      · unfold List.takeWhile
        rw [hxneq]
        rw [List.mem_cons]
        exact Or.inr hab.2

before is irreflexive.


lemma before_irrefl (a : α) (L : List α) : ¬ before a a L := by
  induction L with
  | nil => simp [before]
  | cons x rest ih =>
      intro h
      rw [before_cons] at h
      rcases h with ⟨hxa, ha, hdisj⟩
      rcases hdisj with heq | hrest
      · exact hxa heq.symm
      · exact ih hrest

before implies both elements are present.


lemma before_mem_left {a b : α} {L : List α} (h : before a b L) : a ∈ L := by
  induction L with
  | nil => simp [before] at h
  | cons x rest ih =>
      rw [before_cons] at h
      rcases h with ⟨hxb, hb, hdisj⟩
      rcases hdisj with heq | hrest
      · simp [heq]
      · exact List.mem_cons_of_mem x (ih hrest)

before is asymmetric.


lemma before_asymm {a b : α} {L : List α} (h : before a b L) : ¬ before b a L := by
  induction L with
  | nil => simp [before] at h
  | cons x rest ih =>
      intro hba
      rw [before_cons] at h hba
      rcases h with ⟨hxb, hb, hdisj⟩
      rcases hba with ⟨hxa, ha, hdisj'⟩
      rcases hdisj with heq | hab
      · subst a
        exact hxa rfl
      · rcases hdisj' with heq' | hba'
        · subst b
          exact hxb rfl
        · exact ih hab hba'

before implies the second element is present.

lemma before_mem_right {a b : α} {L : List α} (h : before a b L) : b ∈ L := h.1

For distinct elements of a list, exactly one of before a b L or before b a L holds (trichotomy): scanning from the front, whichever of a, b comes first is the one that is before the other.


lemma before_or_before {a b : α} {L : List α} (ha : a ∈ L) (hb : b ∈ L) (hab : a ≠ b) :
    before a b L ∨ before b a L := by
  revert a b ha hb hab
  induction L with
  | nil =>
      intro a b ha hb hab
      simp at ha
  | cons x rest ih =>
      intro a b ha hb hab
      by_cases hxa : x = a
      · subst a
        left
        rw [before_cons]
        have hbrest : b ∈ rest := by
          rcases (List.mem_cons.mp hb) with hb1 | hb2
          · exact (hab hb1.symm).elim
          · exact hb2
        exact ⟨hab, hbrest, Or.inl rfl⟩
      · by_cases hxb : x = b
        · subst b
          right
          rw [before_cons]
          have harest : a ∈ rest := by
            rcases (List.mem_cons.mp ha) with ha1 | ha2
            · exact (hxa ha1.symm).elim
            · exact ha2
          exact ⟨hxa, harest, Or.inl rfl⟩
        · have ha' : a ∈ rest := by
            rcases (List.mem_cons.mp ha) with ha1 | ha2
            · exact (hxa ha1.symm).elim
            · exact ha2
          have hb' : b ∈ rest := by
            rcases (List.mem_cons.mp hb) with hb1 | hb2
            · exact (hxb hb1.symm).elim
            · exact hb2
          rcases ih ha' hb' hab with hab' | hba'
          · left
            rw [before_cons]
            exact ⟨hxb, hb', Or.inr hab'⟩
          · right
            rw [before_cons]
            exact ⟨hxa, ha', Or.inr hba'⟩

Consequence of trichotomy: if b is not before a, then a is before b.

lemma before_of_not_before {a b : α} {L : List α} (ha : a ∈ L) (hb : b ∈ L) (hab : a ≠ b)
    (hn : ¬ before b a L) : before a b L := by
  rcases before_or_before ha hb hab with h | h
  · exact h
  · exact (hn h).elim

a ∈ L.takeWhile (· ≠ b) is unchanged by erasing an element x that is neither a nor b.

lemma mem_takeWhile_ne_erase (b x : α) (L : List α) {a : α} (hax : a ≠ x) (hbx : b ≠ x) :
    a ∈ (L.erase x).takeWhile (fun c => decide (c ≠ b)) ↔
      a ∈ L.takeWhile (fun c => decide (c ≠ b)) := by
  induction L with
  | nil => simp
  | cons y rest ih =>
      by_cases hya : a = y
      · -- `a` is the head: it survives on both sides unless `y = b` (takeWhile stops
        -- before the first `b`), and erasing `x` removes it only when `y = x`.
        subst a
        by_cases hyb : y = b
        · subst b
          by_cases hyx : y = x
          · subst x
            exfalso
            exact hbx rfl
          · simp [hyx]
        · by_cases hyx : y = x
          · subst x
            exfalso
            exact hax rfl
          · simp [hyb, hyx]
      · -- `a` is not the head: it lives in the tail, where erasing `x` (a ≠ x) and the
        -- `takeWhile` prefix (b ≠ x) are both unchanged.
        by_cases hyb : y = b
        · subst b
          by_cases hyx : y = x
          · subst x
            exfalso
            exact hbx rfl
          · simp [hyx]
        · by_cases hyx : y = x
          · subst x
            simp [hya, hyb]
          · simpa [hya, hyb, hyx] using ih

Erasing an element b does not change the membership of an element a ≠ b (it removes only the first occurrence of b).

lemma mem_erase_of_ne {a b : α} {L : List α} (h : a ≠ b) : a ∈ L.erase b ↔ a ∈ L := by
  induction L with
  | nil => simp
  | cons y rest ih =>
      by_cases hyb : y = b
      · subst b
        simp [h]
      · simp [hyb, ih]

before is invariant under move-to-front of an element distinct from both.

set_option linter.unusedVariables false in


lemma before_moveToFront_iff {a x b : α} {L : List α} (hax : a ≠ x) (hbx : b ≠ x) (hx : x ∈ L) :
    before a b (moveToFront x L) ↔ before a b L := by
  unfold moveToFront
  -- `before a b (x :: L.erase x)` vs `before a b L`: `x ≠ b` keeps the head of the
  -- takeWhile prefix, `a ≠ x` drops it from the front, and the erase is invisible
  -- to `b` (b ≠ x) and to the prefix (mem_takeWhile_ne_erase).
  rw [before]
  rw [before]
  constructor
  · intro h
    rcases h with ⟨hbcons, htw⟩
    have hbL : b ∈ L := by
      rcases (List.mem_cons.mp hbcons) with hbx' | hbEr
      · exact (hbx hbx').elim
      · exact (mem_erase_of_ne hbx).mp hbEr
    have htwL : a ∈ L.takeWhile (fun c => decide (c ≠ b)) := by
      have hhead : a ∈ (x :: L.erase x).takeWhile (fun c => decide (c ≠ b)) ↔
          a ∈ (L.erase x).takeWhile (fun c => decide (c ≠ b)) := by
        have hxnotb : x ≠ b := hbx.symm
        simp [hxnotb, hax]
      have hEr : a ∈ (L.erase x).takeWhile (fun c => decide (c ≠ b)) := (hhead.mp htw)
      exact (mem_takeWhile_ne_erase b x L hax hbx).mp hEr
    exact ⟨hbL, htwL⟩
  · intro h
    rcases h with ⟨hbL, htwL⟩
    have hbEr : b ∈ L.erase x := (mem_erase_of_ne hbx).mpr hbL
    have hbcons : b ∈ x :: L.erase x := by
      simp [hbEr]
    have htw : a ∈ (x :: L.erase x).takeWhile (fun c => decide (c ≠ b)) := by
      have hhead : a ∈ (x :: L.erase x).takeWhile (fun c => decide (c ≠ b)) ↔
          a ∈ (L.erase x).takeWhile (fun c => decide (c ≠ b)) := by
        have hxnotb : x ≠ b := hbx.symm
        simp [hxnotb, hax]
      have hEr : a ∈ (L.erase x).takeWhile (fun c => decide (c ≠ b)) :=
        (mem_takeWhile_ne_erase b x L hax hbx).mpr htwL
      exact (hhead.mpr hEr)
    exact ⟨hbcons, htw⟩

After moving x to the front, x is before every other element of the list.


lemma before_x_front {x b : α} {L : List α} (hb : b ∈ L) (hxb : x ≠ b) :
    before x b (moveToFront x L) := by
  unfold moveToFront
  rw [before]
  constructor
  · have hbEr : b ∈ L.erase x := (mem_erase_of_ne hxb.symm).mpr hb
    simp [hbEr]
  · simp [hxb]

Nothing is before the element moved to the front.

lemma not_before_x_front {x b : α} (L : List α) : ¬ before b x (moveToFront x L) := by
  unfold moveToFront
  simp [before]

The element set of a list is unchanged by moving an element of the list to the front.

lemma toFinset_moveToFront {x : α} {L : List α} (hx : x ∈ L) :
    (moveToFront x L).toFinset = L.toFinset := by
  unfold moveToFront
  ext y
  by_cases hyx : y = x
  · subst y
    simp [hx]
  · simp [hyx, mem_erase_of_ne hyx]

The moved element is at the front after move-to-front.

lemma mem_moveToFront (x : α) (L : List α) : x ∈ moveToFront x L := by
  unfold moveToFront
  simp

Move-to-front of an element already in the list preserves membership of every other element.

lemma mem_moveToFront_of_ne {x y : α} {L : List α} (hxy : x ≠ y) (hy : y ∈ L) :
    y ∈ moveToFront x L := by
  unfold moveToFront
  have hyx : y ≠ x := hxy.symm
  have hyEr : y ∈ L.erase x := (mem_erase_of_ne hyx).mpr hy
  simp [hyx, hyEr]

The position of the moved element after move-to-front is zero.

lemma position_moveToFront (x : α) (L : List α) : position x (moveToFront x L) = 0 := by
  unfold position
  simp [not_before_x_front]

position counts distinct keys preceding x.

lemma position_eq_card {x : α} {L : List α} :
    position x L = (L.toFinset.filter (fun y => before y x L)).card := rfl

Elements before x in both lists: the inversion pairs newly created or destroyed when move-to-front brings x forward.

def commonBefore (x : α) (L M : List α) : ℕ :=
  (L.toFinset.filter (fun y => before y x L ∧ before y x M)).card

The number of elements before x in both lists is at most the number before it in the second.


lemma commonBefore_le_position {x : α} {L M : List α} (hperm : L.toFinset = M.toFinset) :
    commonBefore x L M ≤ position x M := by
  unfold commonBefore position
  rw [← hperm]
  apply Finset.card_le_card
  intro y hy
  simp at hy ⊢
  exact ⟨hy.1, hy.2.2⟩

Number of pairs (a, b) from L₁ (with b ≠ a) such that a is before b in L₁ and b before a in L₂: the row of a in the inversion matrix.

def invFrom (a : α) (L₁ L₂ : List α) : ℕ :=
  (L₁.toFinset.filter (fun b => before a b L₁ ∧ before b a L₂)).card

invDist is the sum of its rows.

lemma invDist_eq_sum_invFrom (L₁ L₂ : List α) :
    invDist L₁ L₂ = ∑ a ∈ L₁.toFinset, invFrom a L₁ L₂ := rfl

The row of a does not change under move-to-front of x ≠ a, except that the b = x entry disappears (as x is now at the front).

set_option linter.unusedVariables false in


lemma invFrom_ne_moveToFront {a x : α} {L M : List α} (hax : a ≠ x) (hx : x ∈ L)
    (hperm : L.toFinset = M.toFinset) :
    invFrom a (moveToFront x L) M + (if before a x L ∧ before x a M then 1 else 0) =
      invFrom a L M := by
  unfold invFrom
  -- Rows a (≠ x): the `b ≠ x` columns are invariant (before_moveToFront_iff), and the
  -- `b = x` column is dropped because nothing precedes the moved front element.
  have hfilter :
      (moveToFront x L).toFinset.filter
          (fun b => before a b (moveToFront x L) ∧ before b a M) =
        (L.toFinset.erase x).filter (fun b => before a b L ∧ before b a M) := by
    rw [toFinset_moveToFront hx]
    ext b
    simp only [Finset.mem_filter]
    by_cases hbx : b = x
    · subst b
      simp [not_before_x_front]
    · simp [hbx, before_moveToFront_iff hax hbx hx]
  rw [hfilter]
  -- The erased column contributes exactly the `(a, x)` entry back.
  have hxS : x ∈ L.toFinset := by simpa using hx
  have hsplit :
      (L.toFinset.filter (fun b => before a b L ∧ before b a M)).card =
        ((L.toFinset.erase x).filter (fun b => before a b L ∧ before b a M)).card +
          (if before a x L ∧ before x a M then 1 else 0) := by
    by_cases hP : before a x L ∧ before x a M
    · have hxfilter : x ∈ L.toFinset.filter (fun b => before a b L ∧ before b a M) := by
        simp [hP, hxS]
      have hsplit' :
          L.toFinset.filter (fun b => before a b L ∧ before b a M) =
            insert x ((L.toFinset.erase x).filter (fun b => before a b L ∧ before b a M)) := by
        ext b
        by_cases hbx : b = x
        · subst b
          simp [hP, hxS]
        · simp [hbx]
      rw [hsplit']
      rw [Finset.card_insert_of_notMem]
      · simp [hP]
      · intro hmem
        rw [Finset.mem_filter, Finset.mem_erase] at hmem
        exact hmem.1.1 rfl
    · have hsplit' :
          L.toFinset.filter (fun b => before a b L ∧ before b a M) =
            (L.toFinset.erase x).filter (fun b => before a b L ∧ before b a M) := by
        ext b
        by_cases hbx : b = x
        · subst b
          simp [hP]
        · simp [hbx]
      rw [hsplit']
      simp [hP]
  rw [hsplit]

The row of x after move-to-front counts exactly the elements before x in M.


lemma invFrom_x_moveToFront {x : α} {L M : List α} (hperm : L.toFinset = M.toFinset) :
    invFrom x (moveToFront x L) M = position x M := by
  unfold invFrom position
  apply congrArg Finset.card
  ext b
  simp only [Finset.mem_filter]
  constructor
  · intro hb
    rcases hb with ⟨hb1, hb2, hb3⟩
    -- `before b x M` already forces `b ∈ M`.
    exact ⟨by simpa using before_mem_left hb3, hb3⟩
  · intro hb
    rcases hb with ⟨hb1, hb3⟩
    have hbx : x ≠ b := by
      intro hxeq
      subst b
      exact before_irrefl x M hb3
    have hbL : b ∈ L := by
      have hbMto : b ∈ M.toFinset := by simpa using (before_mem_left hb3 : b ∈ M)
      have hbLto : b ∈ L.toFinset := by simpa [hperm] using hbMto
      simpa using hbLto
    exact ⟨by simpa using mem_moveToFront_of_ne hbx hbL,
      before_x_front hbL hbx, hb3⟩

The row of x before move-to-front misses exactly the commonBefore pairs: the elements before x in M are split by trichotomy into those also before x in L (the commonBefore pairs) and those that x precedes in L (the invFrom row).

set_option linter.unusedVariables false in


lemma invFrom_x_eq {x : α} {L M : List α} (hperm : L.toFinset = M.toFinset)
    (hxL : x ∈ L) (hxM : x ∈ M) :
    invFrom x L M + commonBefore x L M = position x M := by
  unfold invFrom commonBefore position
  rw [← hperm]
  -- Split `position x M` over `M.toFinset` by whether each element precedes `x` in `L`.
  have hsplit :
      (L.toFinset.filter (fun b => before b x M)).card =
        (L.toFinset.filter (fun b => before b x L ∧ before b x M)).card +
          (L.toFinset.filter (fun b => ¬ before b x L ∧ before b x M)).card := by
    have hdisj : Disjoint (L.toFinset.filter (fun b => before b x L ∧ before b x M))
        (L.toFinset.filter (fun b => ¬ before b x L ∧ before b x M)) := by
      rw [Finset.disjoint_left]
      intro b hb1 hb2
      simp at hb1 hb2
      exact hb2.2.1 hb1.2.1
    have hunion : (L.toFinset.filter (fun b => before b x L ∧ before b x M)) ∪
        (L.toFinset.filter (fun b => ¬ before b x L ∧ before b x M)) =
        L.toFinset.filter (fun b => before b x M) := by
      ext b
      simp
      by_cases h : before b x L
      · simp [h]
      · simp [h]
    rw [← Finset.card_union_of_disjoint hdisj, hunion]
  -- `¬ before b x L` is `before x b L` for the elements before `x` in `M` (trichotomy).
  have hnot :
      (L.toFinset.filter (fun b => ¬ before b x L ∧ before b x M)) =
        (L.toFinset.filter (fun b => before x b L ∧ before b x M)) := by
    ext b
    simp only [Finset.mem_filter]
    by_cases hbL : b ∈ L.toFinset
    · by_cases hbM : before b x M
      · have hb : b ∈ L := by simpa using hbL
        have hbne : b ≠ x := by
          intro hb
          subst b
          exact before_irrefl x M hbM
        -- Trichotomy in `L` (both `b` and `x` are in `L`) decides `¬ before b x L ↔ before x b L`.
        rcases before_or_before hb hxL hbne with hl | hxl
        · simp [hl, before_asymm hl]
        · simp [hxl, before_asymm hxl]
      · simp [hbM]
    · simp [hbL]
  rw [hsplit, hnot]
  rw [Nat.add_comm]

The position of x splits into the elements before x in both lists and those that x precedes in M — the pairs whose inversion is destroyed by move-to-front.


lemma position_eq_common_add_removed {x : α} {L M : List α} (hxL : x ∈ L)
    (hperm : L.toFinset = M.toFinset) :
    position x L =
      commonBefore x L M +
        (L.toFinset.filter (fun a => before a x L ∧ before x a M)).card := by
  unfold position commonBefore
  have hsplit :
      (L.toFinset.filter (fun a => before a x L)).card =
        (L.toFinset.filter (fun a => before a x L ∧ before a x M)).card +
          (L.toFinset.filter (fun a => before a x L ∧ ¬ before a x M)).card := by
    have hdisj : Disjoint (L.toFinset.filter (fun a => before a x L ∧ before a x M))
        (L.toFinset.filter (fun a => before a x L ∧ ¬ before a x M)) := by
      rw [Finset.disjoint_left]
      intro a ha1 ha2
      simp at ha1 ha2
      exact ha2.2.2 ha1.2.2
    have hunion : (L.toFinset.filter (fun a => before a x L ∧ before a x M)) ∪
        (L.toFinset.filter (fun a => before a x L ∧ ¬ before a x M)) =
        L.toFinset.filter (fun a => before a x L) := by
      ext a
      simp
      by_cases h : before a x M
      · simp [h]
      · simp [h]
    rw [← Finset.card_union_of_disjoint hdisj, hunion]
  have hnot :
      (L.toFinset.filter (fun a => before a x L ∧ ¬ before a x M)) =
        (L.toFinset.filter (fun a => before a x L ∧ before x a M)) := by
    ext a
    simp only [Finset.mem_filter]
    by_cases haL : a ∈ L.toFinset
    · by_cases hax : before a x L
      · have ha : a ∈ L := by simpa using haL
        have hane : a ≠ x := by
          intro hxeq
          subst a
          exact before_irrefl x L hax
        have hxM' : x ∈ M := by
          have : x ∈ L.toFinset := by simpa using hxL
          simpa [hperm] using this
        have haM : a ∈ M := by
          have : a ∈ L.toFinset := by simpa using ha
          simpa [hperm] using this
        rcases before_or_before haM hxM' hane with hm | hxm
        · simp [hm, before_asymm hm]
        · simp [hxm, before_asymm hxm]
      · simp [hax]
    · simp [haL]
  rw [hsplit, hnot]

Phase-1 potential change. Moving x to the front of L, with the other list M held fixed, changes the inversion distance by 2·commonBefore x L M − position x L (stated in the truncation-free form). This is the engine of the move-to-front amortized analysis: the amortized cost of the move is roughly 1 + 4·commonBefore.


lemma invDist_moveToFront_add_pos {x : α} {L M : List α} (hxL : x ∈ L) (hxM : x ∈ M)
    (hperm : L.toFinset = M.toFinset) :
    invDist (moveToFront x L) M + position x L = invDist L M + 2 * commonBefore x L M := by
  let S : Finset α := L.toFinset
  let L' : List α := moveToFront x L
  let ind : α → ℕ := fun a => (if before a x L ∧ before x a M then 1 else 0)
  let removed : ℕ := (S.filter (fun a => before a x L ∧ before x a M)).card
  let pos : ℕ := (S.filter (fun a => before a x L)).card
  have hxS : x ∈ S := by simpa [S] using hxL
  have hL'toS : L'.toFinset = S := by
    dsimp [L', S]
    exact toFinset_moveToFront hxL
  -- Row relations of the inversion matrix under move-to-front.
  have hrow_ne : ∀ a, a ≠ x →
      (S.filter (fun b => before a b L' ∧ before b a M)).card + ind a =
      (S.filter (fun b => before a b L ∧ before b a M)).card := by
    intro a ha
    have h := invFrom_ne_moveToFront (a := a) ha hxL hperm
    dsimp [ind, L', S] at h ⊢
    unfold invFrom at h
    rw [toFinset_moveToFront hxL] at h
    exact h
  have hrow_x :
      (S.filter (fun b => before x b L' ∧ before b x M)).card =
        (S.filter (fun b => before x b L ∧ before b x M)).card + commonBefore x L M := by
    have h1 := invFrom_x_moveToFront (x := x) hperm
    have h2 := invFrom_x_eq hperm hxL hxM
    have h1' : (S.filter (fun b => before x b L' ∧ before b x M)).card = position x M := by
      dsimp [L', S] at h1 ⊢
      unfold invFrom at h1
      rw [toFinset_moveToFront hxL] at h1
      exact h1
    have h2' : (S.filter (fun b => before x b L ∧ before b x M)).card + commonBefore x L M =
        position x M := by
      dsimp [S] at h2 ⊢
      exact h2
    rw [h1']
    exact h2'.symm
  -- `removed` collects the destroyed inversions, summed over the rows `a ≠ x`.
  have hrem : removed = (S.erase x).sum ind := by
    have hindx : ind x = 0 := by
      dsimp [ind]
      simp [before_irrefl x L]
    calc
      removed = S.sum ind := by
        simp [removed, ind, Finset.sum_boole]
      _ = (S.erase x).sum ind + ind x := by
        rw [← Finset.sum_erase_add S ind hxS]
      _ = (S.erase x).sum ind := by
        rw [hindx, Nat.add_zero]
  -- `position x L` splits into the destroyed inversions and the common-before pairs.
  have hpos : pos = commonBefore x L M + removed := by
    have h := position_eq_common_add_removed hxL hperm
    dsimp [pos, removed, S] at h ⊢
    exact h
  -- The row-sum identity: moving `x` to the front removes the `removed` inversions and
  -- adds `position x M` of them back (the elements before `x` in `M`).
  have hmid : invDist L' M + removed = invDist L M + commonBefore x L M := by
    let row' : α → ℕ := fun a => (S.filter (fun b => before a b L' ∧ before b a M)).card
    let row : α → ℕ := fun a => (S.filter (fun b => before a b L ∧ before b a M)).card
    calc
      invDist L' M + removed = (S.sum row') + removed := by
        congr 1
        unfold invDist
        rw [hL'toS]
      _ = ((S.erase x).sum row' + row' x) + (S.erase x).sum ind := by
        rw [Finset.sum_erase_add S row' hxS]
        rw [hrem]
      _ = ((S.erase x).sum row' + (S.erase x).sum ind) + row' x := by
        omega
      _ = (S.erase x).sum (fun a => row' a + ind a) + row' x := by
        rw [← Finset.sum_add_distrib]
      _ = (S.erase x).sum row + (row x + commonBefore x L M) := by
        have hcong : (S.erase x).sum (fun a => row' a + ind a) = (S.erase x).sum row := by
          apply Finset.sum_congr rfl
          intro a ha
          have ha' : a ∈ S.erase x := ha
          have hane : a ≠ x := by
            intro hxeq
            subst a
            exact (Finset.mem_erase.mp ha').1 rfl
          exact hrow_ne a hane
        rw [hcong]
        dsimp [row', row]
        rw [hrow_x]
      _ = (S.sum row) + commonBefore x L M := by
        rw [← Finset.sum_erase_add S row hxS]
        ac_rfl
      _ = invDist L M + commonBefore x L M := by
        congr 1
  -- Put the pieces together.
  have htarget : invDist L' M + pos = invDist L M + 2 * commonBefore x L M := by
    omega
  dsimp [pos, S] at htarget
  unfold position at ⊢
  exact htarget

Triangle inequality for the inversion distance. For three lists over the same element set, the inversion distance between the first and the third is at most the sum of the two intermediate distances. Phase 2 of the amortized analysis uses the case L₁ = L' (MTF's new list), L₂ = M, L₃ = M' (OPT's list before and after): OPT's rearrangement of M can increase the potential by at most 2 · invDist M M'.


lemma invDist_triangle {L₁ L₂ L₃ : List α} (h12 : L₁.toFinset = L₂.toFinset)
    (h23 : L₂.toFinset = L₃.toFinset) :
    invDist L₁ L₃ ≤ invDist L₁ L₂ + invDist L₂ L₃ := by
  let S : Finset α := L₁.toFinset
  let r13 : α → ℕ := fun a => (S.filter (fun b => before a b L₁ ∧ before b a L₃)).card
  let r12 : α → ℕ := fun a => (S.filter (fun b => before a b L₁ ∧ before b a L₂)).card
  let r23 : α → ℕ := fun a => (S.filter (fun b => before a b L₂ ∧ before b a L₃)).card
  have hrow_le : ∀ a ∈ S, r13 a ≤ r12 a + r23 a := by
    intro a haS
    have hsplit : r13 a =
        (S.filter (fun b => before a b L₁ ∧ before b a L₃ ∧ before b a L₂)).card +
          (S.filter (fun b => before a b L₁ ∧ before b a L₃ ∧ ¬ before b a L₂)).card := by
      have hdisj : Disjoint (S.filter (fun b => before a b L₁ ∧ before b a L₃ ∧ before b a L₂))
          (S.filter (fun b => before a b L₁ ∧ before b a L₃ ∧ ¬ before b a L₂)) := by
        rw [Finset.disjoint_left]
        intro b hb1 hb2
        simp at hb1 hb2
        exact hb2.2.2.2 hb1.2.2.2
      have hunion : (S.filter (fun b => before a b L₁ ∧ before b a L₃ ∧ before b a L₂)) ∪
          (S.filter (fun b => before a b L₁ ∧ before b a L₃ ∧ ¬ before b a L₂)) =
          S.filter (fun b => before a b L₁ ∧ before b a L₃) := by
        ext b
        simp
        by_cases h : before b a L₂
        · simp [h]
        · simp [h]
      rw [← Finset.card_union_of_disjoint hdisj, hunion]
    have h1 : (S.filter (fun b => before a b L₁ ∧ before b a L₃ ∧ before b a L₂)).card ≤ r12 a := by
      apply Finset.card_le_card
      intro b hb
      simp at hb ⊢
      exact ⟨hb.1, hb.2.1, hb.2.2.2⟩
    have h2 : (S.filter (fun b => before a b L₁ ∧ before b a L₃ ∧ ¬ before b a L₂)).card ≤ r23 a := by
      apply Finset.card_le_card
      intro b hb
      simp at hb ⊢
      rcases hb with ⟨hbS, hbal1, hba3, hnb2⟩
      have hb2 : b ∈ L₂ := by
        have : b ∈ L₃ := before_mem_left hba3
        have : b ∈ L₃.toFinset := by simpa using this
        have : b ∈ L₂.toFinset := by simpa [h23] using this
        simpa using this
      have ha2 : a ∈ L₂ := by
        have ha1 : a ∈ L₁ := before_mem_left hbal1
        have : a ∈ L₁.toFinset := by simpa using ha1
        have : a ∈ L₂.toFinset := by simpa [h12] using this
        simpa using this
      have hbne : b ≠ a := by
        intro hba
        subst b
        exact before_irrefl a L₃ hba3
      rcases before_or_before hb2 ha2 hbne with hba2 | hab2
      · exact (hnb2 hba2).elim
      · exact ⟨hbS, hab2, hba3⟩
    calc
      r13 a = (S.filter (fun b => before a b L₁ ∧ before b a L₃ ∧ before b a L₂)).card +
          (S.filter (fun b => before a b L₁ ∧ before b a L₃ ∧ ¬ before b a L₂)).card := hsplit
      _ ≤ r12 a + r23 a := Nat.add_le_add h1 h2
  calc
    invDist L₁ L₃ = S.sum r13 := by
      unfold invDist
      dsimp [S]
    _ ≤ S.sum (fun a => r12 a + r23 a) := by
      exact Finset.sum_le_sum hrow_le
    _ = S.sum r12 + S.sum r23 := by
      rw [Finset.sum_add_distrib]
    _ = invDist L₁ L₂ + invDist L₂ L₃ := by
      congr 1
      unfold invDist
      dsimp [r23, S]
      rw [h12]

MOVE-TO-FRONT is 4-competitive, per request (amortized). For a request x, with MTF's list L and OPT's list M permutations of the same set, after MTF moves x to the front (list moveToFront x L) and OPT moves to M', the amortized cost of MTF's move — its actual cost plus the change in the potential 2 · invDist — is at most 4 times OPT's cost for the request, plus the previous potential.

theorem mtf_step_four_competitive (x : α) (L M M' : List α)
    (hxL : x ∈ L) (hxM : x ∈ M) (hperm : L.toFinset = M.toFinset)
    (hperm' : (moveToFront x L).toFinset = M'.toFinset) :
    mtfCost x L + 2 * invDist (moveToFront x L) M' ≤
      4 * strategyCost x M M' + 2 * invDist L M := by
  have hL' : (moveToFront x L).toFinset = L.toFinset := toFinset_moveToFront hxL
  have hMM' : M.toFinset = M'.toFinset := (hL'.trans hperm).symm.trans hperm'
  have htri := invDist_triangle (L₁ := moveToFront x L) (L₂ := M) (L₃ := M')
    (hL'.trans hperm) hMM'
  calc
    mtfCost x L + 2 * invDist (moveToFront x L) M' ≤
        2 * position x L + 1 + 2 * invDist (moveToFront x L) M + 2 * invDist M M' := by
      unfold mtfCost
      nlinarith [htri]
    _ = 1 + 2 * invDist L M + 4 * commonBefore x L M + 2 * invDist M M' := by
      have h1 := invDist_moveToFront_add_pos hxL hxM hperm
      nlinarith [h1]
    _ ≤ 4 * (position x M + 1 + invDist M M') + 2 * invDist L M := by
      have hC := commonBefore_le_position (x := x) (L := L) (M := M) hperm
      nlinarith [hC, Nat.zero_le (invDist M M')]
    _ = 4 * strategyCost x M M' + 2 * invDist L M := by
      unfold strategyCost scanCost
      ring

Move-to-front of an element of L preserves membership of every element of L.

lemma mem_moveToFront_all {x : α} {L : List α} : ∀ y ∈ L, y ∈ moveToFront x L := by
  intro y hy
  by_cases hxy : x = y
  · subst y
    exact mem_moveToFront x L
  · exact mem_moveToFront_of_ne hxy hy

MOVE-TO-FRONT is 4-competitive over a request sequence. Against any list-update strategy A that keeps its list a permutation of the initial set, running MOVE-TO-FRONT from the same initial list L costs at most 4 times the strategy's cost plus the initial potential 2 · invDist L L = 0 (the additive term is zero when both start from the same list). This is Theorem 27.2 in CLRS §27.2.


theorem mtf_four_competitive (A : Strategy α) (σ L M : List α)
    (hperm : L.toFinset = M.toFinset)
    (hreq : ∀ x ∈ σ, x ∈ L)
    (hA : ∀ L x, x ∈ L → (A L x).toFinset = L.toFinset) :
    mtfTotalCost σ L ≤ 4 * strategyTotalCost A σ M + 2 * invDist L M := by
  induction σ generalizing L M with
  | nil =>
      simp [mtfTotalCost, strategyTotalCost]
  | cons x σ' ih =>
      have hxL : x ∈ L := hreq x (by simp)
      have hxM : x ∈ M := by
        have : x ∈ L.toFinset := by simpa using hxL
        have : x ∈ M.toFinset := by simpa [hperm] using this
        simpa using this
      let L' : List α := moveToFront x L
      let M' : List α := A M x
      have hperm' : L'.toFinset = M'.toFinset := by
        dsimp [L', M']
        rw [toFinset_moveToFront hxL, hA M x hxM]
        exact hperm
      have hreq' : ∀ y ∈ σ', y ∈ L' := by
        intro y hy
        have hyL : y ∈ L := hreq y (by simp [hy])
        simpa [L'] using mem_moveToFront_all y hyL
      have hstep := mtf_step_four_competitive x L M M' hxL hxM hperm (by simpa [L'] using hperm')
      have hrec := ih L' M' hperm' hreq'
      have hcombo : mtfCost x L + mtfTotalCost σ' L' ≤
          4 * strategyCost x M M' + 4 * strategyTotalCost A σ' M' + 2 * invDist L M := by
        nlinarith [hstep, hrec]
      unfold mtfTotalCost strategyTotalCost
      simp [L', M'] at hcombo ⊢
      nlinarith [hcombo]

Inversion distance between a list and itself is zero.

lemma invDist_self_zero (L : List α) : invDist L L = 0 := by
  unfold invDist
  simp
  intro i hi x hx hix
  exact before_asymm hix

end SearchListend CLRS

Imports

import Mathlib.Data.Finset.Basic
import Mathlib.Data.List.Basic
import Mathlib.Tactic

27.3. Online Caching

This section formalizes the online caching (paging) problem of CLRS §27.3 and the classical competitive-analysis bound that the LRU (least-recently-used) eviction policy is k-competitive. A cache holds at most k pages. A request for a page already in the cache is a hit (free); a request for an absent page is a miss, and the page is loaded, evicting some resident page when the cache is full. An online policy must decide evictions without knowing future requests; the offline optimum knows the whole request sequence.

Main results:

Definition lruStep / lruRun / lruMisses: the LRU policy (cache kept as a most-recent-first list) and its miss count.
Structure Algorithm: a legacy memoryless eviction policy over a finite-set cache, bundled with its validity laws (it loads the request, only adds the request, preserves capacity and hit residency on legal states), and misses. The Policies companion adds history-dependent policies and an actual inhabited LRU instance for positive capacities.
Lemma distinct_fault: a segment requesting k + 1 distinct pages forces a miss for any size-k algorithm.
Lemma resident_fault: a page resident at the start of a segment that then requests k other distinct pages forces a miss.
Lemma lru_head_evict / lru_miss_le_distinct: LRU makes at most one fault per distinct page within a segment of at most k distinct pages.
Definitions phaseGo / firstPhase / phases: the phase partition of a request sequence into maximal segments of at most k distinct pages.
Lemma lru_miss_le_phases: LRU makes at most k misses per phase, so its total miss count is bounded by k times the number of phases.
Lemma phases_le_misses: the number of phases is at most one more than the miss count of any size-k algorithm.
Theorem lru_k_competitive: LRU is k-competitive.
Lemma advSeq_misses: the Sleator-Tarjan adversary (always request the page absent from the online algorithm's cache, over the k + 1-page universe Fin (k + 1)) faults the online algorithm on every request.
Lemma offMisses_bound / offMisses_bound_from_full: the phase-based offline schedule faults at most (phases k σ).length + k times from an empty cache, and at most once per phase from a full cache.
Theorem caching_lower_bound (Theorem 27.4): for any deterministic online algorithm and any request count N there is a request sequence of length N on which the algorithm faults every request while some offline schedule faults at most N / k + k + 1 times — so no deterministic online algorithm is natural-ratio multiplicative bound below k. The stronger Policy.no_real_competitive companion includes real ratios, arbitrary additive constants and auxiliary state; Schedule.lru_k_competitive proves the upper bound against every legal offline trace.

Notation conventions used in this section:

k : the cache size
L : LRU's cache, a List Page ordered most-recent-first
C : an algorithm's cache, a Finset Page
σ : the request sequence
q : a page
A : an arbitrary eviction algorithm

              namespace CLRSnamespace OnlineCachingvariable {Page : Type} [DecidableEq Page]variable {k : ℕ}

The cache size bound: a cache holds at most k pages.

def AtMost (k : ℕ) (C : Finset Page) : Prop := C.card ≤ k

The LRU step: request p against the most-recent-first cache L. A hit moves p to the front; a miss prepends p, evicting the least-recently-used tail when the cache already has k pages.

-- ---------------------------------------------------------------------------
-- LRU: the cache is a most-recent-first list.

def lruStep (k : ℕ) (L : List Page) (p : Page) : List Page :=
  if p ∈ L then p :: L.erase p
  else if L.length < k then p :: L
  else p :: L.dropLast

The LRU cache after processing the request list σ.

def lruRun (k : ℕ) : List Page → List Page → List Page
  | L, [] => L
  | L, p :: σ => lruRun k (lruStep k L p) σ

The number of LRU misses over σ, threading the cache.

def lruMissesGo (k : ℕ) : List Page → List Page → ℕ
  | _, [] => 0
  | L, p :: σ => (if p ∈ L then 0 else 1) + lruMissesGo k (lruStep k L p) σ

The number of LRU misses over σ from the initial cache L₀.

def lruMisses (k : ℕ) (L₀ : List Page) (σ : List Page) : ℕ := lruMissesGo k L₀ σ

The 0-indexed position of q in a most-recent-first list: the number of pages strictly more recent than q (junk when q ∉ L).

def lruPos (q : Page) (L : List Page) : ℕ := (L.takeWhile (fun x => x ≠ q)).length

A deterministic paging algorithm with cache size bound k. step C p is the cache after serving request p from cache C; the bundled laws say it loads p, only ever adds p, and keeps at most k resident pages. This is the legacy memoryless policy interface. Size preservation and hit behavior are required only for legal capacity states; invalid oversized caches cannot force a contradiction. Positive capacity is necessary when pages can be requested. History-dependent online policies and offline schedules are distinct interfaces in the companion development.

-- ---------------------------------------------------------------------------
-- An arbitrary eviction algorithm (the "adversary" / offline optimum).

structure Algorithm (Page : Type) [DecidableEq Page] (k : ℕ) where
  step : Finset Page → Page → Finset Page
  step_loads : ∀ C p, p ∈ step C p
  step_subset : ∀ C p, step C p ⊆ insert p C
  step_size : ∀ C p, C.card ≤ k → (step C p).card ≤ k
  step_hit : ∀ C p, C.card ≤ k → p ∈ C → step C p = C

The algorithm's cache after processing σ.

def runGo (A : Algorithm Page k) : Finset Page → List Page → Finset Page
  | C, [] => C
  | C, p :: σ => runGo A (A.step C p) σ

The number of misses of A over σ, threading the cache.

def missesGo (A : Algorithm Page k) : Finset Page → List Page → ℕ
  | _, [] => 0
  | C, p :: σ => (if p ∈ C then 0 else 1) + missesGo A (A.step C p) σ

The number of misses of A over σ from the initial cache C₀.

def misses (A : Algorithm Page k) (C₀ : Finset Page) (σ : List Page) : ℕ :=
  missesGo A C₀ σ

The algorithm's cache never shrinks the set of requested pages beyond the initial cache: runGo A C σ ⊆ C ∪ σ.toFinset.

-- ---------------------------------------------------------------------------
-- Basic facts about the algorithm's cache.


lemma runGo_subset (A : Algorithm Page k) (C : Finset Page) (σ : List Page) :
    runGo A C σ ⊆ C ∪ σ.toFinset := by
  induction σ generalizing C with
  | nil => simp [runGo]
  | cons p τ ih =>
      rw [runGo]
      refine subset_trans (ih (A.step C p)) ?_
      rw [List.toFinset_cons]
      intro x hx
      rw [Finset.mem_union] at hx ⊢
      rcases hx with hx | hx
      · rw [Finset.mem_insert]
        have hx' := A.step_subset C p hx
        rw [Finset.mem_insert] at hx'
        rcases hx' with rfl | hx'
        · right; simp
        · left; exact hx'
      · right
        rw [Finset.mem_insert]
        exact Or.inr hx

The algorithm's cache has at most k pages throughout (given it starts within the bound).


lemma runGo_size (A : Algorithm Page k) (C : Finset Page) (σ : List Page)
    (hC : C.card ≤ k) : (runGo A C σ).card ≤ k := by
  induction σ generalizing C with
  | nil => simpa [runGo] using hC
  | cons p τ ih =>
      rw [runGo]
      exact ih (A.step C p) (A.step_size C p hC)

If a run has no misses, every requested page was already resident: the requested pages are a subset of the initial cache.


lemma missesGo_eq_zero_subset (A : Algorithm Page k) (C : Finset Page) (σ : List Page)
    (h : missesGo A C σ = 0) : σ.toFinset ⊆ C := by
  induction σ generalizing C with
  | nil => simp
  | cons p τ ih =>
      rw [missesGo] at h
      have hp : p ∈ C := by
        by_cases hp : p ∈ C
        · exact hp
        · simp [hp] at h
      have hτ : missesGo A (A.step C p) τ = 0 := by
        by_cases hp' : p ∈ C
        · simpa [hp'] using h
        · simp [hp'] at h
      rw [List.toFinset_cons]
      intro x hx
      rw [Finset.mem_insert] at hx
      rcases hx with rfl | hx
      · exact hp
      · have hx' := ih (A.step C p) hτ hx
        have hx'' := A.step_subset C p hx'
        rw [Finset.mem_insert] at hx''
        rcases hx'' with rfl | hxC
        · exact hp
        · exact hxC

A segment that requests k + 1 distinct pages forces a miss for any size-k algorithm.


lemma distinct_fault (A : Algorithm Page k) (C : Finset Page) (ρ : List Page)
    (hC : C.card ≤ k) (hk : k < ρ.toFinset.card) : 1 ≤ missesGo A C ρ := by
  by_contra hzero
  have h0 : missesGo A C ρ = 0 := by omega
  have hsub := missesGo_eq_zero_subset A C ρ h0
  have hcard : ρ.toFinset.card ≤ C.card := Finset.card_le_card hsub
  omega

A page resident at the start of a segment that then requests k other distinct pages forces a miss for any size-k algorithm.


lemma resident_fault (A : Algorithm Page k) (C : Finset Page) (p : Page) (ρ : List Page)
    (hC : C.card ≤ k) (hp : p ∈ C) (hk : k ≤ (ρ.toFinset.erase p).card) :
    1 ≤ missesGo A C ρ := by
  by_contra hzero
  have h0 : missesGo A C ρ = 0 := by omega
  have hsub := missesGo_eq_zero_subset A C ρ h0
  -- Every distinct page of ρ lies in C; since ρ also requests k pages other than
  -- p, those k pages live in C.erase p, but C has at most k pages and p already
  -- occupies one of them -- a contradiction.
  have hle : (ρ.toFinset.erase p).card ≤ (C.erase p).card := by
    apply Finset.card_le_card
    intro x hx
    rw [Finset.mem_erase] at hx ⊢
    exact ⟨hx.1, hsub hx.2⟩
  have hCardErase : (C.erase p).card = C.card - 1 := Finset.card_erase_of_mem hp
  have hCp : 0 < C.card := Finset.card_pos.mpr ⟨p, hp⟩
  omega

The pages strictly more recent than p in a most-recent-first cache L (the takeWhile prefix of L up to p), as a Finset.

-- ---------------------------------------------------------------------------
-- Structural facts about the LRU list cache.

def front (p : Page) (L : List Page) : Finset Page :=
  (L.takeWhile (fun x => x ≠ p)).toFinset

The Finset of a no-duplicate list has its length as cardinality.


lemma toFinset_card_of_nodup {L : List Page} (h : L.Nodup) : L.toFinset.card = L.length := by
  rw [List.toFinset, Multiset.card_toFinset, Multiset.coe_dedup, List.dedup_eq_self.mpr h]
  rfl

lruStep preserves the no-duplicate invariant of the cache list.

lemma lruStep_nodup (k : ℕ) (L : List Page) (p : Page) (h : L.Nodup) :
    (lruStep k L p).Nodup := by
  unfold lruStep
  split_ifs with hp hl
  · exact (List.perm_cons_erase hp).nodup_iff.mp h
  · exact List.nodup_cons.mpr ⟨hp, h⟩
  · refine List.nodup_cons.mpr ⟨?_, (List.dropLast_sublist L).nodup h⟩
    intro hpd
    exact hp (List.mem_of_mem_dropLast hpd)

lruRun preserves the no-duplicate invariant of the cache list.

lemma lruRun_nodup (k : ℕ) (L : List Page) (ρ : List Page) (h : L.Nodup) :
    (lruRun k L ρ).Nodup := by
  induction ρ generalizing L with
  | nil => simpa [lruRun] using h
  | cons p ρ' ih => simp [lruRun]; exact ih (lruStep k L p) (lruStep_nodup k L p h)

The cache after a concatenation of request lists is the sequential run.

lemma lruRun_append (k : ℕ) (L : List Page) (σ τ : List Page) :
    lruRun k L (σ ++ τ) = lruRun k (lruRun k L σ) τ := by
  induction σ generalizing L with
  | nil => rfl
  | cons p σ' ih => simp [lruRun, ih]

The miss count over a concatenation splits additively.


lemma lruMissesGo_append (k : ℕ) (L : List Page) (σ τ : List Page) :
    lruMissesGo k L (σ ++ τ) = lruMissesGo k L σ + lruMissesGo k (lruRun k L σ) τ := by
  induction σ generalizing L with
  | nil => simp [lruMissesGo, lruRun]
  | cons p σ' ih =>
      simp [lruMissesGo, lruRun]
      rw [ih (lruStep k L p)]
      omega

Membership after a single lruStep, unfolded into the hit / not-full miss / full miss cases.


lemma mem_lruStep (k : ℕ) (L : List Page) (p q : Page) :
    q ∈ lruStep k L p ↔
      (if p ∈ L then q ∈ L
       else if L.length < k then q = p ∨ q ∈ L
       else q = p ∨ q ∈ L.dropLast) := by
  unfold lruStep
  split_ifs with hp hl
  · -- hit: q ∈ p :: L.erase p ↔ q ∈ L
    rw [List.mem_cons]
    constructor
    · intro h
      rcases h with h | h
      · exact h ▸ hp
      · exact List.mem_of_mem_erase h
    · intro h
      by_cases hqp : q = p
      · exact Or.inl hqp
      · exact Or.inr ((List.mem_erase_of_ne hqp).mpr h)
  · -- miss, not full: q ∈ p :: L ↔ q = p ∨ q ∈ L
    rw [List.mem_cons]
  · -- miss, full: q ∈ p :: L.dropLast ↔ q = p ∨ q ∈ L.dropLast
    rw [List.mem_cons]

Erasing an element that satisfies f cannot enlarge the takeWhile f prefix.

lemma takeWhile_erase_subset {f : Page → Bool} {q : Page} {L : List Page} (hfq : f q = true) :
    (L.erase q).takeWhile f ⊆ L.takeWhile f := by
  induction L with
  | nil => simp
  | cons x rest ih =>
      by_cases hxq : x = q
      · subst x; simp [hfq]
      · by_cases hx : f x = true
        · simp [hxq, hx]
          intro a ha
          exact List.Mem.tail x (ih ha)
        · simp [hxq, hx]

Dropping the last element cannot enlarge the takeWhile f prefix.

automatically included section variable(s) unused in theorem `CLRS.OnlineCaching.takeWhile_dropLast_subset`:
  [DecidableEq Page]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq Page] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.OnlineCaching.takeWhile_dropLast_subset`:
  [DecidableEq Page]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq Page] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.OnlineCaching.takeWhile_dropLast_subset`:
  [DecidableEq Page]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq Page] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.OnlineCaching.takeWhile_dropLast_subset`:
  [DecidableEq Page]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq Page] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.OnlineCaching.takeWhile_dropLast_subset`:
  [DecidableEq Page]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq Page] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.OnlineCaching.takeWhile_dropLast_subset`:
  [DecidableEq Page]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq Page] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.OnlineCaching.takeWhile_dropLast_subset`:
  [DecidableEq Page]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq Page] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.OnlineCaching.takeWhile_dropLast_subset`:
  [DecidableEq Page]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq Page] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.OnlineCaching.takeWhile_dropLast_subset`:
  [DecidableEq Page]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq Page] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.OnlineCaching.takeWhile_dropLast_subset`:
  [DecidableEq Page]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq Page] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.OnlineCaching.takeWhile_dropLast_subset`:
  [DecidableEq Page]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq Page] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.OnlineCaching.takeWhile_dropLast_subset`:
  [DecidableEq Page]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq Page] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.OnlineCaching.takeWhile_dropLast_subset`:
  [DecidableEq Page]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq Page] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.OnlineCaching.takeWhile_dropLast_subset`:
  [DecidableEq Page]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq Page] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.OnlineCaching.takeWhile_dropLast_subset`:
  [DecidableEq Page]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq Page] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.OnlineCaching.takeWhile_dropLast_subset`:
  [DecidableEq Page]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq Page] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.OnlineCaching.takeWhile_dropLast_subset`:
  [DecidableEq Page]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq Page] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
automatically included section variable(s) unused in theorem `CLRS.OnlineCaching.takeWhile_dropLast_subset`:
  [DecidableEq Page]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq Page] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`lemma takeWhile_dropLast_subset {f : Page → Bool} {L : List Page} :
    L.dropLast.takeWhile f ⊆ L.takeWhile f := by
  induction L with
  | nil => simp
  | cons x rest ih =>
      cases rest with
      | nil => simp
      | cons y ys =>
          rw [List.dropLast_cons_of_ne_nil (show y :: ys ≠ [] by simp)]
          by_cases hx : f x = true
          · simp [hx]
            intro a ha
            exact List.Mem.tail x (ih ha)
          · simp [hx]

One step grows the front of a page by at most the requested page.


lemma lruStep_front_subset (k : ℕ) (L : List Page) (p q : Page) :
    front p (lruStep k L q) ⊆ {q} ∪ front p L := by
  by_cases hqp : q = p
  · subst q
    unfold front lruStep
    split_ifs <;> simp [This simp argument is unused:
  front

Hint: Omit it from the simp argument list.
  simp ̵[̵f̵r̵o̵n̵t̵]̵

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`front]
  · unfold front lruStep
    by_cases hq : q ∈ L
    · simp [hq, hqp]
      intro x hx
      rw [Finset.mem_insert] at hx
      rw [Finset.mem_insert]
      rcases hx with hxq | hx
      · exact Or.inl hxq
      · exact Or.inr (List.mem_toFinset.mpr
          (takeWhile_erase_subset (f := fun y => !decide (y = p)) (q := q) (by simp [hqp])
            (List.mem_toFinset.mp hx)))
    · by_cases hl : L.length < k
      · simp [hq, hl, hqp]
      · simp [hq, hl, hqp]
        intro x hx
        rw [Finset.mem_insert] at hx
        rw [Finset.mem_insert]
        rcases hx with hxq | hx
        · exact Or.inl hxq
        · exact Or.inr (List.mem_toFinset.mpr
            (takeWhile_dropLast_subset (f := fun y => !decide (y = p))
              (List.mem_toFinset.mp hx)))

The front of p after a run is a subset of the requested pages together with the pages that were already in front of p initially.


lemma lru_front_bound (k : ℕ) (L : List Page) (p : Page) (ρ : List Page) :
    front p (lruRun k L ρ) ⊆ ρ.toFinset ∪ front p L := by
  induction ρ generalizing L with
  | nil => simp [lruRun]
  | cons q ρ' ih =>
      have hstep := lruStep_front_subset k L p q
      have hih := ih (L := lruStep k L q)
      intro x hx
      have hx' := hih hx
      rw [Finset.mem_union] at hx' ⊢
      rcases hx' with hxρ | hxf
      · left
        rw [List.toFinset_cons, Finset.mem_insert]
        exact Or.inr hxρ
      · have hxf' := hstep hxf
        rw [Finset.mem_union, Finset.mem_singleton] at hxf'
        rcases hxf' with hxq | hxfL
        · left
          rw [List.toFinset_cons, Finset.mem_insert]
          exact Or.inl hxq
        · right; exact hxfL

When h is the last element of a list, the takeWhile (· ≠ h) prefix is exactly the drop-last tail.


lemma takeWhile_ne_dropLast {h : Page} {L : List Page} (hL : h ∈ L)
    (hlast : h ∉ L.dropLast) :
    L.takeWhile (fun x => x ≠ h) = L.dropLast := by
  have hnil : L ≠ [] := by intro h0; subst h0; simp at hL
  have hget : h = L.getLast hnil := by
    have hmem : h ∈ L.dropLast ++ [L.getLast hnil] := by
      rw [List.dropLast_append_getLast hnil]
      exact hL
    rw [List.mem_append] at hmem
    rcases hmem with hmem | hmem
    · exact False.elim (hlast hmem)
    · simpa using hmem
  rw [← List.dropLast_append_getLast hnil]
  rw [← hget]
  rw [List.takeWhile_append_of_pos (p := fun x => x ≠ h)]
  · simp
  · intro x hx
    apply decide_eq_true
    intro hxeq
    exact hlast (by simpa [hxeq] using hx)

When a page h is evicted in a single step, the front of h (which then has k - 1 distinct pages) together with the evicting request has at least k pages.


lemma lruStep_evict_card (k : ℕ) (L : List Page) (h q : Page)
    (hNodup : L.Nodup) (hL : h ∈ L) (hev : h ∉ lruStep k L q) :
    k ≤ (front h L ∪ {q}).card := by
  have hnot : ¬ (if q ∈ L then h ∈ L
      else if L.length < k then h = q ∨ h ∈ L
      else h = q ∨ h ∈ L.dropLast) := by
    intro h'
    exact hev ((mem_lruStep k L q h).mpr h')
  have hqL : q ∉ L := by intro hq; apply hnot; simp [hq, hL]
  have hfull : k ≤ L.length := by
    by_contra hn
    have hl : L.length < k := by omega
    apply hnot; simp [hqL, hl, hL]
  have hlast : h ∉ L.dropLast := by intro hd; apply hnot; simp [hqL, hfull, hd]
  have hfront : front h L = L.dropLast.toFinset := by
    unfold front
    congr 1
    exact takeWhile_ne_dropLast hL hlast
  have hfront_card : k - 1 ≤ (front h L).card := by
    rw [hfront]
    rw [toFinset_card_of_nodup ((List.dropLast_sublist L).nodup hNodup)]
    rw [List.dropLast_eq_take, List.length_take]
    omega
  have hq_front : q ∉ front h L := by
    intro hq'
    rw [hfront] at hq'
    exact hqL (List.mem_of_mem_dropLast (by simpa using hq'))
  have hcard : (front h L ∪ {q}).card = (front h L).card + 1 := by
    rw [Finset.card_union_of_disjoint]
    · simp
    · exact Finset.disjoint_singleton_right.mpr hq_front
  omega

If a page h ∈ L is not in the cache after a run, then the distinct pages of ρ other than h, together with the pages initially in front of h, number at least k. For h at the front this is the "head eviction" lemma: evicting the most-recently-used page needs k other distinct requests.


lemma lru_evict_ge (k : ℕ) (L : List Page) (h : Page) (ρ : List Page)
    (hNodup : L.Nodup) (hL : h ∈ L) (hev : h ∉ lruRun k L ρ) :
    k ≤ (front h L ∪ ρ.toFinset.erase h).card := by
  induction ρ generalizing L with
  | nil => simp [lruRun] at hev; exact (hev hL).elim
  | cons q ρ' ih =>
      let L' := lruStep k L q
      by_cases hL' : h ∈ L'
      · have hih := ih (L := L') (lruStep_nodup k L q hNodup) hL' (by simpa [lruRun, L'] using hev)
        have hle : (front h L' ∪ ρ'.toFinset.erase h).card ≤
            (front h L ∪ (q :: ρ').toFinset.erase h).card := by
          apply Finset.card_le_card
          intro x hx
          rw [Finset.mem_union] at hx ⊢
          rcases hx with hx | hx
          · have hx' := lruStep_front_subset k L h q hx
            rw [Finset.mem_union, Finset.mem_singleton] at hx'
            rcases hx' with hxq | hxf
            · right
              rw [List.toFinset_cons, Finset.mem_erase, Finset.mem_insert]
              refine ⟨?_, Or.inl hxq⟩
              intro hqh
              subst q
              subst h
              have : x ∉ front x (lruStep k L x) := by simp [front, lruStep, hL]
              exact this hx
            · left; exact hxf
          · right
            rw [List.toFinset_cons, Finset.mem_erase, Finset.mem_insert]
            exact ⟨(Finset.mem_erase.mp hx).1, Or.inr (Finset.mem_erase.mp hx).2⟩
        omega
      · have hcard := lruStep_evict_card k L h q hNodup hL hL'
        have hqh : q ≠ h := by
          intro hqh
          subst q
          exact hL' (by change h ∈ lruStep k L h; simp [lruStep, hL])
        have hle : (front h L ∪ {q}).card ≤ (front h L ∪ (q :: ρ').toFinset.erase h).card := by
          apply Finset.card_le_card
          intro x hx
          rw [Finset.mem_union] at hx ⊢
          rcases hx with hxf | hxq
          · left; exact hxf
          · right
            rw [Finset.mem_singleton] at hxq
            rw [List.toFinset_cons, Finset.mem_erase, Finset.mem_insert]
            refine ⟨by simpa [hxq] using hqh, Or.inl hxq⟩
        omega

LRU head eviction. If h is the most-recently-used page of a full cache at the start of a segment, and h is evicted during the segment, then the segment requests at least k other distinct pages. This is the key fact that a single page can only be faulted once within any segment of at most k distinct pages.


lemma lru_head_evict (k : ℕ) (h : Page) (rest ρ : List Page) (hNodup : (h :: rest).Nodup) :
    h ∉ lruRun k (h :: rest) ρ → k ≤ (ρ.toFinset.erase h).card := by
  intro hev
  have hge := lru_evict_ge k (h :: rest) h ρ hNodup (by simp) hev
  simpa [front] using hge

Erasing p before or after dropping the last element commutes, when p is not the last element.


lemma erase_dropLast {p : Page} {L : List Page} (hp : p ∈ L.dropLast) :
    (L.dropLast).erase p = (L.erase p).dropLast := by
  have hnil : L ≠ [] := by intro h0; subst h0; simp at hp
  calc
    (L.dropLast).erase p = ((L.dropLast).erase p ++ [L.getLast hnil]).dropLast := by
        rw [List.dropLast_append_of_ne_nil (show [L.getLast hnil] ≠ [] by simp)]
        simp
    _ = ((L.dropLast ++ [L.getLast hnil]).erase p).dropLast := by
        rw [List.erase_append_left [L.getLast hnil] hp]
    _ = (L.erase p).dropLast := by
        rw [List.dropLast_append_getLast hnil]

When p survives a step q ≠ p, erasing p from the resulting cache equals running the step on the size-(k - 1) cache with p already erased.


lemma lruStep_erase (k : ℕ) (L : List Page) (q p : Page)
    (Variable name `hNodup` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`hNodup : L.Nodup) (hp : p ∈ L) (hqp : q ≠ p) (hkeep : p ∈ lruStep k L q) :
    (lruStep k L q).erase p = lruStep (k - 1) (L.erase p) q := by
  unfold lruStep
  by_cases hq : q ∈ L
  · have hq_erase : q ∈ L.erase p := (List.mem_erase_of_ne hqp).mpr hq
    simp [hq, hqp, hq_erase]
    rw [List.erase_comm q p]
  · by_cases hl : L.length < k
    · have hq_erase : q ∉ L.erase p := by
        intro h; exact hq (List.mem_of_mem_erase h)
      have hlen : (L.erase p).length < k - 1 := by
        rw [List.length_erase_of_mem hp]
        have hpos : 0 < L.length := List.length_pos_of_mem hp
        omega
      simp [hq, hl, hqp, hq_erase, hlen]
    · have hq_erase : q ∉ L.erase p := by
        intro h; exact hq (List.mem_of_mem_erase h)
      have hlen : ¬ (L.erase p).length < k - 1 := by
        rw [List.length_erase_of_mem hp]
        omega
      have hp_dropLast : p ∈ L.dropLast := by
        have : p ∈ q :: L.dropLast := by simpa [lruStep, hq, hl] using hkeep
        rw [List.mem_cons] at this
        rcases this with this | this
        · exact (hqp this.symm).elim
        · exact this
      simp [hq, hl, hqp, hq_erase, hlen]
      exact erase_dropLast hp_dropLast

The miss count commutes with erasing a page that is never evicted: with the page p pinned in the cache, LRU over a size-k cache from L has the same misses as a size-(k - 1) cache from L.erase p over ρ.filter (· ≠ p).


lemma lru_miss_shrink (k : ℕ) (L : List Page) (ρ : List Page) (p : Page)
    (hNodup : L.Nodup) (hp : p ∈ L) (hkeep : ∀ τ, List.IsPrefix τ ρ → p ∈ lruRun k L τ) :
    lruMissesGo k L ρ = lruMissesGo (k - 1) (L.erase p) (ρ.filter (fun x => x ≠ p)) := by
  induction ρ generalizing L with
  | nil => simp [lruMissesGo]
  | cons q rest ih =>
      have hq : p ∈ lruStep k L q := by
        have h := hkeep [q] (⟨rest, by simp⟩ : List.IsPrefix [q] (q :: rest))
        simpa [lruRun] using h
      have hkeep' : ∀ τ, List.IsPrefix τ rest → p ∈ lruRun k (lruStep k L q) τ := by
        intro τ hτ
        rcases hτ with ⟨t, ht⟩
        have hprefix : List.IsPrefix ([q] ++ τ) (q :: rest) := ⟨t, by simp [ht]⟩
        have h := hkeep ([q] ++ τ) hprefix
        rwa [lruRun_append] at h
      have hih := ih (L := lruStep k L q) (lruStep_nodup k L q hNodup) hq hkeep'
      by_cases hqp : q = p
      · subst q
        rw [lruMissesGo]
        simp [hp]
        have hstep : (lruStep k L p).erase p = L.erase p := by
          unfold lruStep
          simp [hp]
        rw [hih, hstep]
        simp
      · have hq_in : q ∈ L ↔ q ∈ L.erase p := (List.mem_erase_of_ne hqp).symm
        have hstep_erase := lruStep_erase k L q p hNodup hp hqp hq
        rw [lruMissesGo]
        rw [hih]
        rw [hstep_erase]
        have hfilter : (q :: rest).filter (fun x => x ≠ p) = q :: rest.filter (fun x => x ≠ p) := by
          simp [hqp]
        rw [hfilter]
        rw [lruMissesGo]
        simp [hq_in]

LRU makes at most one fault per distinct requested page, whenever at most k distinct pages are requested.

try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
lemma lru_miss_le_distinct (k : ℕ) (L : List Page) (ρ : List Page)
    (hNodup : L.Nodup) (hcard : ρ.toFinset.card ≤ k) :
    lruMissesGo k L ρ ≤ ρ.toFinset.card := by
  classical
  have go : ∀ (n : ℕ) (k : ℕ) (L : List Page) (ρ : List Page), ρ.length = n → L.Nodup →
      ρ.toFinset.card ≤ k → lruMissesGo k L ρ ≤ ρ.toFinset.card := by
    intro n
    induction n using Nat.strong_induction_on with
    | h n ih =>
      intro k L ρ hlen hNodup hcard
      cases ρ with
      | nil => simp [lruMissesGo]
      | cons p ρ' =>
          let L' : List Page := lruStep k L p
          have hNodup' : L'.Nodup := lruStep_nodup k L p hNodup
          have hlt : ρ'.length < n := by
            rw [← hlen]
            exact Nat.lt_succ_self ρ'.length
          rw [lruMissesGo, List.toFinset_cons]
          by_cases hpL : p ∈ L
          · have hrec : lruMissesGo k L' ρ' ≤ ρ'.toFinset.card := by
              apply ih ρ'.length hlt k L' ρ' rfl hNodup'
              have : ρ'.toFinset.card ≤ k := by
                have hins : (insert p ρ'.toFinset).card ≤ k := by
                  simpa [List.toFinset_cons] using hcard
                have hle : ρ'.toFinset.card ≤ (insert p ρ'.toFinset).card :=
                  Finset.card_le_card (Finset.subset_insert _ _)
                omega
              exact this
            simp [hpL]
            exact le_trans hrec (Finset.card_le_card (Finset.subset_insert _ _))
          · by_cases hpρ : p ∈ ρ'.toFinset
            · -- p is re-requested: it is pinned, so shrink to a size-(k-1) cache
              have hk : 0 < k := by
                have hpos : 0 < ρ'.toFinset.card := Finset.card_pos.mpr ⟨p, hpρ⟩
                have hle : ρ'.toFinset.card ≤ k := by
                  have hins : (insert p ρ'.toFinset).card ≤ k := by
                    simpa [List.toFinset_cons] using hcard
                  have hle2 : ρ'.toFinset.card ≤ (insert p ρ'.toFinset).card :=
                    Finset.card_le_card (Finset.subset_insert _ _)
                  omega
                omega
              have hcard' : (ρ'.toFinset.erase p).card ≤ k - 1 := by
                have hρ : ρ'.toFinset.card ≤ k := by
                  have hins : (insert p ρ'.toFinset).card ≤ k := by
                    simpa [List.toFinset_cons] using hcard
                  have : (insert p ρ'.toFinset).card = ρ'.toFinset.card :=
                    Finset.card_insert_of_mem hpρ
                  omega
                rw [Finset.card_erase_of_mem hpρ]
                have hpos : 0 < ρ'.toFinset.card := Finset.card_pos.mpr ⟨p, hpρ⟩
                omega
              have hL'head : ∃ t, L' = p :: t := by
                change ∃ t, lruStep k L p = p :: t
                unfold lruStep
                by_cases hl : L.length < k
                · exact ⟨L, by simp [hpL, hl]⟩
                · exact ⟨L.dropLast, by simp [hpL, hl]⟩
              rcases hL'head with ⟨t, hEq⟩
              have hNodup_t : (p :: t).Nodup := by simpa [hEq] using hNodup'
              have hkeep : ∀ τ, List.IsPrefix τ ρ' → p ∈ lruRun k (p :: t) τ := by
                intro τ hτ
                have hcardτ : (τ.toFinset.erase p).card ≤ k - 1 := by
                  have hsub : τ.toFinset.erase p ⊆ ρ'.toFinset.erase p := by
                    intro x hx
                    rw [Finset.mem_erase] at hx ⊢
                    refine ⟨hx.1, ?_⟩
                    rcases hτ with ⟨t', ht'⟩
                    have hsub' : τ.toFinset ⊆ ρ'.toFinset := by
                      rw [← ht', List.toFinset_append]
                      exact Finset.subset_union_left
                    exact hsub' hx.2
                  exact le_trans (Finset.card_le_card hsub) hcard'
                by_contra hnot
                have hge := lru_head_evict k p t τ hNodup_t hnot
                omega
              have hshrink := lru_miss_shrink k (p :: t) ρ' p hNodup_t (by simp) hkeep
              have hrec : lruMissesGo (k - 1) t (ρ'.filter (fun x => x ≠ p)) ≤
                  (ρ'.filter (fun x => x ≠ p)).toFinset.card := by
                have hlenF : (ρ'.filter (fun x => x ≠ p)).length < n := by
                  have hle : (ρ'.filter (fun x => x ≠ p)).length ≤ ρ'.length :=
                    List.length_filter_le _ _
                  omega
                apply ih (ρ'.filter (fun x => x ≠ p)).length hlenF (k - 1) t
                  (ρ'.filter (fun x => x ≠ p)) rfl
                · exact (List.sublist_cons_self p t).nodup hNodup_t
                · have hto : (ρ'.filter (fun x => x ≠ p)).toFinset = ρ'.toFinset.erase p := by
                    ext x
                    by_cases hxp : x = p <;> simp [This simp argument is unused:
  List.mem_filter

Hint: Omit it from the simp argument list.
  simp [̵L̵i̵s̵t̵.̵m̵e̵m̵_̵f̵i̵l̵t̵e̵r̵,̵ ̵L̵i̵s̵t̵.̵m̵e̵m̵_̵t̵o̵F̵i̵n̵s̵e̵t̵,̵[̲L̲i̲s̲t̲.̲m̲e̲m̲_̲t̲o̲F̲i̲n̲s̲e̲t̲,̲ hxp]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`List.mem_filter, List.mem_toFinset, hxp]
                  rw [hto]
                  exact hcard'
              have hpos : 0 < ρ'.toFinset.card := Finset.card_pos.mpr ⟨p, hpρ⟩
              simp [hpL]
              calc
                1 + lruMissesGo k L' ρ' =
                    1 + lruMissesGo (k - 1) t (ρ'.filter (fun x => x ≠ p)) := by
                  try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hEq, hshrink]
                _ ≤ 1 + (ρ'.toFinset.erase p).card := by
                  have hto : (ρ'.filter (fun x => x ≠ p)).toFinset = ρ'.toFinset.erase p := by
                    ext x
                    by_cases hxp : x = p <;> simp [This simp argument is unused:
  List.mem_filter

Hint: Omit it from the simp argument list.
  simp [̵L̵i̵s̵t̵.̵m̵e̵m̵_̵f̵i̵l̵t̵e̵r̵,̵ ̵L̵i̵s̵t̵.̵m̵e̵m̵_̵t̵o̵F̵i̵n̵s̵e̵t̵,̵[̲L̲i̲s̲t̲.̲m̲e̲m̲_̲t̲o̲F̲i̲n̲s̲e̲t̲,̲ hxp]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`List.mem_filter, List.mem_toFinset, hxp]
                  rw [hto] at hrec
                  exact Nat.add_le_add_left hrec 1
                _ = ρ'.toFinset.card := by
                  rw [Finset.card_erase_of_mem hpρ]
                  omega
                _ ≤ (insert p ρ'.toFinset).card := by
                  rw [Finset.card_insert_of_mem hpρ]
            · have hrec : lruMissesGo k L' ρ' ≤ ρ'.toFinset.card := by
                apply ih ρ'.length hlt k L' ρ' rfl hNodup'
                have : ρ'.toFinset.card ≤ k := by
                  have hins : (insert p ρ'.toFinset).card ≤ k := by
                    simpa [List.toFinset_cons] using hcard
                  have hle : ρ'.toFinset.card ≤ (insert p ρ'.toFinset).card :=
                    Finset.card_le_card (Finset.subset_insert _ _)
                  omega
                exact this
              simp [hpL]
              have hins : (insert p ρ'.toFinset).card = ρ'.toFinset.card + 1 := by
                rw [Finset.card_insert_of_notMem hpρ]
              rw [hins]
              rw [Nat.add_comm]
              exact Nat.add_le_add_right hrec 1
  exact go ρ.length k L ρ rfl hNodup hcard

Auxiliary: with seen the pages already accumulated in the current phase, extend it by the longest prefix of σ whose distinct pages (together with seen) stay within k. Returns the extension (forward order) and the leftover suffix.

-- ---------------------------------------------------------------------------
-- The phase partition.

def phaseGo (k : ℕ) (seen : Finset Page) : List Page → List Page × List Page
  | [] => ([], [])
  | q :: τ =>
      let seen' := insert q seen
      if seen'.card ≤ k then
        let (pre, rem) := phaseGo k seen' τ
        (q :: pre, rem)
      else
        ([], q :: τ)
termination_by σ => σ.length

phaseGo splits its input: the phase prefix and the suffix concatenate back to the original list.

lemma phaseGo_split (k : ℕ) (seen : Finset Page) (σ : List Page) :
    (phaseGo k seen σ).1 ++ (phaseGo k seen σ).2 = σ := by
  induction σ generalizing seen with
  | nil => simp [phaseGo]
  | cons q τ ih =>
      by_cases h : (insert q seen).card ≤ k
      · have hi := ih (insert q seen)
        simp [phaseGo, h, hi]
      · simp [phaseGo, h]

The first phase of a nonempty request list: the longest prefix with at most k distinct pages, paired with the remaining suffix.

def firstPhase (k : ℕ) : List Page → List Page × List Page
  | [] => ([], [])
  | p :: rest =>
      let (pre, rem) := phaseGo k {p} rest
      (p :: pre, rem)

The first phase of a nonempty list is nonempty.

lemma firstPhase_nonempty (k : ℕ) (σ : List Page) (h : σ ≠ []) :
    (firstPhase k σ).1 ≠ [] := by
  cases σ with
  | nil => contradiction
  | cons p rest => simp [firstPhase]

The first phase and its suffix split the list.

lemma firstPhase_split (k : ℕ) (σ : List Page) :
    (firstPhase k σ).1 ++ (firstPhase k σ).2 = σ := by
  cases σ with
  | nil => simp [firstPhase]
  | cons p rest =>
      have hs := phaseGo_split k {p} rest
      simp [firstPhase, hs]

The phase partition of σ: maximal segments, each (except possibly the last) containing exactly k distinct pages.


def phases (k : ℕ) (σ : List Page) : List (List Page) :=
  WellFounded.fix (hwf := (measure (fun σ : List Page => σ.length)).wf) (fun σ rec =>
    match σ with
    | [] => []
    | p :: rest =>
        let fp := firstPhase k (p :: rest)
        let pre := fp.1
        let rem := fp.2
        pre :: rec rem (by
          have hsplit := firstPhase_split k (p :: rest)
          have hnonempty := firstPhase_nonempty k (p :: rest) (by simp)
          have hlen : pre.length + rem.length = (p :: rest).length := by
            rw [← hsplit, List.length_append]
          have hpos : 0 < pre.length := List.length_pos_of_ne_nil hnonempty
          change rem.length < (p :: rest).length
          rw [← hlen]
          exact Nat.lt_add_of_pos_left hpos)
  ) σ

The pages of a phaseGo prefix, together with the already-seen pages, stay within the cache size k.


lemma phaseGo_distinct_le (k : ℕ) (seen : Finset Page) (σ : List Page) (hseen : seen.card ≤ k) :
    ((phaseGo k seen σ).1.toFinset ∪ seen).card ≤ k := by
  induction σ generalizing seen with
  | nil => simpa [phaseGo] using hseen
  | cons q τ ih =>
      by_cases h : (insert q seen).card ≤ k
      · have hi := ih (insert q seen) (by simpa using h)
        simp [phaseGo, h]
        rw [← Finset.union_insert]
        exact hi
      · simp [phaseGo, h, hseen]

A phase has at most k distinct pages (requires 0 < k).


lemma firstPhase_distinct_le (k : ℕ) (σ : List Page) (hk : 0 < k) :
    (firstPhase k σ).1.toFinset.card ≤ k := by
  cases σ with
  | nil => simp [firstPhase]
  | cons p rest =>
      have hd := phaseGo_distinct_le k {p} rest (by simpa using (Nat.succ_le_of_lt hk))
      simp [firstPhase]
      rw [Finset.insert_eq, Finset.union_comm]
      exact hd

The phase partition recurses: for a nonempty list, the phases are the first phase followed by the phases of the suffix.


lemma phases_cons_eq (k : ℕ) (σ : List Page) (h : σ ≠ []) :
    phases k σ = (firstPhase k σ).1 :: phases k (firstPhase k σ).2 := by
  cases σ with
  | nil => contradiction
  | cons p rest => simp [phases]; rw [WellFounded.fix_eq]

The phase partition concatenates back to the original list.


lemma phases_join (k : ℕ) (σ : List Page) : (phases k σ).flatten = σ := by
  classical
  have hmain : ∀ (n : ℕ) (σ : List Page), σ.length = n → (phases k σ).flatten = σ := by
    intro n
    induction n using Nat.strong_induction_on with
    | h n ih =>
      intro σ hn
      cases σ with
      | nil => simp [phases, WellFounded.fix_eq]
      | cons p rest =>
          let fp := firstPhase k (p :: rest)
          have hsplit := firstPhase_split k (p :: rest)
          have hnonempty : fp.1 ≠ [] := by
            dsimp [fp]
            exact firstPhase_nonempty k (p :: rest) (by simp)
          have hremlen : fp.2.length < (p :: rest).length := by
            have hlen : fp.1.length + fp.2.length = (p :: rest).length := by
              rw [← hsplit, List.length_append]
            have hpos : 0 < fp.1.length := List.length_pos_of_ne_nil hnonempty
            omega
          have hremlen' : fp.2.length < n := by omega
          have hi := ih fp.2.length hremlen' fp.2 rfl
          rw [phases_cons_eq k (p :: rest) (by simp)]
          simp [fp, List.flatten, hi, hsplit]
  exact hmain σ.length σ rfl

LRU makes at most k misses per phase: its total misses are bounded by k times the number of phases.


lemma lru_miss_le_phases (k : ℕ) (L : List Page) (σ : List Page) (hk : 0 < k) (hNodup : L.Nodup) :
    lruMissesGo k L σ ≤ k * (phases k σ).length := by
  classical
  have go : ∀ (n : ℕ) (L : List Page) (σ : List Page), σ.length = n → L.Nodup →
      lruMissesGo k L σ ≤ k * (phases k σ).length := by
    intro n
    induction n using Nat.strong_induction_on with
    | h n ih =>
      intro L σ hlen hNodup
      cases σ with
      | nil => simp [lruMissesGo, phases]
      | cons p rest =>
          let fp := firstPhase k (p :: rest)
          have hsplit := firstPhase_split k (p :: rest)
          have hcard : (firstPhase k (p :: rest)).1.toFinset.card ≤ k :=
            firstPhase_distinct_le k (p :: rest) hk
          have hnonempty : fp.1 ≠ [] := by
            dsimp [fp]
            exact firstPhase_nonempty k (p :: rest) (by simp)
          have hremlen : fp.2.length < (p :: rest).length := by
            have hlen : fp.1.length + fp.2.length = (p :: rest).length := by
              rw [← hsplit, List.length_append]
            have hpos : 0 < fp.1.length := List.length_pos_of_ne_nil hnonempty
            omega
          have hremlen' : fp.2.length < n := by omega
          have hphase : lruMissesGo k L fp.1 ≤ fp.1.toFinset.card :=
            lru_miss_le_distinct k L fp.1 hNodup (by simpa [fp] using hcard)
          have hrec : lruMissesGo k (lruRun k L fp.1) fp.2 ≤ k * (phases k fp.2).length :=
            ih fp.2.length hremlen' (lruRun k L fp.1) fp.2 rfl (lruRun_nodup k L fp.1 hNodup)
          rw [phases_cons_eq k (p :: rest) (by simp)]
          conv_lhs => rw [← hsplit, lruMissesGo_append]
          calc
            lruMissesGo k L fp.1 + lruMissesGo k (lruRun k L fp.1) fp.2
                ≤ fp.1.toFinset.card + k * (phases k fp.2).length := Nat.add_le_add hphase hrec
            _ ≤ k + k * (phases k fp.2).length := by
              exact Nat.add_le_add_right (by simpa [fp] using hcard) _
            _ = k * (fp.1 :: phases k fp.2).length := by
              simp [List.length_cons, Nat.mul_add, Nat.add_comm]
  exact go σ.length L σ rfl hNodup

The miss count over a concatenation splits additively for an algorithm.

lemma missesGo_append (A : Algorithm Page k) (C : Finset Page) (σ τ : List Page) :
    missesGo A C (σ ++ τ) = missesGo A C σ + missesGo A (runGo A C σ) τ := by
  induction σ generalizing C with
  | nil => simp [missesGo, runGo]
  | cons p σ' ih =>
      simp [missesGo, runGo, ih]
      omega

A run with no misses leaves the cache unchanged.


lemma runGo_eq_self_of_misses_eq_zero (A : Algorithm Page k) (C : Finset Page) (ρ : List Page)
    (h : missesGo A C ρ = 0) (hC : C.card ≤ k) : runGo A C ρ = C := by
  induction ρ generalizing C with
  | nil => simp [runGo]
  | cons p τ ih =>
      have hp : p ∈ C := by
        have h' : (if p ∈ C then 0 else 1) + missesGo A (A.step C p) τ = 0 := by
          simpa [missesGo] using h
        by_contra hnot
        simp [hnot] at h'
      have hτ : missesGo A (A.step C p) τ = 0 := by
        have h' : (if p ∈ C then 0 else 1) + missesGo A (A.step C p) τ = 0 := by
          simpa [missesGo] using h
        simpa [hp] using h'
      rw [runGo]
      simpa [A.step_hit C p hC hp] using ih (A.step C p) hτ (A.step_size C p hC)

When a phaseGo prefix ends because the next request would exceed k, the accumulated pages have cardinality exactly k and the next request is fresh.


lemma phaseGo_maximal (k : ℕ) (seen : Finset Page) (σ : List Page) (hseen : seen.card ≤ k)
    (h : (phaseGo k seen σ).2 ≠ []) :
    ((phaseGo k seen σ).1.toFinset ∪ seen).card = k ∧
    List.head (phaseGo k seen σ).2 h ∉ (phaseGo k seen σ).1.toFinset ∪ seen := by
  induction σ generalizing seen with
  | nil => simp [phaseGo] at h
  | cons q τ ih =>
      by_cases hq : (insert q seen).card ≤ k
      · have hrem : (phaseGo k (insert q seen) τ).2 ≠ [] := by
          simpa [phaseGo, hq] using h
        have hi := ih (insert q seen) (by simpa using hq) hrem
        simpa [phaseGo, hq, Finset.insert_union, Finset.union_insert, Finset.union_assoc,
          Finset.union_comm, Finset.union_left_comm] using hi
      · have hcard : seen.card = k := by
          have hqnotin : q ∉ seen := by
            intro hqin
            have : (insert q seen).card ≤ k := by simpa [hqin] using hseen
            exact hq this
          have hinsert : (insert q seen).card = seen.card + 1 :=
            Finset.card_insert_of_notMem hqnotin
          have hgt : k < (insert q seen).card := by omega
          rw [hinsert] at hgt
          omega
        constructor
        · simp [phaseGo, hq, hcard]
        · simp [phaseGo, hq]
          intro hqin
          have : (insert q seen).card ≤ k := by simpa [hqin] using hseen
          exact hq this

A nonempty first phase is maximal: if its suffix is nonempty, the phase has exactly k distinct pages and the first page of the suffix is fresh.


lemma firstPhase_maximal (k : ℕ) (σ : List Page) (hk : 0 < k) (h : (firstPhase k σ).2 ≠ []) :
    (firstPhase k σ).1.toFinset.card = k ∧
    List.head (firstPhase k σ).2 h ∉ (firstPhase k σ).1.toFinset := by
  cases σ with
  | nil => simp [firstPhase] at h
  | cons p rest =>
      have hseen : ({p} : Finset Page).card ≤ k := by
        simpa using (Nat.succ_le_of_lt hk)
      have hrem : (phaseGo k {p} rest).2 ≠ [] := by
        simpa [firstPhase] using h
      have hmax := phaseGo_maximal k {p} rest hseen hrem
      constructor
      · simp [firstPhase]
        rw [Finset.insert_eq, Finset.union_comm]
        exact hmax.1
      · simp [firstPhase]
        simpa [Finset.mem_union, Finset.mem_singleton, and_comm] using hmax.2

If phaseGo stops at q (its leftover suffix begins with q), then q is fresh with respect to the accumulated seen and the returned prefix.


lemma phaseGo_fresh (k : ℕ) (seen : Finset Page) (σ : List Page) (hseen : seen.card ≤ k)
    (q : Page) (rest' : List Page) (h : (phaseGo k seen σ).2 = q :: rest') :
    q ∉ (phaseGo k seen σ).1.toFinset ∪ seen := by
  induction σ generalizing seen with
  | nil => simp [phaseGo] at h
  | cons x τ ih =>
      by_cases hx : (insert x seen).card ≤ k
      · have h' : (phaseGo k (insert x seen) τ).2 = q :: rest' := by
          simpa [phaseGo, hx] using h
        have hi := ih (insert x seen) (by simpa using hx) h'
        simpa [phaseGo, hx, Finset.insert_union, Finset.union_insert, Finset.union_assoc,
          Finset.union_comm, Finset.union_left_comm] using hi
      · have hxτ : x :: τ = q :: rest' := by simpa [phaseGo, hx] using h
        have hxq : x = q := (List.cons.inj hxτ).1
        subst x
        simp [phaseGo, hx]
        intro hqin
        have hcard : (insert q seen).card ≤ k := by simpa [hqin] using hseen
        exact hx hcard

The first page of the suffix after a maximal first phase is fresh with respect to the pages of the phase.


lemma firstPhase_fresh (k : ℕ) (σ : List Page) (hk : 0 < k) (q : Page) (rest' : List Page)
    (h : (firstPhase k σ).2 = q :: rest') :
    q ∉ (firstPhase k σ).1.toFinset := by
  cases σ with
  | nil => simp [firstPhase] at h
  | cons p rest =>
      have h' : (phaseGo k ({p} : Finset Page) rest).2 = q :: rest' := by
        simpa [firstPhase] using h
      have hseen : ({p} : Finset Page).card ≤ k := by
        simpa using (Nat.succ_le_of_lt hk)
      have hfresh := phaseGo_fresh k {p} rest hseen q rest' h'
      simp [firstPhase]
      simpa [Finset.mem_union, Finset.mem_singleton, and_comm] using hfresh

The number of phases is at most one more than the miss count of any size-k algorithm: (phases k σ).length ≤ missesGo A C σ + 1. This is the lower-bound half of the competitive analysis: the transition between consecutive phases requests k + 1 distinct pages (the k pages of one phase plus the first fresh page of the next), forcing at least one miss (CLRS §27.3).


lemma phases_le_misses (k : ℕ) (σ : List Page) (hk : 0 < k)
    (A : Algorithm Page k) (C : Finset Page) (hC : C.card ≤ k) :
    (phases k σ).length ≤ missesGo A C σ + 1 := by
  classical
  have go : ∀ (n : ℕ) (σ : List Page), σ.length = n → ∀ (A : Algorithm Page k)
      (C : Finset Page), C.card ≤ k → (phases k σ).length ≤ missesGo A C σ + 1 := by
    intro n
    induction n using Nat.strong_induction_on with
    | h n ih =>
      intro σ hlen A C hC
      cases σ with
      | nil => simp [phases, missesGo, WellFounded.fix_eq]
      | cons p rest =>
          let fp := firstPhase k (p :: rest)
          have hsplit := firstPhase_split k (p :: rest)
          have hnonempty : fp.1 ≠ [] := by
            dsimp [fp]
            exact firstPhase_nonempty k (p :: rest) (by simp)
          cases hrem : fp.2 with
          | nil =>
              rw [phases_cons_eq k (p :: rest) (by simp)]
              rw [hrem]
              simp [phases, WellFounded.fix_eq]
          | cons q rest' =>
              have hrem_ne : fp.2 ≠ [] := by simp [hrem]
              have hmax := firstPhase_maximal k (p :: rest) hk hrem_ne
              have hcard : fp.1.toFinset.card = k := by simpa [fp] using hmax.1
              have hqfresh : q ∉ fp.1.toFinset := by
                exact firstPhase_fresh k (p :: rest) hk q rest' (by simpa [fp] using hrem)
              have hremlen : fp.2.length < (p :: rest).length := by
                have hlen : fp.1.length + fp.2.length = (p :: rest).length := by
                  rw [← hsplit, List.length_append]
                have hpos : 0 < fp.1.length := List.length_pos_of_ne_nil hnonempty
                omega
              have hremlen' : fp.2.length < n := by omega
              -- The transition segment fp.1 ++ [q] requests k + 1 distinct pages.
              have htrans : k < (fp.1 ++ [q]).toFinset.card := by
                have hto : (fp.1 ++ [q]).toFinset = insert q fp.1.toFinset := by
                  ext x
                  simp [List.toFinset_append]
                rw [hto, Finset.card_insert_of_notMem hqfresh, hcard]
                omega
              have hforce : 1 ≤ missesGo A C (fp.1 ++ [q]) :=
                distinct_fault A C (fp.1 ++ [q]) hC htrans
              have hforce' : 1 ≤ missesGo A C fp.1 + (if q ∈ runGo A C fp.1 then 0 else 1) := by
                have h := missesGo_append A C fp.1 [q]
                rw [h] at hforce
                simp [missesGo] at hforce ⊢
                exact hforce
              have hih := ih fp.2.length hremlen' fp.2 rfl A (A.step (runGo A C fp.1) q)
                (A.step_size (runGo A C fp.1) q (runGo_size A C fp.1 hC))
              have hqstep : q ∈ A.step (runGo A C fp.1) q := A.step_loads (runGo A C fp.1) q
              have hhit : A.step (A.step (runGo A C fp.1) q) q = A.step (runGo A C fp.1) q :=
                A.step_hit (A.step (runGo A C fp.1) q) q
                  (A.step_size (runGo A C fp.1) q (runGo_size A C fp.1 hC)) hqstep
              have hih' : (phases k fp.2).length ≤
                  missesGo A (A.step (runGo A C fp.1) q) rest' + 1 := by
                have hmiss : missesGo A (A.step (runGo A C fp.1) q) fp.2 =
                    missesGo A (A.step (runGo A C fp.1) q) rest' := by
                  rw [hrem]
                  simp [missesGo, hqstep, hhit]
                rw [hmiss] at hih
                exact hih
              have hmisses : missesGo A C (p :: rest) =
                  missesGo A C fp.1 + (if q ∈ runGo A C fp.1 then 0 else 1) +
                    missesGo A (A.step (runGo A C fp.1) q) rest' := by
                rw [← hsplit, missesGo_append A C fp.1 fp.2, hrem]
                simp only [missesGo]
                ac_rfl
              rw [phases_cons_eq k (p :: rest) (by simp)]
              change (phases k fp.2).length + 1 ≤ missesGo A C (p :: rest) + 1
              rw [hmisses]
              omega
  exact go σ.length σ rfl A C hC

Theorem 27.3 (LRU is k-competitive). For any deterministic paging algorithm A with cache size k, LRU's miss count over a request sequence σ is at most k times A's miss count plus k, both starting from an empty cache. This is the classical competitive-analysis bound of CLRS §27.3.


theorem lru_k_competitive (k : ℕ) (σ : List Page) (hk : 0 < k) (A : Algorithm Page k) :
    lruMissesGo k [] σ ≤ k * missesGo A ∅ σ + k := by
  have hub := lru_miss_le_phases k [] σ hk (by simp)
  have hlb := phases_le_misses k σ hk A ∅ (by simp)
  have hmul : k * (phases k σ).length ≤ k * (missesGo A ∅ σ + 1) :=
    Nat.mul_le_mul_left k hlb
  calc
    lruMissesGo k [] σ ≤ k * (phases k σ).length := hub
    _ ≤ k * (missesGo A ∅ σ + 1) := hmul
    _ = k * missesGo A ∅ σ + k := by rw [Nat.mul_add, Nat.mul_one]

Deterministic lower bound

The matching lower bound of CLRS §27.3: no deterministic online paging algorithm is better than k-competitive. The adversary works over the k + 1-page universe Fin (k + 1) and always requests a page absent from the algorithm's cache, so the algorithm faults on every request. An offline schedule that sees the whole sequence serves the same requests with at most N / k + k + 1 faults, which is the comparison cost of the lower bound.

A cache of at most k pages omits some page of the k + 1-page universe.


lemma exists_page_not_mem (C : Finset (Fin (k + 1))) (hC : C.card ≤ k) :
    ∃ p : Fin (k + 1), p ∉ C := by
  classical
  have huniv : (Finset.univ : Finset (Fin (k + 1))).card = k + 1 := by
    rw [Finset.card_univ, Fintype.card_fin]
  have hsub : ¬ (Finset.univ : Finset (Fin (k + 1))) ⊆ C := by
    intro h
    have hle : (Finset.univ : Finset (Fin (k + 1))).card ≤ C.card := Finset.card_le_card h
    omega
  rw [← Finset.sdiff_nonempty] at hsub
  rcases hsub with ⟨p, hp⟩
  exact ⟨p, (Finset.mem_sdiff.mp hp).2⟩

The adversary's fresh page: a page outside the cache C (junk when C is already the whole universe). The lower-bound adversary always requests this absent page, forcing a fault.

noncomputable def freshPage (C : Finset (Fin (k + 1))) : Fin (k + 1) :=
  if h : ∃ p : Fin (k + 1), p ∉ C then Classical.choose h else 0

freshPage C lies outside C whenever some page does.


lemma freshPage_spec (C : Finset (Fin (k + 1))) (h : ∃ p : Fin (k + 1), p ∉ C) :
    freshPage C ∉ C := by
  unfold freshPage
  rw [dif_pos h]
  exact Classical.choose_spec h

The cache of A after n adversarial requests.

noncomputable def advCache (A : Algorithm (Fin (k + 1)) k) : ℕ → Finset (Fin (k + 1))
  | 0 => ∅
  | n + 1 => A.step (advCache A n) (freshPage (advCache A n))

The adversary's cache always respects the size bound.

lemma advCache_card_le (A : Algorithm (Fin (k + 1)) k) (n : ℕ) :
    (advCache A n).card ≤ k := by
  induction n with
  | zero => simp [advCache]
  | succ n ih =>
      simp [advCache]
      exact A.step_size (advCache A n) (freshPage (advCache A n)) ih

The adversarial request sequence of length n: always request the page absent from the algorithm's current cache.

noncomputable def advSeq (A : Algorithm (Fin (k + 1)) k) (n : ℕ) : List (Fin (k + 1)) :=
  (List.range n).map (fun i => freshPage (advCache A i))

The adversarial sequence of length n + 1 extends the length-n one by the next fresh page.


lemma advSeq_snoc (A : Algorithm (Fin (k + 1)) k) (n : ℕ) :
    advSeq A (n + 1) = advSeq A n ++ [freshPage (advCache A n)] := by
  unfold advSeq
  rw [List.range_succ, List.map_append]
  simp

The length of the adversarial sequence is n.

lemma advSeq_length (A : Algorithm (Fin (k + 1)) k) (n : ℕ) :
    (advSeq A n).length = n := by
  unfold advSeq
  simp

runGo distributes over list concatenation.

lemma runGo_append (A : Algorithm Page k) (C : Finset Page) (σ τ : List Page) :
    runGo A C (σ ++ τ) = runGo A (runGo A C σ) τ := by
  induction σ generalizing C with
  | nil => simp [runGo]
  | cons p σ' ih => simp [runGo, ih]

The cache of A after running the adversarial sequence of length n is exactly the adversary's tracked cache.


lemma runGo_advSeq (A : Algorithm (Fin (k + 1)) k) (n : ℕ) :
    runGo A ∅ (advSeq A n) = advCache A n := by
  induction n with
  | zero => simp [advSeq, advCache, runGo]
  | succ n ih =>
      rw [advSeq_snoc, runGo_append]
      simp [runGo, ih, advCache]

The next adversarial request is always absent from the algorithm's cache.

lemma freshPage_not_mem (A : Algorithm (Fin (k + 1)) k) (n : ℕ) :
    freshPage (advCache A n) ∉ advCache A n := by
  exact freshPage_spec (advCache A n) (exists_page_not_mem (advCache A n) (advCache_card_le A n))

The algorithm faults on every adversarial request: over n requests it misses exactly n times.


lemma advSeq_misses (A : Algorithm (Fin (k + 1)) k) (n : ℕ) :
    misses A ∅ (advSeq A n) = n := by
  induction n with
  | zero => simp [advSeq, misses, missesGo]
  | succ n ih =>
      rw [advSeq_snoc]
      change missesGo A ∅ (advSeq A n ++ [freshPage (advCache A n)]) = n + 1
      rw [missesGo_append, runGo_advSeq]
      simp only [missesGo]
      rw [show missesGo A ∅ (advSeq A n) = n from ih]
      simp [freshPage_not_mem A n]

The offline eviction step: on a fault for p from cache C, evict a page not belonging to the current phase phase (a "stale" page) if one exists, and otherwise just load p. The offline schedule knows the whole sequence, so it knows the phase.

-- ---------------------------------------------------------------------------
-- The offline schedule: a phase-aware policy that realizes the comparison cost.

noncomputable def offlineStep (phase : Finset Page) (C : Finset Page) (p : Page) :
    Finset Page :=
  if p ∈ C then C
  else if h : ∃ q ∈ C, q ∉ phase then insert p (C.erase (Classical.choose h))
  else insert p C

The offline step loads the request.

lemma offlineStep_loads (phase C : Finset Page) (p : Page) :
    p ∈ offlineStep phase C p := by
  unfold offlineStep
  split_ifs with hpC hq
  · exact hpC
  · simp
  · simp

The offline step only ever adds the request.


lemma offlineStep_subset (phase C : Finset Page) (p : Page) :
    offlineStep phase C p ⊆ insert p C := by
  unfold offlineStep
  split_ifs with hp hq <;> intro x hx
  · exact Finset.mem_insert.mpr (Or.inr hx)
  · rw [Finset.mem_insert] at hx ⊢
    rcases hx with hx | hx
    · exact Or.inl hx
    · rw [Finset.mem_erase] at hx
      exact Or.inr hx.2
  · exact hx

The offline step keeps the cache within the size bound when the request is in the phase and the phase has at most k pages.


lemma offlineStep_size (phase C : Finset Page) (p : Page) (hC : C.card ≤ k)
    (hp : p ∈ phase) (hphase : phase.card ≤ k) : (offlineStep phase C p).card ≤ k := by
  unfold offlineStep
  split_ifs with hpC hq
  · exact hC
  · have hqmem : (Classical.choose hq) ∈ C := (Classical.choose_spec hq).1
    have hpos : 0 < C.card := Finset.card_pos.mpr ⟨Classical.choose hq, hqmem⟩
    rw [Finset.card_insert_of_notMem]
    · rw [Finset.card_erase_of_mem hqmem]
      omega
    · intro hp'
      exact hpC (Finset.mem_of_mem_erase hp')
  · have hsub : C ⊆ phase := by
      intro x hx
      by_contra hnot
      exact hq ⟨x, hx, hnot⟩
    have hins : insert p C ⊆ phase := by
      rw [Finset.insert_subset_iff]
      exact ⟨hp, hsub⟩
    exact le_trans (Finset.card_le_card hins) hphase

A hit leaves the offline cache unchanged.

lemma offlineStep_hit (phase C : Finset Page) (p : Page) (hp : p ∈ C) :
    offlineStep phase C p = C := by
  unfold offlineStep
  simp [hp]

The offline step preserves an exactly-full cache.


lemma offlineStep_card_eq (phase C : Finset Page) (p : Page) (hC : C.card = k)
    (hp : p ∈ phase) (hphase : phase.card ≤ k) : (offlineStep phase C p).card = k := by
  unfold offlineStep
  split_ifs with hpC hq
  · exact hC
  · have hqmem : (Classical.choose hq) ∈ C := (Classical.choose_spec hq).1
    have hpos : 0 < C.card := Finset.card_pos.mpr ⟨Classical.choose hq, hqmem⟩
    rw [Finset.card_insert_of_notMem]
    · rw [Finset.card_erase_of_mem hqmem]
      omega
    · intro hp'
      exact hpC (Finset.mem_of_mem_erase hp')
  · exfalso
    have hsub : C ⊆ phase := by
      intro x hx
      by_contra hnot
      exact hq ⟨x, hx, hnot⟩
    have hle : C.card ≤ phase.card := Finset.card_le_card hsub
    have hk_le : k ≤ phase.card := by omega
    have hfull : C = phase := Finset.eq_of_subset_of_card_le hsub (by omega)
    exact hpC (by rw [hfull]; exact hp)

Serve one phase ρ (all requests lie in the phase phase) from cache C, evicting stale pages.

noncomputable def servePhase (phase : Finset Page) (C : Finset Page) : List Page → Finset Page
  | [] => C
  | p :: ρ => servePhase phase (offlineStep phase C p) ρ

The number of misses when serving one phase ρ from cache C.

noncomputable def servePhaseMisses (phase : Finset Page) (C : Finset Page) : List Page → ℕ
  | [] => 0
  | p :: ρ => (if p ∈ C then 0 else 1) + servePhaseMisses phase (offlineStep phase C p) ρ

The offline cache after serving a list of phases from cache C.

noncomputable def offCache (C : Finset Page) : List (List Page) → Finset Page
  | [] => C
  | ρ :: ps => offCache (servePhase ρ.toFinset C ρ) ps

The offline miss count over a list of phases from cache C.

noncomputable def offMisses (C : Finset Page) : List (List Page) → ℕ
  | [] => 0
  | ρ :: ps => servePhaseMisses ρ.toFinset C ρ + offMisses (servePhase ρ.toFinset C ρ) ps

A single offline step removes p from the phase pages S (and nothing else): S \ offlineStep phase C p = (S \ C) \ {p}.


lemma offlineStep_sdiff (phase C : Finset Page) (p : Page) (S : Finset Page) (hS : S ⊆ phase) :
    S \ offlineStep phase C p = (S \ C) \ {p} := by
  unfold offlineStep
  split_ifs with hpC hq
  · ext x
    simp only [Finset.mem_sdiff, This simp argument is unused:
  Finset.mem_erase

Hint: Omit it from the simp argument list.
  simp only [Finset.mem_sdiff, F̵i̵n̵s̵e̵t̵.̵m̵e̵m̵_̵e̵r̵a̵s̵e̵,̵ ̵Finset.mem_singleton]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`Finset.mem_erase, Finset.mem_singleton]
    have hnp : x ∉ C → x ≠ p := by intro hx hxp; subst x; exact hx hpC
    tauto
  · have hqmem : (Classical.choose hq) ∈ C ∧ (Classical.choose hq) ∉ phase := Classical.choose_spec hq
    have hqS : Classical.choose hq ∉ S := by intro h; exact hqmem.2 (hS h)
    ext x
    simp only [Finset.mem_sdiff, Finset.mem_insert, Finset.mem_erase, Finset.mem_singleton]
    have hxq : x ∈ S → x ≠ Classical.choose hq := by intro hx hxq; exact hqS (hxq ▸ hx)
    tauto
  · ext x
    simp only [Finset.mem_sdiff, Finset.mem_insert, This simp argument is unused:
  Finset.mem_erase

Hint: Omit it from the simp argument list.
  simp only [Finset.mem_sdiff, Finset.mem_insert, F̵i̵n̵s̵e̵t̵.̵m̵e̵m̵_̵e̵r̵a̵s̵e̵,̵ ̵Finset.mem_singleton]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`Finset.mem_erase, Finset.mem_singleton]
    tauto

The key one-step cardinal inequality driving the phase miss bound.


lemma card_step_ineq (S C : Finset Page) (p : Page) :
    (if p ∈ C then 0 else 1) + ((S \ C) \ {p}).card ≤ (insert p S \ C).card := by
  by_cases hpC : p ∈ C
  · simp [hpC]
    rw [Finset.insert_sdiff_of_mem S hpC]
    exact Finset.card_le_card (by intro x hx; exact (Finset.mem_sdiff.mp hx).1)
  · simp [hpC]
    by_cases hpS : p ∈ S
    · have hmem : p ∈ S \ C := Finset.mem_sdiff.mpr ⟨hpS, hpC⟩
      have hcard : ((S \ C) \ {p}).card + 1 = (S \ C).card := by
        rw [show (S \ C) \ {p} = (S \ C).erase p by ext x; simp only [Finset.mem_sdiff, Finset.mem_erase, Finset.mem_singleton]; tauto]
        exact Finset.card_erase_add_one hmem
      have hinsert : insert p S \ C = S \ C := by simp [hpS]
      rw [hinsert]
      omega
    · have hnot : p ∉ S \ C := by intro h; exact hpS (Finset.mem_sdiff.mp h).1
      have hins : insert p S \ C = insert p (S \ C) := by
        ext x
        by_cases hxp : x = p <;> simp [Finset.mem_sdiff, Finset.mem_insert, hxp, hpC, hpS]
      rw [hins, Finset.card_insert_of_notMem hnot]
      have heq : (S \ C) \ {p} = S \ C := by
        ext x
        simp only [Finset.mem_sdiff, This simp argument is unused:
  Finset.mem_erase

Hint: Omit it from the simp argument list.
  simp only [Finset.mem_sdiff, F̵i̵n̵s̵e̵t̵.̵m̵e̵m̵_̵e̵r̵a̵s̵e̵,̵ ̵Finset.mem_singleton]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`Finset.mem_erase, Finset.mem_singleton]
        have hnp : x ∈ S → x ≠ p := by intro hx hxp; exact hpS (hxp ▸ hx)
        tauto
      rw [heq]
      omega

Serving one phase faults at most once per distinct requested page not already cached: servePhaseMisses phase C ρ ≤ (ρ.toFinset \ C).card.


lemma servePhaseMisses_le (phase C : Finset Page) (ρ : List Page) (hρ : ρ.toFinset ⊆ phase) :
    servePhaseMisses phase C ρ ≤ (ρ.toFinset \ C).card := by
  induction ρ generalizing C with
  | nil => simp [servePhaseMisses]
  | cons p ρ' ih =>
      have hρ' : ρ'.toFinset ⊆ phase := by
        intro x hx
        exact hρ (by rw [List.toFinset_cons]; exact Finset.mem_insert.mpr (Or.inr hx))
      have hsd := offlineStep_sdiff phase C p ρ'.toFinset hρ'
      have hih := ih (offlineStep phase C p) hρ'
      change (if p ∈ C then 0 else 1) + servePhaseMisses phase (offlineStep phase C p) ρ'
          ≤ ((p :: ρ').toFinset \ C).card
      rw [List.toFinset_cons]
      calc
        (if p ∈ C then 0 else 1) + servePhaseMisses phase (offlineStep phase C p) ρ'
            ≤ (if p ∈ C then 0 else 1) + (ρ'.toFinset \ offlineStep phase C p).card :=
              Nat.add_le_add_left hih _
        _ = (if p ∈ C then 0 else 1) + ((ρ'.toFinset \ C) \ {p}).card := by rw [hsd]
        _ ≤ (insert p ρ'.toFinset \ C).card := card_step_ineq ρ'.toFinset C p

Serving a phase whose requests all lie in phase from a cache within the size bound stays within the size bound.


lemma servePhase_card_le (phase C : Finset Page) (ρ : List Page) (hC : C.card ≤ k)
    (hρ : ρ.toFinset ⊆ phase) (hphase : phase.card ≤ k) :
    (servePhase phase C ρ).card ≤ k := by
  induction ρ generalizing C with
  | nil => simpa [servePhase] using hC
  | cons p ρ' ih =>
      have hp_phase : p ∈ phase := hρ (by simp)
      have hρ' : ρ'.toFinset ⊆ phase := by
        intro x hx
        exact hρ (by rw [List.toFinset_cons]; exact Finset.mem_insert.mpr (Or.inr hx))
      simp [servePhase]
      exact ih (offlineStep phase C p) (offlineStep_size phase C p hC hp_phase hphase) hρ'

Serving a phase preserves an exactly-full cache.


lemma servePhase_card_eq (phase C : Finset Page) (ρ : List Page) (hC : C.card = k)
    (hρ : ρ.toFinset ⊆ phase) (hphase : phase.card ≤ k) :
    (servePhase phase C ρ).card = k := by
  induction ρ generalizing C with
  | nil => simpa [servePhase] using hC
  | cons p ρ' ih =>
      have hp_phase : p ∈ phase := hρ (by simp)
      have hρ' : ρ'.toFinset ⊆ phase := by
        intro x hx
        exact hρ (by rw [List.toFinset_cons]; exact Finset.mem_insert.mpr (Or.inr hx))
      simp [servePhase]
      exact ih (offlineStep phase C p) (offlineStep_card_eq phase C p hC hp_phase hphase) hρ'

Serving one phase from a full cache over the k + 1-page universe faults at most once.


lemma servePhaseMisses_le_one (C : Finset (Fin (k + 1))) (ρ : List (Fin (k + 1)))
    (hC : C.card = k) (Variable name `hρ` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`hρ : ρ.toFinset.card ≤ k) :
    servePhaseMisses ρ.toFinset C ρ ≤ 1 := by
  have hle := servePhaseMisses_le ρ.toFinset C ρ (by intro x hx; exact hx)
  have hcard : (ρ.toFinset \ C).card ≤ 1 := by
    have huniv : (Finset.univ : Finset (Fin (k + 1))).card = k + 1 := by
      rw [Finset.card_univ, Fintype.card_fin]
    have hcup : (C ∪ ρ.toFinset).card ≤ (Finset.univ : Finset (Fin (k + 1))).card :=
      Finset.card_le_card (Finset.subset_univ _)
    have hsd : (ρ.toFinset \ C).card = (C ∪ ρ.toFinset).card - C.card := by
      rw [Finset.card_sdiff]
      have hunion := Finset.card_union_add_card_inter C ρ.toFinset
      omega
    rw [hsd, hC]
    omega
  exact le_trans hle hcard

The number of phases is at most one more than σ.length / k.

try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
lemma phases_length_le (k : ℕ) (σ : List Page) (hk : 0 < k) :
    (phases k σ).length ≤ σ.length / k + 1 := by
  classical
  have go : ∀ (n : ℕ) (σ : List Page), σ.length = n →
      (phases k σ).length ≤ σ.length / k + 1 := by
    intro n
    induction n using Nat.strong_induction_on with
    | h n ih =>
      intro σ hlen
      cases σ with
      | nil => simp [phases, WellFounded.fix_eq]
      | cons p rest =>
          let fp := firstPhase k (p :: rest)
          have hsplit := firstPhase_split k (p :: rest)
          have hnonempty : fp.1 ≠ [] := by
            dsimp [fp]
            exact firstPhase_nonempty k (p :: rest) (by simp)
          by_cases hrem : fp.2 = []
          · rw [phases_cons_eq k (p :: rest) (by simp)]
            rw [hrem]
            simp [phases, WellFounded.fix_eq]
          · have hremlen : fp.2.length < (p :: rest).length := by
              have hlen : fp.1.length + fp.2.length = (p :: rest).length := by
                rw [← hsplit, List.length_append]
              have hpos : 0 < fp.1.length := List.length_pos_of_ne_nil hnonempty
              omega
            have hremlen' : fp.2.length < n := by omega
            have hih := ih fp.2.length hremlen' fp.2 rfl
            have hcard : fp.1.toFinset.card = k := by
              have hmax := firstPhase_maximal k (p :: rest) hk (by intro h; exact hrem (by try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [fp, h] using h))
              simpa [fp] using hmax.1
            have hlen1 : k ≤ fp.1.length := by
              have hle : fp.1.toFinset.card ≤ fp.1.length := by
                rw [List.toFinset, Multiset.card_toFinset]
                exact Multiset.card_le_card (Multiset.dedup_le _)
              omega
            have hdiv : 1 + fp.2.length / k ≤ (k + fp.2.length) / k := by
              rw [Nat.le_div_iff_mul_le hk]
              rw [Nat.add_mul]
              simp only [one_mul]
              have hle : fp.2.length / k * k ≤ fp.2.length := Nat.div_mul_le_self fp.2.length k
              omega
            have hlenσ : k + fp.2.length ≤ (p :: rest).length := by
              rw [← hsplit, List.length_append]
              exact Nat.add_le_add_right hlen1 fp.2.length
            rw [phases_cons_eq k (p :: rest) (by simp)]
            calc
              (fp.1 :: phases k fp.2).length = 1 + (phases k fp.2).length := by simp only [List.length_cons]; omega
              _ ≤ 1 + (fp.2.length / k + 1) := Nat.add_le_add_left hih 1
              _ = 1 + fp.2.length / k + 1 := by omega
              _ ≤ (k + fp.2.length) / k + 1 := Nat.add_le_add_right hdiv 1
              _ ≤ (p :: rest).length / k + 1 := by
                exact Nat.add_le_add_right (Nat.div_le_div_right hlenσ) 1
  exact go σ.length σ rfl

From a full cache (exactly k pages) over the k + 1-page universe, the offline schedule faults at most once per phase.


theorem offMisses_bound_from_full (k : ℕ) (σ : List (Fin (k + 1))) (hk : 0 < k)
    (C : Finset (Fin (k + 1))) (hC : C.card = k) :
    offMisses C (phases k σ) ≤ (phases k σ).length := by
  classical
  have go : ∀ (n : ℕ) (σ : List (Fin (k + 1))), σ.length = n →
      ∀ (C : Finset (Fin (k + 1))), C.card = k → offMisses C (phases k σ) ≤ (phases k σ).length := by
    intro n
    induction n using Nat.strong_induction_on with
    | h n ih =>
      intro σ hlen C hC
      cases σ with
      | nil => simp [offMisses, phases, WellFounded.fix_eq]
      | cons p rest =>
          let fp := firstPhase k (p :: rest)
          have hsplit := firstPhase_split k (p :: rest)
          have hnonempty : fp.1 ≠ [] := by
            dsimp [fp]
            exact firstPhase_nonempty k (p :: rest) (by simp)
          have hcard_fp : fp.1.toFinset.card ≤ k := by
            exact firstPhase_distinct_le k (p :: rest) hk
          have hmisses : servePhaseMisses fp.1.toFinset C fp.1 ≤ 1 := by
            exact servePhaseMisses_le_one C fp.1 hC (by simpa [fp] using hcard_fp)
          have hcache : (servePhase fp.1.toFinset C fp.1).card = k := by
            exact servePhase_card_eq fp.1.toFinset C fp.1 hC (by intro x hx; exact hx) (by simpa [fp] using hcard_fp)
          have hremlen : fp.2.length < (p :: rest).length := by
            have hlen : fp.1.length + fp.2.length = (p :: rest).length := by
              rw [← hsplit, List.length_append]
            have hpos : 0 < fp.1.length := List.length_pos_of_ne_nil hnonempty
            omega
          have hremlen' : fp.2.length < n := by omega
          have hih := ih fp.2.length hremlen' fp.2 rfl (servePhase fp.1.toFinset C fp.1) hcache
          rw [phases_cons_eq k (p :: rest) (by simp)]
          simp [offMisses]
          calc
            servePhaseMisses fp.1.toFinset C fp.1 + offMisses (servePhase fp.1.toFinset C fp.1) (phases k fp.2)
                ≤ 1 + offMisses (servePhase fp.1.toFinset C fp.1) (phases k fp.2) := Nat.add_le_add_right hmisses _
            _ ≤ 1 + (phases k fp.2).length := Nat.add_le_add_left hih 1
            _ = (fp.1 :: phases k fp.2).length := by simp only [List.length_cons]; omega
  exact go σ.length σ rfl C hC

Serving one phase from an empty cache yields exactly the phase's distinct pages as the new cache.


lemma servePhase_eq_union (phase C : Finset Page) (ρ : List Page) (hC : C ⊆ phase)
    (hρ : ρ.toFinset ⊆ phase) : servePhase phase C ρ = C ∪ ρ.toFinset := by
  induction ρ generalizing C with
  | nil => simp [servePhase]
  | cons p ρ' ih =>
      have hp_phase : p ∈ phase := hρ (by simp)
      have hρ' : ρ'.toFinset ⊆ phase := by
        intro x hx
        exact hρ (by rw [List.toFinset_cons]; exact Finset.mem_insert.mpr (Or.inr hx))
      have hstep : offlineStep phase C p = insert p C := by
        unfold offlineStep
        by_cases hpC : p ∈ C
        · simp [hpC]
        · have hnone : ¬ ∃ q ∈ C, q ∉ phase := by
            rintro ⟨q, hqC, hqnot⟩
            exact hqnot (hC hqC)
          simp [hpC, hnone]
      simp [servePhase, hstep]
      have hC' : insert p C ⊆ phase := by
        rw [Finset.insert_subset_iff]
        exact ⟨hp_phase, hC⟩
      rw [ih (insert p C) hC' hρ']
      ext x
      simp only [Finset.mem_insert, Finset.mem_union]
      tauto

Offline upper bound. The offline schedule faults at most (phases k σ).length + k times over any request sequence on the k + 1-page universe, starting from an empty cache.

try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
theorem offMisses_bound (k : ℕ) (σ : List (Fin (k + 1))) (hk : 0 < k) :
    offMisses ∅ (phases k σ) ≤ (phases k σ).length + k := by
  classical
  have go : ∀ (n : ℕ) (σ : List (Fin (k + 1))), σ.length = n →
      offMisses ∅ (phases k σ) ≤ (phases k σ).length + k := by
    intro n
    induction n using Nat.strong_induction_on with
    | h n ih =>
      intro σ hlen
      cases σ with
      | nil => simp [offMisses, phases, WellFounded.fix_eq]
      | cons p rest =>
          let fp := firstPhase k (p :: rest)
          have hsplit := firstPhase_split k (p :: rest)
          have hnonempty : fp.1 ≠ [] := by
            dsimp [fp]
            exact firstPhase_nonempty k (p :: rest) (by simp)
          have hcard_fp : fp.1.toFinset.card ≤ k := by
            exact firstPhase_distinct_le k (p :: rest) hk
          have hmisses : servePhaseMisses fp.1.toFinset ∅ fp.1 ≤ fp.1.toFinset.card := by
            exact servePhaseMisses_le fp.1.toFinset ∅ fp.1 (by intro x hx; exact hx)
          have hremlen : fp.2.length < (p :: rest).length := by
            have hlen : fp.1.length + fp.2.length = (p :: rest).length := by
              rw [← hsplit, List.length_append]
            have hpos : 0 < fp.1.length := List.length_pos_of_ne_nil hnonempty
            omega
          have hremlen' : fp.2.length < n := by omega
          by_cases hrem : fp.2 = []
          · rw [phases_cons_eq k (p :: rest) (by simp), hrem]
            simp [offMisses, phases, WellFounded.fix_eq]
            exact le_trans (le_trans hmisses hcard_fp) (by omega)
          · have hcard_fp_eq : fp.1.toFinset.card = k := by
              have hmax := firstPhase_maximal k (p :: rest) hk (by intro h; exact hrem (by try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [fp, h] using h))
              simpa [fp] using hmax.1
            have hcache_eq : servePhase fp.1.toFinset ∅ fp.1 = fp.1.toFinset := by
              exact servePhase_eq_union fp.1.toFinset ∅ fp.1 (by simp) (by intro x hx; exact hx)
            have hcache : (servePhase fp.1.toFinset ∅ fp.1).card = k := by
              rw [hcache_eq, hcard_fp_eq]
            have hih := offMisses_bound_from_full k fp.2 hk (servePhase fp.1.toFinset ∅ fp.1) hcache
            rw [phases_cons_eq k (p :: rest) (by simp)]
            simp [offMisses]
            calc
              servePhaseMisses fp.1.toFinset ∅ fp.1 + offMisses (servePhase fp.1.toFinset ∅ fp.1) (phases k fp.2)
                  ≤ fp.1.toFinset.card + offMisses (servePhase fp.1.toFinset ∅ fp.1) (phases k fp.2) :=
                    Nat.add_le_add_right hmisses _
              _ ≤ k + (phases k fp.2).length := by
                rw [hcard_fp_eq]
                exact Nat.add_le_add_left hih k
              _ ≤ (fp.1 :: phases k fp.2).length + k := by
                simp only [List.length_cons]
                omega
  exact go σ.length σ rfl

Theorem 27.4 (Sleator-Tarjan lower bound). For any deterministic online paging algorithm A with cache size k ≥ 1, and any request count N, there is a request sequence σ of length N (over k + 1 pages) on which A faults on every request while some offline schedule faults at most N / k + k + 1 times. Hence no deterministic online algorithm is c-competitive for any c < k.


theorem caching_lower_bound (k N : ℕ) (hk : 0 < k) (A : Algorithm (Fin (k + 1)) k) :
    ∃ σ : List (Fin (k + 1)),
      σ.length = N ∧
      misses A ∅ σ = N ∧
      offMisses ∅ (phases k σ) ≤ N / k + k + 1 := by
  refine ⟨advSeq A N, ?_, advSeq_misses A N, ?_⟩
  · exact advSeq_length A N
  · calc
      offMisses ∅ (phases k (advSeq A N)) ≤ (phases k (advSeq A N)).length + k :=
        offMisses_bound k (advSeq A N) hk
      _ ≤ (advSeq A N).length / k + 1 + k := by
        exact Nat.add_le_add_right (phases_length_le k (advSeq A N) hk) k
      _ = N / k + k + 1 := by
        rw [advSeq_length A]
        omega

No c-competitive ratio below k. For any c < k, the adversarial sequence of length k^3 witnesses that A's miss count strictly exceeds c times the offline cost.


theorem caching_no_c_competitive (k : ℕ) (hk : 0 < k) (A : Algorithm (Fin (k + 1)) k) :
    ∀ c : ℕ, c < k → c * offMisses ∅ (phases k (advSeq A (k * k * k))) < misses A ∅ (advSeq A (k * k * k)) := by
  intro c hc
  have hbound : offMisses ∅ (phases k (advSeq A (k * k * k))) ≤ (k * k * k) / k + k + 1 := by
    calc
      offMisses ∅ (phases k (advSeq A (k * k * k))) ≤ (phases k (advSeq A (k * k * k))).length + k :=
        offMisses_bound k (advSeq A (k * k * k)) hk
      _ ≤ (advSeq A (k * k * k)).length / k + 1 + k := by
        exact Nat.add_le_add_right (phases_length_le k (advSeq A (k * k * k)) hk) k
      _ = (k * k * k) / k + k + 1 := by
        rw [advSeq_length A]
        omega
  have hmiss : misses A ∅ (advSeq A (k * k * k)) = k * k * k := advSeq_misses A (k * k * k)
  have hdiv : (k * k * k) / k = k * k := by
    rw [Nat.mul_assoc]
    exact Nat.mul_div_right (k * k) hk
  calc
    c * offMisses ∅ (phases k (advSeq A (k * k * k)))
        ≤ c * ((k * k * k) / k + k + 1) := Nat.mul_le_mul_left c hbound
    _ ≤ (k - 1) * ((k * k * k) / k + k + 1) := by
      exact Nat.mul_le_mul_right _ (by omega : c ≤ k - 1)
    _ = (k - 1) * (k * k + k + 1) := by rw [hdiv]
    _ < k * k * k := by
      obtain ⟨d, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (by omega : k ≠ 0)
      simp only [Nat.succ_eq_add_one]
      have hd : d + 1 - 1 = d := by omega
      rw [hd]
      have h : d * ((d + 1) * (d + 1) + (d + 1) + 1) + 1 = (d + 1) * (d + 1) * (d + 1) := by ring
      rw [← h]
      exact Nat.lt_succ_self _
    _ = misses A ∅ (advSeq A (k * k * k)) := by rw [hmiss]

end OnlineCachingend CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_27.Section_27_3_Online_Caching.Competitive

LRU against policies with arbitrary auxiliary state

Actual policy runs produce legal schedules. The offline trace theorem therefore also proves the online result without replaying any requests or assuming that hits leave auxiliary history unchanged.

              namespace CLRS.OnlineCaching.Policyvariable {Page : Type} [DecidableEq Page] {k : Nat}theorem phases_from_resident (A : Policy Page k) (hk : 0 < k)
    (p : Page) (rest : List Page) (s : A.State) (hp : p ∈ A.cache s) :
    (phases k (p :: rest)).length ≤ A.misses s rest + 1 :=
  Schedule.phases_from_resident hk p rest (A.schedule s rest) hptheorem phases_le_misses (A : Policy Page k) (hk : 0 < k) (s : A.State) (xs : List Page) :
    (phases k xs).length ≤ A.misses s xs + 1 := (A.schedule s xs).phases_le_cost hk

LRU's actual list execution is k-competitive against every history-dependent policy.


theorem lru_k_competitive (A : Policy Page k) (hk : 0 < k) (xs : List Page) :
    (lruPolicy hk).misses (lruPolicy hk).initial xs ≤ k * A.misses A.initial xs + k := by
  rw [lruPolicy_misses]
  have hs := A.schedule A.initial xs
  rw [A.initial_empty] at hs
  exact hs.lru_k_competitive hk

end CLRS.OnlineCaching.Policy

CLRSLean.FourthEdition.Chapter_27.Section_27_3_Online_Caching.LowerBound

Deterministic paging lower bound with real ratios and additive constants

The adversary observes only a policy's current resident set. Arbitrary hidden history is permitted in the online policy. The offline comparator is the existing trace-dependent phase schedule; it is not claimed to be an online finite-set transition. Witness length grows with the additive constant.

              noncomputable sectionnamespace CLRS.OnlineCaching.Policyvariable {k : Nat} (A : Policy (Fin (k + 1)) k)def adversary (s : A.State) : Nat → List (Fin (k + 1))
  | 0 => []
  | n + 1 =>
    let p := freshPage (A.cache s)
    p :: adversary (A.step s p) n@[simp] theorem adversary_length (s : A.State) (n : Nat) :
    (A.adversary s n).length = n := by
  induction n generalizing s with
  | zero => rfl
  | succ n ih => simp [adversary, ih]@[simp] theorem adversary_misses (s : A.State) (n : Nat) :
    A.misses s (A.adversary s n) = n := by
  induction n generalizing s with
  | zero => rfl
  | succ n ih =>
    have hp := freshPage_spec (A.cache s) (exists_page_not_mem _ (A.size s))
    simp [adversary, misses, hp, ih, Nat.add_comm]

A history-dependent online policy misses every request of an arbitrary-length witness.

theorem caching_lower_bound (hk : 0 < k) (N : Nat) :
    ∃ xs : List (Fin (k + 1)), xs.length = N ∧ A.misses A.initial xs = N ∧
      offMisses ∅ (phases k xs) ≤ N / k + k + 1 := by
  refine ⟨A.adversary A.initial N, by simp, by simp, ?_⟩
  have h := offMisses_bound k (A.adversary A.initial N) hk
  have hp := phases_length_le k (A.adversary A.initial N) hk
  simp only [adversary_length] at hp
  omega

Every real ratio below k fails, for every real additive constant. The witness is nonempty and both runs begin with empty caches.


theorem no_real_competitive (hk : 0 < k) (c b : ℝ) (hc0 : 0 ≤ c) (hc : c < k) :
    ∃ xs : List (Fin (k + 1)), 0 < xs.length ∧
      c * (offMisses ∅ (phases k xs) : ℝ) + b < (A.misses A.initial xs : ℝ) := by
  have hgap : 0 < (k : ℝ) - c := sub_pos.mpr hc
  obtain ⟨m,hm⟩ := exists_nat_gt (max 0 ((c * ((k : ℝ) + 1) + b) / ((k : ℝ) - c)))
  have hmpos : 0 < m := by
    have : (0 : ℝ) < m := (le_max_left _ _).trans_lt hm
    exact_mod_cast this
  have hratio : (c * ((k : ℝ) + 1) + b) / ((k : ℝ) - c) < m :=
    (le_max_right _ _).trans_lt hm
  have hlarge : c * ((k : ℝ) + 1) + b < (m : ℝ) * ((k : ℝ) - c) :=
    (div_lt_iff₀ hgap).mp hratio
  obtain ⟨xs,hlen,hmiss,hoff⟩ := A.caching_lower_bound hk (k * m)
  have hdiv : k * m / k = m := Nat.mul_div_cancel_left m hk
  rw [hdiv] at hoff
  refine ⟨xs, by rw [hlen]; exact Nat.mul_pos hk hmpos, ?_⟩
  have hoffR : (offMisses ∅ (phases k xs) : ℝ) ≤ (m : ℝ) + k + 1 := by exact_mod_cast hoff
  have hscaled := mul_le_mul_of_nonneg_left hoffR hc0
  rw [hmiss]
  push_cast
  nlinarith

end CLRS.OnlineCaching.Policy

CLRSLean.FourthEdition.Chapter_27.Section_27_3_Online_Caching.OfflineCompetitive

LRU competitiveness against every legal offline trace

              namespace CLRS.OnlineCaching.Schedulevariable {Page : Type} [DecidableEq Page] {k : Nat}theorem start_size {C F : Finset Page} {xs : List Page} {cost : Nat}
    (h : Schedule k C xs F cost) : C.card ≤ k := by cases h <;> assumptiontheorem split {C F : Finset Page} (xs ys : List Page) {cost : Nat}
    (h : Schedule k C (xs ++ ys) F cost) :
    ∃ D a b, Schedule k C xs D a ∧ Schedule k D ys F b ∧ cost = a + b := by
  induction xs generalizing C cost with
  | nil => exact ⟨C,0,cost,.nil C h.start_size,h,by omega⟩
  | cons p xs ih =>
    cases h with
    | cons C C' p _ F cost hs hl hsub hh ht =>
      obtain ⟨D,a,b,ha,hb,heq⟩ := ih ht
      exact ⟨D,_,b,.cons C C' p xs D a hs hl hsub hh ha,hb,by omega⟩

theorem zero_subset {C F : Finset Page} {xs : List Page} {cost : Nat}
    (h : Schedule k C xs F cost) (hc : cost = 0) : xs.toFinset ⊆ C := by
  induction h with
  | nil => simp
  | cons C C' p xs F cost hs hl hsub hh ht ih =>
    have hp : p ∈ C := by by_contra hn; simp [hn] at hc
    have htail : cost = 0 := by simp [hp] at hc; exact hc
    have hxs := ih htail
    rw [hh hp] at hxs
    simpa using Finset.insert_subset_iff.mpr ⟨hp,hxs⟩

theorem resident_fault {C F : Finset Page} {xs : List Page} {cost : Nat}
    (h : Schedule k C xs F cost) (p : Page) (hp : p ∈ C)
    (hx : k ≤ (xs.toFinset.erase p).card) : 1 ≤ cost := by
  by_contra hn
  have hs := h.zero_subset (by omega)
  have hc := Finset.card_le_card (Finset.erase_subset_erase p hs)
  rw [Finset.card_erase_of_mem hp] at hc
  have hpos := Finset.card_pos.mpr ⟨p,hp⟩
  have hb := h.start_size
  omegatheorem singleton_loads {C F : Finset Page} {p : Page} {cost : Nat}
    (h : Schedule k C [p] F cost) : p ∈ F := by
  cases h with
  | cons C C' p xs F cost hs hl hsub hh ht => cases ht; exact hl

theorem phases_from_resident (hk : 0 < k) (p : Page) (rest : List Page)
    {C F : Finset Page} {cost : Nat} (h : Schedule k C rest F cost) (hp : p ∈ C) :
    (phases k (p :: rest)).length ≤ cost + 1 := by
  classical
  have go : ∀ n (rest : List Page), rest.length = n → ∀ p C F cost,
      Schedule k C rest F cost → p ∈ C → (phases k (p :: rest)).length ≤ cost + 1 := by
    intro n
    induction n using Nat.strong_induction_on with
    | h n ih =>
      intro rest hn p C F cost h hp
      let chunk := phaseGo k ({p} : Finset Page) rest
      have hsplit : chunk.1 ++ chunk.2 = rest := phaseGo_split k {p} rest
      cases ht : chunk.2 with
      | nil =>
        rw [phases_cons_eq k (p :: rest) (by simp)]
        change ((p :: chunk.1) :: phases k chunk.2).length ≤ _
        rw [ht]
        simp [phases, WellFounded.fix_eq]
      | cons q tail =>
        have hfp : firstPhase k (p :: rest) = (p :: chunk.1, chunk.2) := rfl
        have hm := firstPhase_maximal k (p :: rest) hk (by rw [hfp, ht]; simp)
        have hcard : (p :: chunk.1).toFinset.card = k := by simpa [hfp] using hm.1
        have hq : q ∉ (p :: chunk.1).toFinset :=
          firstPhase_fresh k (p :: rest) hk q tail (by rw [hfp]; exact ht)
        have hset : (chunk.1 ++ [q]).toFinset.erase p =
            (insert q (p :: chunk.1).toFinset).erase p := by
          ext x
          simp only [Finset.mem_erase, List.mem_toFinset, List.mem_append,
            Finset.mem_insert, List.mem_cons]
          tauto
        have hcount : ((chunk.1 ++ [q]).toFinset.erase p).card = k := by
          rw [hset, Finset.card_erase_of_mem (by simp), Finset.card_insert_of_notMem hq, hcard]
          omega
        have hrest : rest = (chunk.1 ++ [q]) ++ tail := by
          rw [ht] at hsplit
          simpa [List.append_assoc] using hsplit.symm
        rw [hrest] at h
        obtain ⟨D,a,b,ha,hb,hcost⟩ := split (chunk.1 ++ [q]) tail h
        have hfault := ha.resident_fault p hp hcount.ge
        obtain ⟨M,aa,ab,_,hlast,_⟩ := split chunk.1 [q] ha
        have hresident := hlast.singleton_loads
        have hlen : tail.length < n := by
          have := congrArg List.length hrest
          simp at this
          omega
        have hnext := ih tail.length hlen tail rfl q D F b hb hresident
        rw [phases_cons_eq k (p :: rest) (by simp)]
        change ((p :: chunk.1) :: phases k chunk.2).length ≤ _
        rw [ht]
        simp only [List.length_cons]
        omega
  exact go rest.length rest rfl p C F cost h hp

Every legal trace, including a future-dependent offline schedule, obeys the phase lower bound.

theorem phases_le_cost (hk : 0 < k) {C F : Finset Page} {xs : List Page} {cost : Nat}
    (h : Schedule k C xs F cost) : (phases k xs).length ≤ cost + 1 := by
  cases h with
  | nil => simp [phases, WellFounded.fix_eq]
  | cons C C' p xs F cost hs hl hsub hh ht =>
    have hb := phases_from_resident hk p xs ht hl
    split <;> omega

LRU's actual misses are k-competitive against every legal empty-start offline schedule.


theorem lru_k_competitive (hk : 0 < k) {F : Finset Page} {xs : List Page} {cost : Nat}
    (h : Schedule k ∅ xs F cost) : lruMissesGo k [] xs ≤ k * cost + k := by
  have hu := lru_miss_le_phases k [] xs hk (by simp)
  have hl := h.phases_le_cost hk
  nlinarith [Nat.mul_le_mul_left k hl]

end CLRS.OnlineCaching.Schedule

CLRSLean.FourthEdition.Chapter_27.Section_27_3_Online_Caching.Policies

Inhabited paging policies with auxiliary state

The legacy finite-set interface describes memoryless policies. The new Policy interface has arbitrary internal state and exposes only its resident set. A hit preserves residency, but may update history. The transition receives only the current state and request, so it cannot inspect future requests. Capacity is an invariant of every state in its state type. An offline schedule instead receives a request trace and may choose its evictions from that trace.

namespace CLRS.OnlineCachingvariable {Page : Type} [DecidableEq Page] {k : Nat}

A concrete memoryless policy: retain a hit, flush to the request on a miss.

def flushAlgorithm (hk : 0 < k) : Algorithm Page k where
  step C p := if p ∈ C then C else {p}
  step_loads := by intro C p; split <;> simp_all
  step_subset := by intro C p; split <;> simp_all
  step_size := by intro C p hC; split <;> simp_all; omega
  step_hit := by intro C p _ hp; simp [hp]

Positive-capacity policy space is inhabited even on the k+1 page universe.

theorem algorithm_nonempty (hk : 0 < k) : Nonempty (Algorithm Page k) := ⟨flushAlgorithm hk⟩

              structure Policy (Page : Type) [DecidableEq Page] (k : Nat) where
  State : Type
  cache : State → Finset Page
  initial : State
  initial_empty : cache initial = ∅
  step : State → Page → State
  size : ∀ s, (cache s).card ≤ k
  loads : ∀ s p, p ∈ cache (step s p)
  subset : ∀ s p, cache (step s p) ⊆ insert p (cache s)
  hit : ∀ s p, p ∈ cache s → cache (step s p) = cache snamespace Policyvariable (A : Policy Page k)def run : A.State → List Page → A.State
  | s, [] => s
  | s, p :: ps => run (A.step s p) psdef misses : A.State → List Page → Nat
  | _, [] => 0
  | s, p :: ps => (if p ∈ A.cache s then 0 else 1) + misses (A.step s p) ps@[simp] theorem run_append (s : A.State) (xs ys : List Page) :
    A.run s (xs ++ ys) = A.run (A.run s xs) ys := by
  induction xs generalizing s with
  | nil => rfl
  | cons p xs ih => simp [run, ih]@[simp] theorem misses_append (s : A.State) (xs ys : List Page) :
    A.misses s (xs ++ ys) = A.misses s xs + A.misses (A.run s xs) ys := by
  induction xs generalizing s with
  | nil => simp [misses, run]
  | cons p xs ih => simp [misses, run, ih, Nat.add_assoc]

theorem zero_subset (s : A.State) (xs : List Page) (h : A.misses s xs = 0) :
    xs.toFinset ⊆ A.cache s := by
  induction xs generalizing s with
  | nil => simp
  | cons p xs ih =>
    have hp : p ∈ A.cache s := by
      by_contra hn
      simp [misses, hn] at h
    have ht : A.misses (A.step s p) xs = 0 := by simpa [misses, hp] using h
    have hs := ih (A.step s p) ht
    rw [A.hit s p hp] at hs
    simpa using Finset.insert_subset_iff.mpr ⟨hp, hs⟩

theorem resident_fault (s : A.State) (p : Page) (xs : List Page)
    (hp : p ∈ A.cache s) (hx : k ≤ (xs.toFinset.erase p).card) :
    1 ≤ A.misses s xs := by
  by_contra hn
  have hz : A.misses s xs = 0 := by omega
  have hs := A.zero_subset s xs hz
  have hc : (xs.toFinset.erase p).card ≤ ((A.cache s).erase p).card :=
    Finset.card_le_card (Finset.erase_subset_erase p hs)
  rw [Finset.card_erase_of_mem hp] at hc
  have hpos := Finset.card_pos.mpr ⟨p,hp⟩
  have hb := A.size s
  omegaend Policy

LRU stores recency order as well as residency.

structure LRUState (Page : Type) (k : Nat) where
  recency : List Page
  nodup : recency.Nodup
  size : recency.length ≤ k

theorem lruStep_length_le (hk : 0 < k) (L : List Page) (p : Page) (hL : L.length ≤ k) :
    (lruStep k L p).length ≤ k := by
  unfold lruStep
  split_ifs with hp hl
  · have heq := (List.perm_cons_erase hp).length_eq
    simpa only [← heq] using hL
  · simp only [List.length_cons]; omega
  · simp only [List.length_cons, List.length_dropLast]; omega

def lruPolicy (hk : 0 < k) : Policy Page k where
  State := LRUState Page k
  cache s := s.recency.toFinset
  initial := ⟨[], by simp, by simp⟩
  initial_empty := rfl
  step s p := ⟨lruStep k s.recency p, lruStep_nodup k _ p s.nodup,
    lruStep_length_le hk _ p s.size⟩
  size s := by simpa [toFinset_card_of_nodup s.nodup] using s.size
  loads s p := by simp [lruStep]; split_ifs <;> simp
  subset s p := by
    intro q hq
    simp only [List.mem_toFinset, mem_lruStep] at hq
    split_ifs at hq with hp hl
    · exact Finset.mem_insert_of_mem (List.mem_toFinset.mpr hq)
    · simpa using hq
    · rcases hq with rfl | hq
      · simp
      · exact Finset.mem_insert_of_mem (List.mem_toFinset.mpr (List.mem_of_mem_dropLast hq))
  hit s p hp := by
    ext q
    simp only [List.mem_toFinset] at hp ⊢
    simp [mem_lruStep, hp]

The stateful LRU policy's misses are those of the original list execution.


theorem lruPolicy_misses (hk : 0 < k) (s : LRUState Page k) (xs : List Page) :
    (lruPolicy hk).misses s xs = lruMissesGo k s.recency xs := by
  induction xs generalizing s with
  | nil => rfl
  | cons p xs ih =>
    change (if p ∈ s.recency.toFinset then 0 else 1) +
      (lruPolicy hk).misses ((lruPolicy hk).step s p) xs = _
    rw [ih]
    simp [lruMissesGo, lruPolicy]

end CLRS.OnlineCaching

CLRSLean.FourthEdition.Chapter_27.Section_27_3_Online_Caching.Schedules

Valid offline paging schedules

A schedule records legal cache transitions for an entire request trace, with its actual miss count. It can depend on the future. The existing phase-based offline execution produces such a schedule, including every intermediate capacity invariant; its comparison cost is therefore attainable.

              namespace CLRS.OnlineCachingvariable {Page : Type} [DecidableEq Page] {k : Nat}inductive Schedule (k : Nat) : Finset Page → List Page → Finset Page → Nat → Prop
  | nil (C : Finset Page) (size : C.card ≤ k) : Schedule k C [] C 0
  | cons (C C' : Finset Page) (p : Page) (xs : List Page) (final : Finset Page) (cost : Nat)
      (size : C.card ≤ k) (loads : p ∈ C') (subset : C' ⊆ insert p C)
      (hit : p ∈ C → C' = C) (tail : Schedule k C' xs final cost) :
      Schedule k C (p :: xs) final ((if p ∈ C then 0 else 1) + cost)namespace Scheduletheorem append {C D F : Finset Page} {xs ys : List Page} {a b : Nat}
    (hx : Schedule k C xs D a) (hy : Schedule k D ys F b) :
    Schedule k C (xs ++ ys) F (a + b) := by
  induction hx with
  | nil _ _ => simpa using hy
  | cons C C' p xs final cost hs hl hsub hh ht ih =>
    simpa [Nat.add_assoc] using cons C C' p (xs ++ ys) F (cost+b) hs hl hsub hh (ih hy)end Schedule

theorem servePhase_schedule (phase C : Finset Page) (xs : List Page)
    (hC : C.card ≤ k) (hxs : xs.toFinset ⊆ phase) (hphase : phase.card ≤ k) :
    Schedule k C xs (servePhase phase C xs) (servePhaseMisses phase C xs) := by
  induction xs generalizing C with
  | nil => exact .nil C hC
  | cons p xs ih =>
    have hp := hxs (by simp : p ∈ (p::xs).toFinset)
    have ht : xs.toFinset ⊆ phase := by intro x hx; exact hxs (by simp [hx])
    exact .cons C (offlineStep phase C p) p xs _ _ hC
      (offlineStep_loads _ _ _) (offlineStep_subset _ _ _) (offlineStep_hit _ _ _)
      (ih _ (offlineStep_size _ _ _ hC hp hphase) ht)

theorem off_schedule (C : Finset Page) (ps : List (List Page)) (hC : C.card ≤ k)
    (hps : ∀ xs ∈ ps, xs.toFinset.card ≤ k) :
    Schedule k C ps.flatten (offCache C ps) (offMisses C ps) := by
  induction ps generalizing C with
  | nil => exact .nil C hC
  | cons xs ps ih =>
    have hx := hps xs (by simp)
    have hs := servePhase_schedule xs.toFinset C xs hC (by intro x h; exact h) hx
    have ht := ih (servePhase xs.toFinset C xs)
      (servePhase_card_le _ _ _ hC (by intro x h; exact h) hx)
      (by intro ys hy; exact hps ys (by simp [hy]))
    exact hs.append ht

theorem phases_capacity (hk : 0 < k) (xs : List Page) :
    ∀ ys ∈ phases k xs, ys.toFinset.card ≤ k := by
  classical
  have go : ∀ n (xs : List Page), xs.length = n → ∀ ys ∈ phases k xs, ys.toFinset.card ≤ k := by
    intro n
    induction n using Nat.strong_induction_on with
    | h n ih =>
      intro xs hn ys hy
      by_cases hempty : xs = []
      · subst xs; simp [phases, WellFounded.fix_eq] at hy
      · rw [phases_cons_eq k xs hempty] at hy
        rcases List.mem_cons.mp hy with rfl | hy
        · exact firstPhase_distinct_le k xs hk
        · have hlen : (firstPhase k xs).2.length < n := by
            have hsplit := congrArg List.length (firstPhase_split k xs)
            have hp := List.length_pos_of_ne_nil (firstPhase_nonempty k xs hempty)
            simp only [List.length_append] at hsplit
            omega
          exact ih _ hlen _ rfl ys hy
  exact go xs.length xs rfl

The phase comparator cost is realized by a legal empty-start offline schedule.

theorem offline_schedule_valid (hk : 0 < k) (xs : List Page) :
    Schedule k ∅ xs (offCache ∅ (phases k xs)) (offMisses ∅ (phases k xs)) := by
  simpa only [phases_join] using off_schedule (∅ : Finset Page) (phases k xs)
    (by simp) (phases_capacity hk xs)

A policy's actual run supplies a legal schedule, including hidden-state policies.

theorem Policy.schedule (A : Policy Page k) (s : A.State) (xs : List Page) :
    Schedule k (A.cache s) xs (A.cache (A.run s xs)) (A.misses s xs) := by
  induction xs generalizing s with
  | nil => exact .nil _ (A.size s)
  | cons p xs ih =>
    exact .cons _ _ p xs _ _ (A.size s) (A.loads s p) (A.subset s p) (A.hit s p) (ih _)

end CLRS.OnlineCaching

Scope and implementation notes

Imports

import CLRSLean.FourthEdition.Chapter_27.Section_27_1_Waiting_For_Elevator
import CLRSLean.FourthEdition.Chapter_27.Section_27_2_Maintaining_A_Search_List
import CLRSLean.FourthEdition.Chapter_27.Section_27_3_Online_Caching
import CLRSLean.FourthEdition.Chapter_27.Section_27_3_Online_Caching.Competitive
import CLRSLean.FourthEdition.Chapter_27.Section_27_3_Online_Caching.LowerBound

Current source

Section 27.1 (Waiting for an elevator) is formalized natively in CLRSLean.FourthEdition.Chapter_27.Section_27_1_Waiting_For_Elevator: the rent-or-buy (ski rental) problem — the cost of the deterministic rent-a-days-then-buy strategy, the optimal offline cost, Theorem 27.1 (any strategy with a * r < p ≤ (a + 1) * r is 2-competitive), and the elevator corollary whose wait-S - E-then-take-the-stairs strategy is 2-competitive with worst-case ratio 2 - E/S.

Section 27.2 (Maintaining a search list) is formalized natively in CLRSLean.FourthEdition.Chapter_27.Section_27_2_Maintaining_A_Search_List: the list-update problem, the MOVE-TO-FRONT strategy with its per-request cost, the inversion-distance potential, and Theorem 27.2 (MOVE-TO-FRONT is 4-competitive against any list-update strategy that keeps its list a permutation of the initial set).

Section 27.3 (Online caching) is formalized natively in CLRSLean.FourthEdition.Chapter_27.Section_27_3_Online_Caching: the paging model with the least-recently-used (LRU) policy as a most-recent-first list, the legacy memoryless Algorithm with legal-state capacity/hit laws, and the new Policy interface with arbitrary auxiliary state. An inhabited LRU policy preserves recency order, so equal resident sets can produce different evictions. Schedule describes future-dependent offline traces separately.

Schedule.lru_k_competitive proves the actual LRU miss bound against every legal offline schedule. Policy.lru_k_competitive follows for actual online policy runs. The actual phase-based offline execution is a valid schedule. Policy.no_real_competitive proves that for every real ratio 0 ≤ c < k and every real additive constant there is a nonempty request sequence defeating that ratio. The witness length grows with the constant; this theorem permits arbitrary hidden history and requires positive capacity.

No legacy source is promoted into this chapter.

Coverage boundary

The represented rental lower bounds retain positive horizons and strictly positive offline costs; skiRental_not_competitive_below rules out every strictly smaller ratio. The list-update theorem uses equality of distinct-key sets. Physical index and adjacent-swap interpretations require duplicate-free permutations; arbitrary offline list traces are not covered by its strategy interface. Paging uses explicit valid states, history-dependent online policies, and separately validated offline schedules. These are abstract competitive cost models, not machine-runtime bounds.

See docs/clrs-fourth-edition-map.csv for the section-level mapping and docs/migrations/clrs4.md for compatibility and deprecation policy.

CLRS, fourth edition · Chapter 27 of 35