simple functional queue from Okasaki

Cslib.lean

@@ -1,7 +1,9 @@
 module  -- shake: keep-all --deprecated_module: ignore
 
+public import Cslib.Algorithms.Lean.FunctionalQueue.FunctionalQueue
 public import Cslib.Algorithms.Lean.MergeSort.MergeSort
 public import Cslib.Algorithms.Lean.TimeM
+public import Cslib.Algorithms.Lean.Amortized
 public import Cslib.Computability.Automata.Acceptors.Acceptor
 public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
 public import Cslib.Computability.Automata.DA.Basic

Cslib/Algorithms/Lean/Amortized.lean

@@ -0,0 +1,93 @@
+/-
+Copyright (c) 2026 Simon Cruanes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Simon Cruanes
+-/
+
+module
+
+import Cslib.Init
+import Mathlib
+public import Cslib.Algorithms.Lean.TimeM
+public import Mathlib.Algebra.Ring.Defs
+public import Mathlib.Order.Defs.PartialOrder
+public import Mathlib.Algebra.Order.Ring.Defs
+public import Mathlib.Algebra.Ring.Int.Defs
+public import Mathlib.Algebra.Order.Ring.Int
+
+/-!
+# Amortized cost analysis
+
+This complements `TimeM` in the cases where amortized costs are necessary.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.Lean.Amortized
+
+/-- Physicist method: a potential (lower bound on savings) defined on a
+    data structure.
+    [Okasaki, *Purely Functional Data Structures*, 1996][okasaki1996] -/
+class Potential (φ α : Type*) [CommRing φ] [LinearOrder φ] [IsStrictOrderedRing φ] where
+  /-- The potential, a representation of savings accumulated (just like
+      potential energy), to be released later. In some functional data
+      structures, amortized costs allow some operations to be more expensive
+      by "using" potential previously accumulated in cheaper operations. -/
+  potential : α → φ
+
+class Op α o where
+  applyOp : α → o → TimeM ℕ α
+
+@[simp] def applyOps {α o : Type*} [Op α o] (x : α) (ops : List o)
+    : TimeM ℕ α :=
+  List.foldlM (fun x op => Op.applyOp x op) x ops
+
+/-- Amortized cost with the physicist's method,
+    following Okasaki, chapter 5 -/
+def amortizedCost {α o φ : Type*}
+    [Op α o] [CommRing φ] [LinearOrder φ] [IsStrictOrderedRing φ] [Potential φ α]
+    (x : α) (op : o) : φ :=
+  Nat.cast (Op.applyOp x op).time
+    + Potential.potential (Op.applyOp x op).ret
+    - Potential.potential x
+
+/-- If each operation's cost is bounded by `k`, then the amortized
+  cost over a series of operations is bounded by `k * ops.length`. -/
+theorem constantAmortizedCostL {α o φ : Type*}
+    [CommRing φ] [LinearOrder φ] [IsStrictOrderedRing φ]
+    [h_op : Op α o] [h_pot : Potential φ α]
+    (k : φ) (h_bounded : ∀ (x : α) (op : o), amortizedCost x op ≤ k)
+    (x : α) (ops : List o)
+    : (applyOps x ops).time
+        + Potential.potential (applyOps x ops).ret - Potential.potential x
+      ≤ k * Nat.cast ops.length
+    := by
+  simp only [applyOps]
+  revert x
+  induction ops with
+  | nil =>
+    intro x
+    simp only [List.foldlM, TimeM.time_pure, CharP.cast_eq_zero,
+      TimeM.ret_pure, zero_add, sub_self,
+      List.length_nil, mul_zero, Std.le_refl]
+  | cons op ops2 h_ind =>
+    intro x
+    simp only [amortizedCost] at h_bounded
+    simp only [List.foldlM, TimeM.time_bind, Nat.cast_add, TimeM.ret_bind, List.length_cons,
+      Nat.cast_one]
+    have bound1 := h_bounded x op
+    have bound2 := h_ind (Op.applyOp x op).ret
+    set applyOpX := (Op.applyOp x op : TimeM ℕ α)
+    set applyOps2 := (List.foldlM (fun x op => Op.applyOp x op) (Op.applyOp x op).ret ops2)
+    set potX := (Potential.potential x : φ)
+    set potOpX := (Potential.potential applyOpX.ret : φ)
+    set potOps2 := (Potential.potential applyOps2.ret : φ)
+    /- have potOpXPos := (Potential.potentialNonNegative (φ := φ) applyOpX.ret) -/
+    ring_nf
+    have jfdoit := add_le_add bound1 bound2
+    ring_nf at jfdoit
+    linarith
+
+end Cslib.Algorithms.Lean.Amortized
+
+end

Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean

