feat(DataStructure/StateTransition): refinements by abstraction functions with stacked potentials

Complexity.lean

@@ -2921,6 +2921,7 @@ public import Complexity.DataStructure.StateTransition.CostHoare
 public import Complexity.DataStructure.StateTransition.Hoare
 public import Complexity.DataStructure.StateTransition.Impl
 public import Complexity.DataStructure.StateTransition.Module
+public import Complexity.DataStructure.StateTransition.Refinement
 public import Complexity.DataStructure.StateTransition.Resource
 public import Complexity.DataStructure.VanEmdeBoas.Basic
 public import Complexity.DataStructure.VanEmdeBoas.Elements
@@ -2944,6 +2945,7 @@ public import Complexity.DataStructure.WordRAM.StateTransition
 public import Complexity.Foundations.Algebra.FiniteMagnitude
 public import Complexity.Foundations.Algebra.GeometricTail
 public import Complexity.Foundations.Algebra.Shear
+public import Complexity.Foundations.Analysis.Asymptotics.CostBound
 public import Complexity.Foundations.Analysis.Asymptotics.Exponential
 public import Complexity.Foundations.Analysis.BernoulliInequality
 public import Complexity.Foundations.Analysis.ENNRealTsum

Complexity/DataStructure/Queue/Spec.lean

@@ -28,6 +28,8 @@ method is described in Chapter 17.
 ## Main results
 
 * `transfer_run`: stack operations reverse the rear contents into the front stack.
+* `runClient_dequeue_nil`, `stepFn_methods`: the methods realize the FIFO step on the represented
+  list.
 * `potential_step`: at most three amortized stack calls, including the size query.
 * `realized_client`: every adaptive client has a correct backend execution with its bound.
 * `realized_client_bound`: every supplied linked execution satisfies correctness and the bound.
@@ -118,10 +120,40 @@ theorem transfer_run (front back : List α) :
   induction back generalizing front with
   | nil => rfl
   | cons a back ih =>
-    simpa [transfer, stackPair, stack, transferTrace,
-      List.reverse_cons, List.append_assoc] using congrArg
-        (fun r : Unit × (stackPair α).State × List (stackPair α).Op =>
-          (r.1, r.2.1, .inr .pop :: .inl (.push a) :: r.2.2)) (ih (a :: front))
+    change (let (v, s, os) := (stackPair α).runClient (a :: front, back) (transfer back.length)
+      (v, s, (Sum.inr StackOp.pop : (stackPair α).Op) :: Sum.inl (StackOp.push a) :: os)) = _
+    rw [ih]
+    simp [transferTrace, List.reverse_cons, List.append_assoc]
+
+/-- A dequeue from an empty front stack asks for the rear size, transfers the rear, and pops the
+front again. -/
+theorem runClient_dequeue_nil (back : List α) :
+    (stackPair α).runClient ([], back) (methods .dequeue) =
+      (back.reverse.head?, (back.reverse.tail, []),
+        .inl .pop :: .inr .size :: (transferTrace back ++ [.inl .pop])) := by
+  simp only [methods, bind, StateTransitionSpec.runClient_liftBind, stackPair, stack,
+    List.tail_nil, List.head?_nil]
+  rw [StateTransitionSpec.runClient_bind, transfer_run, List.append_nil]
+  rfl
+
+/-- Each method returns the FIFO answer, and the stacks then represent the FIFO successor of the
+represented list. -/
+theorem stepFn_methods (front back : List α) (o : QueueOp α) :
+    (queue α).stepFn (front ++ back.reverse) o =
+      (((stackPair α).clientState (front, back) (methods o)).1 ++
+          ((stackPair α).clientState (front, back) (methods o)).2.reverse,
+        (stackPair α).clientResult (front, back) (methods o)) := by
+  cases o with
+  | enqueue n =>
+    change ((front ++ back.reverse) ++ [n], ()) = (front ++ (n :: back).reverse, ())
+    simp [List.reverse_cons, List.append_assoc]
+  | dequeue =>
+    cases front with
+    | cons a front => rfl
+    | nil =>
+      simp only [StateTransitionSpec.clientState, StateTransitionSpec.clientResult]
+      rw [runClient_dequeue_nil]
+      simp
 
 /-- Representation and behavior are proved once, before selecting a backend or cost model. -/
 def implementation : Module (queue α) (stackPair α) :=
