Synchronous One-Error Gossip with Correction

Basics

Here we define: agents, values, distributions, calls, sequents.

We use n for the number of agents.

@[reducible, inline]

abbrev Error.Agent {n : ℕ} : Type

Equations

• Error.Agent = Fin n

@[reducible, inline]

abbrev Error.Value {n : ℕ} : Type

Equations

• Error.Value = (Error.Agent × Bool)

instance Error.instCoeAgentValue {n : ℕ} : Coe Agent Value

We allow writing just the agent a for the value ⟨a, true⟩.

Equations

• Error.instCoeAgentValue = { coe := fun (a : Error.Agent) => (a, true) }

def Error.«term‾_» : Lean.ParserDescr

We write ‾a for the value ⟨a, false⟩.

Equations

• Error.«term‾_» = Lean.ParserDescr.node `Error.«term‾_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "‾") (Lean.ParserDescr.cat `term 1023))

@[reducible, inline]

abbrev Error.Dist {n : ℕ} : Type

An initial secret distribution, each agent only has their own value.

Equations

• Error.Dist = (Error.Agent → Bool)

def Error.Dist.switch {n : ℕ} : Agent → Dist → Dist

In the given distribution, invert the value for this agent i

Equations

• Error.Dist.switch x✝¹ x✝ = fun (a : Error.Agent) => if a = x✝¹ then !x✝ a else x✝ a

inductive Error.Call {n : ℕ} : Type

• normal {n : ℕ} (caller callee : Agent) : Call
• fstE {n : ℕ} (caller err callee : Agent) : Call
• sndE {n : ℕ} (caller callee err : Agent) : Call

def Error.«term⌜__⌝» : Lean.ParserDescr

Equations

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

def Error.«term⌜_^__⌝» : Lean.ParserDescr

Equations

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

def Error.«term⌜__^_⌝» : Lean.ParserDescr

Equations

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

def Error.Call.pair {n : ℕ} : Call → Agent × Agent

The pair of agents in the call, ignoring whether an error is made.

Equations

• ⌜a b⌝.pair = (a, b)
• ⌜a^err b⌝.pair = (a, b)
• ⌜a b^err⌝.pair = (a, b)

@[reducible, inline]

abbrev Error.Sequence {n : ℕ} : Type

(Def 2) A sequence is a list of calls. For easy pattern matching this is in reverse order: the newest call is the first element.

Equations

• Error.Sequence = List Error.Call

def Error.invert {n : ℕ} : Agent → Set Value → Set Value

Flip the value of the secret of this agent in the given set.

Equations

• Error.invert x✝¹ x✝ = (fun (x : Error.Value) => match x with | (j, b) => if j = x✝¹ then (j, !b) else (j, b)) '' x✝

Syntax

inductive Error.Form {n : ℕ} : Type

(Def 3) Logical language

• Top {n : ℕ} : Form

  True constant

• Con {n : ℕ} : Form → Form → Form

  Conjunction

• Neg {n : ℕ} : Form → Form

  Negation

• Has {n : ℕ} (a : Agent) : Value → Form

  Has a (b, k) means agent a has value k of agent b.

• K {n : ℕ} (a : Agent) (φ : Form) : Form

  K a φ means agent a knows that φ is true.

def Error.Form.length {n : ℕ} : Form → ℕ

Equations

