sequential_preserves_conservation

formal source

 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
 248  · intro e tail ih s h
 249    have heH : e ∈ H := by
 250      have : e ∈ (e :: tail).toFinset := by
 251        simpa using List.mem_toFinset.mpr (by simp)
 252      simpa [hcover] using this
 253    have h' : Conservation (post s e) := preserve_single s e heH h
 254    simpa using ih (post s e) h'
 255
 256/-- Atomic tick (finite history): any finite recognition history admits a
 257    serialization with exactly one posting per tick that respects precedence. -/
 258theorem atomic_tick
 259    (prec : Precedence E) [DecidableRel prec] [DecidableEq E]
 260    (wf : WellFounded prec) (H : Finset E) :
 261    ∃ σ : Schedule E,
 262      σ.order.toFinset = H ∧
 263      ∀ {e₁ e₂}, e₁ ∈ H → e₂ ∈ H → prec e₁ e₂ →
 264        σ.order.indexOf e₁ < σ.order.indexOf e₂ := by