Documentation

Mathlib.Data.List.Sort

Sorting algorithms on lists #

In this file we define List.Sorted r l to be an alias for Pairwise r l. This alias is preferred in the case that r is a < or -like relation. Then we define two sorting algorithms: List.insertionSort and List.mergeSort, and prove their correctness.

The predicate List.Sorted #

def List.Sorted {α : Type u_1} (R : ααProp) :
List αProp

Sorted r l is the same as Pairwise r l, preferred in the case that r is a < or -like relation (transitive and antisymmetric or asymmetric)

Equations
Instances For
    instance List.decidableSorted {α : Type uu} {r : ααProp} [DecidableRel r] (l : List α) :
    Equations
    theorem List.Sorted.le_of_lt {α : Type uu} [Preorder α] {l : List α} (h : List.Sorted (fun (x x_1 : α) => x < x_1) l) :
    List.Sorted (fun (x x_1 : α) => x x_1) l
    theorem List.Sorted.lt_of_le {α : Type uu} [PartialOrder α] {l : List α} (h₁ : List.Sorted (fun (x x_1 : α) => x x_1) l) (h₂ : List.Nodup l) :
    List.Sorted (fun (x x_1 : α) => x < x_1) l
    theorem List.Sorted.ge_of_gt {α : Type uu} [Preorder α] {l : List α} (h : List.Sorted (fun (x x_1 : α) => x > x_1) l) :
    List.Sorted (fun (x x_1 : α) => x x_1) l
    theorem List.Sorted.gt_of_ge {α : Type uu} [PartialOrder α] {l : List α} (h₁ : List.Sorted (fun (x x_1 : α) => x x_1) l) (h₂ : List.Nodup l) :
    List.Sorted (fun (x x_1 : α) => x > x_1) l
    @[simp]
    theorem List.sorted_nil {α : Type uu} {r : ααProp} :
    theorem List.Sorted.of_cons {α : Type uu} {r : ααProp} {a : α} {l : List α} :
    List.Sorted r (a :: l)List.Sorted r l
    theorem List.Sorted.tail {α : Type uu} {r : ααProp} {l : List α} (h : List.Sorted r l) :
    theorem List.rel_of_sorted_cons {α : Type uu} {r : ααProp} {a : α} {l : List α} :
    List.Sorted r (a :: l)bl, r a b
    theorem List.Sorted.head!_le {α : Type uu} [Inhabited α] [Preorder α] {a : α} {l : List α} (h : List.Sorted (fun (x x_1 : α) => x < x_1) l) (ha : a l) :
    theorem List.Sorted.le_head! {α : Type uu} [Inhabited α] [Preorder α] {a : α} {l : List α} (h : List.Sorted (fun (x x_1 : α) => x > x_1) l) (ha : a l) :
    @[simp]
    theorem List.sorted_cons {α : Type uu} {r : ααProp} {a : α} {l : List α} :
    List.Sorted r (a :: l) (bl, r a b) List.Sorted r l
    theorem List.Sorted.nodup {α : Type uu} {r : ααProp} [IsIrrefl α r] {l : List α} (h : List.Sorted r l) :
    theorem List.eq_of_perm_of_sorted {α : Type uu} {r : ααProp} [IsAntisymm α r] {l₁ : List α} {l₂ : List α} (hp : List.Perm l₁ l₂) (hs₁ : List.Sorted r l₁) (hs₂ : List.Sorted r l₂) :
    l₁ = l₂
    theorem List.sublist_of_subperm_of_sorted {α : Type uu} {r : ααProp} [IsAntisymm α r] {l₁ : List α} {l₂ : List α} (hp : List.Subperm l₁ l₂) (hs₁ : List.Sorted r l₁) (hs₂ : List.Sorted r l₂) :
    List.Sublist l₁ l₂
    @[simp]
    theorem List.sorted_singleton {α : Type uu} {r : ααProp} (a : α) :
    theorem List.Sorted.rel_get_of_lt {α : Type uu} {r : ααProp} {l : List α} (h : List.Sorted r l) {a : Fin (List.length l)} {b : Fin (List.length l)} (hab : a < b) :
    r (List.get l a) (List.get l b)
    theorem List.Sorted.rel_nthLe_of_lt {α : Type uu} {r : ααProp} {l : List α} (h : List.Sorted r l) {a : } {b : } (ha : a < List.length l) (hb : b < List.length l) (hab : a < b) :
    r (List.nthLe l a ha) (List.nthLe l b hb)
    theorem List.Sorted.rel_get_of_le {α : Type uu} {r : ααProp} [IsRefl α r] {l : List α} (h : List.Sorted r l) {a : Fin (List.length l)} {b : Fin (List.length l)} (hab : a b) :
    r (List.get l a) (List.get l b)
    theorem List.Sorted.rel_nthLe_of_le {α : Type uu} {r : ααProp} [IsRefl α r] {l : List α} (h : List.Sorted r l) {a : } {b : } (ha : a < List.length l) (hb : b < List.length l) (hab : a b) :
    r (List.nthLe l a ha) (List.nthLe l b hb)
    theorem List.Sorted.rel_of_mem_take_of_mem_drop {α : Type uu} {r : ααProp} {l : List α} (h : List.Sorted r l) {k : } {x : α} {y : α} (hx : x List.take k l) (hy : y List.drop k l) :
    r x y
    theorem List.sorted_ofFn_iff {n : } {α : Type uu} {f : Fin nα} {r : ααProp} :
    List.Sorted r (List.ofFn f) ((fun (x x_1 : Fin n) => x < x_1) r) f f
    @[simp]
    theorem List.sorted_lt_ofFn_iff {n : } {α : Type uu} [Preorder α] {f : Fin nα} :
    List.Sorted (fun (x x_1 : α) => x < x_1) (List.ofFn f) StrictMono f

    The list List.ofFn f is strictly sorted with respect to (· ≤ ·) if and only if f is strictly monotone.

    @[simp]
    theorem List.sorted_le_ofFn_iff {n : } {α : Type uu} [Preorder α] {f : Fin nα} :
    List.Sorted (fun (x x_1 : α) => x x_1) (List.ofFn f) Monotone f

    The list List.ofFn f is sorted with respect to (· ≤ ·) if and only if f is monotone.

    @[deprecated List.sorted_le_ofFn_iff]
    theorem List.monotone_iff_ofFn_sorted {n : } {α : Type uu} [Preorder α] {f : Fin nα} :
    Monotone f List.Sorted (fun (x x_1 : α) => x x_1) (List.ofFn f)

    A tuple is monotone if and only if the list obtained from it is sorted.

    theorem Monotone.ofFn_sorted {n : } {α : Type uu} [Preorder α] {f : Fin nα} :
    Monotone fList.Sorted (fun (x x_1 : α) => x x_1) (List.ofFn f)

    The list obtained from a monotone tuple is sorted.

    Insertion sort #

    def List.orderedInsert {α : Type uu} (r : ααProp) [DecidableRel r] (a : α) :
    List αList α

    orderedInsert a l inserts a into l at such that orderedInsert a l is sorted if l is.

    Equations
    Instances For
      def List.insertionSort {α : Type uu} (r : ααProp) [DecidableRel r] :
      List αList α

      insertionSort l returns l sorted using the insertion sort algorithm.

      Equations
      Instances For
        @[simp]
        theorem List.orderedInsert_nil {α : Type uu} (r : ααProp) [DecidableRel r] (a : α) :
        theorem List.orderedInsert_length {α : Type uu} (r : ααProp) [DecidableRel r] (L : List α) (a : α) :
        theorem List.orderedInsert_eq_take_drop {α : Type uu} (r : ααProp) [DecidableRel r] (a : α) (l : List α) :
        List.orderedInsert r a l = List.takeWhile (fun (b : α) => decide ¬r a b) l ++ a :: List.dropWhile (fun (b : α) => decide ¬r a b) l

        An alternative definition of orderedInsert using takeWhile and dropWhile.

        theorem List.insertionSort_cons_eq_take_drop {α : Type uu} (r : ααProp) [DecidableRel r] (a : α) (l : List α) :
        List.insertionSort r (a :: l) = List.takeWhile (fun (b : α) => decide ¬r a b) (List.insertionSort r l) ++ a :: List.dropWhile (fun (b : α) => decide ¬r a b) (List.insertionSort r l)
        @[simp]
        theorem List.mem_orderedInsert {α : Type uu} (r : ααProp) [DecidableRel r] {a : α} {b : α} {l : List α} :
        a List.orderedInsert r b l a = b a l
        theorem List.perm_orderedInsert {α : Type uu} (r : ααProp) [DecidableRel r] (a : α) (l : List α) :
        theorem List.orderedInsert_count {α : Type uu} (r : ααProp) [DecidableRel r] [DecidableEq α] (L : List α) (a : α) (b : α) :
        List.count a (List.orderedInsert r b L) = List.count a L + if a = b then 1 else 0
        theorem List.perm_insertionSort {α : Type uu} (r : ααProp) [DecidableRel r] (l : List α) :
        theorem List.Sorted.insertionSort_eq {α : Type uu} {r : ααProp} [DecidableRel r] {l : List α} :

        If l is already List.Sorted with respect to r, then insertionSort does not change it.

        theorem List.erase_orderedInsert {α : Type uu} {r : ααProp} [DecidableRel r] [DecidableEq α] [IsRefl α r] (x : α) (xs : List α) :

        For a reflexive relation, insert then erasing is the identity.

        theorem List.erase_orderedInsert_of_not_mem {α : Type uu} {r : ααProp} [DecidableRel r] [DecidableEq α] {x : α} {xs : List α} (hx : xxs) :

        Inserting then erasing an element that is absent is the identity.

        theorem List.orderedInsert_erase {α : Type uu} {r : ααProp} [DecidableRel r] [DecidableEq α] [IsAntisymm α r] (x : α) (xs : List α) (hx : x xs) (hxs : List.Sorted r xs) :

        For an antisymmetric relation, erasing then inserting is the identity.

        theorem List.sublist_orderedInsert {α : Type uu} {r : ααProp} [DecidableRel r] (x : α) (xs : List α) :
        theorem List.Sorted.orderedInsert {α : Type uu} {r : ααProp} [DecidableRel r] [IsTotal α r] [IsTrans α r] (a : α) (l : List α) :
        theorem List.sorted_insertionSort {α : Type uu} (r : ααProp) [DecidableRel r] [IsTotal α r] [IsTrans α r] (l : List α) :

        The list List.insertionSort r l is List.Sorted with respect to r.

        Merge sort #

        def List.split {α : Type uu} :
        List αList α × List α

        Split l into two lists of approximately equal length.

        split [1, 2, 3, 4, 5] = ([1, 3, 5], [2, 4])

        Equations
        Instances For
          theorem List.split_cons_of_eq {α : Type uu} (a : α) {l : List α} {l₁ : List α} {l₂ : List α} (h : List.split l = (l₁, l₂)) :
          List.split (a :: l) = (a :: l₂, l₁)
          theorem List.length_split_le {α : Type uu} {l : List α} {l₁ : List α} {l₂ : List α} :
          theorem List.length_split_lt {α : Type uu} {a : α} {b : α} {l : List α} {l₁ : List α} {l₂ : List α} (h : List.split (a :: b :: l) = (l₁, l₂)) :
          theorem List.perm_split {α : Type uu} {l : List α} {l₁ : List α} {l₂ : List α} :
          List.split l = (l₁, l₂)List.Perm l (l₁ ++ l₂)
          def List.mergeSort {α : Type uu} (r : ααProp) [DecidableRel r] :
          List αList α

          Implementation of a merge sort algorithm to sort a list.

          Equations
          Instances For
            theorem List.mergeSort_cons_cons {α : Type uu} (r : ααProp) [DecidableRel r] {a : α} {b : α} {l : List α} {l₁ : List α} {l₂ : List α} (h : List.split (a :: b :: l) = (l₁, l₂)) :
            List.mergeSort r (a :: b :: l) = List.merge (fun (x x_1 : α) => decide (r x x_1)) (List.mergeSort r l₁) (List.mergeSort r l₂)
            theorem List.perm_mergeSort {α : Type uu} (r : ααProp) [DecidableRel r] (l : List α) :
            @[simp]
            theorem List.length_mergeSort {α : Type uu} (r : ααProp) [DecidableRel r] (l : List α) :
            theorem List.Sorted.merge {α : Type uu} {r : ααProp} [DecidableRel r] [IsTotal α r] [IsTrans α r] {l : List α} {l' : List α} :
            List.Sorted r lList.Sorted r l'List.Sorted r (List.merge (fun (x x_1 : α) => decide (r x x_1)) l l')
            theorem List.sorted_mergeSort {α : Type uu} (r : ααProp) [DecidableRel r] [IsTotal α r] [IsTrans α r] (l : List α) :
            theorem List.mergeSort_eq_self {α : Type uu} (r : ααProp) [DecidableRel r] [IsTotal α r] [IsTrans α r] [IsAntisymm α r] {l : List α} :
            theorem List.mergeSort_eq_insertionSort {α : Type uu} (r : ααProp) [DecidableRel r] [IsTotal α r] [IsTrans α r] [IsAntisymm α r] (l : List α) :
            @[simp]
            theorem List.mergeSort_nil {α : Type uu} (r : ααProp) [DecidableRel r] :
            @[simp]
            theorem List.mergeSort_singleton {α : Type uu} (r : ααProp) [DecidableRel r] (a : α) :
            List.mergeSort r [a] = [a]