Encounters and reachability: helper lemmas (CRN-3)

Generic facts about Protocol.interact, Protocol.Step, Protocol.Reaches and Protocol.OutputStable, used by all constructions of CRN-3, and two counting lemmas for sums over agents in which only the two agents of an encounter change.

theorem Crn.Protocol.interact_apply {X : Type u_1} {Q : Type u_2} {n : ℕ} (P : Protocol X Q) (c : Fin n → Q) (e : AgentPair n) (w : Fin n) : P.interact c e w = if w = (↑e).2 then (P.δ (c (↑e).1, c (↑e).2)).2 else if w = (↑e).1 then (P.δ (c (↑e).1, c (↑e).2)).1 else c w

The state of agent w after the encounter e.

theorem Crn.Protocol.interact_fst {X : Type u_1} {Q : Type u_2} {n : ℕ} (P : Protocol X Q) (c : Fin n → Q) (e : AgentPair n) : P.interact c e (↑e).1 = (P.δ (c (↑e).1, c (↑e).2)).1

The initiator gets δ₁.

theorem Crn.Protocol.interact_snd {X : Type u_1} {Q : Type u_2} {n : ℕ} (P : Protocol X Q) (c : Fin n → Q) (e : AgentPair n) : P.interact c e (↑e).2 = (P.δ (c (↑e).1, c (↑e).2)).2

The responder gets δ₂.

theorem Crn.Protocol.interact_of_ne {X : Type u_1} {Q : Type u_2} {n : ℕ} (P : Protocol X Q) (c : Fin n → Q) (e : AgentPair n) {w : Fin n} (h1 : w ≠ (↑e).1) (h2 : w ≠ (↑e).2) : P.interact c e w = c w

The other agents keep their states.

theorem Crn.Protocol.interact_eq_self {X : Type u_1} {Q : Type u_2} {n : ℕ} (P : Protocol X Q) (c : Fin n → Q) (e : AgentPair n) (h : P.δ (c (↑e).1, c (↑e).2) = (c (↑e).1, c (↑e).2)) : P.interact c e = c

An encounter whose transition leaves both states unchanged leaves the configuration unchanged.

theorem Crn.Protocol.Reaches.refl {X : Type u_1} {Q : Type u_2} {n : ℕ} {P : Protocol X Q} (c : Fin n → Q) : P.Reaches c c

Every configuration reaches itself.

theorem Crn.Protocol.Reaches.trans {X : Type u_1} {Q : Type u_2} {n : ℕ} {P : Protocol X Q} {c d e : Fin n → Q} (h₁ : P.Reaches c d) (h₂ : P.Reaches d e) : P.Reaches c e

Reachability is transitive.

theorem Crn.Protocol.Step.reaches {X : Type u_1} {Q : Type u_2} {n : ℕ} {P : Protocol X Q} {c d : Fin n → Q} (h : P.Step c d) : P.Reaches c d

A step is a path.

theorem Crn.Protocol.Reaches.tail {X : Type u_1} {Q : Type u_2} {n : ℕ} {P : Protocol X Q} {c d e : Fin n → Q} (h₁ : P.Reaches c d) (h₂ : P.Step d e) : P.Reaches c e

A path followed by a step is a path.

theorem Crn.Protocol.reaches_interact {X : Type u_1} {Q : Type u_2} {n : ℕ} {P : Protocol X Q} (c : Fin n → Q) (e : AgentPair n) : P.Reaches c (P.interact c e)

One encounter is a step.

theorem Crn.Protocol.Reaches.invariant {X : Type u_1} {Q : Type u_2} {n : ℕ} {P : Protocol X Q} {I : (Fin n → Q) → Prop} (hI : ∀ (c d : Fin n → Q), I c → P.Step c d → I d) {c d : Fin n → Q} (h : P.Reaches c d) (hc : I c) : I d

A property preserved by every step holds along reachability.

theorem Crn.Protocol.OutputStable.reaches {X : Type u_1} {Q : Type u_2} {n : ℕ} {P : Protocol X Q} {b : Bool} {c d : Fin n → Q} (hc : P.OutputStable b c) (h : P.Reaches c d) : P.OutputStable b d

Output-stability is inherited along reachability.

theorem Crn.Protocol.outputStable_of_invariant {X : Type u_1} {Q : Type u_2} {n : ℕ} {P : Protocol X Q} {I : (Fin n → Q) → Prop} (hI : ∀ (c d : Fin n → Q), I c → P.Step c d → I d) {b : Bool} (hb : ∀ (c : Fin n → Q), I c → ∀ (v : Fin n), P.output (c v) = b) {c : Fin n → Q} (hc : I c) : P.OutputStable b c

A property preserved by every step, under which all agents output b, gives output-stability.

theorem Crn.sum_add_pair {n : ℕ} {M : Type u_3} [AddCommMonoid M] {u v : Fin n} (huv : u ≠ v) (G G' : Fin n → M) (h : ∀ (w : Fin n), w ≠ u → w ≠ v → G' w = G w) : ∑ w : Fin n, G' w + (G u + G v) = ∑ w : Fin n, G w + (G' u + G' v)

Sums over agents when only the agents u ≠ v change: ∑ G' + (G u + G v) = ∑ G + (G' u + G' v).

theorem Crn.add_le_sum_pair {n : ℕ} {G : Fin n → ℕ} {u v : Fin n} (huv : u ≠ v) : G u + G v ≤ ∑ w : Fin n, G w

A sum over agents is at least its terms at two distinct agents.

theorem Crn.sum_comp_eq_sum_counts {X : Type u_1} {n : ℕ} [Fintype X] [DecidableEq X] {M : Type u_3} [AddCommMonoid M] (ι : Fin n → X) (F : X → M) : ∑ w : Fin n, F (ι w) = ∑ i : X, ↑(counts ι) i • F i

A sum over agents of a function of their input symbols, grouped by symbol: ∑_w F(ι w) = ∑_i (counts ι)ᵢ • F i.