@@ -134,21 +166,8 @@ def implementation : Module (queue α) (stackPair α) :=
       intro q s o hr _
       subst q
       obtain ⟨front, back⟩ := s
-      cases o with
-      | enqueue n =>
-        constructor
-        · rfl
-        · change (front ++ back.reverse) ++ [n] = front ++ (n :: back).reverse
-          simp [List.reverse_cons, List.append_assoc]
-      | dequeue =>
-        cases front with
-        | cons a front => exact ⟨rfl, rfl⟩
-        | nil =>
-          simp only [methods, bind, StateTransitionSpec.clientResult,
-            StateTransitionSpec.clientState, StateTransitionSpec.runClient_liftBind,
-            stackPair, stack, List.tail_nil, List.head?_nil]
-          rw [StateTransitionSpec.runClient_bind, transfer_run]
-          simp)
+      have h := stepFn_methods front back o
+      exact ⟨(congrArg Prod.snd h).symm, congrArg Prod.fst h⟩)
 
 /-- Each transferred element incurs one pop and one push. -/
 theorem transferTrace_length (back : List α) : (transferTrace back).length = 2 * back.length := by
@@ -173,13 +192,9 @@ theorem potential_step (s : (stackPair α).State) (o : QueueOp α) :
       change 1 + 2 * back.length ≤ 3 + 2 * back.length
       omega
     | nil =>
-      simp only [methods, bind, StateTransitionSpec.runClient_liftBind, stackPair,
-        stack, List.tail_nil, List.head?_nil]
-      rw [StateTransitionSpec.runClient_bind, transfer_run]
-      simp only [StateTransitionSpec.runClient_liftBind, StateTransitionSpec.runClient_pure]
-      change (transferTrace back ++ [Sum.inl StackOp.pop]).length + 2 ≤ 3 + 2 * back.length
-      rw [List.length_append, transferTrace_length]
-      simp only [List.length_singleton]
+      rw [runClient_dequeue_nil]
+      simp only [List.length_cons, List.length_append, List.length_nil]
+      rw [transferTrace_length]
       omega
 
 private theorem weighted_potential_step (K : Nat) {q : (queue α).State} {s : (stackPair α).State}

Complexity/DataStructure/StateTransition.lean

@@ -1098,13 +1098,14 @@ theorem eval_eq_liftM {D : StateTransitionSpec.{u, v, u}}
   | pure a => rfl
   | liftBind o k ih => exact ih (D.stepFn s o).2 (D.stepFn s o).1
 
-/-- Two independent abstract components. A backend must separately justify their independence. -/
+/-- Two independent abstract components. A backend must separately justify their independence.
+The answer types are `Sum.elim D.Result E.Result`, so the signature of a product depends only on
+the signatures of its components: clients of `product D E` are clients of `product D' E'` when
+`D`, `D'` and `E`, `E'` differ only in their states' admissibility. -/
 abbrev product (D E : StateTransitionSpec.{u, v, w}) : StateTransitionSpec where
   State := D.State × E.State
   Op := D.Op ⊕ E.Op
-  Result
-    | .inl o => D.Result o
-    | .inr o => E.Result o
+  Result := Sum.elim D.Result E.Result
   step s
     | .inl o, s', a => D.step s.1 o s'.1 a ∧ s'.2 = s.2
     | .inr o, s', a => s'.1 = s.1 ∧ E.step s.2 o s'.2 a