Precedence

formal source

  30open Finset
  31
  32/-- A precedence relation on events. Read `prec e₁ e₂` as “e₁ must occur before e₂”. -/
  33abbrev Precedence (E : Type _) := E → E → Prop
  34
  35namespace Atomicity
  36
  37variable {E : Type _}
  38
  39/-- `isMinimalIn prec H e` means `e` is in `H` and has no predecessors in `H`. -/
  40def isMinimalIn (prec : Precedence E) [DecidableEq E] [DecidableRel prec]
  41    (H : Finset E) (e : E) : Prop :=
  42  e ∈ H ∧ ∀ e' ∈ H, ¬ prec e' e
  43
  44lemma isMinimalIn.mem {prec : Precedence E} [DecidableEq E] [DecidableRel prec]
  45    {H : Finset E} {e : E} :
  46    isMinimalIn (E:=E) prec H e → e ∈ H :=
  47  And.left
  48
  49/-- Minimality existence on a finite, nonempty `H` under well‑founded precedence. -/
  50lemma exists_minimal_in
  51    (prec : Precedence E) [DecidableRel prec] [DecidableEq E]
  52    (wf : WellFounded prec) {H : Finset E} (hH : H.Nonempty) :
  53    ∃ e ∈ H, ∀ e' ∈ H, ¬ prec e' e := by
  54  classical
  55  refine hH.elim ?_
  56  intro a ha
  57  have : ∀ x : E, x ∈ H → ∃ m ∈ H, ∀ y ∈ H, ¬ prec y m := by
  58    intro x hx
  59    -- Well-founded recursion down the precedence relation until a minimal element is reached.
  60    refine wf.induction x (C := fun x => x ∈ H → ∃ m ∈ H, ∀ y ∈ H, ¬ prec y m) ?_ hx
  61    intro x ih hx
  62    by_cases hmin : ∀ y ∈ H, ¬ prec y x
  63    · exact ⟨x, hx, hmin⟩