CommunicationComplexity.Deterministic.Subprotocol

inductive CommunicationComplexity.Deterministic.Protocol.IsSubprotocol {X : Type u_1} {Y : Type u_2} {α : Type u_3} :

IsSubprotocol s p means s is a (rooted) subtree of protocol p.

refl {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) : p.IsSubprotocol p
alice_false {X : Type u_1} {Y : Type u_2} {α : Type u_3} (f : X → Bool) (P : Bool → Protocol X Y α) (s : Protocol X Y α) : s.IsSubprotocol (P false) → s.IsSubprotocol (alice f P)
alice_true {X : Type u_1} {Y : Type u_2} {α : Type u_3} (f : X → Bool) (P : Bool → Protocol X Y α) (s : Protocol X Y α) : s.IsSubprotocol (P true) → s.IsSubprotocol (alice f P)
bob_false {X : Type u_1} {Y : Type u_2} {α : Type u_3} (f : Y → Bool) (P : Bool → Protocol X Y α) (s : Protocol X Y α) : s.IsSubprotocol (P false) → s.IsSubprotocol (bob f P)
bob_true {X : Type u_1} {Y : Type u_2} {α : Type u_3} (f : Y → Bool) (P : Bool → Protocol X Y α) (s : Protocol X Y α) : s.IsSubprotocol (P true) → s.IsSubprotocol (bob f P)

Instances For

theorem CommunicationComplexity.Deterministic.Protocol.IsSubprotocol.trans {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s t u : Protocol X Y α} (h1 : s.IsSubprotocol t) (h2 : t.IsSubprotocol u) :

s.IsSubprotocol u

Transitivity of subprotocol embeddings.

source

theorem CommunicationComplexity.Deterministic.Protocol.balanced_subprotocol {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) (hn : 1 < p.numLeaves) :

∃ (s : Protocol X Y α), s.IsSubprotocol p ∧ 3 * s.numLeaves ≥ p.numLeaves ∧ 3 * s.numLeaves < 2 * p.numLeaves

Protocol-level version of R&Y Lemma 1.8: if a protocol has more than 1 leaf there is a subprotocol with a reasonable number of leaves.

source

inductive CommunicationComplexity.Deterministic.Protocol.SubprotocolPath {X : Type u_1} {Y : Type u_2} {α : Type u_3} :

Protocol X Y α → Protocol X Y α → Type (max (max u_1 u_2) u_3)

Type-valued witness for a subtree embedding, used for data-carrying recursion. It is a witness that s is a subprotocol of p containing the choices from the root of p to the root of s.

refl {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) : p.SubprotocolPath p
alice_false {X : Type u_1} {Y : Type u_2} {α : Type u_3} (f : X → Bool) (P : Bool → Protocol X Y α) (s : Protocol X Y α) : s.SubprotocolPath (P false) → s.SubprotocolPath (alice f P)
alice_true {X : Type u_1} {Y : Type u_2} {α : Type u_3} (f : X → Bool) (P : Bool → Protocol X Y α) (s : Protocol X Y α) : s.SubprotocolPath (P true) → s.SubprotocolPath (alice f P)
bob_false {X : Type u_1} {Y : Type u_2} {α : Type u_3} (f : Y → Bool) (P : Bool → Protocol X Y α) (s : Protocol X Y α) : s.SubprotocolPath (P false) → s.SubprotocolPath (bob f P)
bob_true {X : Type u_1} {Y : Type u_2} {α : Type u_3} (f : Y → Bool) (P : Bool → Protocol X Y α) (s : Protocol X Y α) : s.SubprotocolPath (P true) → s.SubprotocolPath (bob f P)

Instances For

source

def CommunicationComplexity.Deterministic.Protocol.SubprotocolPath.toIsSubprotocol {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} :

∀ (a : s.SubprotocolPath p), s.IsSubprotocol p

Every SubprotocolPath induces an IsSubprotocol proof.

Equations

⋯ = ⋯

Instances For

source

theorem CommunicationComplexity.Deterministic.Protocol.path_exists_of_isSubprotocol {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.IsSubprotocol p) :

Nonempty (s.SubprotocolPath p)

If s is a subprotocol of p, then there is a path from the root of p to the root of s.

source

noncomputable def CommunicationComplexity.Deterministic.Protocol.choosePath {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.IsSubprotocol p) :

s.SubprotocolPath p

Classical choice of a witness (a SubprotocolPath) from a proof that something is a Subprotocol.

Equations

CommunicationComplexity.Deterministic.Protocol.choosePath hsp = Classical.choice ⋯

Instances For

source

theorem CommunicationComplexity.Deterministic.Protocol.SubprotocolPath.numLeaves_le {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.SubprotocolPath p) :

s.numLeaves ≤ p.numLeaves

A SubprotocolPath won't have any more leaves than its parent.

source

def CommunicationComplexity.Deterministic.Protocol.reachXPath {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.SubprotocolPath p) :

Set X

Alice-side predicate set for the inputs that reach a chosen subprotocol path.

Equations

