From 719a66720a552359acf37aca2eb83681a7ff42f8 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 8 May 2026 00:16:03 -0400
Subject: [PATCH 1/8] wip: basic functional queue in lean

---
 .../Lean/FunctionalQueue/FunctionalQueue.lean | 123 ++++++++++++++++++
 1 file changed, 123 insertions(+)
 create mode 100644 Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean

diff --git a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
new file mode 100644
index 000000000..c21c037ad
--- /dev/null
+++ b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
@@ -0,0 +1,123 @@
+
+
+module
+
+/- public import Cslib.Algorithms.Lean.TimeM -/
+
+/-!
+  The simplest functional queue. -/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.Lean
+
+universe u
+
+@[ext] structure RawFunctionalQueue (α : Type u) where
+  front : List α
+  back : List α
+
+@[simp] def invariant {α : Type u} (q : RawFunctionalQueue α) : Prop :=
+  q.front = [] → q.back = []
+
+@[simp] def ghostList {α : Type u} (q : RawFunctionalQueue α) : List α :=
+  List.append q.front q.back.reverse
+
+@[simp] def empty {α : Type u} : RawFunctionalQueue α := ⟨ [], [] ⟩
+
+@[simp] def rebalance {α : Type u} (q : RawFunctionalQueue α) : RawFunctionalQueue α :=
+  match q.front with
+  | [] => ⟨ (q.back).reverse, [] ⟩
+  | _ => q
+
+theorem rebalanceInvert {α : Type u} (q : RawFunctionalQueue α) : (rebalance q).front = [] → q = empty := by
+  intro h_reb
+  generalize gen_reb : (rebalance q).front = q_reb_hd
+  obtain ⟨ q_hd, q_tl ⟩ := q
+  simp; simp at h_reb
+  induction q_reb_hd with
+  | nil =>
+    induction q_hd with
+    | nil =>
+      simp at h_reb
+      grind only
+    | cons q_hd_hd q_hd_tl q_hd_hyp =>
+      grind only
+  | cons q_reb_hd_hd q_reb_hd_tl q_reb_hd_hyp =>
+    induction q_hd with
+    | nil =>
+      simp at h_reb
+      grind only
+    | cons _ _ _ =>
+      simp at h_reb
+
+theorem rebalanceInvariant {α : Type u} {q : RawFunctionalQueue α} : invariant (rebalance q) := by
+  generalize h_front : q.front = l
+  induction l with
+  | nil => simp; rw [h_front]; simp
+  | cons x tl h_cons =>
+    simp; rw [h_front]; simp; rw [h_front]; grind only
+
+@[simp] theorem rebalanceIdempotent {α : Type u} (q : RawFunctionalQueue α) : rebalance (rebalance q) = rebalance q := by
+  generalize h : (rebalance q).front = hd
+  induction hd with
+  | nil =>
+    have h_q_empty : q = empty := rebalanceInvert q h
+    rw [h_q_empty]
+    simp
+  | cons hd_hd hd_tl hd_hyp =>
+    generalize def_q2 : rebalance q = q2
+    rw [def_q2] at h
+    simp
+    rw [h]
+
+@[simp] theorem rebalancePreserveGhost {α : Type u} (q : RawFunctionalQueue α) : ghostList (rebalance q) = ghostList q := by
+  generalize def_hd : q.front = hd
+  induction hd with
+  | nil => simp; rw [def_hd]; simp
+  | cons hd_hd hd_tl h_ind =>
+    simp; rw [def_hd]; simp; grind only [=_ List.cons_append]
+
+@[simp] def push {α : Type u} (x : α) (q : RawFunctionalQueue α) : (RawFunctionalQueue α) :=
+  let q : RawFunctionalQueue α := ⟨ q.front, x :: q.back ⟩
+  rebalance q
+
+theorem appendInvariant {α : Type u} (x : α) (q : RawFunctionalQueue α)
+  : invariant q → invariant (push x q) := by
+  intro h
+  rw [push]
+  apply rebalanceInvariant
+
+theorem appendGhost {α : Type u} (x : α) (q : RawFunctionalQueue α) : ghostList (push x q) = ghostList q ++ [x] := by
+  generalize h_front : q.front = l
+  cases l with
+  | nil =>
+    simp; rw [h_front]; simp
+  | cons l_hd l_tl =>
+    rw [push]
+    rw [rebalancePreserveGhost]
+    rw [ghostList]
+    simp
+
+def pop {α : Type} (q : RawFunctionalQueue α) : Option (α × RawFunctionalQueue α) :=
+  match q.front with
+  | [] => none
+  | x :: tl =>
+    some (x, rebalance ⟨ tl, q.back ⟩)
+
+theorem pop_invariant {α : Type} (x : α) (q q2 : RawFunctionalQueue α) :
+    invariant q → pop q = some (x, q2) → invariant q2 := by
+  intro hq hpop_is_some
+  simp at hq
+  rw [pop] at hpop_is_some
+  generalize h_front : q.front = l
+  cases l with
+  | nil =>
+    rw [h_front] at hpop_is_some; simp at hpop_is_some
+  | cons _ _ =>
+    rw [h_front] at hpop_is_some
+    simp only at hpop_is_some
+    obtain ⟨ rfl, rfl ⟩ := hpop_is_some
+    apply rebalanceInvariant
+
+end Cslib.Algorithms.Lean

From 88bd163102a0c4d0df838a33672d5deee1706a17 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 8 May 2026 21:58:50 -0400
Subject: [PATCH 2/8] remove @[simp] from some defs

---
 .../Lean/FunctionalQueue/FunctionalQueue.lean | 33 +++++++++----------
 1 file changed, 16 insertions(+), 17 deletions(-)

diff --git a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
index c21c037ad..cceb8d8dc 100644
--- a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
+++ b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
@@ -23,24 +23,24 @@ universe u
 @[simp] def ghostList {α : Type u} (q : RawFunctionalQueue α) : List α :=
   List.append q.front q.back.reverse
 
-@[simp] def empty {α : Type u} : RawFunctionalQueue α := ⟨ [], [] ⟩
+def empty {α : Type u} : RawFunctionalQueue α := ⟨ [], [] ⟩
 
-@[simp] def rebalance {α : Type u} (q : RawFunctionalQueue α) : RawFunctionalQueue α :=
+def rebalance {α : Type u} (q : RawFunctionalQueue α) : RawFunctionalQueue α :=
   match q.front with
   | [] => ⟨ (q.back).reverse, [] ⟩
   | _ => q
 
 theorem rebalanceInvert {α : Type u} (q : RawFunctionalQueue α) : (rebalance q).front = [] → q = empty := by
   intro h_reb
+  rw [empty]
   generalize gen_reb : (rebalance q).front = q_reb_hd
   obtain ⟨ q_hd, q_tl ⟩ := q
-  simp; simp at h_reb
+  simp [rebalance] at h_reb
   induction q_reb_hd with
   | nil =>
     induction q_hd with
     | nil =>