@@ -0,0 +1,256 @@
+/-
+Copyright (c) 2026 Simon Cruanes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Simon Cruanes
+-/
+
+module
+
+import Cslib.Init
+import Mathlib
+public import Mathlib.Algebra.Ring.Int.Defs
+public import Mathlib.Algebra.Order.Ring.Int
+public import Cslib.Algorithms.Lean.Amortized
+public import Cslib.Algorithms.Lean.TimeM
+
+/-!
+# Functional Queue
+
+A classic two-list queue with amortized O(1) `push` and `pop`.
+
+The representation uses two lists: a front list (for dequeue) and a back list
+(for enqueue). When the front list becomes empty, the back list is reversed
+and becomes the new front. This yields amortized O(1) operations.
+
+Cost model: each list cons is worth one `TimeM` tick.
+
+## References
+
+* [Okasaki, *Purely Functional Data Structures*, 1996][okasaki1996]
+-/
+
+set_option autoImplicit false
+
+namespace Cslib.Algorithms.Lean
+
+@[expose] public section
+
+universe u
+
+namespace Raw
+
+structure FunctionalQueue (α : Type u) where
+  front : List α
+  back : List α
+
+/-- Well-formedness: if front is empty, back must be empty too. -/
+def Invariant {α : Type u} (q : Raw.FunctionalQueue α) : Prop :=
+  q.front = [] → q.back = []
+
+/-- The logical contents of the queue: `front ++ back.reverse`. -/
+def toList {α : Type u} (q : FunctionalQueue α) : List α :=
+  q.front ++ q.back.reverse
+
+/-- The empty queue. -/
+def empty {α : Type u} : FunctionalQueue α := ⟨ [], [] ⟩
+
+/-- Internal: rebalance by moving `back.reverse` to `front` when `front` is empty. -/
+def rebalance {α : Type u} (q : FunctionalQueue α)
+    : TimeM ℕ (FunctionalQueue α) :=
+  match q.front with
+  | [] => do
+    TimeM.tick q.back.length
+    pure ⟨ (q.back).reverse, [] ⟩
+  | _ => pure q
+
+theorem rebalanceInvert {α : Type u} (q : FunctionalQueue α) :
+    (rebalance q).ret.front = [] → q = empty := by
+  intro h
+  obtain ⟨f, b⟩ := q
+  simp only [rebalance, Raw.empty] at h ⊢
+  split at h <;> simp_all
+
+theorem rebalanceInvariant {α : Type u} {q : FunctionalQueue α} :
+    Invariant (rebalance q).ret := by
+  obtain ⟨f, b⟩ := q
+  simp [rebalance, Invariant]
+  split <;> grind
+
+@[simp] theorem rebalanceIdempotent {α : Type u} (q : FunctionalQueue α) :
+    (rebalance (rebalance q).ret).ret = (rebalance q).ret := by
+  obtain ⟨f, b⟩ := q
+  simp [rebalance]
+  split <;> grind
+
+@[simp] theorem rebalancePreserveGhost {α : Type u} (q : FunctionalQueue α) :
+    toList (rebalance q).ret = toList q := by
+  obtain ⟨f, b⟩ := q
+  simp [rebalance, toList]
+  split <;> grind [List.reverse_append]
+
+/-- Enqueue an element. -/
+def push {α : Type u} (x : α) (q : FunctionalQueue α)
+    : TimeM ℕ (FunctionalQueue α) := do
+  TimeM.tick 1
+  rebalance ⟨ q.front, x :: q.back ⟩
+
+theorem Invariant.push {α : Type u} (x : α) (q : FunctionalQueue α)
+    : Invariant q → Invariant (push x q).ret := by
+  intro h
+  rw [Raw.push]
+  apply rebalanceInvariant
+
+theorem pushToList {α : Type u} (x : α) (q : Raw.FunctionalQueue α)
+    : toList (push x q).ret = toList q ++ [x] := by
+  rw [push]
+  simp only [TimeM.ret_bind, rebalancePreserveGhost]
+  rw [toList]
+  simp [toList, List.append_assoc]
+
+/-- Dequeue: returns `some (head, remaining)` or `none` if empty. -/
+def pop {α : Type u} (q : Raw.FunctionalQueue α)
+    : TimeM ℕ (Option (α × Raw.FunctionalQueue α)) :=
+  match q.front with
+  | [] => pure none
+  | x :: tl => do
+    let q2 ← rebalance ⟨ tl, q.back ⟩
+    pure (some (x, q2))
+
+theorem Invariant.pop {α : Type u} (x : α) (q q2 : FunctionalQueue α)
+    : Invariant q →
+      (pop q).ret = some (x, q2) →
+      Invariant q2 := by
+  intro hq hpop
+  obtain ⟨f, b⟩ := q
+  simp [Invariant] at hq
+  unfold Raw.pop at hpop
+  cases f with
+  | nil => simp at hpop
+  | cons y tl =>
+    simp only at hpop
+    obtain ⟨rfl, rfl⟩ := hpop
+    exact rebalanceInvariant
+
+@[simp] theorem Invariant.empty {α : Type u} : Invariant (@Raw.empty α) := by
+  simp [Invariant, Raw.empty]
+
+@[simp] theorem emptyToList {α : Type u} : toList (@Raw.empty α) = [] := by
+  simp [toList, Raw.empty]
+
+theorem popToList {α : Type u} {x : α} {q q2 : Raw.FunctionalQueue α}
+    : Invariant q →
+      (pop q).ret = some (x, q2) →
+      toList q = x :: toList q2 := by
+  intro hq hpop
+  obtain ⟨f, b⟩ := q
+  simp [Invariant] at hq
+  unfold pop at hpop
+  cases f with
+  | nil => simp at hpop
+  | cons y tl =>
+    simp only at hpop
+    obtain ⟨rfl, rfl⟩ := hpop
+    simp only [rebalancePreserveGhost]
+    simp [toList]
+
+end Raw
+
+namespace Complexity
+
+def potential {α : Type u} (q : Raw.FunctionalQueue α) : ℤ :=
+  q.back.length
+
+instance functionalQueuePotential {α : Type u}
+    : Amortized.Potential ℤ (Raw.FunctionalQueue α) :=
+  ⟨ potential ⟩
+
+inductive queueOp (α : Type u) where
+  | push : α → queueOp α
+  | pop
+
+def applyOp {α : Type u} (q : Raw.FunctionalQueue α) (op : queueOp α)
+    : TimeM ℕ (Raw.FunctionalQueue α) :=
+  match op with
+  | .push x => Raw.push x q
+  | .pop => do
+    match (← Raw.pop q) with
+    | none => pure q
+    | some (_, q2) => pure q2
+
+instance functionalQueueApplyOp {α : Type u}
+    : Amortized.Op (Raw.FunctionalQueue α) (queueOp α) :=
+  ⟨ applyOp ⟩
+
+theorem potentialEmptyIsZero {α : Type u}
+    : potential (@Raw.empty α) = 0 := by
+  simp [potential, Raw.empty]
+
+theorem amortizedCostQueueOp {α : Type u} (q : Raw.FunctionalQueue α) (op : queueOp α)
+    : Amortized.amortizedCost q op ≤ (2 : ℤ) := by
+  simp only [Amortized.amortizedCost, Amortized.Potential.potential, tsub_le_iff_right]
+  cases op with
+  | push x =>
+    simp only [Amortized.Op.applyOp, applyOp, potential]
+    cases h_front : q.front <;> (rw [Raw.push, Raw.rebalance, h_front] at ⊢; grind)
+  | pop =>
+    simp only [Amortized.Op.applyOp, applyOp, potential]
+    cases h_front : q.front <;> (rw [Raw.pop, h_front] at ⊢; grind [Raw.rebalance])
+
+/-- cost of applying operations to a queue -/
+theorem costQueueOps {α : Type u}
+    (q : Raw.FunctionalQueue α) (ops : List (queueOp α))
+    : (Amortized.applyOps q ops).time
+        + potential (Amortized.applyOps q ops).ret
+        - potential q
+      ≤ (2 : ℤ) * ops.length
+    := by
+  have useful
+    := Amortized.constantAmortizedCostL 2 amortizedCostQueueOp q ops
+  simp only [Amortized.Potential.potential]
+    at useful
+  grind only
+
+end Complexity
+
+/-- A functional queue with invariant. -/
+@[ext]
+structure FunctionalQueue (α : Type u) where
+  raw : Raw.FunctionalQueue α
+  inv : Raw.Invariant raw
+
+def empty {α : Type u} : FunctionalQueue α := ⟨ @Raw.empty α, Raw.Invariant.empty ⟩
+
+def push {α : Type u} (x : α) (q : FunctionalQueue α)
+    : TimeM ℕ (FunctionalQueue α) :=
+  let r := Raw.push x q.raw
+  ⟨ ⟨ r.ret, Raw.Invariant.push x q.raw q.inv ⟩, r.time ⟩
+
+def pop {α : Type u} (q : FunctionalQueue α)
+    : TimeM ℕ (Option (α × FunctionalQueue α)) :=
+  let r := Raw.pop q.raw
+  match h : r.ret with
+  | none => ⟨ none, r.time ⟩
+  | some (x, q2) =>
+    ⟨ some (x, ⟨ q2, Raw.Invariant.pop x q.raw q2 q.inv h ⟩), r.time ⟩
+
+/-- project to a list view, an ordered sequence of elements -/
+def toList {α : Type u} (q : FunctionalQueue α) : List α := Raw.toList q.raw
+
+theorem pushGhost {α : Type u} (x : α) (q : FunctionalQueue α) :
+    toList (push x q).ret = toList q ++ [x] :=
+  Raw.pushToList x q.raw
+
+theorem popGhost {α : Type u} {x : α} {q2 : FunctionalQueue α} :
+    ∀ {q : FunctionalQueue α},
+    (pop q).ret = some (x, q2) → toList q = x :: toList q2 := by
+  intro q h
+  simp only [pop, toList] at h ⊢
+  split at h
+  · simp only [reduceCtorEq] at h
+  · rename_i x2 q2' heq
+    obtain ⟨h1, h2⟩ := h
+    exact @Raw.popToList α x q.raw q2' q.inv heq
+
+end
+
+end Cslib.Algorithms.Lean

Cslib/Algorithms/Lean/TimeM.lean

@@ -85,7 +85,7 @@ instance [Add T] : SeqLeft (TimeM T) where
 instance [Add T] : SeqRight (TimeM T) where
   seqRight x y := ⟨(y ()).ret, x.time + (y ()).time⟩
 
-instance [AddZero T] : Monad (TimeM T) where
+instance [Add T] [Zero T] : Monad (TimeM T) where
   pure := Pure.pure
   bind := Bind.bind
   map := Functor.map