One or more equations did not get rendered due to their size.
CommunicationComplexity.Deterministic.Protocol.reachXPath (CommunicationComplexity.Deterministic.Protocol.SubprotocolPath.refl s) = Set.univ

Instances For

source

def CommunicationComplexity.Deterministic.Protocol.reachYPath {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.SubprotocolPath p) :

Set Y

Bob-side predicate set for the inputs that reach a chosen subprotocol path.

Equations

One or more equations did not get rendered due to their size.
CommunicationComplexity.Deterministic.Protocol.reachYPath (CommunicationComplexity.Deterministic.Protocol.SubprotocolPath.refl s) = Set.univ

Instances For

source

def CommunicationComplexity.Deterministic.Protocol.reachesPath {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.SubprotocolPath p) (x : X) (y : Y) :

Prop

A Prop which states that inputs x : X and y : Y will get you to a particular SubprotocolPath of p.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def CommunicationComplexity.Deterministic.Protocol.reachX {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.IsSubprotocol p) :

Set X

The set of Alice's inputs that reach any subprotocol path to the given subprotocol.

Equations

CommunicationComplexity.Deterministic.Protocol.reachX hsp = CommunicationComplexity.Deterministic.Protocol.reachXPath (CommunicationComplexity.Deterministic.Protocol.choosePath hsp)

Instances For

source

def CommunicationComplexity.Deterministic.Protocol.reachY {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.IsSubprotocol p) :

Set Y

The set of Bob's inputs that reach any subprotocol path to the given subprotocol.

Equations

CommunicationComplexity.Deterministic.Protocol.reachY hsp = CommunicationComplexity.Deterministic.Protocol.reachYPath (CommunicationComplexity.Deterministic.Protocol.choosePath hsp)

Instances For

source

def CommunicationComplexity.Deterministic.Protocol.reaches {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.IsSubprotocol p) (x : X) (y : Y) :

Prop

A Prop which states that on input x : X and y : Y the protocol p reaches the subprotocol s.

Equations

CommunicationComplexity.Deterministic.Protocol.reaches hsp x y = (x ∈ CommunicationComplexity.Deterministic.Protocol.reachX hsp ∧ y ∈ CommunicationComplexity.Deterministic.Protocol.reachY hsp)

Instances For

source

theorem CommunicationComplexity.Deterministic.Protocol.subprotocol_run_eq_of_reachesPath {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.SubprotocolPath p) {x : X} {y : Y} (hxy : reachesPath hsp x y) :

p.run x y = s.run x y

If on input x,y the protocol reaches subprotocolpath s of p, then running s and running p produce the same output.

source

theorem CommunicationComplexity.Deterministic.Protocol.subprotocol_run_eq_of_reaches {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.IsSubprotocol p) {x : X} {y : Y} (hxy : reaches hsp x y) :

p.run x y = s.run x y

If on input x,y the protocol reaches subprotocol s of p, then running s and running p produce the same output.

source

def CommunicationComplexity.Deterministic.Protocol.chooseOutput {X : Type u_1} {Y : Type u_2} {α : Type u_3} :

Protocol X Y α → α

Pick a canonical output value from a protocol (leftmost leaf).

Equations

Instances For

source

def CommunicationComplexity.Deterministic.Protocol.erasePath {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.SubprotocolPath p) :

Protocol X Y α

Gives you a protocol which is just p with the subprotocol s collapsed to a single leaf, and the value at that leaf is the leftmost leaf of s.

We need subprotocolpath because we need to find s, and that's how we do it.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem CommunicationComplexity.Deterministic.Protocol.erasePath_numLeaves {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.SubprotocolPath p) :

(erasePath hsp).numLeaves = p.numLeaves - s.numLeaves + 1

After we erase s from p, the resulting protocol has p.numLeaves - s.numLeaves + 1 leaves.

source

theorem CommunicationComplexity.Deterministic.Protocol.erasePath_run_outside {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.SubprotocolPath p) {x : X} {y : Y} (hxy : ¬reachesPath hsp x y) :

(erasePath hsp).run x y = p.run x y

If the input doesn't reach a subprotocolpath s, then running p on that input is the same as running p with s erased.

source

noncomputable def CommunicationComplexity.Deterministic.Protocol.erase {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.IsSubprotocol p) :

Protocol X Y α

Subprotocol not-path versions of the above.

Equations

CommunicationComplexity.Deterministic.Protocol.erase hsp = CommunicationComplexity.Deterministic.Protocol.erasePath (CommunicationComplexity.Deterministic.Protocol.choosePath hsp)

Instances For

source

theorem CommunicationComplexity.Deterministic.Protocol.erase_numLeaves {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.IsSubprotocol p) :

(erase hsp).numLeaves = p.numLeaves - s.numLeaves + 1

source

theorem CommunicationComplexity.Deterministic.Protocol.erase_run_outside {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.IsSubprotocol p) {x : X} {y : Y} (hxy : ¬reaches hsp x y) :

(erase hsp).run x y = p.run x y

source

def CommunicationComplexity.Deterministic.Protocol.deletePath {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.SubprotocolPath p) :