-      simp at h_reb
-      grind only
+      simp at h_reb; simp [rebalance] at gen_reb; rw [h_reb]
     | cons q_hd_hd q_hd_tl q_hd_hyp =>
       grind only
   | cons q_reb_hd_hd q_reb_hd_tl q_reb_hd_hyp =>
@@ -51,34 +51,33 @@ theorem rebalanceInvert {α : Type u} (q : RawFunctionalQueue α) : (rebalance q
     | cons _ _ _ =>
       simp at h_reb
 
-theorem rebalanceInvariant {α : Type u} {q : RawFunctionalQueue α} : invariant (rebalance q) := by
+@[simp] theorem rebalanceInvariant {α : Type u} {q : RawFunctionalQueue α} : invariant (rebalance q) := by
   generalize h_front : q.front = l
   induction l with
-  | nil => simp; rw [h_front]; simp
+  | nil => simp [rebalance]; rw [h_front]; simp
   | cons x tl h_cons =>
-    simp; rw [h_front]; simp; rw [h_front]; grind only
+    simp [rebalance]; rw [h_front]; simp; rw [h_front]; grind only
 
 @[simp] theorem rebalanceIdempotent {α : Type u} (q : RawFunctionalQueue α) : rebalance (rebalance q) = rebalance q := by
   generalize h : (rebalance q).front = hd
   induction hd with
   | nil =>
     have h_q_empty : q = empty := rebalanceInvert q h
-    rw [h_q_empty]
-    simp
+    simp [rebalance]; rw [h_q_empty]; simp [empty]
   | cons hd_hd hd_tl hd_hyp =>
     generalize def_q2 : rebalance q = q2
     rw [def_q2] at h
-    simp
+    simp [rebalance]
     rw [h]
 
 @[simp] theorem rebalancePreserveGhost {α : Type u} (q : RawFunctionalQueue α) : ghostList (rebalance q) = ghostList q := by
   generalize def_hd : q.front = hd
   induction hd with
-  | nil => simp; rw [def_hd]; simp
+  | nil => simp [rebalance]; rw [def_hd]; simp
   | cons hd_hd hd_tl h_ind =>
-    simp; rw [def_hd]; simp; grind only [=_ List.cons_append]
+    simp [rebalance]; rw [def_hd]; simp; grind only [=_ List.cons_append]
 
-@[simp] def push {α : Type u} (x : α) (q : RawFunctionalQueue α) : (RawFunctionalQueue α) :=
+def push {α : Type u} (x : α) (q : RawFunctionalQueue α) : (RawFunctionalQueue α) :=
   let q : RawFunctionalQueue α := ⟨ q.front, x :: q.back ⟩
   rebalance q
 
@@ -92,20 +91,20 @@ theorem appendGhost {α : Type u} (x : α) (q : RawFunctionalQueue α) : ghostLi
   generalize h_front : q.front = l
   cases l with
   | nil =>
-    simp; rw [h_front]; simp
+    simp [push, rebalance]; rw [h_front]; simp
   | cons l_hd l_tl =>
     rw [push]
     rw [rebalancePreserveGhost]
     rw [ghostList]
     simp
 
-def pop {α : Type} (q : RawFunctionalQueue α) : Option (α × RawFunctionalQueue α) :=
+def pop {α : Type u} (q : RawFunctionalQueue α) : Option (α × RawFunctionalQueue α) :=
   match q.front with
   | [] => none
   | x :: tl =>
     some (x, rebalance ⟨ tl, q.back ⟩)
 
-theorem pop_invariant {α : Type} (x : α) (q q2 : RawFunctionalQueue α) :
+theorem pop_invariant {α : Type u} (x : α) (q q2 : RawFunctionalQueue α) :
     invariant q → pop q = some (x, q2) → invariant q2 := by
   intro hq hpop_is_some
   simp at hq

From ebe0603575e4ab00612f41b8472f3b49845d5ef1 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 8 May 2026 22:37:58 -0400
Subject: [PATCH 3/8] simplify proofs and cleanup

---
 Cslib.lean                                    |   1 +
 .../Lean/FunctionalQueue/FunctionalQueue.lean | 164 +++++++++---------
 2 files changed, 85 insertions(+), 80 deletions(-)

diff --git a/Cslib.lean b/Cslib.lean
index 92a251cdf..9cf0abfc0 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -1,5 +1,6 @@
 module  -- shake: keep-all
 
+public import Cslib.Algorithms.Lean.FunctionalQueue.FunctionalQueue
 public import Cslib.Algorithms.Lean.MergeSort.MergeSort
 public import Cslib.Algorithms.Lean.TimeM
 public import Cslib.Computability.Automata.Acceptors.Acceptor
diff --git a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
index cceb8d8dc..c51a63deb 100644
--- a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
+++ b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
@@ -1,14 +1,23 @@
-
+/-
+Copyright (c) 2026 Simon Cruanes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Simon Cruanes
+-/
 
 module
 
-/- public import Cslib.Algorithms.Lean.TimeM -/
+import Cslib.Init
 
 /-!
-  The simplest functional queue. -/
+# Functional Queue
+
+A classic two-list queue with amortized O(1) `push` and `pop`.
+-/
 
 @[expose] public section
 
+set_option autoImplicit false
+
 namespace Cslib.Algorithms.Lean
 
 universe u
@@ -17,87 +26,64 @@ universe u
   front : List α
   back : List α
 
-@[simp] def invariant {α : Type u} (q : RawFunctionalQueue α) : Prop :=
+/-- Well-formedness: if front is empty, back must be empty too. -/
+def invariant {α : Type u} (q : RawFunctionalQueue α) : Prop :=
   q.front = [] → q.back = []
 
-@[simp] def ghostList {α : Type u} (q : RawFunctionalQueue α) : List α :=
+/-- The logical contents of the queue: `front ++ back.reverse`. -/
+def ghostList {α : Type u} (q : RawFunctionalQueue α) : List α :=
   List.append q.front q.back.reverse
 
+/-- The empty queue. -/
 def empty {α : Type u} : RawFunctionalQueue α := ⟨ [], [] ⟩
 
+/-- Internal: rebalance by moving `back.reverse` to `front` when `front` is empty. -/
 def rebalance {α : Type u} (q : RawFunctionalQueue α) : RawFunctionalQueue α :=
   match q.front with
   | [] => ⟨ (q.back).reverse, [] ⟩
   | _ => q
 
-theorem rebalanceInvert {α : Type u} (q : RawFunctionalQueue α) : (rebalance q).front = [] → q = empty := by
-  intro h_reb
-  rw [empty]
-  generalize gen_reb : (rebalance q).front = q_reb_hd
-  obtain ⟨ q_hd, q_tl ⟩ := q
-  simp [rebalance] at h_reb
-  induction q_reb_hd with
-  | nil =>
-    induction q_hd with
-    | nil =>
-      simp at h_reb; simp [rebalance] at gen_reb; rw [h_reb]
-    | cons q_hd_hd q_hd_tl q_hd_hyp =>
-      grind only
-  | cons q_reb_hd_hd q_reb_hd_tl q_reb_hd_hyp =>
-    induction q_hd with
-    | nil =>
-      simp at h_reb
-      grind only
-    | cons _ _ _ =>
-      simp at h_reb
-
-@[simp] theorem rebalanceInvariant {α : Type u} {q : RawFunctionalQueue α} : invariant (rebalance q) := by
-  generalize h_front : q.front = l
-  induction l with
-  | nil => simp [rebalance]; rw [h_front]; simp
-  | cons x tl h_cons =>
-    simp [rebalance]; rw [h_front]; simp; rw [h_front]; grind only
-
-@[simp] theorem rebalanceIdempotent {α : Type u} (q : RawFunctionalQueue α) : rebalance (rebalance q) = rebalance q := by
-  generalize h : (rebalance q).front = hd
-  induction hd with
-  | nil =>
-    have h_q_empty : q = empty := rebalanceInvert q h
-    simp [rebalance]; rw [h_q_empty]; simp [empty]
-  | cons hd_hd hd_tl hd_hyp =>
-    generalize def_q2 : rebalance q = q2
-    rw [def_q2] at h
-    simp [rebalance]
-    rw [h]
-
-@[simp] theorem rebalancePreserveGhost {α : Type u} (q : RawFunctionalQueue α) : ghostList (rebalance q) = ghostList q := by
-  generalize def_hd : q.front = hd
-  induction hd with
-  | nil => simp [rebalance]; rw [def_hd]; simp
-  | cons hd_hd hd_tl h_ind =>
-    simp [rebalance]; rw [def_hd]; simp; grind only [=_ List.cons_append]
-
-def push {α : Type u} (x : α) (q : RawFunctionalQueue α) : (RawFunctionalQueue α) :=
-  let q : RawFunctionalQueue α := ⟨ q.front, x :: q.back ⟩
-  rebalance q
-
-theorem appendInvariant {α : Type u} (x : α) (q : RawFunctionalQueue α)
-  : invariant q → invariant (push x q) := by
+theorem rebalanceInvert {α : Type u} (q : RawFunctionalQueue α) :
+    (rebalance q).front = [] → q = empty := by
+  intro h
+  obtain ⟨f, b⟩ := q
+  simp only [rebalance, empty] at h ⊢
+  split at h <;> simp_all
+
+theorem rebalanceInvariant {α : Type u} {q : RawFunctionalQueue α} :
+    invariant (rebalance q) := by
+  obtain ⟨f, b⟩ := q
+  simp [rebalance, invariant]
+  split <;> grind
+
+@[simp] theorem rebalanceIdempotent {α : Type u} (q : RawFunctionalQueue α) :
+    rebalance (rebalance q) = rebalance q := by
+  obtain ⟨f, b⟩ := q
+  simp [rebalance]
+  split <;> grind
+
+@[simp] theorem rebalancePreserveGhost {α : Type u} (q : RawFunctionalQueue α) :
+    ghostList (rebalance q) = ghostList q := by
+  obtain ⟨f, b⟩ := q
+  simp [rebalance, ghostList]
+  split <;> grind [List.reverse_append]
+
+/-- Enqueue an element. -/
+def push {α : Type u} (x : α) (q : RawFunctionalQueue α) : RawFunctionalQueue α :=
+  rebalance ⟨ q.front, x :: q.back ⟩
+
+theorem pushInvariant {α : Type u} (x : α) (q : RawFunctionalQueue α) :
+    invariant q → invariant (push x q) := by
   intro h
   rw [push]
   apply rebalanceInvariant
 
-theorem appendGhost {α : Type u} (x : α) (q : RawFunctionalQueue α) : ghostList (push x q) = ghostList q ++ [x] := by
-  generalize h_front : q.front = l
-  cases l with
-  | nil =>
-    simp [push, rebalance]; rw [h_front]; simp
-  | cons l_hd l_tl =>
-    rw [push]
-    rw [rebalancePreserveGhost]
-    rw [ghostList]
-    simp
+theorem pushGhost {α : Type u} (x : α) (q : RawFunctionalQueue α) :
+    ghostList (push x q) = ghostList q ++ [x] := by
+  rw [push, rebalancePreserveGhost, ghostList]
+  simp [ghostList, List.append_assoc]
 
+/-- Dequeue: returns `some (head, remaining)` or `none` if empty. -/
 def pop {α : Type u} (q : RawFunctionalQueue α) : Option (α × RawFunctionalQueue α) :=
   match q.front with
   | [] => none
@@ -106,17 +92,35 @@ def pop {α : Type u} (q : RawFunctionalQueue α) : Option (α × RawFunctionalQ
 
 theorem pop_invariant {α : Type u} (x : α) (q q2 : RawFunctionalQueue α) :
     invariant q → pop q = some (x, q2) → invariant q2 := by
-  intro hq hpop_is_some
-  simp at hq
-  rw [pop] at hpop_is_some
-  generalize h_front : q.front = l
-  cases l with
-  | nil =>
-    rw [h_front] at hpop_is_some; simp at hpop_is_some
-  | cons _ _ =>
-    rw [h_front] at hpop_is_some
-    simp only at hpop_is_some
-    obtain ⟨ rfl, rfl ⟩ := hpop_is_some
-    apply rebalanceInvariant
+  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
+    exact rebalanceInvariant
+
+@[simp] theorem emptyInvariant {α : Type u} : invariant (@empty α) := by
+  simp [invariant, empty]
+
+@[simp] theorem emptyGhost {α : Type u} : ghostList (@empty α) = [] := by
+  simp [ghostList, empty]
+
+theorem pop_ghost {α : Type u} {x : α} {q q2 : RawFunctionalQueue α} :
+    invariant q → pop q = some (x, q2) → ghostList q = x :: ghostList 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 [ghostList]
 
 end Cslib.Algorithms.Lean

From 0f1a4d6c628b807fa67ba5d01fbb1f049ee6dccc Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 8 May 2026 23:18:25 -0400
Subject: [PATCH 4/8] define queue with invariant

---
 .../Lean/FunctionalQueue/FunctionalQueue.lean | 74 ++++++++++++++-----
 1 file changed, 55 insertions(+), 19 deletions(-)

diff --git a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
index c51a63deb..b0eb395e8 100644
--- a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
+++ b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
@@ -26,6 +26,8 @@ universe u
   front : List α
   back : List α
 
+namespace Raw
+
 /-- Well-formedness: if front is empty, back must be empty too. -/
 def invariant {α : Type u} (q : RawFunctionalQueue α) : Prop :=
   q.front = [] → q.back = []
@@ -35,7 +37,7 @@ def ghostList {α : Type u} (q : RawFunctionalQueue α) : List α :=
   List.append q.front q.back.reverse
 
 /-- The empty queue. -/
-def empty {α : Type u} : RawFunctionalQueue α := ⟨ [], [] ⟩
+def emptyRaw {α : Type u} : RawFunctionalQueue α := ⟨ [], [] ⟩
 
 /-- Internal: rebalance by moving `back.reverse` to `front` when `front` is empty. -/
 def rebalance {α : Type u} (q : RawFunctionalQueue α) : RawFunctionalQueue α :=
@@ -44,10 +46,10 @@ def rebalance {α : Type u} (q : RawFunctionalQueue α) : RawFunctionalQueue α
   | _ => q
 
 theorem rebalanceInvert {α : Type u} (q : RawFunctionalQueue α) :
-    (rebalance q).front = [] → q = empty := by
+    (rebalance q).front = [] → q = emptyRaw := by
   intro h
   obtain ⟨f, b⟩ := q
-  simp only [rebalance, empty] at h ⊢
+  simp only [rebalance, emptyRaw] at h ⊢
   split at h <;> simp_all
 
 theorem rebalanceInvariant {α : Type u} {q : RawFunctionalQueue α} :
@@ -69,33 +71,33 @@ theorem rebalanceInvariant {α : Type u} {q : RawFunctionalQueue α} :
   split <;> grind [List.reverse_append]
 
 /-- Enqueue an element. -/
-def push {α : Type u} (x : α) (q : RawFunctionalQueue α) : RawFunctionalQueue α :=
+def pushRaw {α : Type u} (x : α) (q : RawFunctionalQueue α) : RawFunctionalQueue α :=
   rebalance ⟨ q.front, x :: q.back ⟩
 
 theorem pushInvariant {α : Type u} (x : α) (q : RawFunctionalQueue α) :
-    invariant q → invariant (push x q) := by
+    invariant q → invariant (pushRaw x q) := by
   intro h
-  rw [push]
+  rw [pushRaw]
   apply rebalanceInvariant
 
 theorem pushGhost {α : Type u} (x : α) (q : RawFunctionalQueue α) :
-    ghostList (push x q) = ghostList q ++ [x] := by
-  rw [push, rebalancePreserveGhost, ghostList]
+    ghostList (pushRaw x q) = ghostList q ++ [x] := by
+  rw [pushRaw, rebalancePreserveGhost, ghostList]
   simp [ghostList, List.append_assoc]
 
 /-- Dequeue: returns `some (head, remaining)` or `none` if empty. -/
-def pop {α : Type u} (q : RawFunctionalQueue α) : Option (α × RawFunctionalQueue α) :=
+def popRaw {α : Type u} (q : RawFunctionalQueue α) : Option (α × RawFunctionalQueue α) :=
   match q.front with
   | [] => none
   | x :: tl =>
     some (x, rebalance ⟨ tl, q.back ⟩)
 
-theorem pop_invariant {α : Type u} (x : α) (q q2 : RawFunctionalQueue α) :
-    invariant q → pop q = some (x, q2) → invariant q2 := by
+theorem popInvariant {α : Type u} (x : α) (q q2 : RawFunctionalQueue α) :
+    invariant q → popRaw q = some (x, q2) → invariant q2 := by
   intro hq hpop
   obtain ⟨f, b⟩ := q
   simp [invariant] at hq
-  unfold pop at hpop
+  unfold popRaw at hpop
   cases f with
   | nil => simp at hpop
   | cons y tl =>
@@ -103,18 +105,18 @@ theorem pop_invariant {α : Type u} (x : α) (q q2 : RawFunctionalQueue α) :
     obtain ⟨rfl, rfl⟩ := hpop
     exact rebalanceInvariant
 
-@[simp] theorem emptyInvariant {α : Type u} : invariant (@empty α) := by
-  simp [invariant, empty]
+@[simp] theorem emptyInvariant {α : Type u} : invariant (@emptyRaw α) := by
+  simp [invariant, emptyRaw]
 
-@[simp] theorem emptyGhost {α : Type u} : ghostList (@empty α) = [] := by
-  simp [ghostList, empty]
+@[simp] theorem emptyGhost {α : Type u} : ghostList (@emptyRaw α) = [] := by
+  simp [ghostList, emptyRaw]
 
-theorem pop_ghost {α : Type u} {x : α} {q q2 : RawFunctionalQueue α} :
-    invariant q → pop q = some (x, q2) → ghostList q = x :: ghostList q2 := by
+theorem popGhost {α : Type u} {x : α} {q q2 : RawFunctionalQueue α} :
+    invariant q → popRaw q = some (x, q2) → ghostList q = x :: ghostList q2 := by
   intro hq hpop
   obtain ⟨f, b⟩ := q
   simp [invariant] at hq
-  unfold pop at hpop
+  unfold popRaw at hpop
   cases f with
   | nil => simp at hpop
   | cons y tl =>
@@ -123,4 +125,38 @@ theorem pop_ghost {α : Type u} {x : α} {q q2 : RawFunctionalQueue α} :
     simp only [rebalancePreserveGhost]
     simp [ghostList]
 
+end Raw
+
+/-- A functional queue with invariant. -/
+structure FunctionalQueue (α : Type u) where
+  q : RawFunctionalQueue α
+  inv : Raw.invariant q
+
+def empty {α : Type u} : FunctionalQueue α := ⟨ @Raw.emptyRaw α, Raw.emptyInvariant ⟩
+
+def push {α : Type u} (x : α) (q : FunctionalQueue α) : FunctionalQueue α :=
+  ⟨ Raw.pushRaw x q.q, Raw.pushInvariant x q.q q.inv ⟩
+
+def pop {α : Type u} (q : FunctionalQueue α) : Option (α × FunctionalQueue α) :=
+  match h : Raw.popRaw q.q with
+  | none => none
+  | some (x, q2) =>
+    some (x, ⟨ q2, Raw.popInvariant x q.q q2 q.inv h ⟩)
+
+@[simp] def ghostList {α : Type u} (q : FunctionalQueue α) : List α := Raw.ghostList q.q
+
+theorem pushGhost {α : Type u} (x : α) (q : FunctionalQueue α) :
+    ghostList (push x q) = ghostList q ++ [x] :=
+  Raw.pushGhost x q.q
+
+theorem popGhost {α : Type u} {x : α} {q q2 : FunctionalQueue α} :
+    pop q = some (x, q2) → ghostList q = x :: ghostList q2 := by
+  intro h
+  simp only [pop, ghostList] at h ⊢
+  split at h
+  · simp only [reduceCtorEq] at h
+  · rename_i x2 q2' heq
+    obtain ⟨ h1, h2 ⟩ := h
+    apply @Raw.popGhost α x q.q q2' q.inv; grind
+
 end Cslib.Algorithms.Lean

From 47549d1980e05c844fd562ee1bf96c4c3a269e06 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 8 May 2026 23:36:13 -0400
Subject: [PATCH 5/8] add Raw namespace

---
 .../Lean/FunctionalQueue/FunctionalQueue.lean | 58 ++++++++++---------
 1 file changed, 30 insertions(+), 28 deletions(-)

diff --git a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
index b0eb395e8..db2f31f78 100644
--- a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
+++ b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
@@ -22,7 +22,7 @@ namespace Cslib.Algorithms.Lean
 
 universe u
 
-@[ext] structure RawFunctionalQueue (α : Type u) where
+structure RawFunctionalQueue (α : Type u) where
   front : List α
   back : List α
 
@@ -37,7 +37,7 @@ def ghostList {α : Type u} (q : RawFunctionalQueue α) : List α :=
   List.append q.front q.back.reverse
 
 /-- The empty queue. -/
-def emptyRaw {α : Type u} : RawFunctionalQueue α := ⟨ [], [] ⟩
+def empty {α : Type u} : RawFunctionalQueue α := ⟨ [], [] ⟩
 
 /-- Internal: rebalance by moving `back.reverse` to `front` when `front` is empty. -/
 def rebalance {α : Type u} (q : RawFunctionalQueue α) : RawFunctionalQueue α :=
@@ -46,10 +46,10 @@ def rebalance {α : Type u} (q : RawFunctionalQueue α) : RawFunctionalQueue α
   | _ => q
 
 theorem rebalanceInvert {α : Type u} (q : RawFunctionalQueue α) :
-    (rebalance q).front = [] → q = emptyRaw := by
+    (rebalance q).front = [] → q = Raw.empty := by
   intro h
   obtain ⟨f, b⟩ := q
-  simp only [rebalance, emptyRaw] at h ⊢
+  simp only [rebalance, Raw.empty] at h ⊢
   split at h <;> simp_all
 
 theorem rebalanceInvariant {α : Type u} {q : RawFunctionalQueue α} :
@@ -71,33 +71,33 @@ theorem rebalanceInvariant {α : Type u} {q : RawFunctionalQueue α} :
   split <;> grind [List.reverse_append]
 
 /-- Enqueue an element. -/
-def pushRaw {α : Type u} (x : α) (q : RawFunctionalQueue α) : RawFunctionalQueue α :=
+def push {α : Type u} (x : α) (q : RawFunctionalQueue α) : RawFunctionalQueue α :=
   rebalance ⟨ q.front, x :: q.back ⟩
 
 theorem pushInvariant {α : Type u} (x : α) (q : RawFunctionalQueue α) :
-    invariant q → invariant (pushRaw x q) := by
+    invariant q → invariant (push x q) := by
   intro h
-  rw [pushRaw]
+  rw [push]
   apply rebalanceInvariant
 
 theorem pushGhost {α : Type u} (x : α) (q : RawFunctionalQueue α) :
-    ghostList (pushRaw x q) = ghostList q ++ [x] := by
-  rw [pushRaw, rebalancePreserveGhost, ghostList]
+    ghostList (push x q) = ghostList q ++ [x] := by
+  rw [push, rebalancePreserveGhost, ghostList]
   simp [ghostList, List.append_assoc]
 
 /-- Dequeue: returns `some (head, remaining)` or `none` if empty. -/
-def popRaw {α : Type u} (q : RawFunctionalQueue α) : Option (α × RawFunctionalQueue α) :=
+def pop {α : Type u} (q : RawFunctionalQueue α) : Option (α × RawFunctionalQueue α) :=
   match q.front with
   | [] => none
   | x :: tl =>
     some (x, rebalance ⟨ tl, q.back ⟩)
 
 theorem popInvariant {α : Type u} (x : α) (q q2 : RawFunctionalQueue α) :
-    invariant q → popRaw q = some (x, q2) → invariant q2 := by
+    invariant q → pop q = some (x, q2) → invariant q2 := by
   intro hq hpop
   obtain ⟨f, b⟩ := q
   simp [invariant] at hq
-  unfold popRaw at hpop
+  unfold pop at hpop
   cases f with
   | nil => simp at hpop
   | cons y tl =>
@@ -105,18 +105,18 @@ theorem popInvariant {α : Type u} (x : α) (q q2 : RawFunctionalQueue α) :
     obtain ⟨rfl, rfl⟩ := hpop
     exact rebalanceInvariant
 
-@[simp] theorem emptyInvariant {α : Type u} : invariant (@emptyRaw α) := by
-  simp [invariant, emptyRaw]
+@[simp] theorem emptyInvariant {α : Type u} : invariant (@Raw.empty α) := by
+  simp [invariant, Raw.empty]
 
-@[simp] theorem emptyGhost {α : Type u} : ghostList (@emptyRaw α) = [] := by
-  simp [ghostList, emptyRaw]
+@[simp] theorem emptyGhost {α : Type u} : ghostList (@Raw.empty α) = [] := by
+  simp [ghostList, Raw.empty]
 
 theorem popGhost {α : Type u} {x : α} {q q2 : RawFunctionalQueue α} :
-    invariant q → popRaw q = some (x, q2) → ghostList q = x :: ghostList q2 := by
+    invariant q → pop q = some (x, q2) → ghostList q = x :: ghostList q2 := by
   intro hq hpop
   obtain ⟨f, b⟩ := q
   simp [invariant] at hq
-  unfold popRaw at hpop
+  unfold pop at hpop
   cases f with
   | nil => simp at hpop
   | cons y tl =>
@@ -128,26 +128,28 @@ theorem popGhost {α : Type u} {x : α} {q q2 : RawFunctionalQueue α} :
 end Raw
 
 /-- A functional queue with invariant. -/
+@[ext]
 structure FunctionalQueue (α : Type u) where
-  q : RawFunctionalQueue α
-  inv : Raw.invariant q
+  raw : RawFunctionalQueue α
+  inv : Raw.invariant raw
 
-def empty {α : Type u} : FunctionalQueue α := ⟨ @Raw.emptyRaw α, Raw.emptyInvariant ⟩
+def empty {α : Type u} : FunctionalQueue α := ⟨ @Raw.empty α, Raw.emptyInvariant ⟩
 
 def push {α : Type u} (x : α) (q : FunctionalQueue α) : FunctionalQueue α :=
-  ⟨ Raw.pushRaw x q.q, Raw.pushInvariant x q.q q.inv ⟩
+  ⟨ Raw.push x q.raw, Raw.pushInvariant x q.raw q.inv ⟩
 
 def pop {α : Type u} (q : FunctionalQueue α) : Option (α × FunctionalQueue α) :=
-  match h : Raw.popRaw q.q with
+  match h : Raw.pop q.raw with
   | none => none
   | some (x, q2) =>
-    some (x, ⟨ q2, Raw.popInvariant x q.q q2 q.inv h ⟩)
+    some (x, ⟨ q2, Raw.popInvariant x q.raw q2 q.inv h ⟩)
 
-@[simp] def ghostList {α : Type u} (q : FunctionalQueue α) : List α := Raw.ghostList q.q
+/-- project to a list view, an ordered sequence of elements -/
+def ghostList {α : Type u} (q : FunctionalQueue α) : List α := Raw.ghostList q.raw
 
 theorem pushGhost {α : Type u} (x : α) (q : FunctionalQueue α) :
     ghostList (push x q) = ghostList q ++ [x] :=
-  Raw.pushGhost x q.q
+  Raw.pushGhost x q.raw
 
 theorem popGhost {α : Type u} {x : α} {q q2 : FunctionalQueue α} :
     pop q = some (x, q2) → ghostList q = x :: ghostList q2 := by
@@ -156,7 +158,7 @@ theorem popGhost {α : Type u} {x : α} {q q2 : FunctionalQueue α} :
   split at h
   · simp only [reduceCtorEq] at h
   · rename_i x2 q2' heq
-    obtain ⟨ h1, h2 ⟩ := h
-    apply @Raw.popGhost α x q.q q2' q.inv; grind
+    obtain ⟨h1, h2⟩ := h
+    exact @Raw.popGhost α x q.raw q2' q.inv heq
 
 end Cslib.Algorithms.Lean

From a9def5302e82329118414205a0fec46bb3107d6d Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sat, 9 May 2026 22:14:15 -0400
Subject: [PATCH 6/8] wip: amortized analysis

---
 Cslib.lean                                    |  1 +
 Cslib/Algorithms/Lean/Amortized.lean          | 31 ++++++++++++
 .../Lean/FunctionalQueue/FunctionalQueue.lean | 48 ++++++++++++++++++-
 3 files changed, 78 insertions(+), 2 deletions(-)
 create mode 100644 Cslib/Algorithms/Lean/Amortized.lean

diff --git a/Cslib.lean b/Cslib.lean
index 9cf0abfc0..8b1715b2d 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -3,6 +3,7 @@ module  -- shake: keep-all
 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
diff --git a/Cslib/Algorithms/Lean/Amortized.lean b/Cslib/Algorithms/Lean/Amortized.lean
new file mode 100644
index 000000000..7d111cdcc
--- /dev/null
+++ b/Cslib/Algorithms/Lean/Amortized.lean
@@ -0,0 +1,31 @@
+
+/-
+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
+
+/-!
+# 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 -/
+class Potential α where
+  /-- non-negative potential. Initial potential should be 0.
+      [Okasaki, *Purely Functional Data Structures*, 1996][okasaki1996] -/
+  potential : α → Nat
+
+end Cslib.Algorithms.Lean.Amortized
+
+end
diff --git a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
index db2f31f78..fc3284420 100644
--- a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
+++ b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
@@ -7,19 +7,28 @@ Authors: Simon Cruanes
 module
 
 import Cslib.Init
+public import Cslib.Algorithms.Lean.Amortized
 
 /-!
 # Functional Queue
 
 A classic two-list queue with amortized O(1) `push` and `pop`.
--/
 
-@[expose] public section
+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.
+
+## References
+
+* [Okasaki, *Purely Functional Data Structures*, 1996][okasaki1996]
+-/
 
 set_option autoImplicit false
 
 namespace Cslib.Algorithms.Lean
 
+@[expose] public section
+
 universe u
 
 structure RawFunctionalQueue (α : Type u) where
@@ -127,6 +136,39 @@ theorem popGhost {α : Type u} {x : α} {q q2 : RawFunctionalQueue α} :
 
 end Raw
 
+namespace Complexity
+
+def potential {α : Type u} (q : RawFunctionalQueue α) : Nat :=
+  q.back.length
+
+instance functionalQueuePotential {α : Type u}
+    : Amortized.Potential (RawFunctionalQueue α) :=
+  ⟨ potential ⟩
+
+inductive queueOp (α : Type u) where
+  | push : α → queueOp α
+  | pop
+
+def applyOp {α : Type u} (op : queueOp α) (q : RawFunctionalQueue α) : RawFunctionalQueue α :=
+  match op with
+  | .push x => Raw.push x q
+  | .pop =>
+    match Raw.pop q with
+    | none => q
+    | some (_, q2) => q2
+
+def applyOps {α : Type u} (ops : List (queueOp α)) (q : RawFunctionalQueue α)
+    : RawFunctionalQueue α :=
+  ops.foldl (fun q op => applyOp op q) q
+
+theorem constantTimeAmortized {α : Type u} :
+    ∀ (q : RawFunctionalQueue α) (ops:List (queueOp α)),
+    false
+ := by
+   sorry
+
+end Complexity
+
 /-- A functional queue with invariant. -/
 @[ext]
 structure FunctionalQueue (α : Type u) where
@@ -161,4 +203,6 @@ theorem popGhost {α : Type u} {x : α} {q q2 : FunctionalQueue α} :
     obtain ⟨h1, h2⟩ := h
     exact @Raw.popGhost α x q.raw q2' q.inv heq
 
+end
+
 end Cslib.Algorithms.Lean

From b93816b64f7e2e5bc753b213f87fcc9b780870f7 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sun, 10 May 2026 00:14:34 -0400
Subject: [PATCH 7/8] wip: define physicist method in Amortized.lean, start
 using it for the queue

---
 Cslib/Algorithms/Lean/Amortized.lean          |  14 +-
 .../Lean/FunctionalQueue/FunctionalQueue.lean | 169 ++++++++++++------
 Cslib/Algorithms/Lean/TimeM.lean              |   2 +-
 3 files changed, 126 insertions(+), 59 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Amortized.lean b/Cslib/Algorithms/Lean/Amortized.lean
index 7d111cdcc..5c3895e34 100644
--- a/Cslib/Algorithms/Lean/Amortized.lean
+++ b/Cslib/Algorithms/Lean/Amortized.lean
@@ -1,4 +1,3 @@
-
 /-
 Copyright (c) 2026 Simon Cruanes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -8,6 +7,7 @@ Authors: Simon Cruanes
 module
 
 import Cslib.Init
+public import Cslib.Algorithms.Lean.TimeM
 
 /-!
 # Amortized cost analysis
@@ -26,6 +26,18 @@ class Potential α where
       [Okasaki, *Purely Functional Data Structures*, 1996][okasaki1996] -/
   potential : α → Nat
 
+class Op α o where
+  applyOp : α → o → TimeM ℕ α
+
+@[simp] def applyOps {α o : Type u} [Op α o] (ops : List o) (x : α)
+    : 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] [Potential α] (x : α) (op : o) : ℕ :=
+  (Op.applyOp x op).time + Potential.potential (Op.applyOp x op).ret - Potential.potential x
+
 end Cslib.Algorithms.Lean.Amortized
 
 end
diff --git a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
index fc3284420..859a3b45f 100644
--- a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
+++ b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
@@ -8,6 +8,7 @@ module
 
 import Cslib.Init
 public import Cslib.Algorithms.Lean.Amortized
+public import Cslib.Algorithms.Lean.TimeM
 
 /-!
 # Functional Queue
@@ -31,78 +32,89 @@ namespace Cslib.Algorithms.Lean
 
 universe u
 
-structure RawFunctionalQueue (α : Type u) where
+namespace Raw
+
+structure FunctionalQueue (α : Type u) where
   front : List α
   back : List α
 
-namespace Raw
-
 /-- Well-formedness: if front is empty, back must be empty too. -/
-def invariant {α : Type u} (q : RawFunctionalQueue α) : Prop :=
+def invariant {α : Type u} (q : Raw.FunctionalQueue α) : Prop :=
   q.front = [] → q.back = []
 
 /-- The logical contents of the queue: `front ++ back.reverse`. -/
-def ghostList {α : Type u} (q : RawFunctionalQueue α) : List α :=
+def ghostList {α : Type u} (q : FunctionalQueue α) : List α :=
   List.append q.front q.back.reverse
 
 /-- The empty queue. -/
-def empty {α : Type u} : RawFunctionalQueue α := ⟨ [], [] ⟩
+def empty {α : Type u} : FunctionalQueue α := ⟨ [], [] ⟩
 
 /-- Internal: rebalance by moving `back.reverse` to `front` when `front` is empty. -/
-def rebalance {α : Type u} (q : RawFunctionalQueue α) : RawFunctionalQueue α :=
+def rebalance {α : Type u} (q : FunctionalQueue α)
+    : TimeM ℕ (FunctionalQueue α) :=
   match q.front with
-  | [] => ⟨ (q.back).reverse, [] ⟩
-  | _ => q
+  | [] => do
+    TimeM.tick q.back.length
+    pure ⟨ (q.back).reverse, [] ⟩
+  | _ => pure q
 
-theorem rebalanceInvert {α : Type u} (q : RawFunctionalQueue α) :
-    (rebalance q).front = [] → q = Raw.empty := by
+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 : RawFunctionalQueue α} :
-    invariant (rebalance q) := by
+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 : RawFunctionalQueue α) :
-    rebalance (rebalance q) = rebalance q := by
+@[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 : RawFunctionalQueue α) :
-    ghostList (rebalance q) = ghostList q := by
+@[simp] theorem rebalancePreserveGhost {α : Type u} (q : FunctionalQueue α) :
+    ghostList (rebalance q).ret = ghostList q := by
   obtain ⟨f, b⟩ := q
   simp [rebalance, ghostList]
   split <;> grind [List.reverse_append]
 
 /-- Enqueue an element. -/