• Error.Form.Top.length = 0
• (φ1 ⋀ φ2).length = 1 + φ1.length + φ2.length
• ( ¬'φ).length = 1 + φ.length
• (a_1@a).length = 1
• (Error.Form.K a φ).length = 1 + φ.length

Roles

inductive Error.Role : Type

• Caller : Role
• Callee : Role
• Other : Role

  Not participating in the call

instance Error.instDecidableEqRole : DecidableEq Role

Equations

• Error.instDecidableEqRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Error.roleOfIn {n : ℕ} (i : Agent) (c : Call) : Role

What is the Role of i in this call?

Equations

• Error.roleOfIn i ⌜a b⌝ = if i = a then Error.Role.Caller else if i = b then Error.Role.Callee else Error.Role.Other
• Error.roleOfIn i ⌜a^err b⌝ = if i = a then Error.Role.Caller else if i = b then Error.Role.Callee else Error.Role.Other
• Error.roleOfIn i ⌜a b^err⌝ = if i = a then Error.Role.Caller else if i = b then Error.Role.Callee else Error.Role.Other

@[simp]

theorem Error.roleOfIn_a {n✝ : ℕ} {a b : Agent} : roleOfIn a ⌜a b⌝ = Role.Caller

@[simp]

theorem Error.roleOfIn_eq_Caller_iff {n✝ : ℕ} {a x y : Agent} : roleOfIn a ⌜x y⌝ = Role.Caller ↔ a = x

@[simp]

theorem Error.roleOfIn_eq_Callee_iff {n✝ : ℕ} {a x y : Agent} : roleOfIn a ⌜x y⌝ = Role.Callee ↔ a ≠ x ∧ a = y

@[simp]

theorem Error.roleOfIn_eq_Other_iff {n✝ : ℕ} {a x y : Agent} : roleOfIn a ⌜x y⌝ = Role.Other ↔ a ≠ x ∧ a ≠ y

@[simp]

theorem Error.roleOfIn_fstE_eq_Caller_iff {n✝ : ℕ} {a x z y : Agent} : roleOfIn a ⌜x^z y⌝ = Role.Caller ↔ a = x

@[simp]

theorem Error.roleOfIn_fstE_eq_Callee_iff {n✝ : ℕ} {a x z y : Agent} : roleOfIn a ⌜x^z y⌝ = Role.Callee ↔ a ≠ x ∧ a = y

@[simp]

theorem Error.roleOfIn_fstE_eq_Other_iff {n✝ : ℕ} {a x z y : Agent} : roleOfIn a ⌜x^z y⌝ = Role.Other ↔ a ≠ x ∧ a ≠ y

@[simp]

theorem Error.roleOfIn_sndE_eq_Caller_iff {n✝ : ℕ} {a x y z : Agent} : roleOfIn a ⌜x y^z⌝ = Role.Caller ↔ a = x

@[simp]

theorem Error.roleOfIn_sndE_eq_Callee_iff {n✝ : ℕ} {a x y z : Agent} : roleOfIn a ⌜x y^z⌝ = Role.Callee ↔ a ≠ x ∧ a = y

@[simp]

theorem Error.roleOfIn_sndE_eq_Other_iff {n✝ : ℕ} {a x y z : Agent} : roleOfIn a ⌜x y^z⌝ = Role.Other ↔ a ≠ x ∧ a ≠ y

def Error.other {n : ℕ} (i : Agent) (c : Call) : Agent

Who is the other agent than i in this call? If i is not in the call, return caller.

Equations

• Error.other i ⌜a b⌝ = if i = a then b else a
• Error.other i ⌜a^err b⌝ = if i = a then b else a
• Error.other i ⌜a b^err⌝ = if i = a then b else a

Sequences with at most one transmission error

def Error.errFree {n : ℕ} : Sequence → Prop

This sequence contains no transmission errors.

Equations

• Error.errFree [] = True
• Error.errFree (⌜caller callee⌝ :: rest) = Error.errFree rest
• Error.errFree (⌜caller^err callee⌝ :: tail) = False
• Error.errFree (⌜caller callee^err⌝ :: tail) = False

@[simp]

theorem Error.errFree_nil {n : ℕ} : errFree []

def Error.maxOne {n : ℕ} : Sequence → Prop

This sequence contains at most one transmission error.

Equations

• Error.maxOne [] = True
• Error.maxOne (⌜caller callee⌝ :: rest) = Error.maxOne rest
• Error.maxOne (⌜caller^err callee⌝ :: tail) = Error.errFree tail
• Error.maxOne (⌜caller callee^err⌝ :: tail) = Error.errFree tail

@[simp]

theorem Error.maxOne_nil {n : ℕ} : maxOne []

theorem Error.Sequence.maxOne_of_errFree {n✝ : ℕ} {σ : Sequence} : errFree σ → maxOne σ

theorem Error.Sequence.maxOne_cons {n✝ : ℕ} {C : Call} {σ : List Call} : maxOne (C :: σ) → maxOne σ

def Error.«term⁻_» : Lean.ParserDescr

If o proves that C :: σ has at most one error then we use the short notation ⁻o for the prove that σ has at most one error.

Equations

• Error.«term⁻_» = Lean.ParserDescr.node `Error.«term⁻_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⁻") (Lean.ParserDescr.cat `term 1023))

