refactor(probability): replace positional projection chains in public declarations (#1764)

Complexity/Computability/Probabilistic/Oracle/Parameter.lean

@@ -103,7 +103,8 @@ theorem IsOraclePPT.run_interpret_preprocess {Caller State : Type}
     (hprepare : ComputableTidilyInPolyTime prepare input (encPair encUnary encBits))
     (hhandler : IsPPTOn
       (encPair input (encPair (encPair operationEncoding encBits) stateEncoding))
-      (encPair encBits stateEncoding) (fun pair => handler pair.1 pair.2.1 pair.2.2))
+      (encPair encBits stateEncoding)
+      (fun ⟨caller, request, state⟩ => handler caller request state))
     (hinitial : ComputableTidilyInPolyTime initial input stateEncoding)
     (invariant : Caller → State → Prop) (hinit : ∀ a, invariant a (initial a))
     (hresources : ComputableTidilyInPolyTime (fun pair => resources pair.1 pair.2)
@@ -133,7 +134,8 @@ theorem IsOraclePPT.run_interpret_preprocess_open {External Caller State : Type}
     (hprepare : ComputableTidilyInPolyTime prepare input (encPair encUnary encBits))
     (hhandler : IsOraclePPTOn
       (encPair input (encPair (encPair operationEncoding encBits) stateEncoding))
-      (encPair encBits stateEncoding) (fun pair => handler pair.1 pair.2.1 pair.2.2))
+      (encPair encBits stateEncoding)
+      (fun ⟨caller, request, state⟩ => handler caller request state))
     (hinitial : ComputableTidilyInPolyTime initial input stateEncoding)
     (invariant : Caller → State → Prop) (hinit : ∀ a, invariant a (initial a))
     (hresources : ComputableTidilyInPolyTime (fun pair => resources pair.1 pair.2)
@@ -163,7 +165,8 @@ theorem IsOraclePPT.run_interpret_preprocess_open' {External Caller State : Type
     (hprepare : ComputableInPolyTime prepare input (encPair encUnary encBits))
     (hhandler : IsOraclePPTOn
       (encPair input (encPair (encPair operationEncoding encBits) stateEncoding))
-      (encPair encBits stateEncoding) (fun pair => handler pair.1 pair.2.1 pair.2.2))
+      (encPair encBits stateEncoding)
+      (fun ⟨caller, request, state⟩ => handler caller request state))
     (hinitial : ComputableInPolyTime initial input stateEncoding)
     (invariant : Caller → State → Prop) (hinit : ∀ a, invariant a (initial a))
     (hresources : ComputableInPolyTime (fun pair => resources pair.1 pair.2)

Complexity/Computability/Probabilistic/Oracle/Substitution.lean

@@ -68,7 +68,8 @@ theorem IsOraclePPTOn.run_interpret_preprocess_open
     (hprepare : ComputableTidilyInPolyTime prepare input source)
     (hhandler : IsOraclePPTOn
       (encPair input (encPair (encPair operationEncoding encBits) stateEncoding))
-      (encPair encBits stateEncoding) (fun pair => handler pair.1 pair.2.1 pair.2.2))
+      (encPair encBits stateEncoding)
+      (fun ⟨caller, request, state⟩ => handler caller request state))
     (hinitial : ComputableTidilyInPolyTime initial input stateEncoding)
     (invariant : Caller → State → Prop) (hinit : ∀ a, invariant a (initial a))
     (hresources : ComputableTidilyInPolyTime (fun pair => resources pair.1 pair.2)
@@ -138,7 +139,8 @@ theorem IsOraclePPTOn.run_interpret_preprocess_open'
     (hprepare : ComputableInPolyTime prepare input source)
     (hhandler : IsOraclePPTOn
       (encPair input (encPair (encPair operationEncoding encBits) stateEncoding))
-      (encPair encBits stateEncoding) (fun pair => handler pair.1 pair.2.1 pair.2.2))
+      (encPair encBits stateEncoding)
+      (fun ⟨caller, request, state⟩ => handler caller request state))
     (hinitial : ComputableInPolyTime initial input stateEncoding)
     (invariant : Caller → State → Prop) (hinit : ∀ a, invariant a (initial a))
     (hresources : ComputableInPolyTime (fun pair => resources pair.1 pair.2)

Complexity/Computability/Probabilistic/OracleSimulation.lean

@@ -57,7 +57,8 @@ theorem IsOraclePPTOn.run_interpret_preprocess {Operation α β Caller State : T
     (hprepare : ComputableTidilyInPolyTime prepare input source)
     (hhandler : IsPPTOn
       (encPair input (encPair (encPair operationEncoding encBits) stateEncoding))
-      (encPair encBits stateEncoding) (fun pair => handler pair.1 pair.2.1 pair.2.2))
+      (encPair encBits stateEncoding)
+      (fun ⟨caller, request, state⟩ => handler caller request state))
     (hinitial : ComputableTidilyInPolyTime initial input stateEncoding)
     (invariant : Caller → State → Prop) (hinit : ∀ a, invariant a (initial a))
     (hresources : ComputableTidilyInPolyTime (fun pair => resources pair.1 pair.2)

Complexity/Computability/Probabilistic/Presample.lean

@@ -55,7 +55,8 @@ theorem IsOraclePPTOn.run_interpret_withSampleList
     (horacle : IsPPTOn
       (encPair (encPair input valueEncoding)
         (encPair (encPair operationEncoding encBits) stateEncoding))
-      (encPair encBits stateEncoding) (fun pair => oracle pair.1.1 pair.1.2 pair.2.1 pair.2.2))
+      (encPair encBits stateEncoding)
+      (fun ⟨⟨caller, value⟩, ⟨request, state⟩⟩ => oracle caller value request state))
     (hinitial : ComputableTidilyInPolyTime initial input stateEncoding)
     (hvalues : ComputableTidilyInPolyTime values input (encList valueEncoding))
     (invariant : Caller → State → Prop) (hinit : ∀ a, invariant a (initial a))
@@ -115,7 +116,8 @@ theorem IsOraclePPT.run_interpret_withSampleList
     (horacle : IsPPTOn
       (encPair (encPair input valueEncoding)
         (encPair (encPair operationEncoding encBits) stateEncoding))
-      (encPair encBits stateEncoding) (fun pair => oracle pair.1.1 pair.1.2 pair.2.1 pair.2.2))
+      (encPair encBits stateEncoding)
+      (fun ⟨⟨caller, value⟩, ⟨request, state⟩⟩ => oracle caller value request state))
     (hinitial : ComputableTidilyInPolyTime initial input stateEncoding)
     (hvalues : ComputableTidilyInPolyTime values input (encList valueEncoding))
     (invariant : Caller → State → Prop) (hinit : ∀ a, invariant a (initial a))