-def push {α : Type u} (x : α) (q : RawFunctionalQueue α) : RawFunctionalQueue α :=
+def push {α : Type u} (x : α) (q : FunctionalQueue α)
+    : TimeM ℕ (FunctionalQueue α) := do
+  TimeM.tick 1
   rebalance ⟨ q.front, x :: q.back ⟩
 
-theorem pushInvariant {α : Type u} (x : α) (q : RawFunctionalQueue α) :
-    invariant q → invariant (push x q) := by
+theorem pushInvariant {α : Type u} (x : α) (q : FunctionalQueue α)
+    : invariant q → invariant (push x q).ret := by
   intro h
   rw [push]
   apply rebalanceInvariant
 
-theorem pushGhost {α : Type u} (x : α) (q : RawFunctionalQueue α) :
-    ghostList (push x q) = ghostList q ++ [x] := by
-  rw [push, rebalancePreserveGhost, ghostList]
+theorem pushGhost {α : Type u} (x : α) (q : Raw.FunctionalQueue α)
+    : ghostList (push x q).ret = ghostList q ++ [x] := by
+  rw [push]
+  simp only [TimeM.ret_bind, rebalancePreserveGhost]
+  rw [ghostList]
   simp [ghostList, List.append_assoc]
 
 /-- Dequeue: returns `some (head, remaining)` or `none` if empty. -/