def Error.OSequence {n : ℕ} : Type

Sequence with at most one error.

Equations

• Error.OSequence = Subtype Error.maxOne

def Error.«term_⊑_» : Lean.TrailingParserDescr

Subsequence relation: σ⊑τ means that τ extends σ. Because sequences are lists with the newest call first we define this as List.IsSuffix σ τ.

Equations

• Error.«term_⊑_» = Lean.ParserDescr.trailingNode `Error.«term_⊑_» 1022 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊑") (Lean.ParserDescr.cat `term 1023))

instance Error.instCoeOSequenceSequence {n : ℕ} : Coe OSequence Sequence

Equations

• Error.instCoeOSequenceSequence = { coe := Subtype.val }

def Error.OSequence.length {n : ℕ} (σ : OSequence) : ℕ

Equations

• σ.length = List.length ↑σ

@[simp]

theorem Error.OSequence.length_nil {n : ℕ} {h : Error.maxOne []} : length ⟨[], h⟩ = 0

@[simp]

theorem Error.OSequence.length_def {n : ℕ} (σ : Sequence) (h : Error.maxOne σ) : length ⟨σ, h⟩ = List.length σ

@[simp]

theorem Error.OSequence.maxOne {n : ℕ} {σ : OSequence} : Error.maxOne ↑σ

Semantics

@[irreducible]

def Error.resultSet {n : ℕ} (i : Agent) : Dist → OSequence → Set Value

(Def 4) Semantics of call. What values does this agent have after this sequence?

Equations

• One or more equations did not get rendered due to their size.
• x✝⌈⟨[], property⟩⌉i = {(i, x✝ i)}
• x⌈⟨C :: σ, o⟩⌉i = x⌈⟨σ, ⋯⟩⌉i

@[irreducible]

def Error.contribSet {n : ℕ} (S : Dist) (σ : OSequence) : Call → Set Value × Set Value

Right after sequence σ, what values will caller and callee contribute to the call?

Equations

• Error.contribSet S σ ⌜a b⌝ = (S⌈σ⌉a, S⌈σ⌉b)
• Error.contribSet S σ ⌜a^err b⌝ = (Error.invert err (S⌈σ⌉a), S⌈σ⌉b)
• Error.contribSet S σ ⌜a b^err⌝ = (S⌈σ⌉a, Error.invert err (S⌈σ⌉b))

@[irreducible]

def Error.equiv {n k : ℕ} (a : Agent) : Dist × { σ : OSequence // σ.length = k } → Dist × { σ : OSequence // σ.length = k } → Prop

(Def 5) Observation relation. This is synchronous.

Equations

• One or more equations did not get rendered due to their size.
• Error.equiv a (S, ⟨⟨[], property⟩, property_1⟩) (T, ⟨⟨[], property_2⟩, property_3⟩) = (S a = T a)

@[irreducible]

def Error.eval {n : ℕ} : Dist → OSequence → Form → Prop

(Def 6) Semantics.

Equations

• x✝¹⌈x✝⌉ ⊧ Error.Form.Top = True
• x✝¹⌈x✝⌉ ⊧ ( ¬'φ) = ¬x✝¹⌈x✝⌉ ⊧ φ
• x✝¹⌈x✝⌉ ⊧ (j, k)@a = ((j, k) ∈ x✝¹⌈x✝⌉a)
• x✝¹⌈x✝⌉ ⊧ (φ ⋀ ψ) = (x✝¹⌈x✝⌉ ⊧ φ ∧ x✝¹⌈x✝⌉ ⊧ ψ)
• x✝¹⌈x✝⌉ ⊧ Error.Form.K a φ = ∀ (T : Error.Dist) (τ : { σ : Error.OSequence // σ.length = x✝.length }), Error.equiv a (x✝¹, ⟨x✝, ⋯⟩) (T, τ) → T⌈↑τ⌉ ⊧ φ

def Error.«term_⌈_⌉_» : Lean.TrailingParserDescr

Equations

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

@[simp]

theorem Error.resultSet_nil {n : ℕ} {o : maxOne []} {S : Dist} {i : Agent} : S⌈⟨[], o⟩⌉i = {(i, S i)}

@[simp]

theorem Error.equiv_nil {n✝ : ℕ} {i : Agent} {S : Dist} {o1 : maxOne []} {a✝ : ℕ} {h1 : OSequence.length ⟨[], o1⟩ = a✝} {T : Dist} {o2 : maxOne []} {h2 : OSequence.length ⟨[], o2⟩ = a✝} : equiv i (S, ⟨⟨[], o1⟩, h1⟩) (T, ⟨⟨[], o2⟩, h2⟩) ↔ S i = T i

Notation and Abbreviations

def Error.«term¬'_» : Lean.ParserDescr

Equations

• Error.«term¬'_» = Lean.ParserDescr.node `Error.«term¬'_» 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ¬'") (Lean.ParserDescr.cat `term 70))

def Error.«term_⋀_» : Lean.TrailingParserDescr

Equations

• Error.«term_⋀_» = Lean.ParserDescr.trailingNode `Error.«term_⋀_» 60 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋀ ") (Lean.ParserDescr.cat `term 60))

def Error.«term_⋁_» : Lean.TrailingParserDescr

Equations

• Error.«term_⋁_» = Lean.ParserDescr.trailingNode `Error.«term_⋁_» 1022 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋁ ") (Lean.ParserDescr.cat `term 1023))