Complexity/Computability/Probabilistic/Realization/OpenOracleSimulation.lean

@@ -101,7 +101,8 @@ theorem isOraclePPTOn_step [Fintype Operation] {input : α ↪ List Bool}
     {handler : α → Operation × List Bool → State → WordOracleComp External (List Bool × State)}
     (hhandler : IsOraclePPTOn
       (encPair input (encPair (encPair operationEncoding encBits) stateEncoding))
-      (encPair encBits stateEncoding) (fun pair => handler pair.1 pair.2.1 pair.2.2)) :
+      (encPair encBits stateEncoding)
+      (fun ⟨caller, request, state⟩ => handler caller request state)) :
     IsOraclePPTOn (encPair input (encPair encFiniteConfig stateEncoding))
       (encPair encFiniteConfig stateEncoding)
       (fun pair => step machine handler pair.1 pair.2) := by
@@ -160,7 +161,8 @@ theorem isOraclePPTOn_run [Finite Operation] {input : α ↪ List Bool}
     (hcount : ComputableInPolyTime count input encUnary)
     (hhandler : IsOraclePPTOn
       (encPair input (encPair (encPair operationEncoding encBits) stateEncoding))
-      (encPair encBits stateEncoding) (fun pair => handler pair.1 pair.2.1 pair.2.2))
+      (encPair encBits stateEncoding)
+      (fun ⟨caller, request, state⟩ => handler caller request state))
     (hinitial : ComputableInPolyTime initial input stateEncoding)
     (invariant : α → State → Prop) (hinit : ∀ a, invariant a (initial a))
     {resources : ℕ → ℕ} (hresources : PolynomiallyBounded resources)

Complexity/Computability/Probabilistic/Realization/OracleSimulation.lean