-def pop {α : Type u} (q : RawFunctionalQueue α) : Option (α × RawFunctionalQueue α) :=
+def pop {α : Type u} (q : Raw.FunctionalQueue α)
+    : TimeM ℕ (Option (α × Raw.FunctionalQueue α)) :=
   match q.front with
-  | [] => none
-  | x :: tl =>
-    some (x, rebalance ⟨ tl, q.back ⟩)
-
-theorem popInvariant {α : Type u} (x : α) (q q2 : RawFunctionalQueue α) :
-    invariant q → pop q = some (x, q2) → invariant q2 := by
+  | [] => pure none
+  | x :: tl => do
+    let q2 ← rebalance ⟨ tl, q.back ⟩
+    pure (some (x, q2))
+
+theorem popInvariant {α : 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
@@ -120,8 +132,10 @@ theorem popInvariant {α : Type u} (x : α) (q q2 : RawFunctionalQueue α) :
 @[simp] theorem emptyGhost {α : Type u} : ghostList (@Raw.empty α) = [] := by
   simp [ghostList, Raw.empty]
 
-theorem popGhost {α : Type u} {x : α} {q q2 : RawFunctionalQueue α} :
-    invariant q → pop q = some (x, q2) → ghostList q = x :: ghostList q2 := by
+theorem popGhost {α : Type u} {x : α} {q q2 : Raw.FunctionalQueue α}
+    : invariant q →
+      (pop q).ret = some (x, q2) →
+      ghostList q = x :: ghostList q2 := by
   intro hq hpop
   obtain ⟨f, b⟩ := q
   simp [invariant] at hq
@@ -138,65 +152,106 @@ end Raw
 
 namespace Complexity
 
-def potential {α : Type u} (q : RawFunctionalQueue α) : Nat :=
+def potential {α : Type u} (q : Raw.FunctionalQueue α) : Nat :=
   q.back.length
 
 instance functionalQueuePotential {α : Type u}
-    : Amortized.Potential (RawFunctionalQueue α) :=
+    : Amortized.Potential (Raw.FunctionalQueue α) :=
   ⟨ potential ⟩
 
 inductive queueOp (α : Type u) where
   | push : α → queueOp α
   | pop
 
-def applyOp {α : Type u} (op : queueOp α) (q : RawFunctionalQueue α) : RawFunctionalQueue α :=
+def applyOp {α : Type u} (q : Raw.FunctionalQueue α) (op : queueOp α)
+    : TimeM ℕ (Raw.FunctionalQueue α) :=
   match op with
   | .push x => Raw.push x q
-  | .pop =>
-    match Raw.pop q with
-    | none => q
-    | some (_, q2) => q2
+  | .pop => do
+    match (← Raw.pop q) with
+    | none => pure q
+    | some (_, q2) => pure q2
+
+instance functionalQueueApplyOp {α : Type u}
+    : Amortized.Op (Raw.FunctionalQueue α) (queueOp α) :=
+  ⟨ applyOp ⟩
 
-def applyOps {α : Type u} (ops : List (queueOp α)) (q : RawFunctionalQueue α)
-    : RawFunctionalQueue α :=
-  ops.foldl (fun q op => applyOp op q) q
+theorem costRebalanceEmpty {α : Type u} (q : Raw.FunctionalQueue α)
+    : q.front = [] → (Raw.rebalance q).time = potential q := by
+  intro h
+  simp only [Raw.rebalance]; rw [h]; simp [potential]
+
+grind_pattern costRebalanceEmpty => (Raw.rebalance q).time
+
+theorem costRebalanceNonEmpty {α : Type u} (q : Raw.FunctionalQueue α)
+    : q.front ≠ [] → (Raw.rebalance q).time = 0 := by
+  intro h
+  simp [Raw.rebalance]
+
+grind_pattern costRebalanceNonEmpty => (Raw.rebalance q).time
+
+theorem costPush {α : Type u} (x : α) (q : Raw.FunctionalQueue α)
+    : (Raw.push x q).time ≤ potential q := by
+  simp [Raw.push]
+  sorry
+  /- cases q.front <;> grind -/
+  /-     grind [Raw.push] -/
+
+theorem costApplyOp {α : Type u} (op : queueOp α) (q : Raw.FunctionalQueue α)
+    : (applyOp q op).time ≤ 1 + potential q := by
+  sorry
+  /- cases op with -/
+  /- | .pu -/
+  /- simp [applyOp] -/
+  /- grind -/
 
 theorem constantTimeAmortized {α : Type u} :
-    ∀ (q : RawFunctionalQueue α) (ops:List (queueOp α)),
-    false
- := by
-   sorry
+    ∀ (q : Raw.FunctionalQueue α) (ops : List (queueOp α)),
+    (Amortized.applyOps ops q).time ≤ 2 * potential (Amortized.applyOps ops q).ret
+    := by
+  intro q ops
+  induction ops generalizing q with
+  | nil => simp
+  | cons op otherOps hOps =>
+    simp
+    sorry
 
 end Complexity
 
 /-- A functional queue with invariant. -/
 @[ext]
 structure FunctionalQueue (α : Type u) where
-  raw : RawFunctionalQueue α
+  raw : Raw.FunctionalQueue α
   inv : Raw.invariant raw
 
 def empty {α : Type u} : FunctionalQueue α := ⟨ @Raw.empty α, Raw.emptyInvariant ⟩
 
-def push {α : Type u} (x : α) (q : FunctionalQueue α) : FunctionalQueue α :=
-  ⟨ Raw.push x q.raw, Raw.pushInvariant x q.raw q.inv ⟩
+def push {α : Type u} (x : α) (q : FunctionalQueue α)
+    : TimeM ℕ (FunctionalQueue α) :=
+  let r := Raw.push x q.raw
+  ⟨ ⟨ r.ret, Raw.pushInvariant x q.raw q.inv ⟩, r.time ⟩
 
-def pop {α : Type u} (q : FunctionalQueue α) : Option (α × FunctionalQueue α) :=
-  match h : Raw.pop q.raw with
-  | none => none
+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.popInvariant x q.raw q2 q.inv h ⟩)
+    ⟨ some (x, ⟨ q2, Raw.popInvariant x q.raw q2 q.inv h ⟩), r.time ⟩
 
 /-- project to a list view, an ordered sequence of elements -/
 def ghostList {α : Type u} (q : FunctionalQueue α) : List α := Raw.ghostList q.raw
 
 theorem pushGhost {α : Type u} (x : α) (q : FunctionalQueue α) :