def Error.«term_⟹_» : Lean.TrailingParserDescr

Equations

• Error.«term_⟹_» = Lean.ParserDescr.trailingNode `Error.«term_⟹_» 1022 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⟹") (Lean.ParserDescr.cat `term 1023))

def Error.«term_⇔_» : Lean.TrailingParserDescr

Equations

• Error.«term_⇔_» = Lean.ParserDescr.trailingNode `Error.«term_⇔_» 1022 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇔ ") (Lean.ParserDescr.cat `term 1022))

def Error.«term_@_» : Lean.TrailingParserDescr

We write v @ a to say that agent a has value v.

Equations

• Error.«term_@_» = Lean.ParserDescr.trailingNode `Error.«term_@_» 1022 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "@") (Lean.ParserDescr.cat `term 1023))

def Error.termKv__ : Lean.ParserDescr

Equations

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

def Error.«term_⌈_⌉⊧_» : Lean.TrailingParserDescr

Equations

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

def Error.valid {n : ℕ} (φ : Form) : Prop

Validity of formulas

Equations

• ⊨ φ = ∀ (S : Error.Dist) (σ : Error.OSequence), S⌈σ⌉ ⊧ φ

def Error.«term⊨_» : Lean.ParserDescr

Equations

• Error.«term⊨_» = Lean.ParserDescr.node `Error.«term⊨_» 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊨ ") (Lean.ParserDescr.cat `term 100))

theorem Error.eval_biimpl {n✝ : ℕ} {S : Dist} {σ : OSequence} {φ1 φ2 : Form} : S⌈σ⌉ ⊧ ( ¬'( ¬' ¬'φ1 ⋀ ¬'φ2) ⋀ ¬'( ¬' ¬'φ2 ⋀ ¬'φ1)) ↔ (S⌈σ⌉ ⊧ φ1 ↔ S⌈σ⌉ ⊧ φ2)

theorem Error.eval_impl {n✝ : ℕ} {S : Dist} {σ : OSequence} {φ1 φ2 : Form} : S⌈σ⌉ ⊧ ( ¬'( ¬' ¬'φ1 ⋀ ¬'φ2)) ↔ S⌈σ⌉ ⊧ φ1 → S⌈σ⌉ ⊧ φ2

