feat(Data/*/Sort): lemmas on sorted lists (#16078)

The main thing we prove is that if `l` is a list, and `a` is smaller than all elements on it, then `sort r (a :: l) = a :: sort r l`.

Author: vihdzp

Mathlib/Data/Finset/Basic.lean

@@ -2912,6 +2912,11 @@ theorem toList_toFinset [DecidableEq α] (s : Finset α) : s.toList.toFinset = s
   ext
   simp
 
+theorem _root_.List.toFinset_toList [DecidableEq α] {s : List α} (hs : s.Nodup) :
+    s.toFinset.toList.Perm s := by
+  apply List.perm_of_nodup_nodup_toFinset_eq (nodup_toList _) hs
+  rw [toList_toFinset]
+
 @[simp]
 theorem toList_eq_singleton_iff {a : α} {s : Finset α} : s.toList = [a] ↔ s = {a} := by
   rw [toList, Multiset.toList_eq_singleton_iff, val_eq_singleton_iff]

Mathlib/Data/Finset/Sort.lean

@@ -32,6 +32,10 @@ variable (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α
 def sort (s : Finset α) : List α :=
   Multiset.sort r s.1
 
+@[simp]
+theorem sort_val (s : Finset α) : Multiset.sort r s.val = sort r s :=
+  rfl
+
 @[simp]
 theorem sort_sorted (s : Finset α) : List.Sorted r (sort r s) :=
   Multiset.sort_sorted _ _
@@ -64,11 +68,27 @@ theorem sort_empty : sort r ∅ = [] :=
 theorem sort_singleton (a : α) : sort r {a} = [a] :=
   Multiset.sort_singleton r a
 
+theorem sort_cons {a : α} {s : Finset α} (h₁ : ∀ b ∈ s, r a b) (h₂ : a ∉ s) :
+    sort r (cons a s h₂) = a :: sort r s := by
+  rw [sort, cons_val, Multiset.sort_cons r a _ h₁, sort_val]
+
+theorem sort_insert [DecidableEq α] {a : α} {s : Finset α} (h₁ : ∀ b ∈ s, r a b) (h₂ : a ∉ s) :
+    sort r (insert a s) = a :: sort r s := by
+  rw [← cons_eq_insert _ _ h₂, sort_cons r h₁]
+
 open scoped List in
 theorem sort_perm_toList (s : Finset α) : sort r s ~ s.toList := by
   rw [← Multiset.coe_eq_coe]
   simp only [coe_toList, sort_eq]
 
+theorem _root_.List.toFinset_sort [DecidableEq α] {l : List α} (hl : l.Nodup) :
+    sort r l.toFinset = l ↔ l.Sorted r := by
+  refine ⟨?_, List.eq_of_perm_of_sorted ((sort_perm_toList r _).trans (List.toFinset_toList hl))
+    (sort_sorted r _)⟩
+  intro h
+  rw [← h]
+  exact sort_sorted r _
+
 end sort
 
 section SortLinearOrder

Mathlib/Data/List/Sort.lean

@@ -198,6 +198,10 @@ def orderedInsert (a : α) : List α → List α
   | [] => [a]
   | b :: l => if a ≼ b then a :: b :: l else b :: orderedInsert a l
 
+theorem orderedInsert_of_le {a b : α} (l : List α) (h : a ≼ b) :
+    orderedInsert r a (b :: l) = a :: b :: l :=
+  dif_pos h
+
 /-- `insertionSort l` returns `l` sorted using the insertion sort algorithm. -/
 @[simp]
 def insertionSort : List α → List α
@@ -281,6 +285,17 @@ theorem mem_insertionSort {l : List α} {x : α} : x ∈ l.insertionSort r ↔ x
 theorem length_insertionSort (l : List α) : (insertionSort r l).length = l.length :=
   (perm_insertionSort r _).length_eq
 
+theorem insertionSort_cons {a : α} {l : List α} (h : ∀ b ∈ l, r a b) :
+    insertionSort r (a :: l) = a :: insertionSort r l := by
+  rw [insertionSort]
+  cases hi : insertionSort r l with
+  | nil => rfl
+  | cons b m =>
+    rw [orderedInsert_of_le]
+    apply h b <| (mem_insertionSort r).1 _
+    rw [hi]
+    exact mem_cons_self b m
+
 theorem map_insertionSort (f : α → β) (l : List α) (hl : ∀ a ∈ l, ∀ b ∈ l, a ≼ b ↔ f a ≼ f b) :
     (l.insertionSort r).map f = (l.map f).insertionSort s := by
   induction l with

Mathlib/Data/Multiset/Sort.lean

@@ -62,6 +62,11 @@ theorem map_sort (f : α → β) (s : Multiset α)
   revert s
   exact Quot.ind fun _ => List.map_mergeSort' _ _ _ _
 
+theorem sort_cons (a : α) (s : Multiset α) :
+    (∀ b ∈ s, r a b) → sort r (a ::ₘ s) = a :: sort r s := by
+  refine Quot.inductionOn s fun l => ?_
+  simpa [mergeSort'_eq_insertionSort] using insertionSort_cons r
+
 end sort
 
 -- TODO: use a sort order if available, gh-18166