@@ -110,7 +110,8 @@ theorem isPPTOn_step [Fintype Operation] {input : α ↪ List Bool}
     {handler : α → Operation × List Bool → State → ProbComp (List Bool × State)}
     (hhandler : IsPPTOn
       (encPair input (encPair (encPair operationEncoding encBits) stateEncoding))
-      (encPair encBits stateEncoding) (fun pair => handler pair.1 pair.2.1 pair.2.2)) :
+      (encPair encBits stateEncoding)
+      (fun ⟨caller, request, state⟩ => handler caller request state)) :
     IsPPTOn (encPair input (encPair encFiniteConfig stateEncoding))
       (encPair encFiniteConfig stateEncoding)
       (fun pair => step machine handler pair.1 pair.2) :=
@@ -129,7 +130,8 @@ theorem isPPTOn_run [Finite Operation] {input : α ↪ List Bool}
     (hcount : ComputableInPolyTime count input encUnary)
     (hhandler : IsPPTOn
       (encPair input (encPair (encPair operationEncoding encBits) stateEncoding))
-      (encPair encBits stateEncoding) (fun pair => handler pair.1 pair.2.1 pair.2.2))
+      (encPair encBits stateEncoding)
+      (fun ⟨caller, request, state⟩ => handler caller request state))
     (hinitial : ComputableInPolyTime initial input stateEncoding)
     (invariant : α → State → Prop) (hinit : ∀ a, invariant a (initial a))
     {resources : ℕ → ℕ} (hresources : PolynomiallyBounded resources)

Complexity/Computability/Probabilistic/Selection.lean

@@ -61,27 +61,33 @@ theorem IsPPTOn.selectBest {α : Type} {input : α ↪ List Bool}
       (fun pair => OracleComp.selectStep (trials pair.1) (test pair.1) pair.2) := by
     unfold OracleComp.selectStep
     apply (htest'.countTrue htrials').map_with
-    dsimp only [OracleComp.selectUpdate, stateEncoding]
-    apply ComputableInPolyTime.prod
-    · exact ComputableInPolyTime.unary_succ.comp (by fun_prop)
-    · have hc := ComputableInPolyTime.unary_le'
-        (by fun_prop : ComputableInPolyTime
-          (fun pair : (α × (ℕ × ℕ × ℕ)) × ℕ => pair.1.2.2.2)
-          (encPair (encPair input (encPair encUnary (encPair encUnary encUnary))) encUnary)
-          encUnary)
-        (by fun_prop : ComputableInPolyTime
-          (fun pair : (α × (ℕ × ℕ × ℕ)) × ℕ => pair.2)
-          (encPair (encPair input (encPair encUnary (encPair encUnary encUnary))) encUnary)
-          encUnary)
-      simpa only [decide_eq_true_eq] using hc.ite (by fun_prop) (by fun_prop)
+    have hupd : ComputableInPolyTime
+        (fun pair : (α × (ℕ × ℕ × ℕ)) × ℕ =>
+          (pair.1.2.1 + 1,
+            if pair.1.2.2.2 ≤ pair.2 then (pair.1.2.1, pair.2) else pair.1.2.2))
+        (encPair (encPair input stateEncoding) encUnary) stateEncoding := by
+      dsimp only [stateEncoding]
+      apply ComputableInPolyTime.prod
+      · exact ComputableInPolyTime.unary_succ.comp (by fun_prop)
+      · have hc := ComputableInPolyTime.unary_le'
+          (by fun_prop : ComputableInPolyTime
+            (fun pair : (α × (ℕ × ℕ × ℕ)) × ℕ => pair.1.2.2.2)
+            (encPair (encPair input (encPair encUnary (encPair encUnary encUnary))) encUnary)
+            encUnary)
+          (by fun_prop : ComputableInPolyTime
+            (fun pair : (α × (ℕ × ℕ × ℕ)) × ℕ => pair.2)
+            (encPair (encPair input (encPair encUnary (encPair encUnary encUnary))) encUnary)
+            encUnary)
+        simpa only [decide_eq_true_eq] using hc.ite (by fun_prop) (by fun_prop)
+    exact hupd.of_enc_eq fun ⟨⟨_, ⟨_, _, _⟩⟩, _⟩ => rfl
   have horacle := IsOraclePPTOn.iterateWith_spec' (Operation := Empty)
     (stateEncoding := stateEncoding) (initial := fun _ => (0, 0, 0))
     (step := fun a s => ProbOracleComp.sample (OracleComp.selectStep (trials a) (test a) s))
     hcount (by dsimp only [stateEncoding]; fun_prop)
     (hstep.isOraclePPTOn (Operation := Empty))
     (fun a i state => state.1 = i ∧ state.2.1 ≤ i ∧ state.2.2 ≤ trials a)
