From cf8dbccd60691b3d60802b7242bc59d4d6e3a22a Mon Sep 17 00:00:00 2001 From: Marc Ilunga Date: Mon, 12 Oct 2026 17:16:49 +0100 Subject: [PATCH] Couplings of random systems MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A coupling of two PDSs is a joint distribution `J` of the two (`Distribution.IsCoupling J P Q`), with no new structure. New file `RandomSystems/Distance/Coupling.lean`: - `System.tr s σ n`: the transcript of a deterministic system with a strategy within `n` rounds (Lanzenberger–Maurer, Definition 7, printed p. 12), with `tr_eq_iff`: when the system answers the strategy's queries, its transcript is the only complete transcript it replies. - `PDS.sLaw_behavior_eq_fTransform`: for a strategy compatible with the random system of a PDS, the transcript law is the transformation of the PDS by the transcript map (footnote 9, printed p. 14; Definition 4, printed p. 10). - `PDS.statDist_sLaw_behavior_le_of_isCoupling`: under a coupling, the transcript laws are at statistical distance at most the probability that the two transcripts differ. - `PDS.transcriptDistance_behavior_le_of_isCoupling`: under a coupling, the transcript distance of the two random systems is at most the probability that the two systems differ, stated in ℝ≥0: the inequality of Theorem 2 (printed p. 15) for every coupling. THEORY.md §1.4 gets a paragraph on couplings; `#print axioms` lines in Tests/Axioms/Systems. The transcript of a deterministic system with a strategy replaces the run of an environment against a total resource (`TotRes`, `eRun`, `tr E n s` and their lemmas in `Distance/Transcript.lean`), which nothing used; one transcript function remains. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01E7GPy1oUx164NSZsxJT3N9 --- THEORY.md | 24 ++ src/RandomSystems.lean | 1 + src/RandomSystems/Distance/Coupling.lean | 263 +++++++++++++++++++++ src/RandomSystems/Distance/Transcript.lean | 97 -------- src/Tests/Axioms/Systems.lean | 6 +- 5 files changed, 293 insertions(+), 98 deletions(-) create mode 100644 src/RandomSystems/Distance/Coupling.lean diff --git a/THEORY.md b/THEORY.md index 9c8e26f..5270f2e 100644 --- a/THEORY.md +++ b/THEORY.md @@ -121,6 +121,26 @@ The [**behavior**][Domain.DistinguisherBehavior] of a probabilistic distinguishe probability of outputting 1 on each system, as the behavior of a PDC is its random system; the transcript distance [is also the largest advantage of a behavior][RandomSystem.transcriptDistance_eq_iSup_behavior]. +**Couplings**: the [transcript][System.tr] $`\mathrm{tr}(s, E, n)`$ of a deterministic system $`s`$ +with an environment $`E`$ within $`n`$ rounds is the sequence of their query–reply pairs +[1, Definition 7]. For an environment compatible with the random system $`R`$ of a PDS $`P`$, the +transcript law of $`R`$ [is the transformation][PDS.sLaw_behavior_eq_fTransform] of $`P`$ by +$`\mathrm{tr}(\cdot, E, n)`$ [1, Definition 4 and footnote 9]. A [coupling][IsCoupling] $`J`$ of +$`P`$ and a PDS $`Q`$ with random system $`S`$ therefore bounds the distance of the transcript laws +by the [probability that the transcripts differ][PDS.statDist_sLaw_behavior_le_of_isCoupling], and +the transcript distance by the +[probability that the systems differ][PDS.transcriptDistance_behavior_le_of_isCoupling]: + +```math +\delta\big(\mathrm{tr}(R, E, n),\ \mathrm{tr}(S, E, n)\big) +\le \Pr_{(s, t) \sim J}\big[\mathrm{tr}(s, E, n) \ne \mathrm{tr}(t, E, n)\big], +\qquad +\Delta(R, S) \le \Pr_{(s, t) \sim J}[s \ne t] . +``` + +The second bound holds for every coupling; [1, Theorem 2] states in addition that some +presentations of $`R`$ and $`S`$ have a coupling attaining it. + **Absorption**: [absorbing][DistinguisherBehavior.absorb] a PDC $`\alpha`$ into a behavior $`d`$ gives $`d \circ \alpha`$, which decides on a system as $`d`$ decides on $`\alpha`$ attached to it, $`\Pr[(d \circ \alpha)(R) = 1] = \Pr[d(\alpha R) = 1]`$. Absorbing a serial composition @@ -891,6 +911,10 @@ agreeing with a map on a finite set $`S`$: there are $`\lvert Y \rvert^{\lvert X [DistinguisherBehavior.advantage_triangle]: src/RandomSystems/Distance/Distinguisher.lean#L233 [DistinguisherBehavior.advantage_le_transcriptDistance]: src/RandomSystems/Distance/Distinguisher.lean#L238 [RandomSystem.transcriptDistance_eq_iSup_behavior]: src/RandomSystems/Distance/Distinguisher.lean#L246 +[System.tr]: src/RandomSystems/Distance/Coupling.lean#L50 +[PDS.sLaw_behavior_eq_fTransform]: src/RandomSystems/Distance/Coupling.lean#L165 +[PDS.statDist_sLaw_behavior_le_of_isCoupling]: src/RandomSystems/Distance/Coupling.lean#L213 +[PDS.transcriptDistance_behavior_le_of_isCoupling]: src/RandomSystems/Distance/Coupling.lean#L241 [DistinguisherBehavior.absorb]: src/RandomSystems/Distance/Distinguisher.lean#L291 [DistinguisherBehavior.absorb_comp]: src/RandomSystems/Distance/Distinguisher.lean#L304 [Domain.Distinguisher.exists_absorbAll]: src/RandomSystems/Distance/Distinguisher.lean#L265 diff --git a/src/RandomSystems.lean b/src/RandomSystems.lean index e8f092b..c9bd9fd 100644 --- a/src/RandomSystems.lean +++ b/src/RandomSystems.lean @@ -29,6 +29,7 @@ import RandomSystems.DDC.Serial import RandomSystems.DDC.SingleAlphabet import RandomSystems.DDC.Tensor import RandomSystems.Distance.Absorption +import RandomSystems.Distance.Coupling import RandomSystems.Distance.Decision import RandomSystems.Distance.Distinguisher import RandomSystems.Distance.ParallelObservation diff --git a/src/RandomSystems/Distance/Coupling.lean b/src/RandomSystems/Distance/Coupling.lean new file mode 100644 index 0000000..bb043a8 --- /dev/null +++ b/src/RandomSystems/Distance/Coupling.lean @@ -0,0 +1,263 @@ +import RandomSystems.Distance.Decision +import Probability.Coupling + +/-! +# Couplings of random systems + +The transcript of a deterministic system with a strategy within `n` rounds is the sequence of +query–reply pairs they exchange. For a strategy compatible with the random system of a PDS, the +transcript law of that random system is the transformation of the PDS by the transcript map. A +coupling of two PDSs is a joint distribution of the two; it bounds the statistical distance of +the transcript laws by the probability that the two sampled systems give different transcripts, +and the transcript distance of the two random systems by the probability that the two sampled +systems differ. Sources: Lanzenberger–Maurer, Definitions 4 and 7 (printed pp. 10, 12), +footnote 9 (printed p. 14), Definition 11 and Theorem 2 (printed p. 15). + +## Main definitions + +* `System.tr s σ n`: the transcript of the deterministic system `s` with `σ` within `n` rounds + +## Main results + +* `System.tr_eq_iff`: when `s` answers the queries of `σ`, its transcript is the only transcript + of `σ` within `n` rounds that `s` replies +* `PDS.sLaw_behavior_eq_fTransform`: the transcript law of the random system of a PDS is the + transformation of the PDS by the transcript map +* `PDS.statDist_sLaw_behavior_le_of_isCoupling`: under a coupling, the transcript laws are at + statistical distance at most the probability that the transcripts differ +* `PDS.transcriptDistance_behavior_le_of_isCoupling`: under a coupling, the transcript distance is + at most the probability that the systems differ +-/ + +namespace SystemAlgebra + +open Probability +open scoped NNReal + +variable {A B : Type} + +/-! ## The transcript of a deterministic system -/ + +namespace System + +open scoped Classical in +/-- **The transcript** of the deterministic system `s` with the strategy `σ` within `n` rounds +(Lanzenberger–Maurer, Definition 7, printed p. 12): "the sequence of pairs (x₁, y₁), (x₂, y₂), +…, (x_l, y_l), defined for i ≥ 1 by xᵢ = e(y₁, …, yᵢ₋₁) and yᵢ = s(x₁, …, xᵢ)", and "If +e(y₁, …, yᵢ₋₁) is undefined (the environment stops), the transcript ends and has length +l = i − 1." It also ends after `n` rounds, and when `s` does not answer the query, which a +compatible strategy never asks. -/ +noncomputable def tr (s : System A B) (σ : List B →. A) : ℕ → List (A × B) + | 0 => [] + | n + 1 => + -- The transcript `h` of the first `n` rounds, extended by the query `x` of `σ` and the + -- reply of `s` to it, if both are defined. + let h := tr s σ n + if hx : (σ (h.map Prod.snd)).Dom then + let x := (σ (h.map Prod.snd)).get hx + if hy : (s (h.map Prod.fst ++ [x])).Dom then h ++ [(x, (s (h.map Prod.fst ++ [x])).get hy)] + else h + else h + +variable {s : System A B} {σ : List B →. A} + +/-- The queries of the transcript follow `σ`. -/ +theorem cons_tr (n : ℕ) : Cons σ (s.tr σ n) := by + induction n with + | zero => exact cons_nil + | succ n ih => + rw [tr] + dsimp only + split_ifs with hx hy + -- A new round: its query is the strategy's query after the replies so far. + · exact cons_snoc.mpr ⟨ih, Part.get_mem hx⟩ + all_goals exact ih + +/-- The system gives the replies of its transcript. -/ +theorem replies_tr (n : ℕ) : + Replies s ((s.tr σ n).map Prod.fst) ((s.tr σ n).map Prod.snd) := by + induction n with + | zero => exact replies_nil s + | succ n ih => + rw [tr] + dsimp only + split_ifs with hx hy + -- A new round: its reply is the system's answer to the queries so far. + · simp only [List.map_append, List.map_singleton] + exact replies_snoc.mpr ⟨ih, Part.get_eq_iff_eq_some.mp rfl⟩ + all_goals exact ih + +/-- **The transcript is complete** within `n` rounds when `s` answers every query `σ` asks after +it: it has `n` rounds, or the strategy has stopped. -/ +theorem good_tr {n : ℕ} + (hs : ∀ x ∈ σ ((s.tr σ n).map Prod.snd), (s ((s.tr σ n).map Prod.fst ++ [x])).Dom) : + Good σ n (s.tr σ n) := by + -- By induction: the transcript has `n` rounds, or it ended early and `s` does not answer + -- the next query of `σ` (vacuously so when `σ` has stopped). + have key : ∀ m, (s.tr σ m).length = m ∨ ((s.tr σ m).length < m ∧ + ∀ x ∈ σ ((s.tr σ m).map Prod.snd), ¬ (s ((s.tr σ m).map Prod.fst ++ [x])).Dom) := by + intro m + induction m with + | zero => exact Or.inl rfl + | succ m ih => + rw [tr] + dsimp only + split_ifs with hx hy + -- A new round: the transcript did not end early, since `s` answered. + · refine Or.inl ?_ + rcases ih with hl | ⟨-, hn⟩ + · simp [hl] + · exact absurd hy (hn _ (Part.get_mem hx)) + -- `s` does not answer the query `x` of `σ`, its only query. + · refine Or.inr ⟨by rcases ih with hl | ⟨hl, -⟩ <;> omega, fun x hx' hd => hy ?_⟩ + rwa [Part.get_eq_of_mem hx' hx] + -- `σ` has stopped. + · exact Or.inr ⟨by rcases ih with hl | ⟨hl, -⟩ <;> omega, + fun x hx' => absurd (Part.dom_iff_mem.mpr ⟨x, hx'⟩) hx⟩ + refine ⟨cons_tr n, ?_⟩ + rcases key n with hl | ⟨hl, hn⟩ + · exact Or.inl hl + -- Ended early: as `s` answers every query of `σ`, the strategy must have stopped. + · exact Or.inr ⟨hl, fun hx => hn _ (Part.get_mem hx) (hs _ (Part.get_mem hx))⟩ + +/-- **The transcript is the only complete transcript the system replies**: when `s` answers +every query `σ` asks after its transcript, a transcript of `σ` complete within `n` rounds is +replied by `s` exactly when it is the transcript of `s`. -/ +theorem tr_eq_iff {n : ℕ} + (hs : ∀ x ∈ σ ((s.tr σ n).map Prod.snd), (s ((s.tr σ n).map Prod.fst ++ [x])).Dom) + (h : List (A × B)) : + s.tr σ n = h ↔ Good σ n h ∧ Replies s (h.map Prod.fst) (h.map Prod.snd) := by + refine ⟨fun he => he ▸ ⟨good_tr hs, replies_tr n⟩, fun ⟨hg, hr⟩ => ?_⟩ + -- Both `h` and the transcript of `s` are interaction transcripts of `s` with `σ`. + have hg' := good_tr hs + have tt := transcript_of_cons hg'.1 (replies_tr (s := s) n) + have th := transcript_of_cons hg.1 hr + -- Their queries and replies agree: both have `n` rounds, or both end when `σ` stops; one + -- with `n` rounds and one ending earlier is impossible, since a transcript ending when `σ` + -- stops is at least as long as any other. + have he : (s.tr σ n).map Prod.fst = h.map Prod.fst ∧ + (s.tr σ n).map Prod.snd = h.map Prod.snd := by + rcases hg'.2 with hl | ⟨hl, hd⟩ <;> rcases hg.2 with hl' | ⟨hl', hd'⟩ + · exact tt.eq_of_length_eq th (by simp [hl, hl']) + · have := th.length_le_of_stopped hd' tt + simp only [List.length_map] at this + omega + · have := tt.length_le_of_stopped hd th + simp only [List.length_map] at this + omega + · exact tt.eq_of_stopped th hd hd' + -- A list of pairs is determined by its queries and its replies. + exact (List.zip_of_prod he.1 he.2).trans (List.zip_of_prod rfl rfl).symm + +end System + +/-! ## The transcript law of a PDS -/ + +namespace PDS + +variable [Fintype A] [Fintype B] {D : Domain A B} + +/-- **The transcript law of the random system of a PDS is the transformation of the PDS by the +transcript** (Lanzenberger–Maurer, footnote 9, printed p. 14): "tr(S, e) denotes the +tr(·, e)-transformation of the distribution S (see Definition 4)". For a strategy `σ` +compatible with the random system of `P`, the transcript law within `n` rounds is the +pushforward of `P` by the transcript of the sampled system with `σ` within `n` rounds. -/ +theorem sLaw_behavior_eq_fTransform (P : PDS A B D) (hP : P.isProbDist) {σ : List B →. A} + (hC : (PDS.behavior P hP).Compatible σ) (n : ℕ) : + (PDS.behavior P hP).sLaw σ n = Distribution.fTransform (fun s => s.1.tr σ n) P := by + -- 1. A sampled system answers every query of `σ` after its transcript: the transcript has + -- probability at least the weight of the sample, so the compatible `σ` asks an admitted + -- query, and the sample has the domain `D`. + have hans : ∀ s ∈ P.support, ∀ x ∈ σ ((s.1.tr σ n).map Prod.snd), + (s.1 ((s.1.tr σ n).map Prod.fst ++ [x])).Dom := by + intro s hs x hx + have hpos : PDS.behavior P hP (s.1.tr σ n) ≠ 0 := by + rw [PDS.behavior_mass] + refine ne_of_gt (lt_of_lt_of_le + (lt_of_le_of_ne (hP.1 s) (Ne.symm (Finsupp.mem_support_iff.mp hs))) ?_) + exact Distribution.apply_le_mass hP.1 (P := fun t => Replies t.1 _ _) + (System.replies_tr n) + exact (s.2.2 _ x (System.replies_tr n)).mpr (hC _ x (System.cons_tr n) hpos hx) + -- 2. Compare the two laws at each transcript `h`: the left side is the mass of the samples + -- replying `h` if `h` is complete for `σ` within `n` rounds, and zero otherwise; the right + -- side is the mass of the samples whose transcript is `h`. + ext h + rw [RandomSystem.sLaw_apply, PDS.behavior_mass, Distribution.fTransform_apply_eq_mass] + by_cases hg : Good σ n h + -- A complete `h`: the samples replying `h` are those whose transcript is `h`. + · rw [if_pos hg] + exact Distribution.mass_congr_of_support P fun s hs => + ⟨fun hr => (System.tr_eq_iff (hans s hs) h).mpr ⟨hg, hr⟩, + fun ht => ((System.tr_eq_iff (hans s hs) h).mp ht).2⟩ + -- An incomplete `h` is the transcript of no sample. + · rw [if_neg hg] + refine ((Distribution.mass_congr_of_support P (Q := fun _ => False) fun s hs => + ⟨fun ht => hg ((System.tr_eq_iff (hans s hs) h).mp ht).1, False.elim⟩).trans + (Distribution.mass_eq_zero_of_forall_not P fun _ hf => hf)).symm + +/-! ## Couplings -/ + +/-- **A coupling bounds the distance of the transcript laws.** If `J` is a joint distribution +of the PDSs `P` and `Q`, then for a strategy `σ` compatible with both random systems, their +transcript laws within `n` rounds are at statistical distance at most the probability under `J` +that the two sampled systems give different transcripts: + +``` + σ ⇄ s gives tr(s, σ, n) s ~ P + (s, t) ~ J + σ ⇄ t gives tr(t, σ, n) t ~ Q +``` + +Both transcript laws are transformations of `J` (`sLaw_behavior_eq_fTransform`), which agree +where the two transcripts agree. -/ +theorem statDist_sLaw_behavior_le_of_isCoupling {P Q : PDS A B D} (hP : P.isProbDist) + (hQ : Q.isProbDist) + {J : Distribution ({s : System A B // IsDDS s ∧ HasDomain D s} × + {s : System A B // IsDDS s ∧ HasDomain D s})} + (hJ : Distribution.IsCoupling J P Q) (hJ0 : J.NonNeg) {σ : List B →. A} + (hCP : (PDS.behavior P hP).Compatible σ) (hCQ : (PDS.behavior Q hQ).Compatible σ) + (n : ℕ) : + statDist ((PDS.behavior P hP).sLaw σ n) ((PDS.behavior Q hQ).sLaw σ n) ≤ + J.mass fun st => st.1.1.tr σ n ≠ st.2.1.tr σ n := by + -- The transcript law of `P` is the transformation of `J` by the transcript of the first + -- system, since `P` is the first marginal of `J`; the same for `Q` and the second. + rw [sLaw_behavior_eq_fTransform P hP hCP, sLaw_behavior_eq_fTransform Q hQ hCQ, ← hJ.1, + ← hJ.2, Distribution.fTransform_fTransform, Distribution.fTransform_fTransform] + -- Two transformations of one law that agree off an event are within its probability. + exact statDist_fTransform_le_mass_of_eq_off hJ0 _ _ _ fun _ _ h => not_not.mp h + +variable {I : Type} [Fintype I] {X Y : I → Type} [∀ i, Fintype (X i)] [∀ i, Fintype (Y i)] + {𝒟 : Domain (Σ i, X i) (Σ i, Y i)} + +/-- **A coupling bounds the transcript distance** (the inequality of Lanzenberger–Maurer, +Theorem 2, printed p. 15, for an arbitrary coupling): "For any two random systems S and T there +exist PDS S ∈ S and T ∈ T with a joint distribution (or coupling) such that +Adv(S, T) = Pr(S ≠ T)". If `J` is a joint distribution of the PDSs `P` and `Q` and the +probability under `J` that the two sampled systems differ is at most `b`, the transcript +distance of the random systems of `P` and `Q` is at most `b`. The paper obtains Theorem 2 as "an +immediate consequence of Theorem 1 and the classical Coupling Lemma (Lemma 4)"; here, under +every environment the transcript laws are within the probability that the transcripts differ +(`statDist_sLaw_behavior_le_of_isCoupling`), and equal systems give equal transcripts. -/ +theorem transcriptDistance_behavior_le_of_isCoupling {P Q : PDS (Σ i, X i) (Σ i, Y i) 𝒟} + (hP : P.isProbDist) (hQ : Q.isProbDist) + (hPR : (PDS.behavior P hP).RepliesAtQueriedInterface) + (hQR : (PDS.behavior Q hQ).RepliesAtQueriedInterface) + {J : Distribution ({s : System (Σ i, X i) (Σ i, Y i) // IsDDS s ∧ HasDomain 𝒟 s} × + {s : System (Σ i, X i) (Σ i, Y i) // IsDDS s ∧ HasDomain 𝒟 s})} + (hJ : Distribution.IsCoupling J P Q) (hJ0 : J.NonNeg) {b : ℝ≥0} + (hb : Distribution.offDiagonalMass J ≤ b) : + (PDS.behavior P hP).transcriptDistance (PDS.behavior Q hQ) ≤ b := by + -- It suffices to bound the transcript laws under each query-bounded environment `E` + -- compatible with the domain; such an `E` is compatible with both random systems. + refine RandomSystem.transcriptDistance_le fun E n _ hc => ?_ + calc statDist ((PDS.behavior P hP).sLaw E.1 n) ((PDS.behavior Q hQ).sLaw E.1 n) + ≤ J.mass fun st => st.1.1.tr E.1 n ≠ st.2.1.tr E.1 n := + statDist_sLaw_behavior_le_of_isCoupling hP hQ hJ hJ0 (hc _ hPR) (hc _ hQR) n + -- Different transcripts come from different systems. + _ ≤ Distribution.offDiagonalMass J := + Distribution.mass_mono hJ0 fun st hne he => hne (by rw [he]) + _ ≤ b := hb + +end PDS + +end SystemAlgebra diff --git a/src/RandomSystems/Distance/Transcript.lean b/src/RandomSystems/Distance/Transcript.lean index a1d9c18..da0baa4 100644 --- a/src/RandomSystems/Distance/Transcript.lean +++ b/src/RandomSystems/Distance/Transcript.lean @@ -13,7 +13,6 @@ environment. Source: Lanzenberger, Definitions 2.11–2.12 and 2.26 (printed pp. ## Main definitions -* `eRun`, `tr E n s`: the run of an environment against a total system * `envProbe E A`: an environment with a transcript test, as a distinguisher * `ddeOf hD`: the queries of a distinguisher, as an environment * `DPort.map`, `trigMap`, `decMap`: relabeling a distinguisher @@ -37,49 +36,6 @@ open Probability (Distribution statDist) variable {X Y K : Type} -/-! ## The run of an environment against a total system -/ - -section Run - -/-- Total resources on labels `K`: the samples of a probabilistic resource. -/ -abbrev TotRes (X Y K : Type) := {R : SingleAlphabetSystem X Y K // TotalResource R} - -/-- The reply of a total resource to a nonempty history. -/ -noncomputable def reply (s : TotRes X Y K) (h : List (Σ _ : K, X)) (hne : h ≠ []) : Σ _ : K, Y := - (s.1 h).get ((s.2.1 h).mpr hne) - -variable (e : List (Σ _ : K, Y) →. Σ _ : K, X) (s : TotRes X Y K) - -/-- The first `n` rounds of the environment `e` against `s`: queries and replies. -/ -noncomputable def eRun : ℕ → List (Σ _ : K, X) × List (Σ _ : K, Y) - | 0 => ([], []) - | n + 1 => - let p := eRun n - if hd : (e p.2).Dom then - (p.1 ++ [(e p.2).get hd], - p.2 ++ [reply s (p.1 ++ [(e p.2).get hd]) (by simp)]) - else p - -theorem eRun_succ_of_dom (n : ℕ) (hd : (e (eRun e s n).2).Dom) : - eRun e s (n + 1) = ((eRun e s n).1 ++ [(e (eRun e s n).2).get hd], - (eRun e s n).2 ++ [reply s ((eRun e s n).1 ++ [(e (eRun e s n).2).get hd]) (by simp)]) := by - simp only [eRun, dif_pos hd] - -theorem eRun_succ_of_not_dom (n : ℕ) (hd : ¬ (e (eRun e s n).2).Dom) : - eRun e s (n + 1) = eRun e s n := by - simp only [eRun, dif_neg hd] - -theorem reply_mem (h : List (Σ _ : K, X)) (x : Σ _ : K, X) : - reply s (h ++ [x]) (by simp) ∈ s.1 (h ++ [x]) := - Part.get_mem _ - -end Run - -/-- The transcript of `s` with `E` after at most `n` rounds. -/ -noncomputable def tr (E : DDE (Σ _ : K, X) (Σ _ : K, Y)) (n : ℕ) (s : TotRes X Y K) : - List (Σ _ : K, X) × List (Σ _ : K, Y) := - eRun E.1 s n - /-! ## The queries of a transcript are a function of its replies -/ section Queries @@ -97,38 +53,6 @@ theorem qsOf_snoc {A B : Type} {e : List B →. A} {ys : List B} {x y} rw [List.take_append_of_le_length (List.mem_range.mp hk).le] · simp [List.take_left', Part.toOption_eq_some_iff.mpr hx] -theorem eRun_fst (e : List (Σ _ : K, Y) →. Σ _ : K, X) (s : TotRes X Y K) : - ∀ m, (eRun e s m).1 = qsOf e (eRun e s m).2 := by - intro m - induction m with - | zero => rfl - | succ m ih => - by_cases hd : (e (eRun e s m).2).Dom - · rw [eRun_succ_of_dom e s m hd] - simp only - rw [qsOf_snoc (Part.get_mem hd), ih] - · rw [eRun_succ_of_not_dom e s m hd, ih] - -theorem tr_fst (E : DDE (Σ _ : K, X) (Σ _ : K, Y)) (n : ℕ) (s : TotRes X Y K) : - (tr E n s).1 = qsOf E.1 (tr E n s).2 := - eRun_fst _ _ _ - -/-- Runs of two environments that agree along the run coincide. -/ -theorem eRun_congr {e e' : List (Σ _ : K, Y) →. Σ _ : K, X} (s : TotRes X Y K) - (H : ∀ m, e' (eRun e s m).2 = e (eRun e s m).2) : ∀ m, eRun e' s m = eRun e s m := by - intro m - induction m with - | zero => rfl - | succ m ih => - by_cases hd : (e (eRun e s m).2).Dom - · have hd' : (e' (eRun e' s m).2).Dom := by rw [ih, H m]; exact hd - rw [eRun_succ_of_dom e' s m hd', eRun_succ_of_dom e s m hd] - have hx : ∀ h, (e' (eRun e s m).2).get h = (e (eRun e s m).2).get hd := fun h => - Part.get_eq_of_mem (by rw [H m]; exact Part.get_mem hd) h - simp only [ih, hx] - · have hd' : ¬ (e' (eRun e' s m).2).Dom := by rw [ih, H m]; exact hd - rw [eRun_succ_of_not_dom e' s m hd', eRun_succ_of_not_dom e s m hd, ih] - end Queries /-! ## An environment with a test is a decision-producing distinguisher -/ @@ -265,27 +189,6 @@ theorem envOf_envProbe {ys : List (Σ i, Yi i)} (hv : EFits E.1 ys) : end EnvProbe -section TotalEnvProbe - -variable {E : DDE (Σ _ : K, X) (Σ _ : K, Y)} - {A : List (Σ _ : K, X) × List (Σ _ : K, Y) → Prop} {n : ℕ} - -theorem eRun_fits (s : TotRes X Y K) : ∀ m, EFits E.1 (eRun E.1 s m).2 := by - intro m - induction m with - | zero => exact EFits.nil - | succ m ih => - by_cases hd : (E.1 (eRun E.1 s m).2).Dom - · rw [eRun_succ_of_dom _ s m hd] - exact ih.snoc (Part.get_mem hd) (s.2.2 _ _ _ (reply_mem s _ _)) - · rw [eRun_succ_of_not_dom _ s m hd]; exact ih - -theorem eRun_envProbe (s : TotRes X Y K) (m : ℕ) : - eRun (envOf (envProbe E A)) s m = eRun E.1 s m := - eRun_congr s (fun m => envOf_envProbe (eRun_fits s m)) m - -end TotalEnvProbe - /-! ## A distinguisher's bit is determined by its transcript -/ section OfDDD diff --git a/src/Tests/Axioms/Systems.lean b/src/Tests/Axioms/Systems.lean index 74f6106..eff8f80 100644 --- a/src/Tests/Axioms/Systems.lean +++ b/src/Tests/Axioms/Systems.lean @@ -129,6 +129,11 @@ parallel composition, distance and games, and the counterexamples, depend only o #print axioms SystemAlgebra.close_apply #print axioms SystemAlgebra.absorbAll_isDDD +-- RandomSystems.Distance.Coupling +#print axioms SystemAlgebra.PDS.sLaw_behavior_eq_fTransform +#print axioms SystemAlgebra.PDS.statDist_sLaw_behavior_le_of_isCoupling +#print axioms SystemAlgebra.PDS.transcriptDistance_behavior_le_of_isCoupling + -- RandomSystems.Distance.Decision #print axioms SystemAlgebra.RandomSystem.statDist_le_transcriptDistance #print axioms SystemAlgebra.Domain.decisionCompatible_iff_deterministic @@ -157,7 +162,6 @@ parallel composition, distance and games, and the counterexamples, depend only o -- RandomSystems.Distance.Transcript #print axioms SystemAlgebra.IsDDD.relabel -#print axioms SystemAlgebra.eRun_fst #print axioms SystemAlgebra.envProbe_isDDD #print axioms SystemAlgebra.ddeOf_bounded