refactor(probability): one scoped Pr[…] notation for Boolean experiments

Complexity.lean

@@ -1741,6 +1741,7 @@ public import Complexity.Languages.Probabilistic.Forking
 public import Complexity.Languages.Probabilistic.Iteration
 public import Complexity.Languages.Probabilistic.LinearHash
 public import Complexity.Languages.Probabilistic.Memoize
+public import Complexity.Languages.Probabilistic.Notation
 public import Complexity.Languages.Probabilistic.Oracle
 public import Complexity.Languages.Probabilistic.Oracle.Interaction
 public import Complexity.Languages.Probabilistic.Oracle.Simulation

Complexity/Crypto/Computational/Basic.lean

@@ -81,15 +81,6 @@ theorem eval_bind_eq_distinguishingGame (sample : ProbComp (List Bool))
     ProbComp.eval (sample >>= adversary) = distinguishingGame (ProbComp.eval sample) adversary :=
   ProbComp.eval_bind _ _
 
-/-- Success after sampling a finite intermediate value is its weighted average. -/
-theorem Game.coe_succProbability_eval_bind {α : Type} [Fintype α]
-    (source : ProbComp α) (next : α → ProbComp Bool) :
-    (Game.succProbability (ProbComp.eval (source >>= next)) : ℝ) =
-      ∑ a, (ProbComp.eval source a).toReal *
-        (Game.succProbability (ProbComp.eval (next a)) : ℝ) := by
-  simp only [Game.succProbability, ENNReal.coe_toNNReal_eq_toReal, ProbComp.eval_bind,
-    Probability.PMF.bind_apply_toReal]
-
 /-- Postprocessing the distinguisher's answer postprocesses the experiment's answer. -/
 theorem distinguishingGame_map (distribution : PMF (List Bool))
     (adversary : List Bool → ProbComp Bool) (f : Bool → Bool) :

Complexity/Crypto/Computational/GoldreichLevin/WordReduction.lean

@@ -10,6 +10,7 @@ module
 public import Complexity.Crypto.Computational.GoldreichLevin.WordDecoder
 public import Complexity.Crypto.Computational.Basic
 public import Complexity.Crypto.Computational.OneWay
+import Complexity.Languages.Probabilistic.Notation
 import Complexity.Computability.Probabilistic.CoinTape
 import Complexity.Tactic.PPT
 
@@ -53,8 +54,6 @@ namespace Cslib.Crypto.GoldreichLevin
 
 open Probability BitString Turing.MultiTapeTM
 
-local notation "Pr[" p "]" => (Game.succProbability (ProbComp.eval p) : ℝ)
-
 /-- The saved tape covers the unary parameter, the whole image and an `n`-bit query. -/
 def coinBudget (c d n imageLength : ℕ) : ℕ := c * (3 * n + imageLength + 2) ^ d
 
