leanprover · ctchou · Jun 1, 2026 · Jun 5, 2026 · Jun 7, 2026 · Jun 7, 2026
@@ -23,7 +23,9 @@ public import Cslib.Computability.Automata.NA.Sum
 public import Cslib.Computability.Automata.NA.ToDA
 public import Cslib.Computability.Automata.NA.Total
 public import Cslib.Computability.Distributed.FLP.Algorithm
+public import Cslib.Computability.Distributed.FLP.CanReachVia
 public import Cslib.Computability.Distributed.FLP.Consensus
+public import Cslib.Computability.Distributed.FLP.FairScheduler
 public import Cslib.Computability.Languages.Congruences.BuchiCongruence
 public import Cslib.Computability.Languages.Congruences.RightCongruence
 public import Cslib.Computability.Languages.ExampleEventuallyZero

@@ -0,0 +1,135 @@
+/-
+Copyright (c) 2026 Ching-Tsun Chou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ching-Tsun Chou
+-/
+
+module
+
+public import Cslib.Computability.Distributed.FLP.Algorithm
+
+/-! # Reachability via a subset of processes
+-/
+
+@[expose] public section
+
+namespace Cslib.FLP
+
+open Function Set Sum Multiset
+
+variable {P M S : Type*} [DecidableEq P] [DecidableEq M]
+
+/-- `a.CanReachVia ps s1 s2` means that state `s2` is reachable from state `s1` via a finite
+execution of algorithm `a` in which all messages received have destinations in `ps`. -/
+def Algorithm.CanReachVia (a : Algorithm P M S) (ps : Set P) (s1 s2 : State P M S) : Prop :=
+  ∃ xs, a.lts.MTr s1 xs s2 ∧ xs.Forall (DestIn ps)
+
+/-- `InpEqOn ps inp1 inp2` means that inputs `inp1` and `inp2` agree on all processes in `ps`. -/
+def InpEqOn (ps : Set P) (inp1 inp2 : P → Bool) : Prop :=
+  ∀ p, p ∈ ps → inp1 p = inp2 p
+
+namespace CanReachVia
+
+variable {a : Algorithm P M S}
+
+/-- `a.CanReachVia ps s s'` implies `a.lts.CanReach s s'` for any `ps`. -/
+theorem canReach {ps : Set P} {s s' : State P M S}
+    (h : a.CanReachVia ps s s') : a.lts.CanReach s s' := by
+  obtain ⟨xs, h_mtr, _⟩ := h
+  use xs
+
+/-- `a.CanReachVia ps s s` is true for any `ps`. -/
+theorem refl (ps : Set P) (s : State P M S) :
+    a.CanReachVia ps s s := by
+  use []
+  simp [LTS.MTr.refl]
+
+/-- Extending `CanReachVia` on the left by one step. -/
+theorem stepL {ps : Set P} {x : Action P M} {s1 s2 s3 : State P M S}
+    (hx : DestIn ps x) (h1 : a.lts.Tr s1 x s2) (h2 : a.CanReachVia ps s2 s3) :
+    a.CanReachVia ps s1 s3 := by
+  obtain ⟨xs, _, _⟩ := h2
+  use (x :: xs)
+  grind [LTS.MTr.stepL, List.forall_cons]
+
+private lemma diamond_helper
+    {ps : Set P} {x : Action P M} {s s1 s2 : State P M S}
+    (hx : DestIn ps x) (h1 : a.lts.Tr s x s1) (h2 : a.CanReachVia psᶜ s s2) :
+    ∃ s', a.CanReachVia psᶜ s1 s' ∧ a.lts.Tr s2 x s' := by
+  obtain ⟨xs2, h_mtr2, h_via2⟩ := h2
+  induction h_mtr2 generalizing s1
+  case refl s =>
+    use s1
+    simp_all [refl]
+  case stepL s y t2 ys s2 h_tr2 h_mtr2 h_ind =>
+    obtain ⟨h_y, h_ys⟩ := (List.forall_cons (DestIn psᶜ) y ys).mp h_via2
+    obtain ⟨t1, h_tr1, h_tr21⟩ := Algorithm.tr_diamond hx h1 h_y h_tr2
+    obtain ⟨s', h_crv1, h_tr2'⟩ := h_ind h_tr21 h_ys
+    use s', ?_, h_tr2'
+    exact stepL h_y h_tr1 h_crv1
+
+/-- A diamond property for `CanReachVia`. This theorem formalizes Proposition 1 of [Volzer2004]. -/
+theorem diamond {ps : Set P} {s s1 s2 : State P M S}
+    (h1 : a.CanReachVia ps s s1) (h2 : a.CanReachVia psᶜ s s2) :
+    ∃ s', a.CanReachVia psᶜ s1 s' ∧ a.CanReachVia ps s2 s' := by
+  obtain ⟨xs1, h_mtr1, h_via1⟩ := h1
+  induction h_mtr1 generalizing s2
+  case refl s =>
+    use s2
+    simp_all [refl]
+  case stepL s x t1 xs s1 h_tr1 h_mtr1 h_ind =>
+    obtain ⟨h_x, h_xs⟩ := (List.forall_cons (DestIn ps) x xs).mp h_via1
+    obtain ⟨t2, h_crv, h_tr2⟩:= diamond_helper h_x h_tr1 h2
+    obtain ⟨s', h_crv1, h_crv2⟩ := h_ind h_crv h_xs
+    use s', h_crv1
+    exact stepL h_x h_tr2 h_crv2
+
+/-- If inputs `inp1` and `inp2` agree on all processes in `ps` and state `s` is reachable from
+the initial state determined by `inp1` by receiving messages with destinations in `ps` only,
+then there exists a state `s2` that agrees with `s` on the states of all processes and is
+reachable from the initial state determined by `inp2` by receiving messages with destinations
+in `ps` only. This theorem is implicitly used in the proof of Lemma 1 of [Volzer2004]. -/
+theorem subset_inp [Fintype P] {ps : Set P} {inp1 inp2 : P → Bool} {s1 : State P M S}
+    (he : InpEqOn ps inp1 inp2) (hr : a.CanReachVia ps (a.start inp1) s1) :
+    ∃ s2, a.CanReachVia ps (a.start inp2) s2 ∧ s2.proc = s1.proc := by
+  obtain ⟨xs, h_mtr, h_xs⟩ := hr
+  obtain ⟨ss, _, h_ss0, _, _⟩ := LTS.Execution.of_mTr h_mtr
+  suffices h_inv : ∀ k, (_ : k ≤ xs.length) →
+    ∃ s2, a.lts.MTr (a.start inp2) (xs.take k) s2 ∧ s2.proc = ss[k].proc ∧
+      ∀ m, m.dest ∈ ps → s2.msgs.count m = ss[k].msgs.count m by
+    obtain ⟨s2, _⟩ := h_inv xs.length (by simp)
+    use s2, ?_, by grind
+    use xs, by grind
+  intro k h_k
+  induction k
+  case zero =>
+    use a.start inp2, by grind [LTS.MTr], by grind [Algorithm.start]
+    intro m h_m
+    simp only [h_ss0, Algorithm.start, count_map, Message.ext_iff]
+    congr
+    grind [InpEqOn]
+  case succ k h_ind =>
+    obtain ⟨s2, h_mtr, h_proc, h_msgs⟩ := h_ind (by grind)
+    obtain (_ | ⟨m, h_m⟩) := Option.eq_none_or_eq_some xs[k]
+    · use s2, ?_, ?_, ?_
+      · have h_tr : a.lts.Tr s2 xs[k] s2 := by grind [Algorithm.lts]
+        grind [List.take_add_one, LTS.MTr.stepR (lts := a.lts) h_mtr h_tr]
+      · grind [Algorithm.tr_none]
+      · grind [Algorithm.tr_none]
+    · obtain ⟨_, h_k1⟩ : m ∈ ss[k].msgs ∧ ss[k + 1] = a.recvMsg m ss[k] := by grind [Algorithm.lts]
+      use a.recvMsg m s2, ?_, ?_, ?_
+      · have := List.forall_mem_iff_forall_getElem.mp <| List.forall_iff_forall_mem.mp h_xs
+        have h_tr : a.lts.Tr s2 xs[k] (a.recvMsg m s2) := by
+          grind [Algorithm.lts, DestIn, one_le_count_iff_mem]
+        grind [List.take_add_one, LTS.MTr.stepR (lts := a.lts) h_mtr h_tr]
+      · grind [Algorithm.recvMsg]
+      · intro m1 h_m1
+        by_cases h1 : m1 = m
+        · simp [h_k1, Algorithm.recvMsg, h_proc, h1, count_erase_self]
+          grind
+        · simp [h_k1, Algorithm.recvMsg, h_proc, count_erase_of_ne h1]
+          grind
+
+end CanReachVia
+
+end Cslib.FLP
@@ -0,0 +1,250 @@
+/-
+Copyright (c) 2026 Ching-Tsun Chou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ching-Tsun Chou
+-/
+
+module
+
+public import Cslib.Computability.Distributed.FLP.Consensus
+public import Cslib.Foundations.Data.OmegaSequence.InfOcc
+public import Mathlib.Data.List.ReduceOption
+
+/-! # Machinery for constructing infinite fair executions
+
+The main goal of this file is to define a `fairScheduler` that, given a function `d`
+of type `DeliverMsg`, a state predicate `q`, and a state `s0` of an algorithm `a`,
+constructs an infinite execution of `a` starting from state `s0` in which all processes
+from a set `ps` are fair and `q` is true infinitely often.  With additional assumptions,
+we may also want to require that all actions in the infinite execution satisfy an action
+predicate `r`.
+-/
+
+@[expose] public section
+
+namespace Cslib.FLP
+
+open Function Set Multiset Filter ωSequence
+
+variable {P M S : Type*} [DecidableEq P] [DecidableEq M]
+
+/-- Given a state `s` and a message `m`, a function `d` of type `DeliverMsg` is supposed to
+return `(xs, t)` where `xs` is a finite execution from `s` to `t` in which `m` is delivered. -/
+def DeliverMsg P M S := State P M S → Message P M → List (Action P M) × State P M S
+
+/-- `d.ForallActions r` requires that all actions returned by `d` satisfy `r`. -/
+def DeliverMsg.ForallActions (d : DeliverMsg P M S) (r : Action P M → Prop) : Prop :=
+  ∀ s m, (d s m).fst.Forall r
+
+/-- `d.foldList s ml ms` uses `d` to deliver all messages that are in `ml` but not in `ms` from
+state `s`. Note that if a message `m` in `ml` is delivered during the delivery of an earlier
+message, `m` is added to `ms` so that it is not processed again. -/
+def DeliverMsg.foldList (d : DeliverMsg P M S) (s : State P M S) :
+    List (Message P M) → Finset (Message P M) → List (Action P M) × State P M S
+  | [], _ => ([], s)
+  | m :: ml, ms =>
+    if m ∈ ms then
+      d.foldList s ml ms
+    else
+      let (xl1, s1) := d s m
+      let ms' := ms ∪ xl1.reduceOption.toFinset
+      let (xl2, s2) := d.foldList s1 ml ms'
+      (xl1 ++ xl2, s2)
+
+open scoped Classical in
+/-- `d.scheduleMsgs ps s` schedules and delivers all messages which are in-flight in state `s`
+and have destinations in `ps` in some order (as determined by choice).  If no such message exists,
+then the the stuttering step is taken. -/
+noncomputable def DeliverMsg.scheduleMsgs (d : DeliverMsg P M S) (ps : Set P)
+    (s : State P M S) : List (Action P M) × State P M S :=
+  let ms := s.msgs.filter (fun m ↦ m.dest ∈ ps)
+  if ms = 0 then
+    ([none], s)
+  else
+    d.foldList s ms.toList ∅
+
+namespace DeliverMsg
+
+variable {d : DeliverMsg P M S}
+
+/-- If `d.ForallActions r`, then `d.foldList s ml ms` can only use actions satisfying `r`. -/
+theorem foldList_forallActions {r : Action P M → Prop}
+    (s : State P M S) (ml : List (Message P M)) (ms : Finset (Message P M))
+    (h : d.ForallActions r) : (d.foldList s ml ms).fst.Forall r := by
+  induction ml generalizing s ms <;>
+    grind [DeliverMsg.foldList, DeliverMsg.ForallActions, List.Forall, List.forall_append]
+
+end DeliverMsg
+
+/-- Starting from state `s0`, `a.fairSchedular d ps s0` constructs an infinite sequence of
+finite executions of `a` by repeatedly applying `d.scheduleMsgs ps`. -/
+noncomputable def Algorithm.fairScheduler (a : Algorithm P M S) (d : DeliverMsg P M S) (ps : Set P)
+    (s0 : State P M S) : ℕ → List (Action P M) × State P M S
+  | 0 => ([], s0)
+  | k + 1 => d.scheduleMsgs ps (a.fairScheduler d ps s0 k).snd
+
+/-- The infinite sequence of states forming the end states of the finite executions constructed
+by `Algorithm.fairScheduler`. -/
+noncomputable def Algorithm.fairSegEnds (a : Algorithm P M S) (d : DeliverMsg P M S)
+    (ps : Set P) (s0 : State P M S) : ωSequence (State P M S) :=
+  ωSequence.mk (fun k ↦ (a.fairScheduler d ps s0 k).snd)
+
+/-- The infinite sequence of finite action sequences from the finite executions constructed
+by `Algorithm.fairScheduler`. -/
+noncomputable def Algorithm.fairSegActions (a : Algorithm P M S) (d : DeliverMsg P M S)
+    (ps : Set P) (s0 : State P M S) : ωSequence (List (Action P M)) :=
+  (ωSequence.mk (fun k ↦ (a.fairScheduler d ps s0 k).fst)).tail
+
+/-- `a.FairDeliverMsg d ps q` says that for any state `s` of `a` satisfying `q` and
+any message `m` which is in-flight in `s` and whose destination is in `ps`, `d s m`
+produces a legal finite execution of `a` in which `m` is delivered and which ends in
+a state satisfying `q` again. -/
+def Algorithm.FairDeliverMsg (a : Algorithm P M S) (d : DeliverMsg P M S)
+    (ps : Set P) (q : State P M S → Prop) : Prop :=
+  ∀ s m, m ∈ s.msgs ∧ m.dest ∈ ps ∧ q s →
+    let (xl, t) := d s m
+    a.lts.MTr s xl t ∧ some m ∈ xl ∧ q t
+
+namespace FairScheduler
+
+variable {a : Algorithm P M S}
+
+/-- Re-stating the definition of `Algorithm.fairScheduler` as a mutual recursion of
+`Algorithm.fairSegEnds` and `Algorithm.fairSegActions`. -/
+theorem fairScheduler_init {d : DeliverMsg P M S} (ps : Set P) (s0 : State P M S) :
+    a.fairSegEnds d ps s0 0 = s0 := by
+  grind [Algorithm.fairScheduler, Algorithm.fairSegEnds]
+
+/-- Re-stating the definition of `Algorithm.fairScheduler` as a mutual recursion of
+`Algorithm.fairSegEnds` and `Algorithm.fairSegActions`. -/
+theorem fairScheduler_step {d : DeliverMsg P M S} (ps : Set P) (s0 : State P M S) (k : ℕ) :
+    d.scheduleMsgs ps (a.fairSegEnds d ps s0 k) =
+    (a.fairSegActions d ps s0 k, a.fairSegEnds d ps s0 (k + 1)) := by
+  grind [Algorithm.fairScheduler, Algorithm.fairSegEnds, Algorithm.fairSegActions]
+
+/-- If `d.ForallActions r`, then `a.fairSegActions d ps s0` can only use actions satisfying `r`. -/
+theorem fairSeg_forallActions {d : DeliverMsg P M S} {r : Action P M → Prop}
+    (ps : Set P) (s0 : State P M S) (k : ℕ) (ha : d.ForallActions r) (hn : r none) :
+    (a.fairSegActions d ps s0 k).Forall r := by
+  grind [fairScheduler_step (a := a) (d := d) ps s0 k,
+    DeliverMsg.scheduleMsgs, DeliverMsg.foldList_forallActions, List.Forall]
+
+/-- The correctness of `d.foldList s ml ms` under the assumption `a.FairDeliverMsg d ps q`. -/
+theorem fairDeliverMsg_foldList {d : DeliverMsg P M S} {ps : Set P} {q : State P M S → Prop}
+    (hd : a.FairDeliverMsg d ps q) (s : State P M S)
+    (ml : List (Message P M)) (ms : Finset (Message P M))
+    (hs : q s ∧ ∀ m, m ∈ ml → ¬ m ∈ ms → m ∈ s.msgs ∧ m.dest ∈ ps) :
+    let (xl, t) := d.foldList s ml ms
+    a.lts.MTr s xl t ∧ q t ∧ ∀ m, m ∈ ml → ¬ m ∈ ms → some m ∈ xl := by
+  induction ml generalizing s ms
+  case nil => grind [DeliverMsg.foldList, LTS.MTr]
+  case cons m ml h_ind =>
+    by_cases h_m : m ∈ ms
+    · grind [DeliverMsg.foldList]
+    · let xl1 := (d s m).fst
+      let s1 := (d s m).snd
+      let ms' := ms ∪ xl1.reduceOption.toFinset
+      have (m' : Message P M) : m' ∈ xl1.reduceOption.toFinset ↔ some m' ∈ xl1 := by
+        simp [List.mem_toFinset, List.reduceOption_mem_iff]
+      have (m' : Message P M) : m' ∈ ml → ¬ m' ∈ ms' → m' ∈ s1.msgs := by
+        grind [Algorithm.FairDeliverMsg, Algorithm.mTr_notRcvd_enabled]
+      grind [DeliverMsg.foldList, Algorithm.FairDeliverMsg, LTS.MTr.comp]
+
+/-- The correctness of `d.scheduleMsgs ps s` under the assumption `a.FairDeliverMsg d ps q`. -/
+theorem fairDeliverMsg_scheduleMsgs {d : DeliverMsg P M S} {ps : Set P} {q : State P M S → Prop}
+    (hd : a.FairDeliverMsg d ps q) (s : State P M S) (hs : q s) :
+    let xl := (d.scheduleMsgs ps s).fst
+    let t := (d.scheduleMsgs ps s).snd
+    q t ∧ a.lts.MTr s xl t ∧ xl.length > 0 ∧ ∀ m, m ∈ s.msgs → m.dest ∈ ps → some m ∈ xl := by
+  classical
+  intro xl t
+  let ms := s.msgs.filter (fun m ↦ m.dest ∈ ps)
+  by_cases h_ms : ms = 0
+  · have h1 : xl = [none] ∧ t = s := by grind [DeliverMsg.scheduleMsgs]
+    simp [ms, eq_zero_iff_forall_notMem] at h_ms
+    split_ands <;> try grind
+    simp only [h1]
+    apply LTS.MTr.single
+    grind [Algorithm.lts]
+  · have : q t ∧ a.lts.MTr s xl t ∧ ∀ m, m ∈ ms.toList → some m ∈ xl := by
+      grind [DeliverMsg.scheduleMsgs, fairDeliverMsg_foldList hd s ms.toList ∅ (by simp [ms, hs])]
+    split_ands <;> try grind [mem_toList, mem_filter]
+    obtain ⟨m, h_ms⟩ := exists_mem_of_ne_zero h_ms
+    suffices some m ∈ xl by grind
+    grind [mem_toList]
+
+/-- The correctness of `a.fairSegEnds d ps s0` and `a.fairSegActions d ps s0`
+under the assumption `a.FairDeliverMsg d ps q`. -/
+theorem fair_fairSegs {d : DeliverMsg P M S} {ps : Set P} {q : State P M S → Prop}
+    (hd : a.FairDeliverMsg d ps q) (s0 : State P M S) (hs0 : q s0) :
+    let ts := a.fairSegEnds d ps s0
+    let xls := a.fairSegActions d ps s0
+    ∀ k, q (ts k) ∧ a.lts.MTr (ts k) (xls k) (ts (k + 1)) ∧ (xls k).length > 0 ∧
+      ∀ m, m ∈ (ts k).msgs → m.dest ∈ ps → some m ∈ xls k := by
+  classical
+  intro ts xls k
+  induction k <;> grind [fairScheduler_init, fairScheduler_step, fairDeliverMsg_scheduleMsgs]
+
+/-- Given an infinite sequence of non-empty finite executions of algorithm `a`,
+if all messages with destinations in `ps` that are in-flight at the beginning of each
+finite execution are delivered in that finite execution, then those finite executions can
+be concatenated into an infinite execution of `a` in which every process in `ps` is fair. -/
+theorem flatten_fairSegs {ps : Set P}
+    {ts : ωSequence (State P M S)} {xls : ωSequence (List (Action P M))}
+    (hmtr : ∀ k, a.lts.MTr (ts k) (xls k) (ts (k + 1)))
+    (hpos : ∀ k, (xls k).length > 0)
+    (hsch : ∀ k m, m ∈ (ts k).msgs → m.dest ∈ ps → some m ∈ xls k) :
+    ∃ ss, a.lts.OmegaExecution ss xls.flatten ∧ (∀ k, ss (xls.cumLen k) = ts k) ∧
+      ∀ p, p ∈ ps → ProcFair p ss xls.flatten := by
+  obtain ⟨ss, h_omega, h_ts⟩ := LTS.OmegaExecution.flatten_mTr hmtr hpos
+  use ss, h_omega, h_ts
+  rintro p h_m m ⟨rfl⟩
+  by_contra! ⟨k, h_k, h_k'⟩
+  have h_xls : ∃ᶠ n in atTop, n ∈ xls.cumLen '' univ := by
+    apply frequently_iff_strictMono.mpr
+    use xls.cumLen
+    grind [cumLen_strictMono]
+  obtain ⟨j, _, h_j⟩ : ∃ j, k ≤ xls.cumLen j ∧ m ∈ (ts j).msgs := by
+    obtain ⟨n, _, j, _, _⟩ := frequently_atTop.mp h_xls k
+    grind [Algorithm.omega_notRcvd_enabled h_omega h_k h_k']
+  obtain ⟨i, _, _⟩ := List.getElem_of_mem <| hsch j m h_j h_m
+  grind [extract_flatten hpos j]
+
+/-- Under the assumption `a.FairDeliverMsg d ps q`, the infinite sequence of finite executions
+of `a` represented by `a.fairSegEnds d ps s0` and `a.fairSegActions d ps s0` can be concatenated
+into an infinite execution of `a` in which every process in `ps` is fair and `q` is true at
+the ends of all those finite executions. -/
+theorem fair_omegaExecution {d : DeliverMsg P M S} {ps : Set P} {q : State P M S → Prop}
+    (hd : a.FairDeliverMsg d ps q) (s0 : State P M S) (hs0 : q s0) :
+    let ts := a.fairSegEnds d ps s0
+    let xls := a.fairSegActions d ps s0
+    ∃ ss, a.lts.OmegaExecution ss xls.flatten ∧
+      ss 0 = s0 ∧ (∀ k, ss (xls.cumLen k) = ts k) ∧
+      (∀ k, q (ss (xls.cumLen k))) ∧ (∀ k, (xls k).length > 0) ∧
+      ∀ p, p ∈ ps → ProcFair p ss xls.flatten := by
+  intro ts xls
+  obtain ⟨h_q, hmtr, hpos, hsch⟩ :
+      (∀ k, q (ts k)) ∧
+      (∀ k, a.lts.MTr (ts k) (xls k) (ts (k + 1))) ∧
+      (∀ k, (xls k).length > 0) ∧
+      (∀ k m, m ∈ (ts k).msgs → m.dest ∈ ps → some m ∈ xls k) := by
+    grind [fair_fairSegs hd s0 hs0]
+  obtain ⟨ss, _, _, _⟩ := flatten_fairSegs hmtr hpos hsch
+  have : ss 0 = s0 := by grind [fairScheduler_init]
+  use ss
+  grind
+
+/-- If `d.ForallActions r`, then the concatenation of all `a.fairSegActions d ps s0` segments
+can only use actions satisfying `r`. -/
+theorem omega_forall_actions {d : DeliverMsg P M S} {ps : Set P}
+    {q : State P M S → Prop} {r : Action P M → Prop}
+    (hd : a.FairDeliverMsg d ps q) (s0 : State P M S) (hs0 : q s0)
+    (ha : d.ForallActions r) (hn : r none) :
+    ∀ k, r ((a.fairSegActions d ps s0).flatten k) := by
+  have hpos : ∀ k, (a.fairSegActions d ps s0 k).length > 0 := by grind [fair_fairSegs hd s0 hs0]
+  simp only [forall_flatten_iff hpos]
+  grind [fairSeg_forallActions]
+
+end FairScheduler
+
+end Cslib.FLP