Synchronous One-Error Gossip with Correction

Properties of the Semantics

theorem Error.indistinguishable_then_same_values {n : ℕ} {a : Agent} {S T : Dist} {σ τ : OSequence} : (S, σ) ~_ a(T, τ) → S⌈σ⌉a = T⌈τ⌉a

Lemma 7, also could have been named resultSet_eq_of_equiv

theorem Error.true_of_knowldege {n : ℕ} {S : Dist} {σ : OSequence} {a : Agent} {φ : Form} : S⌈σ⌉ ⊧ Form.K a φ → S⌈σ⌉ ⊧ φ

Knowledge is truthful. This follows from equiv_refl.

theorem Error.know_self {n✝ : ℕ} {a : Agent} {S T : Dist} (m : ℕ) (σ τ : OSequence) (h1 : σ.length = m) (h2 : List.length ↑τ = m) : equiv a (S, ⟨σ, h1⟩) (T, ⟨τ, h2⟩) → S a = T a

Agents know their own initial state. This is not the same as Lemma 7.

theorem Error.local_is_known {n : ℕ} {a b : Agent} (k : Bool) : ⊨ ( ¬'( ¬' ¬'(b, k)@a ⋀ ¬'Form.K a ((b, k)@a))) ∧ ⊨ ( ¬'( ¬' ¬' ¬'(b, k)@a ⋀ ¬'Form.K a ( ¬'(b, k)@a)))

Lemma 8. The truth value of any $b_a$ atom is known by agent $a$. Note that k here says whether we have $b$ or $\overline{b}$.

@[simp]

theorem Error.stubbornness {n✝ : ℕ} {S : Dist} {a : Agent} {k : Bool} (m : ℕ) (σ : OSequence) (h : σ.length = m) : S⌈σ⌉ ⊧ (a, k)@a ↔ S a = k

Lemma 9. Agents are stubborn about their own secrets.

@[simp]

theorem Error.not_notMem_resultSet {n✝ : ℕ} {b : Agent} {S : Dist} {σ : OSequence} : (b, !S b) ∉ S⌈σ⌉b

A useful corollary of stubbornness.

theorem Error.knowledge_of_secrets_is_preserved {n✝ : ℕ} {S : Dist} {σ τ : OSequence} {a b : Agent} (k : Bool) (hKv : S⌈σ⌉ ⊧ Form.K a ((b, k)@b)) (hSub : ↑σ <:+ ↑τ) : S⌈τ⌉ ⊧ Form.K a ((b, k)@b)

Lemma 10. Parts (i) and (ii) are given by the two k values. The proof uses stubbornness.

theorem Error.kv_of_secrets_is_preserved {n : ℕ} {S : Dist} {σ τ : OSequence} {a b : Agent} (hKv : S⌈σ⌉ ⊧ ( ¬'( ¬'Form.K a ((b, true)@b) ⋀ ¬'Form.K a ((b, false)@b)))) (hSub : ↑σ <:+ ↑τ) : S⌈τ⌉ ⊧ ( ¬'( ¬'Form.K a ((b, true)@b) ⋀ ¬'Form.K a ((b, false)@b)))

Corollary 11. Kv of secrets is preserved.

theorem Error.know_your_own {n : ℕ} {a : Agent} : ⊨ ( ¬'( ¬'Form.K a ((a, true)@a) ⋀ ¬'Form.K a ((a, false)@a)))

Agents know their own value. Follows from stubbornness.

theorem Error.not_in_call_then_invariant_resultSet {n : ℕ} {a : Agent} {C : Call} (h : roleOfIn a C = Role.Other) (S : Dist) (σ : List Call) (o : maxOne (C :: σ)) : S⌈⟨C :: σ, o⟩⌉a = S⌈⟨σ, ⋯⟩⌉a

Helper for knowledge_implies_correct_belief

theorem Error.not_in_call_then_invariant_kv {n : ℕ} {a : Agent} {C : Call} (h : roleOfIn a C = Role.Other) (b : Agent) (S : Dist) (σ : List Call) (o : maxOne (C :: σ)) : S⌈⟨C :: σ, o⟩⌉ ⊧ ( ¬'( ¬'Form.K a ((b, true)@b) ⋀ ¬'Form.K a ((b, false)@b))) ↔ S⌈⟨σ, ⋯⟩⌉ ⊧ ( ¬'( ¬'Form.K a ((b, true)@b) ⋀ ¬'Form.K a ((b, false)@b)))

Helper for Prop 12 "iff (semantics of formulas and observation relation)"

theorem Error.not_in_call_then_invariant_k {n : ℕ} {k : Bool} {a : Agent} {C : Call} (h : roleOfIn a C = Role.Other) (b : Agent) (S : Dist) (σ : List Call) (o : maxOne (C :: σ)) : S⌈⟨C :: σ, o⟩⌉ ⊧ Form.K a ((b, k)@b) ↔ S⌈⟨σ, ⋯⟩⌉ ⊧ Form.K a ((b, k)@b)

Stronger value-specific helper for Prop 12 "iff (semantics of formulas and observation relation)"

theorem Error.caller_keeps_known_value {n : ℕ} {a b : Agent} {k : Bool} (C : Call) (ra : roleOfIn a C = Role.Caller) (S : Dist) (σ : Sequence) (o : maxOne (C :: σ)) (know_before : S⌈⟨σ, ⋯⟩⌉ ⊧ Form.K a ((b, k)@b)) (had_before : S⌈⟨σ, ⋯⟩⌉ ⊧ (b, k)@a) : S⌈⟨C :: σ, o⟩⌉ ⊧ (b, k)@a

theorem Error.caller_rejects_opposite_of_known_value {n : ℕ} {a b : Agent} {k : Bool} (C : Call) (ra : roleOfIn a C = Role.Caller) (S : Dist) (σ : Sequence) (o : maxOne (C :: σ)) (know_before : S⌈⟨σ, ⋯⟩⌉ ⊧ Form.K a ((b, k)@b)) : S⌈⟨C :: σ, o⟩⌉ ⊧ ( ¬'(b, !k)@a)

theorem Error.caller_rejects_opposite_of_afterwards_known_value {n : ℕ} {a b : Agent} {k : Bool} (C : Call) (ra : roleOfIn a C = Role.Caller) (S : Dist) (σ : List Call) (o : maxOne (C :: σ)) (know_after : S⌈⟨C :: σ, o⟩⌉ ⊧ Form.K a ((b, k)@b)) : S⌈⟨C :: σ, o⟩⌉ ⊧ ( ¬'(b, !k)@a)

Footnote 1. "in fact the knowledge is already there"

theorem Error.caller_contribSet_eq_of_resultSet_eq {n : ℕ} {a : Agent} {C : Call} {S T : Dist} {σ : OSequence} (r_def : roleOfIn a C = Role.Caller) (h : S⌈σ⌉a = T⌈σ⌉a) : (contribSet S σ C).1 = (contribSet T σ C).1

theorem Error.callee_contribSet_eq_of_resultSet_eq {n : ℕ} {a : Agent} {C : Call} {S T : Dist} {σ : OSequence} (r_def : roleOfIn a C = Role.Callee) (h : S⌈σ⌉a = T⌈σ⌉a) : (contribSet S σ C).2 = (contribSet T σ C).2