Insertion sort with exposed bodies

Mathlib does not expose the bodies of List.orderedInsert and List.insertionSort to other modules, so the kernel cannot reduce a computation that sorts through them, and a decide-checked equation about a computed relation gets stuck there. The two functions below are the same ones, written out again with their bodies exposed. The evaluators sort through these; each comes with a simp lemma rewriting it to Mathlib's, so that proofs reason with Mathlib's lemmas.

def List.orderedIns {α : Type u_1} (r : α → α → Prop) [DecidableRel r] (a : α) : List α → List α

List.orderedInsert, with an exposed body.

Equations

• List.orderedIns r a [] = [a]
• List.orderedIns r a (b :: l) = if r a b then a :: b :: l else b :: List.orderedIns r a l

def List.insSort {α : Type u_1} (r : α → α → Prop) [DecidableRel r] : List α → List α

List.insertionSort, with an exposed body.

Equations

• List.insSort r = List.foldr (List.orderedIns r) []

@[simp]

theorem List.orderedIns_eq {α : Type u_1} (r : α → α → Prop) [DecidableRel r] (a : α) (l : List α) : orderedIns r a l = orderedInsert r a l

Home · Documentation · Publications · Contributors · Source · Cite