-    (by simp) (fun a i state _ hstate next hnext =>
-      ProbComp.selectStep_bounded (trials a) (test a) i state hstate next
+    (by simp) (fun a i ⟨next, best, count⟩ _ hstate ⟨next', best', count'⟩ hnext =>
+      ProbComp.selectStep_bounded (trials a) (test a) i next best count hstate next' best' count'
         ((ProbOracleComp.support_sample _).subset hnext))
     (size := fun a => 4 * count a + trials a + 2)
     (ComputableInPolyTime.polyBounded (by fun_prop)) (by
@@ -94,7 +100,9 @@ theorem IsPPTOn.selectBest {α : Type} {input : α ↪ List Bool}
         (OracleComp.selectStep (trials a) (test a)) (0, 0, 0)) := by
     apply IsOraclePPTOn.isPPTOn
     simpa only [ProbOracleComp.sample, OracleComp.interpret_iterate] using horacle.1
-  exact hloop.map (by dsimp only [stateEncoding]; fun_prop)
+  have hproj : ComputableInPolyTime (fun s : ℕ × ℕ × ℕ => s.2.1) stateEncoding encUnary := by
+    dsimp only [stateEncoding]; fun_prop
+  exact hloop.map (hproj.of_enc_eq fun ⟨_, _, _⟩ => rfl)
 
 /-- Selecting from an efficiently computed list charges for the whole list and each test. -/
 @[program_certificate]

Complexity/Languages/Probabilistic/Forking.lean

@@ -147,6 +147,13 @@ theorem IsQueryBounded.length_runWithAnswers_le (default : H)
     rw [runWithAnswers_query_bind, List.length_cons]
     exact Nat.succ_le_succ (ih _ _)
 
+/-- The result component of a `runWithAnswers` output pair `(result, queries)`. -/
+abbrev runWithAnswersOutput {α γ : Type} (out : α × γ) : α := out.1
+
+/-- The final handler state produced by `runWithAnswers` on a stateful handler execution. -/
+abbrev runWithAnswersState {σ β : Type} (out : (β × σ) × List Query) : σ :=
+  (runWithAnswersOutput out).2
+
 /-- **An invariant of a handler's run on a list of answers.** A program runs through a stateful
 handler whose calls are oracle programs, and the resulting program runs on a list of answers. A
 property of the handler's state and of the queries asked so far that every handler call
@@ -155,12 +162,14 @@ theorem runWithAnswers_run_interpret_invariant {ι σ β : Type} {spec : ι →
     (handler : (q : ι) → StateT σ (OracleComp (fun _ : Query => H)) (spec q))
     (answers : List H) (invariant : σ → List Query → Prop)
     (step : ∀ q s queries, invariant s queries →
-      invariant (runWithAnswers default ((handler q).run s) (answers.drop queries.length)).1.2
+      invariant
+        (runWithAnswersState (runWithAnswers default ((handler q).run s)
+          (answers.drop queries.length)))
         (queries ++ (runWithAnswers default ((handler q).run s)
           (answers.drop queries.length)).2))
     (program : OracleComp spec β) (s : σ) (queries : List Query) (hs : invariant s queries) :
-    invariant (runWithAnswers default ((interpret handler program).run s)
-        (answers.drop queries.length)).1.2
+    invariant (runWithAnswersState (runWithAnswers default ((interpret handler program).run s)
+        (answers.drop queries.length)))
       (queries ++ (runWithAnswers default ((interpret handler program).run s)
         (answers.drop queries.length)).2) := by
   induction program using OracleComp.induction generalizing s queries with
@@ -328,14 +337,17 @@ theorem validIndex_eq_some {q count : ℕ} {position : Option ℕ} {j : Fin q}
     subst h
     exact ⟨rfl, hp.2⟩
 
+/-- The named query position returned by a forking-lemma program execution. -/
+abbrev forkNamedPosition {β γ : Type} (out : (Option ℕ × β) × γ) : Option ℕ :=
+  (runWithAnswersOutput out).1
+
 /-- A program with explicit coins as an algorithm on coins and `q` answers, for the general
 forking lemma: the validly named position, and the result with the queries. -/
 def forkingAlgorithm {S β : Type} (default : H) (q : ℕ)
     (program : S → OracleComp (fun _ : Query => H) (Option ℕ × β)) (s : S) (h : Fin q → H) :
     Option (Fin q) × ((Option ℕ × β) × List Query) :=
-  (validIndex q (runWithAnswers default (program s) (List.ofFn h)).2.length
-      (runWithAnswers default (program s) (List.ofFn h)).1.1,
-    runWithAnswers default (program s) (List.ofFn h))
+  let run := runWithAnswers default (program s) (List.ofFn h)
+  (validIndex q run.2.length (forkNamedPosition run), run)
 
 variable {S β : Type} [Fintype H] [Nonempty H] [DecidableEq H]
 
@@ -349,7 +361,7 @@ theorem le_add_sqrt_fork (first : PMF S)
     ((do
       let s ← first
       let run ← (interpret countingUniform (program s)).run 0
-      return (validIndex q run.2 run.1.1).isSome : PMF Bool) true).toReal ≤
+      return (validIndex q run.2 (forkNamedPosition run)).isSome : PMF Bool) true).toReal ≤
       q / Fintype.card H + √(q * ((Forking.fork first (forkingAlgorithm default q program)).map
         Option.isSome true).toReal) := by
   have hacc : (do
@@ -377,7 +389,7 @@ theorem mem_support_fork {first : PMF S}
     ∃ s ∈ first.support, ∃ h h' : Fin q → H, (∀ i < j, h i = h' i) ∧ h j ≠ h' j ∧
       out = runWithAnswers default (program s) (List.ofFn h) ∧
       out' = runWithAnswers default (program s) (List.ofFn h') ∧