-    ghostList (push x q) = ghostList q ++ [x] :=
+    ghostList (push x q).ret = ghostList q ++ [x] :=
   Raw.pushGhost x q.raw
 
-theorem popGhost {α : Type u} {x : α} {q q2 : FunctionalQueue α} :
-    pop q = some (x, q2) → ghostList q = x :: ghostList q2 := by
-  intro h
+theorem popGhost {α : Type u} {x : α} {q2 : FunctionalQueue α} :
+    ∀ {q : FunctionalQueue α},
+    (pop q).ret = some (x, q2) → ghostList q = x :: ghostList q2 := by
+  intro q h
   simp only [pop, ghostList] at h ⊢
+  simp only [TimeM.ret] at h
   split at h
   · simp only [reduceCtorEq] at h
   · rename_i x2 q2' heq
diff --git a/Cslib/Algorithms/Lean/TimeM.lean b/Cslib/Algorithms/Lean/TimeM.lean
index 389d6945b..164a653cd 100644
--- a/Cslib/Algorithms/Lean/TimeM.lean
+++ b/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

From a3c04241e20e2d00774206b31430a1a92672fb97 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sun, 10 May 2026 21:42:18 -0400
Subject: [PATCH 8/8] directly use amortized cost for proofs

---
 .../Lean/FunctionalQueue/FunctionalQueue.lean | 54 +++++--------------
 1 file changed, 14 insertions(+), 40 deletions(-)

