exists_sequential_schedule

formal source

 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
 233    for a finite history. -/
 234theorem sequential_preserves_conservation
 235    {S : Type _} (Conservation : S → Prop) (post : S → E → S)
 236    (prec : Precedence E)
 237    [DecidableRel prec] [DecidableEq E]
 238    (H : Finset E) (σ : Schedule E)
 239    (hcover : σ.order.toFinset = H)
 240    (s0 : S)
 241    (h0 : Conservation s0)
 242    (preserve_single : ∀ s e, e ∈ H → Conservation s → Conservation (post s e)) :
 243    Conservation (σ.order.foldl post s0) := by
 244  classical
 245  revert s0 h0
 246  refine σ.order.rec ?base ?step
 247  · intro s h; simpa using h