`topoSort`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.Atomicity
domain: Foundation
line: 72 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.Atomicity on GitHub at line 72.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  69  exact this a ha
  70
  71/-- Topological ordering on finite histories by iteratively removing minimal elements. -/
  72def topoSort
  73    (prec : Precedence E) [DecidableRel prec] [DecidableEq E]
  74    (wf : WellFounded prec) :
  75    ∀ H : Finset E, List E
  76  | H =>
  77    if h : H.Nonempty then
  78      let ⟨e, heH, hmin⟩ := exists_minimal_in (E:=E) prec wf h
  79      e :: topoSort prec wf (H.erase e)
  80    else []
  81  termination_by H => H.card
  82  decreasing_by
  83    classical
  84    simp_wf
  85    have : (H.erase _) .card < H.card := by
  86      simpa [Nat.lt_iff_add_one_le, Nat.succ_le_succ_iff] using
  87        Finset.card_erase_lt_of_mem heH
  88    simpa using this
  89
  90/-- `topoSort` covers exactly the elements of `H` with no duplicates. -/
  91lemma topoSort_perm
  92    (prec : Precedence E) [DecidableRel prec] [DecidableEq E]
  93    (wf : WellFounded prec) (H : Finset E) :
  94    (topoSort (E:=E) prec wf H).Pairwise (· ≠ ·) ∧
  95    (topoSort (E:=E) prec wf H).toFinset = H := by
  96  classical
  97  have hAux : ∀ n, ∀ H : Finset E, H.card = n →
  98      (topoSort (E:=E) prec wf H).Pairwise (· ≠ ·) ∧
  99      (topoSort (E:=E) prec wf H).toFinset = H := by
 100    refine Nat.rec ?base ?step
 101    · intro H hcard
 102      have hH : H = (∅ : Finset E) :=

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.