@@ -183,7 +182,7 @@ theorem word_prediction_advantage_le (f : List Bool → List Bool) (adversary :
     |Pr[parityPredictionGame f adversary n] - 1 / 2| ≤
       1 / (precision degree n : ℝ) +
         8 * Pr[inversionGame f (wordInverter f evaluate c d degree) n] := by
-  simp only [Game.succProbability, eval_parityPredictionGame f adversary evaluate c d hrealize,
+  simp only [eval_parityPredictionGame f adversary evaluate c d hrealize,
     eval_wordInversionGame f]
   exact invertSigned_advantage_le _ _ _ _ (precision_pos degree n)
 

Complexity/Crypto/Computational/HardCore.lean

@@ -11,6 +11,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Poly
 public import Complexity.Crypto.Computational.OneWay
 public import Complexity.Crypto.Computational.Prediction
 public import Complexity.Crypto.Computational.PseudorandomGenerator
+import Complexity.Languages.Probabilistic.Notation
 import Complexity.Tactic.PPT
 
 /-!
@@ -24,7 +25,8 @@ to be one-way or injective.
 The reduction appends a fixed trial bit to the image, runs a distinguisher, and predicts the trial
 on acceptance or its complement on rejection. The distinguishing gap is the average of the signed
 biases of the two fixed predictors. Both are single uniform programs, with no choice depending on
-the security parameter. `Pr[p]` abbreviates the existing game's success probability in the reals.
+the security parameter. `Pr[p]` is the probability, in the reals, that the program `p` returns
+`true` (the scoped notation of `Cslib.Probability`).
 
 Appending a hard-core predicate to an efficient length-preserving permutation gives a one-bit PRG
 in the existing finite-family security API. This is conditional on the hard-core predicate;
@@ -58,11 +60,6 @@ namespace Cslib.Crypto
 open Probability Turing.MultiTapeTM
 open scoped NNReal
 
-local notation "Pr[" p "]" => (Game.succProbability (ProbComp.eval p) : ℝ)
-
-private theorem coe_probability (game : Game) :
-    (Game.succProbability game : ℝ) = (game true).toReal := rfl
-
 /-- Predict a predicate of a uniform seed, given only its image and the security parameter. -/
 noncomputable def predictionGame (f : List Bool → List Bool) (predicate : List Bool → Bool)
     (adversary : Distinguisher) (n : ℕ) : ProbComp Bool := do
@@ -138,7 +135,7 @@ private theorem real_probability (f : List Bool → List Bool) (predicate : List
     Pr[prgRealGame (fun seed => f seed ++ [predicate seed]) adversary n] =
       ∑ bits : BitString n, ((PMF.uniformOfFintype (BitString n)) bits).toReal *
         Pr[adversary n (f (List.ofFn bits) ++ [predicate (List.ofFn bits)])] := by
-  simp only [coe_probability, eval_prgRealGame, distinguishingGame, PMF.monad_bind_eq_bind,
+  simp only [eval_prgRealGame, distinguishingGame, PMF.monad_bind_eq_bind,
     generatorEnsemble,
     BitString.uniformList, PMF.bind_map, Function.comp_def, PMF.map_comp, PMF.bind_apply_toReal]
 
@@ -148,7 +145,7 @@ private theorem ideal_probability (f : List Bool → List Bool) (adversary : Dis
       ∑ bits : BitString n, ((PMF.uniformOfFintype (BitString n)) bits).toReal *
         ((Pr[adversary n (f (List.ofFn bits) ++ [false])] +
           Pr[adversary n (f (List.ofFn bits) ++ [true])]) / 2) := by
-  simp only [coe_probability, distinguishingGame, hardCoreIdeal, PMF.monad_bind_eq_bind,
+  simp only [Game.coe_succProbability, distinguishingGame, hardCoreIdeal, PMF.monad_bind_eq_bind,
     BitString.uniformList,
     PMF.bind_map, PMF.bind_bind, Function.comp_def, PMF.bind_apply_toReal]
   apply Finset.sum_congr rfl
@@ -162,7 +159,7 @@ private theorem prediction_probability (f : List Bool → List Bool) (predicate
       ∑ bits : BitString n, ((PMF.uniformOfFintype (BitString n)) bits).toReal *
         Pr[(fun guess => guess == predicate (List.ofFn bits)) <$> adversary n (f (List.ofFn bits))]
       := by
-  simp only [coe_probability, predictionGame, ProbComp.eval_bind, BitString.eval_sampleList,
+  simp only [predictionGame, ProbComp.eval_bind, BitString.eval_sampleList,
     BitString.uniformList, PMF.bind_map, Function.comp_def, ProbComp.eval_map, ProbComp.eval_pure]
   rw [PMF.bind_apply_toReal]
   rfl
@@ -194,7 +191,8 @@ theorem hardCore_advantage_le (f : List Bool → List Bool) (predicate : List Bo
   apply NNReal.coe_le_coe.mp
   rw [Game.coe_advantage, NNReal.coe_div, NNReal.coe_add, NNReal.coe_ofNat,
     predictionAdvantage, predictionAdvantage, Game.coe_guessingAdvantage,
-    Game.coe_guessingAdvantage, hardCore_gap]
+    Game.coe_guessingAdvantage,
+    Game.coe_succProbability (ProbComp.eval (prgRealGame _ adversary n)), hardCore_gap]
   let left := Pr[predictionGame f predicate (hardCorePredictor adversary false) n]
   let right := Pr[predictionGame f predicate (hardCorePredictor adversary true) n]
   change |(left + right - 1) / 2| ≤ (|left - 1 / 2| + |right - 1 / 2|) / 2

Complexity/Crypto/Computational/Prediction.lean

@@ -8,6 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Crypto.Computational.Basic
+import Complexity.Languages.Probabilistic.Notation
 import Complexity.Probability.PMF
 import Complexity.Tactic.PPT
 
@@ -18,8 +19,8 @@ The predictor supplies a trial bit to a test and returns that bit on acceptance,
 on rejection. Averaging over an independent fair trial turns the test's signed distinguishing gap
 into prediction bias. The hidden bit is not an input to the predictor.
 
-`Pr[p]` below is local notation for the existing game's success probability, coerced to the reals
-to express signed differences. It introduces no additional probability or security definition.
+`Pr[p]` is the scoped notation of `Cslib.Probability` for the probability, in the reals, that `p`
+returns `true`, so gaps and biases are signed differences.
 
 ## Main definitions
 
@@ -48,8 +49,6 @@ namespace Cslib.Crypto
 
 open Probability Turing.MultiTapeTM
 
-local notation "Pr[" p "]" => (Game.succProbability (ProbComp.eval p) : ℝ)
-
 /-- Predict a trial bit on acceptance and its complement on rejection. -/
 def trialPredictor (test : Bool → ProbComp Bool) (trial : Bool) : ProbComp Bool :=
   (fun accept => if accept then trial else !trial) <$> test trial
@@ -68,14 +67,12 @@ theorem trialPredictor_gap (test : Bool → ProbComp Bool) (truth : Bool) :
   | false =>
     simp only [trialPredictor, Bool.not_false, Bool.not_true, beq_false,
       Functor.map_map, Bool.ite_true_right, Bool.ite_false_right, Bool.decide_eq_true,
-      Bool.or_false, Bool.and_true, Bool.not_not, id_map',
-      Game.succProbability, ENNReal.coe_toNNReal_eq_toReal, ProbComp.probability_not]
+      Bool.or_false, Bool.and_true, Bool.not_not, id_map', ProbComp.probability_not]
     ring
   | true =>
     simp only [beq_true, trialPredictor, Bool.not_false, Bool.ite_true_right,
       Bool.decide_eq_true, Bool.or_false, Functor.map_map, Bool.not_true, Bool.ite_false_right,
-      Bool.and_true, id_map',
-      Game.succProbability, ENNReal.coe_toNNReal_eq_toReal]
+      Bool.and_true, id_map']
     rw [show (fun accept => !accept) = Bool.not from rfl, ProbComp.probability_not]
     ring
 
@@ -84,11 +81,9 @@ theorem probability_bitPredictor (test : Bool → ProbComp Bool) (truth : Bool)
     Pr[(fun guess => guess == truth) <$> bitPredictor test] =
       (Pr[(fun guess => guess == truth) <$> trialPredictor test false] +
         Pr[(fun guess => guess == truth) <$> trialPredictor test true]) / 2 := by
-  change (ProbComp.eval _ true).toReal = _
   simp only [bitPredictor, map_bind, ProbComp.eval_bind, ProbComp.eval_uniform,
     PMF.bind_apply_toReal]
-  norm_num [Fintype.sum_bool, PMF.uniformOfFintype_apply, Game.succProbability, ENNReal.toReal,
-    ENNReal.toNNReal_ofNat]
+  norm_num [Fintype.sum_bool, PMF.uniformOfFintype_apply]
   ring
 
 /-- The randomized predictor's bias equals the gap between the real label and a fair label. -/
@@ -130,20 +125,18 @@ theorem probability_calibratedTest (real ideal challenge : ProbComp Bool) :
   let direction := bitPredictor (fun trial => if trial then real else ideal)
   have htotal := PMF.toReal_true_add_toReal_false (ProbComp.eval direction)
   have hbias := bitPredictor_bias (fun trial => if trial then real else ideal) true
-  simp only [beq_true, id_map', ite_true, Bool.false_eq_true, ite_false,
-    Game.succProbability, ENNReal.coe_toNNReal_eq_toReal] at hbias
-  simp only [calibratedTest, Game.coe_succProbability_eval_bind, Fintype.sum_bool, beq_false,
-    beq_true, id_map']
-  simp only [Game.succProbability, ENNReal.coe_toNNReal_eq_toReal, ProbComp.probability_not]
-  linear_combination (1 - (ProbComp.eval challenge true).toReal) * htotal +
-    (2 * (ProbComp.eval challenge true).toReal - 1) * hbias
+  simp only [beq_true, id_map', ite_true, Bool.false_eq_true, ite_false] at hbias
+  simp only [calibratedTest, ProbComp.probability_bind, Fintype.sum_bool, beq_false,
+    beq_true, id_map', ProbComp.probability_not]
+  linear_combination (1 - Pr[challenge]) * htotal +
+    (2 * Pr[challenge] - 1) * hbias
 
 /-- The same calibration on both sides turns a possibly negative gap into its square. -/
 theorem calibratedTest_gap (real ideal : ProbComp Bool) :
     Pr[calibratedTest real ideal real] -
       Pr[calibratedTest real ideal ideal] =
       (Game.advantage (ProbComp.eval real) (ProbComp.eval ideal) : ℝ) ^ 2 := by
-  simp only [probability_calibratedTest, Game.coe_advantage, sq_abs]
+  simp only [probability_calibratedTest, Game.coe_advantage, Game.coe_succProbability, sq_abs]
   ring
 
 /-- Calibration is an ordinary PPT composition of its three supplied experiments. -/

Complexity/Crypto/Computational/Pseudoentropy/Basic.lean

@@ -9,6 +9,7 @@ module
 
 public import Complexity.Crypto.Computational.Basic
 public import Complexity.Probability.Entropy
+import Complexity.Languages.Probabilistic.Notation
 import Complexity.Tactic.PPT
 
 /-!
@@ -55,8 +56,6 @@ namespace Cslib.Crypto.Pseudoentropy
 
 open Probability Filter Turing.MultiTapeTM
 
-local notation "Pr[" p "]" => (Game.succProbability (ProbComp.eval p) : ℝ)
-
 /-- Predict the hidden bit from the public component of a sampled pair. -/
 def predictionGame (sample : ℕ → ProbComp (List Bool × Bool))
     (adversary : Distinguisher) (n : ℕ) : ProbComp Bool := do
@@ -129,7 +128,6 @@ theorem HasGap.eventually_error_ge {pair : SamplablePair} {gap : ℕ → ℝ}
   filter_upwards [hgap adversary hefficient] with n hn
   have hsum := PMF.toReal_true_add_toReal_false
     (ProbComp.eval (predictionGame pair.sample adversary n))
-  simp only [Game.succProbability, ENNReal.coe_toNNReal_eq_toReal] at hn
   linarith
 
 /-- A fair-bit predictor has zero correlation, so entropy plus the prediction gap cannot
@@ -140,8 +138,7 @@ theorem HasGap.eventually_entropy_add_gap_le_one {pair : SamplablePair} {gap : 
   have h := hgap (fun _ _ => ProbComp.uniform Bool) (by ppt)
   have hfair (n : ℕ) :
       Pr[predictionGame pair.sample (fun _ _ => ProbComp.uniform Bool) n] = 1 / 2 := by
-    simp [Game.succProbability, ENNReal.coe_toNNReal_eq_toReal, predictionGame,
-      ProbComp.eval_bind, ProbComp.eval_map, PMF.bind_apply, PMF.map_apply,
+    simp [predictionGame, ProbComp.eval_bind, ProbComp.eval_map, PMF.bind_apply, PMF.map_apply,
       PMF.uniformOfFintype_apply, ENNReal.tsum_mul_right, PMF.tsum_coe]
   filter_upwards [h] with n hn
   rw [hfair] at hn

Complexity/Crypto/Computational/Pseudoentropy/Boosting/Learner.lean

@@ -9,6 +9,7 @@ module
 
 public import Complexity.Crypto.Computational.Pseudoentropy.Boosting.Loop
 public import Complexity.Computability.Probabilistic.Selection
+import Complexity.Languages.Probabilistic.Notation
 import Complexity.Probability.PMF.Expect
 import Complexity.Tactic.PPT
 
@@ -52,8 +53,6 @@ namespace Cslib.Crypto.Pseudoentropy.Boosting
 
 open Probability BitString Turing.MultiTapeTM
 
-local notation "Pr[" p "]" => ENNReal.toReal (ProbComp.eval p true)
-
 variable {α : Type}
 
 /-- Run a trial on a freshly weighted example, with a fair baseline when its weight coin fails. -/
@@ -72,7 +71,7 @@ private theorem gate_probability (mask test : ProbComp Bool) :
   have hfair : Pr[ProbComp.uniform Bool] = 1 / 2 := by
     simp [PMF.uniformOfFintype_apply]
   rw [hfair]
-  change _ = 1 / 2 + (ProbComp.eval mask true).toReal * _
+  change _ = 1 / 2 + Pr[mask] * _
   nlinarith
 
 /-- Acceptance above a fair baseline is exactly the mask-weighted trial bias. -/

Complexity/Crypto/Computational/Pseudoentropy/DenseMask.lean

@@ -9,6 +9,7 @@ module
 
 public import Complexity.Crypto.Computational.Pseudoentropy.Basic
 public import Complexity.Crypto.Computational.Pseudoentropy.Masking
+import Complexity.Languages.Probabilistic.Notation
 import Complexity.Crypto.Computational.Pseudoentropy.Selection
 import Complexity.Crypto.Computational.Pseudoentropy.SequenceLearner
 import Complexity.Tactic.PPT
@@ -50,8 +51,6 @@ namespace Cslib.Crypto.Pseudoentropy.SamplablePair
 
 open Probability Probability.PMF BitString Boosting Filter Turing.MultiTapeTM
 
-local notation "Pr[" p "]" => ENNReal.toReal (ProbComp.eval p true)
-
 /-- All tests in a uniformly efficient polynomial-size family eventually admit dense soft masks
 with small distinguishing gap whenever their density is valid. The common eventual threshold
 allows arbitrary choices of index in the proof without supplying that choice to the program. -/
@@ -183,8 +182,7 @@ theorem HasGap.eventually_exists_indexed_mask {pair : SamplablePair} {gap : ℕ
       (fun value => pair.encode n value.1) Prod.snd (count n) (width n) (params n i) state
         (pair.encode n value.1)
         (hsize' n value (by simpa only [pair.eval_latentSample] using hvalue)))
-    (by simpa only [source, pair.eval_latentSample, Game.coe_advantage, Game.succProbability,
-      ENNReal.coe_toNNReal_eq_toReal]
+    (by simpa only [source, pair.eval_latentSample, Game.coe_advantage, Game.coe_succProbability]
       using hdistinguish)
   have hlaw : ProbComp.eval (predictionGame pair.sample (fun n => adversary n i) n) =
       ProbComp.eval (do

Complexity/Crypto/Computational/Pseudoentropy/Learning.lean

@@ -10,6 +10,7 @@ module
 public import Complexity.Crypto.Computational.Pseudoentropy.Masking
 public import Complexity.Crypto.Computational.Pseudoentropy.RepeatedExtraction
 public import Complexity.Crypto.Computational.Pseudoentropy.Boosting.Learner
+import Complexity.Languages.Probabilistic.Notation
 
 /-!
 # From sequence distinguishers to a learned predictor
@@ -46,8 +47,6 @@ namespace Cslib.Crypto.Pseudoentropy
 
 open Probability Probability.PMF BitString Boosting
 
-local notation "Pr[" p "]" => ENNReal.toReal (ProbComp.eval p true)
-
 variable {α β : Type}
 
 /-- The complete sequence gap is the dyadic coordinate count times the average weighted
@@ -80,9 +79,7 @@ theorem maskedSequence_validation_gap [Finite α]
         candidates >>= fun code => pure (predict code (observe value) == truth value))] :=
     congrArg (fun law : PMF Bool => (law true).toReal)
       (eval_weightedTrial_bind candidates source mask _)
-  have hgap := maskedSequence_prediction_gap source observe truth mask count test
-  simp only [Game.succProbability, ENNReal.coe_toNNReal_eq_toReal] at hgap
-  rw [hgap, hvalidation, weightedTrial_probability]
+  rw [maskedSequence_prediction_gap, hvalidation, weightedTrial_probability]
   simp only [add_sub_cancel_left]
   congr 1
   apply Finset.sum_congr rfl
@@ -167,7 +164,6 @@ theorem extractedSequence_learn_error_pow {Seed Output : Type} [Fintype α]
   have h := extractLabels_sequence_gap ((fun value => (observe value, truth value)) <$> source)
     (maskedSample source observe truth mask) count seed hash test ideal hclose
   have hgap' := (le_sub_iff_add_le.mpr hdistinguish).trans h
-  simpa only [Game.coe_advantage, Game.succProbability, ENNReal.coe_toNNReal_eq_toReal]
-    using hgap'
+  simpa only [Game.coe_advantage, Game.coe_succProbability] using hgap'
 
 end Cslib.Crypto.Pseudoentropy

Complexity/Crypto/Computational/Pseudoentropy/MaskedExtraction.lean

@@ -9,6 +9,7 @@ module
 
 public import Complexity.Crypto.Computational.Pseudoentropy.Masking
 public import Complexity.Crypto.Computational.Pseudoentropy.RepeatedExtraction
+import Complexity.Languages.Probabilistic.Notation
 
 /-!
 # Extracting fresh masked labels
@@ -46,8 +47,6 @@ open Probability Probability.PMF BitString
 
 open scoped NNReal
 
-local notation "Pr[" p "]" => ENNReal.toReal (ProbComp.eval p true)
-
 /-- Fresh masking preserves the complete public marginal. -/
 theorem maskedSample_map_fst {α β : Type} (source : ProbComp α)
     (observe : α → β) (truth : α → Bool) (mask : α → ProbComp Bool) :
@@ -64,7 +63,7 @@ theorem maskedSample_map_fst {α β : Type} (source : ProbComp α)
 probability at least `mass / 2`. Keeping the original label always has probability at least half. -/
 theorem maskBit_mass_ge (mask : ProbComp Bool) (truth bit : Bool) {mass : ℝ}
     (hmass : mass ≤ 1)
-    (hmask : 0 < (ProbComp.eval mask true).toReal → mass ≤ (ProbComp.eval mask true).toReal)
+    (hmask : 0 < Pr[mask] → mass ≤ Pr[mask])
     (hbit : bit ∈ (ProbComp.eval (maskBit mask truth)).support) :
     mass / 2 ≤ (ProbComp.eval (maskBit mask truth) bit).toReal := by
   have hpositive : 0 < (ProbComp.eval (maskBit mask truth) bit).toReal :=
@@ -87,8 +86,7 @@ theorem maskedSample_mass_ge {α β : Type} (source : ProbComp α)
     (hsource : ∀ value ∈ (ProbComp.eval source).support,
       sourceMass ≤ (ProbComp.eval source value).toReal)
     (hmask : ∀ value ∈ (ProbComp.eval source).support,
-      0 < (ProbComp.eval (mask value) true).toReal →
-        maskMass ≤ (ProbComp.eval (mask value) true).toReal)
+      0 < Pr[mask value] → maskMass ≤ Pr[mask value])
     (pair : β × Bool) (hpair : pair ∈ (ProbComp.eval
       (maskedSample source observe truth mask)).support) :
     sourceMass * (maskMass / 2) ≤