diff --git a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
index 859a3b45f..4e5b9db13 100644
--- a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
+++ b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
@@ -176,45 +176,20 @@ instance functionalQueueApplyOp {α : Type u}
     : Amortized.Op (Raw.FunctionalQueue α) (queueOp α) :=
   ⟨ applyOp ⟩
 
-theorem costRebalanceEmpty {α : Type u} (q : Raw.FunctionalQueue α)
-    : q.front = [] → (Raw.rebalance q).time = potential q := by
-  intro h
-  simp only [Raw.rebalance]; rw [h]; simp [potential]
-
-grind_pattern costRebalanceEmpty => (Raw.rebalance q).time
-
-theorem costRebalanceNonEmpty {α : Type u} (q : Raw.FunctionalQueue α)
-    : q.front ≠ [] → (Raw.rebalance q).time = 0 := by
-  intro h
-  simp [Raw.rebalance]
-
-grind_pattern costRebalanceNonEmpty => (Raw.rebalance q).time
-
-theorem costPush {α : Type u} (x : α) (q : Raw.FunctionalQueue α)
-    : (Raw.push x q).time ≤ potential q := by
-  simp [Raw.push]
-  sorry
-  /- cases q.front <;> grind -/
-  /-     grind [Raw.push] -/
-
-theorem costApplyOp {α : Type u} (op : queueOp α) (q : Raw.FunctionalQueue α)
-    : (applyOp q op).time ≤ 1 + potential q := by
-  sorry
-  /- cases op with -/
-  /- | .pu -/
-  /- simp [applyOp] -/
-  /- grind -/
-
-theorem constantTimeAmortized {α : Type u} :
-    ∀ (q : Raw.FunctionalQueue α) (ops : List (queueOp α)),
-    (Amortized.applyOps ops q).time ≤ 2 * potential (Amortized.applyOps ops q).ret
-    := by
-  intro q ops
-  induction ops generalizing q with
-  | nil => simp
-  | cons op otherOps hOps =>
-    simp
-    sorry
+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, Nat.sub_le_iff_le_add]
+  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])
 
 end Complexity
 
@@ -251,7 +226,6 @@ theorem popGhost {α : Type u} {x : α} {q2 : FunctionalQueue α} :
     (pop q).ret = some (x, q2) → ghostList q = x :: ghostList q2 := by
   intro q h
   simp only [pop, ghostList] at h ⊢
-  simp only [TimeM.ret] at h
   split at h
   · simp only [reduceCtorEq] at h
   · rename_i x2 q2' heq