theorem Error.eval_dis {n✝ : ℕ} {S : Dist} {σ : OSequence} {φ1 φ2 : Form} : S⌈σ⌉ ⊧ ( ¬'( ¬'φ1 ⋀ ¬'φ2)) ↔ S⌈σ⌉ ⊧ φ1 ∨ S⌈σ⌉ ⊧ φ2

The observation relation is an equivalence

def Error.equi {n : ℕ} (a : Agent) (Sσ Tτ : Dist × OSequence) : Prop

An abbreviation to easily say that we have the same length and (can thus say) equiv.

Equations

• Sσ ~_ a Tτ = ∃ (h : Sσ.2.length = Tτ.2.length), Error.equiv a (Sσ.1, ⟨Sσ.2, ⋯⟩) (Tτ.1, ⟨Tτ.2, ⋯⟩)

def Error.«term_~___» : Lean.TrailingParserDescr

Equations

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

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

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

theorem Error.sameRole_of_equiv {n✝ : ℕ} {a : Agent} {S : Dist} {C₁ : Call} {σ : List Call} {o1 : maxOne (C₁ :: σ)} {a✝ : ℕ} {h1 : OSequence.length ⟨C₁ :: σ, o1⟩ = a✝} {T : Dist} {C₂ : Call} {τ : List Call} {o2 : maxOne (C₂ :: τ)} {h2 : OSequence.length ⟨C₂ :: τ, o2⟩ = a✝} : equiv a (S, ⟨⟨C₁ :: σ, o1⟩, h1⟩) (T, ⟨⟨C₂ :: τ, o2⟩, h2⟩) → roleOfIn a C₁ = roleOfIn a C₂

@[simp, irreducible]

theorem Error.equiv_refl {n : ℕ} {a : Agent} {S : Dist} {k : ℕ} {σ : { σ : OSequence // σ.length = k }} : equiv a (S, σ) (S, σ)

theorem Error.equiv_symm {n : ℕ} {i : Agent} {m : ℕ} {S : Dist} {σ : OSequence} {h1 : σ.length = m} {T : Dist} {τ : OSequence} {h2 : τ.length = m} : equiv i (S, ⟨σ, h1⟩) (T, ⟨τ, h2⟩) ↔ equiv i (T, ⟨τ, h2⟩) (S, ⟨σ, h1⟩)

theorem Error.equiv_trans {n : ℕ} {a : Agent} {m : ℕ} {S : Dist} {σ : OSequence} {h1 : σ.length = m} {T : Dist} {τ : OSequence} {h2 : τ.length = m} {R : Dist} {ρ : OSequence} {h3 : ρ.length = m} : equiv a (S, ⟨σ, h1⟩) (T, ⟨τ, h2⟩) → equiv a (T, ⟨τ, h2⟩) (R, ⟨ρ, h3⟩) → equiv a (S, ⟨σ, h1⟩) (R, ⟨ρ, h3⟩)

theorem Error.equiv_Equivalence {n k : ℕ} {i : Agent} : Equivalence (equiv i)

The observation relation equiv $∼_a$ is an equivalence relation.

theorem Error.equiv_then_know_same {n : ℕ} {a : Agent} {m : ℕ} {S : Dist} {σ : OSequence} {h1 : σ.length = m} {T : Dist} {τ : OSequence} {h2 : τ.length = m} (equ : equiv a (S, ⟨σ, h1⟩) (T, ⟨τ, h2⟩)) (φ : Form) : S⌈σ⌉ ⊧ Form.K a φ ↔ T⌈τ⌉ ⊧ Form.K a φ

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

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

Corollary 12. 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 9. Parts (i) and (ii) are given by the two k values. The proof here uses stubbornness.

theorem Error.knowledge_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 10. Knowledge 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 Prop 13 "iff (call semantics)"

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 13 "iff (semantics of formulas and observation relation)"

theorem Error.not_in_call_then_invariant {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 13 "iff (semantics of formulas and observation relation)"

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

Proposition 13.

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

Corollary 14.

Examples

def Error.ini (n : ℕ) : Dist

Initial distribution with all values set to true.

Equations

• Error.ini n x✝ = true

theorem Error.example_correct_belief_does_not_imply_knowledege (a b : Agent) (h : a ≠ b) : (ini 2)⌈⟨[⌜a b⌝], True.intro⟩⌉ ⊧ ((b, true)@a ⋀ ¬'(b, false)@a ⋀ (b, true)@b ⋀ ¬' ¬'( ¬'Form.K a ((b, true)@b) ⋀ ¬'Form.K a ((b, false)@b)))

Correct belief need not imply knowledge: given ini 2, after an initial call ab agent a correclty believes b, but a does not know the secret of b, because a also considers it possible that the call was a b^b instead.