@[reducible, inline]

abbrev GossipState (n : ℕ) : Type

Equations

• GossipState n = (Fin n → Fin n → Prop)

@[reducible, inline]

abbrev Call (n : ℕ) : Type

Equations

• Call n = (Fin n × Fin n)

def initialState (n : ℕ) : GossipState n

Equations

• initialState n i j = (i = j)

instance instDecidableRelFinInitialState {n : ℕ} : DecidableRel (initialState n)

Equations

• instDecidableRelFinInitialState = decEq

def isExpert {n : ℕ} (s : GossipState n) (i : Fin n) : Prop

Equations

• isExpert s i = ∀ (j : Fin n), s i j

def allKnow {n : ℕ} (s : GossipState n) (i : Fin n) : Prop

All other agents know the secret of this one.

Equations

• allKnow s i = ∀ (j : Fin n), s j i

instance instDecidableIsExpertOfDecidableRelFin {n : ℕ} {s : GossipState n} [DecidableRel s] {i : Fin n} : Decidable (isExpert s i)

Equations

• instDecidableIsExpertOfDecidableRelFin = Fintype.decidableForallFintype

def allExpert {n : ℕ} (s : GossipState n) : Prop

Equations

• allExpert s = ∀ (i : Fin n), isExpert s i

instance instDecidableAllExpertOfDecidableRelFin {n : ℕ} {s : GossipState n} [DecidableRel s] : Decidable (allExpert s)

Equations

• instDecidableAllExpertOfDecidableRelFin = Fintype.decidableForallFintype

def makeCall {n : ℕ} (s : GossipState n) : Call n → GossipState n

Equations

• makeCall s (i, j) x✝¹ x✝ = if x✝¹ = i then s x✝¹ x✝ ∨ s j x✝ else if x✝¹ = j then s x✝¹ x✝ ∨ s i x✝ else s x✝¹ x✝

instance instDecidableRelFinMakeCall {n : ℕ} {s : GossipState n} [DecidableRel s] {c : Call n} : DecidableRel (makeCall s c)

Equations

• instDecidableRelFinMakeCall x✝¹ x✝ = if h : x✝¹ = i then decidable_of_iff (s i x✝ ∨ s j x✝) ⋯ else if h' : x✝¹ = j then decidable_of_iff (s j x✝ ∨ s i x✝) ⋯ else decidable_of_iff (s x✝¹ x✝) ⋯

def makeCalls {n : ℕ} (s : GossipState n) (cs : List (Call n)) : GossipState n

Equations

• makeCalls s cs = List.foldl makeCall s cs

instance instDecidableRelFinMakeCalls {n : ℕ} {s : GossipState n} [DecidableRel s] {cs : List (Call n)} : DecidableRel (makeCalls s cs)

Equations

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

def showState {n : ℕ} (s : GossipState n) [DecidableRel s] : Std.Format

Equations

• showState s = repr fun (i j : Fin n) => if s i j then "True " else "False"

def moreGossip {n : ℕ} (s1 s2 : GossipState n) : Prop

Equations

• moreGossip s1 s2 = ∀ (a b : Fin n), s1 a b → s2 a b

def addAgent {n : ℕ} (s : GossipState n) : GossipState n.succ

Equations

• addAgent s a b = Fin.lastCases ((b == Fin.last n) = true) (fun (i : Fin n) => Fin.lastCases (false = true) (fun (b : Fin n) => s i b) b) a

instance instCoeCallSucc {n : ℕ} : Coe (Call n) (Call n.succ)

A call among the n agents is also a call among the n+1 agents.

Equations

• instCoeCallSucc = { coe := fun (x : Call n) => match x with | (i, j) => (i.castSucc, j.castSucc) }

def stateEquivalence {n : ℕ} : GossipState n → GossipState n → Prop

Equations

• stateEquivalence s1 s2 = ∀ (a b : Fin n), s1 a b ↔ s2 a b

def contains {n : ℕ} (σ : List (Call n)) (a : Fin n) : Bool

Equations

• contains σ a = σ.any fun (c' : Call n) => decide (c'.1 = a ∨ c'.2 = a)

theorem expertMakesExpert {n : ℕ} {s : GossipState n} {i j : Fin n} : isExpert s i → isExpert (makeCall s (i, j)) j

theorem makeCalls_cons {n : ℕ} (s : GossipState n) (c : Call n) (cs : List (Call n)) : makeCalls s (c :: cs) = makeCalls (makeCall s c) cs

theorem makeCalls_snoc {n : ℕ} (s : GossipState n) (cs : List (Call n)) (c : Call n) : makeCalls s (cs ++ [c]) = makeCall (makeCalls s cs) c

theorem makeCall_increases_gossip {n : ℕ} (s1 s2 : GossipState n) (c : Call n) : moreGossip s1 s2 → moreGossip (makeCall s1 c) (makeCall s2 c)

theorem makeCallsIncreasesGossip {n : ℕ} (s1 s2 : GossipState n) (cs : List (Call n)) : moreGossip s1 s2 → moreGossip (makeCalls s1 cs) (makeCalls s2 cs)

theorem makeCallMakesGossip {n : ℕ} (s : GossipState n) (c : Call n) : moreGossip s (makeCall s c)

theorem callsIncreaseGossip {n : ℕ} (s : GossipState n) (cs : List (Call n)) : moreGossip s (makeCalls s cs)

theorem addAgentExpertOld {n : ℕ} {s : GossipState n} {i : Fin n} : isExpert s i ↔ ∀ (j : Fin n), addAgent s i.castSucc j.castSucc