Synchronous One-Error Gossip with Correction

Examples

instance instOfNatSubtypeAgentNeOfNatNat {k : ℕ} : OfNat { b : Error.Agent // b ≠ 0 } 1

Just write 1 for an Agent that is not 0.

Equations

• instOfNatSubtypeAgentNeOfNatNat = { ofNat := ⟨1, ⋯⟩ }

instance instOfNatSubtypeAgentNeOfNatNat_1 {k : ℕ} : OfNat { b : Error.Agent // b ≠ 0 } 2

Just write 2 for a second Agent that is not 0.

Equations

• instOfNatSubtypeAgentNeOfNatNat_1 = { ofNat := ⟨⟨2, ⋯⟩, ⋯⟩ }

def claimForm {n : ℕ} (a b : Error.Agent) : Error.Form

Equations

• claimForm a b = ¬'( ¬' ¬'Error.Form.K a ((b, true)@b) ⋀ ¬'(b, true)@a)

def counterExampleForm {n : ℕ} (a b : Error.Agent) : Error.Form

Equations

• counterExampleForm a b = ¬'(b, true)@a ⋀ Error.Form.K a ((b, true)@b)

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

Equations

• validAt k φ = ∀ (S : Error.Dist) (σ : { σ : Error.OSequence // σ.length = k }), S⌈↑σ⌉ ⊧ φ

instance instDecValidAt {n k : ℕ} {φ : Error.Form} : Decidable (validAt k φ)

Equations

• instDecValidAt = id (Decidable.forall_of_list_mem ⋯ fun (S : Error.Dist) => Decidable.forall_of_list_mem ⋯ fun (σ : { σ : Error.OSequence // σ.length = k }) => Error.instDecEval)

Examples

def ini (n : ℕ) : Error.Dist

Initial distribution with all values set to true.

Equations

• ini n x✝ = true