-      out.1.1 = some j.val ∧ out'.1.1 = some j.val ∧
+      forkNamedPosition out = some j.val ∧ forkNamedPosition out' = some j.val ∧
       out.2.take (j + 1) = out'.2.take (j + 1) ∧
       ∃ query, out.2[j.val]? = some query ∧ out'.2[j.val]? = some query := by
   obtain ⟨s, hs, h, h', hagree, hne, hrun, hrun'⟩ := Forking.mem_support_fork hfork

Complexity/Languages/Probabilistic/Oracle/Simulation.lean

@@ -194,8 +194,9 @@ theorem run_interpret_run_interpret {Query' : Type} {spec' : Query' → Type}
       (fun q state => ((OracleComp.interpret
         (handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
           ((inner q).run state.1)).run state.2).map
-            (fun result => (result.1.1, result.1.2, result.2)))) program).run
-        (hidden, external)).map (fun result => ((result.1, result.2.1), result.2.2)) := by
+            (fun ⟨⟨a, b⟩, c⟩ => (a, b, c)))) program).run
+        (hidden, external)).map
+          (fun ⟨a, b, c⟩ => ((a, b), c)) := by
   rw [OracleComp.run_interpret_run_interpret, _root_.PMF.monad_map_eq_map]
   congr 3
   funext q state

Complexity/Languages/Probabilistic/Presample.lean

@@ -77,7 +77,7 @@ theorem IsQueryBounded.run_interpret_presample {program : ProbOracleComp spec α
     ((PMF.iid source n).map List.ofFn).bind (fun values =>
       ((interpret (handler (fun k => StateT.lift (ProbComp.unifOracle k))
         (withSampleList fallback oracle)) program).run (s, values)).map
-          fun result => (result.1, result.2.1)) =
+          fun (result, next, _) => (result, next)) =
       (interpret (handler (fun k => StateT.lift (ProbComp.unifOracle k))
         (fun q state => source.bind fun value => oracle value q state)) program).run s := by
   induction h generalizing s with
@@ -137,7 +137,7 @@ theorem OracleComp.IsQueryBounded.run_interpret_presample {Query State Value γ
     (oracle : Value → (q : Query) → StateT State PMF (spec q)) (s : State) :
     ((Probability.PMF.iid source n).map List.ofFn).bind (fun values =>
       ((interpret (withSampleList fallback oracle) program).run (s, values)).map
-        fun result => (result.1, result.2.1)) =
+        fun (result, next, _) => (result, next)) =
       (interpret (m := StateT State PMF)
         (fun q state => source.bind fun value => oracle value q state) program).run s := by
   simpa only [interpret_interpret, ProbOracleComp.interpret_query] using