Option (Protocol X Y α)

Delete a selected subtree by splicing; returns none only at the root case.

Equations

One or more equations did not get rendered due to their size.
CommunicationComplexity.Deterministic.Protocol.deletePath (CommunicationComplexity.Deterministic.Protocol.SubprotocolPath.refl s) = none

Instances For

source

theorem CommunicationComplexity.Deterministic.Protocol.deletePath_ne_none_of_lt {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.SubprotocolPath p) (hlt : s.numLeaves < p.numLeaves) :

deletePath hsp ≠ none

source

theorem CommunicationComplexity.Deterministic.Protocol.deletePath_exists_of_lt {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.SubprotocolPath p) (hlt : s.numLeaves < p.numLeaves) :

∃ (q : Protocol X Y α), deletePath hsp = some q

source

noncomputable def CommunicationComplexity.Deterministic.Protocol.prunePath {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.SubprotocolPath p) (hlt : s.numLeaves < p.numLeaves) :

Protocol X Y α

Equations

CommunicationComplexity.Deterministic.Protocol.prunePath hsp hlt = Classical.choose ⋯

Instances For

source

theorem CommunicationComplexity.Deterministic.Protocol.prunePath_spec {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.SubprotocolPath p) (hlt : s.numLeaves < p.numLeaves) :

deletePath hsp = some (prunePath hsp hlt)

source

theorem CommunicationComplexity.Deterministic.Protocol.eq_of_deletePath_none {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.SubprotocolPath p) (hnone : deletePath hsp = none) :

s = p

source

theorem CommunicationComplexity.Deterministic.Protocol.deletePath_numLeaves_of_some {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.SubprotocolPath p) {q : Protocol X Y α} (hq : deletePath hsp = some q) :

q.numLeaves = p.numLeaves - s.numLeaves

source

theorem CommunicationComplexity.Deterministic.Protocol.prunePath_numLeaves_of_lt {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.SubprotocolPath p) (hlt : s.numLeaves < p.numLeaves) :

(prunePath hsp hlt).numLeaves = p.numLeaves - s.numLeaves

source

theorem CommunicationComplexity.Deterministic.Protocol.reachesPath_of_deletePath_none {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.SubprotocolPath p) (hnone : deletePath hsp = none) (x : X) (y : Y) :

reachesPath hsp x y

source

theorem CommunicationComplexity.Deterministic.Protocol.deletePath_run_outside_of_some {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.SubprotocolPath p) {q : Protocol X Y α} (hq : deletePath hsp = some q) {x : X} {y : Y} (hxy : ¬reachesPath hsp x y) :

q.run x y = p.run x y

source

theorem CommunicationComplexity.Deterministic.Protocol.prunePath_run_outside_of_lt {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.SubprotocolPath p) (hlt : s.numLeaves < p.numLeaves) {x : X} {y : Y} (hxy : ¬reachesPath hsp x y) :

(prunePath hsp hlt).run x y = p.run x y

source

noncomputable def CommunicationComplexity.Deterministic.Protocol.prune {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.IsSubprotocol p) (hlt : s.numLeaves < p.numLeaves) :

Protocol X Y α

Equations

CommunicationComplexity.Deterministic.Protocol.prune hsp hlt = CommunicationComplexity.Deterministic.Protocol.prunePath (CommunicationComplexity.Deterministic.Protocol.choosePath hsp) hlt

Instances For

source

theorem CommunicationComplexity.Deterministic.Protocol.prune_numLeaves_of_lt {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.IsSubprotocol p) (hlt : s.numLeaves < p.numLeaves) :

(prune hsp hlt).numLeaves = p.numLeaves - s.numLeaves

source

theorem CommunicationComplexity.Deterministic.Protocol.prune_run_outside_of_lt {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.IsSubprotocol p) (hlt : s.numLeaves < p.numLeaves) {x : X} {y : Y} (hxy : ¬reaches hsp x y) :

(prune hsp hlt).run x y = p.run x y

source

noncomputable def CommunicationComplexity.Deterministic.Protocol.testSubprotocol {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.IsSubprotocol p) (qIn qOut : Protocol X Y α) :

Protocol X Y α

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem CommunicationComplexity.Deterministic.Protocol.testSubprotocol_complexity {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.IsSubprotocol p) (qIn qOut : Protocol X Y α) :

(testSubprotocol hsp qIn qOut).complexity = 2 + max qIn.complexity qOut.complexity

source

theorem CommunicationComplexity.Deterministic.Protocol.testSubprotocol_run_inside {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p qIn qOut : Protocol X Y α} (hsp : s.IsSubprotocol p) {x : X} {y : Y} (hxy : reaches hsp x y) :

(testSubprotocol hsp qIn qOut).run x y = qIn.run x y

source

theorem CommunicationComplexity.Deterministic.Protocol.testSubprotocol_run_outside {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p qIn qOut : Protocol X Y α} (hsp : s.IsSubprotocol p) {x : X} {y : Y} (hxy : ¬reaches hsp x y) :

(testSubprotocol hsp qIn qOut).run x y = qOut.run x y