Schedule

formal source

 199  exact hAux H.card H rfl
 200
 201/-- A sequential, one‑per‑tick schedule for a finite history `H`. -/
 202structure Schedule (E : Type _) where
 203  order : List E
 204  nodup : order.Pairwise (· ≠ ·)
 205
 206namespace Schedule
 207
 208variable [DecidableEq E]
 209
 210/-- Event at a given tick (index into the order), if any. -/
 211def postAtTick (σ : Schedule E) (n : ℕ) : Option E :=
 212  (σ.order.get? n)
 213
 214end Schedule
 215
 216/-- Existence of a one‑per‑tick schedule (finite history version). -/
 217theorem exists_sequential_schedule
 218    (prec : Precedence E) [DecidableRel prec] [DecidableEq E]
 219    (wf : WellFounded prec) (H : Finset E) :
 220    ∃ σ : Schedule E,
 221      σ.order.Pairwise (· ≠ ·) ∧
 222      σ.order.toFinset = H ∧
 223      (∀ {e₁ e₂}, e₁ ∈ H → e₂ ∈ H → prec e₁ e₂ →
 224        σ.order.indexOf e₁ < σ.order.indexOf e₂) := by
 225  classical
 226  refine ⟨⟨topoSort (E:=E) prec wf H, ?_⟩, ?_, ?_, ?_⟩
 227  · exact (topoSort_perm (E:=E) prec wf H).1
 228  · exact (topoSort_perm (E:=E) prec wf H).2
 229  · intro e₁ e₂ h₁ h₂ h12; exact topoSort_respects (E:=E) prec wf H h₁ h₂ h12
 230
 231/-- Generic preservation: if conservation holds initially and is preserved
 232    by single postings, then conservation holds along any sequential schedule