Documentation

Mathlib.Data.List.Sort

Sorting algorithms on lists #

In this file we define List.Sorted r l to be an alias for List.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 List.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 u} {r : ααProp} [DecidableRel r] (l : List α) :
    Equations
    • l.decidableSorted = l.instDecidablePairwise
    theorem List.Sorted.le_of_lt {α : Type u} [Preorder α] {l : List α} (h : List.Sorted (fun (x1 x2 : α) => x1 < x2) l) :
    List.Sorted (fun (x1 x2 : α) => x1 x2) l
    theorem List.Sorted.lt_of_le {α : Type u} [PartialOrder α] {l : List α} (h₁ : List.Sorted (fun (x1 x2 : α) => x1 x2) l) (h₂ : l.Nodup) :
    List.Sorted (fun (x1 x2 : α) => x1 < x2) l
    theorem List.Sorted.ge_of_gt {α : Type u} [Preorder α] {l : List α} (h : List.Sorted (fun (x1 x2 : α) => x1 > x2) l) :
    List.Sorted (fun (x1 x2 : α) => x1 x2) l
    theorem List.Sorted.gt_of_ge {α : Type u} [PartialOrder α] {l : List α} (h₁ : List.Sorted (fun (x1 x2 : α) => x1 x2) l) (h₂ : l.Nodup) :
    List.Sorted (fun (x1 x2 : α) => x1 > x2) l
    @[simp]
    theorem List.sorted_nil {α : Type u} {r : ααProp} :
    theorem List.Sorted.of_cons {α : Type u} {r : ααProp} {a : α} {l : List α} :
    List.Sorted r (a :: l)List.Sorted r l
    theorem List.Sorted.tail {α : Type u} {r : ααProp} {l : List α} (h : List.Sorted r l) :
    List.Sorted r l.tail
    theorem List.rel_of_sorted_cons {α : Type u} {r : ααProp} {a : α} {l : List α} :
    List.Sorted r (a :: l)bl, r a b
    theorem List.Sorted.head!_le {α : Type u} [Inhabited α] [Preorder α] {a : α} {l : List α} (h : List.Sorted (fun (x1 x2 : α) => x1 < x2) l) (ha : a l) :
    l.head! a
    theorem List.Sorted.le_head! {α : Type u} [Inhabited α] [Preorder α] {a : α} {l : List α} (h : List.Sorted (fun (x1 x2 : α) => x1 > x2) l) (ha : a l) :
    a l.head!
    @[simp]
    theorem List.sorted_cons {α : Type u} {r : ααProp} {a : α} {l : List α} :
    List.Sorted r (a :: l) (∀ bl, r a b) List.Sorted r l
    theorem List.Sorted.nodup {α : Type u} {r : ααProp} [IsIrrefl α r] {l : List α} (h : List.Sorted r l) :
    l.Nodup
    theorem List.eq_of_perm_of_sorted {α : Type u} {r : ααProp} [IsAntisymm α r] {l₁ : List α} {l₂ : List α} (hp : l₁.Perm l₂) (hs₁ : List.Sorted r l₁) (hs₂ : List.Sorted r l₂) :
    l₁ = l₂
    theorem List.sublist_of_subperm_of_sorted {α : Type u} {r : ααProp} [IsAntisymm α r] {l₁ : List α} {l₂ : List α} (hp : l₁.Subperm l₂) (hs₁ : List.Sorted r l₁) (hs₂ : List.Sorted r l₂) :
    l₁.Sublist l₂
    @[simp]
    theorem List.sorted_singleton {α : Type u} {r : ααProp} (a : α) :
    theorem List.Sorted.rel_get_of_lt {α : Type u} {r : ααProp} {l : List α} (h : List.Sorted r l) {a : Fin l.length} {b : Fin l.length} (hab : a < b) :
    r (l.get a) (l.get b)
    theorem List.Sorted.rel_get_of_le {α : Type u} {r : ααProp} [IsRefl α r] {l : List α} (h : List.Sorted r l) {a : Fin l.length} {b : Fin l.length} (hab : a b) :
    r (l.get a) (l.get b)
    theorem List.Sorted.rel_of_mem_take_of_mem_drop {α : Type u} {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 u} {f : Fin nα} {r : ααProp} :
    List.Sorted r (List.ofFn f) ((fun (x1 x2 : Fin n) => x1 < x2) r) f f
    @[simp]
    theorem List.sorted_lt_ofFn_iff {n : } {α : Type u} {f : Fin nα} [Preorder α] :
    List.Sorted (fun (x1 x2 : α) => x1 < x2) (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 u} {f : Fin nα} [Preorder α] :
    List.Sorted (fun (x1 x2 : α) => x1 x2) (List.ofFn f) Monotone f

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

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

    The list obtained from a monotone tuple is sorted.

    Insertion sort #

    def List.orderedInsert {α : Type u} (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
      theorem List.orderedInsert_of_le {α : Type u} (r : ααProp) [DecidableRel r] {a : α} {b : α} (l : List α) (h : r a b) :
      List.orderedInsert r a (b :: l) = a :: b :: l
      def List.insertionSort {α : Type u} (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 u} (r : ααProp) [DecidableRel r] (a : α) :
        theorem List.orderedInsert_length {α : Type u} (r : ααProp) [DecidableRel r] (L : List α) (a : α) :
        (List.orderedInsert r a L).length = L.length + 1
        theorem List.orderedInsert_eq_take_drop {α : Type u} (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 u} (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 u} (r : ααProp) [DecidableRel r] {a : α} {b : α} {l : List α} :
        a List.orderedInsert r b l a = b a l
        theorem List.map_orderedInsert {α : Type u} {β : Type v} (r : ααProp) (s : ββProp) [DecidableRel r] [DecidableRel s] (f : αβ) (l : List α) (x : α) (hl₁ : al, r a x s (f a) (f x)) (hl₂ : al, r x a s (f x) (f a)) :
        theorem List.perm_orderedInsert {α : Type u} (r : ααProp) [DecidableRel r] (a : α) (l : List α) :
        (List.orderedInsert r a l).Perm (a :: l)
        theorem List.orderedInsert_count {α : Type u} (r : ααProp) [DecidableRel r] [DecidableEq α] (L : List α) (a : α) (b : α) :
        List.count a (List.orderedInsert r b L) = List.count a L + if b = a then 1 else 0
        theorem List.perm_insertionSort {α : Type u} (r : ααProp) [DecidableRel r] (l : List α) :
        (List.insertionSort r l).Perm l
        @[simp]
        theorem List.mem_insertionSort {α : Type u} (r : ααProp) [DecidableRel r] {l : List α} {x : α} :
        @[simp]
        theorem List.length_insertionSort {α : Type u} (r : ααProp) [DecidableRel r] (l : List α) :
        (List.insertionSort r l).length = l.length
        theorem List.insertionSort_cons {α : Type u} (r : ααProp) [DecidableRel r] {a : α} {l : List α} (h : bl, r a b) :
        theorem List.map_insertionSort {α : Type u} {β : Type v} (r : ααProp) (s : ββProp) [DecidableRel r] [DecidableRel s] (f : αβ) (l : List α) (hl : al, bl, r a b s (f a) (f b)) :
        theorem List.Sorted.insertionSort_eq {α : Type u} {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 u} {r : ααProp} [DecidableRel r] [DecidableEq α] [IsRefl α r] (x : α) (xs : List α) :
        (List.orderedInsert r x xs).erase x = xs

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

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

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

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

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

        theorem List.sublist_orderedInsert {α : Type u} {r : ααProp} [DecidableRel r] (x : α) (xs : List α) :
        xs.Sublist (List.orderedInsert r x xs)
        theorem List.cons_sublist_orderedInsert {α : Type u} {r : ααProp} [DecidableRel r] {l : List α} {c : List α} {a : α} (hl : c.Sublist l) (ha : a'c, r a a') :
        (a :: c).Sublist (List.orderedInsert r a l)
        theorem List.Sublist.orderedInsert_sublist {α : Type u} {r : ααProp} [DecidableRel r] [IsTrans α r] {as : List α} {bs : List α} (x : α) (hs : as.Sublist bs) (hb : List.Sorted r bs) :
        (List.orderedInsert r x as).Sublist (List.orderedInsert r x bs)
        theorem List.Sorted.orderedInsert {α : Type u} {r : ααProp} [DecidableRel r] [IsTotal α r] [IsTrans α r] (a : α) (l : List α) :
        theorem List.sorted_insertionSort {α : Type u} (r : ααProp) [DecidableRel r] [IsTotal α r] [IsTrans α r] (l : List α) :

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

        theorem List.sublist_insertionSort {α : Type u} {r : ααProp} [DecidableRel r] {l : List α} {c : List α} (hr : List.Pairwise r c) (hc : c.Sublist l) :
        c.Sublist (List.insertionSort r l)

        If c is a sorted sublist of l, then c is still a sublist of insertionSort r l.

        theorem List.pair_sublist_insertionSort {α : Type u} {r : ααProp} [DecidableRel r] {a : α} {b : α} {l : List α} (hab : r a b) (h : [a, b].Sublist l) :
        [a, b].Sublist (List.insertionSort r l)

        Another statement of stability of insertion sort. If a pair [a, b] is a sublist of l and r a b, then [a, b] is still a sublist of insertionSort r l.

        theorem List.sublist_insertionSort' {α : Type u} {r : ααProp} [DecidableRel r] [IsAntisymm α r] [IsTotal α r] [IsTrans α r] {l : List α} {c : List α} (hs : List.Sorted r c) (hc : c.Subperm l) :
        c.Sublist (List.insertionSort r l)

        A version of insertionSort_stable which only assumes c <+~ l (instead of c <+ l), but additionally requires IsAntisymm α r, IsTotal α r and IsTrans α r.

        theorem List.pair_sublist_insertionSort' {α : Type u} {r : ααProp} [DecidableRel r] [IsAntisymm α r] [IsTotal α r] [IsTrans α r] {a : α} {b : α} {l : List α} (hab : r a b) (h : [a, b].Subperm l) :
        [a, b].Sublist (List.insertionSort r l)

        Another statement of stability of insertion sort. If a pair [a, b] is a sublist of a permutation of l and a ≼ b, then [a, b] is still a sublist of insertionSort r l.

        Merge sort #

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

        Split l into two lists of approximately equal length.

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

        Equations
        • [].split = ([], [])
        • (b :: l).split = match l.split with | (l₁, l₂) => (b :: l₂, l₁)
        Instances For
          theorem List.split_cons_of_eq {α : Type u} (a : α) {l : List α} {l₁ : List α} {l₂ : List α} (h : l.split = (l₁, l₂)) :
          (a :: l).split = (a :: l₂, l₁)
          @[simp]
          theorem List.map_split {α : Type u} {β : Type v} (f : αβ) (l : List α) :
          (List.map f l).split = (List.map f l.split.1, List.map f l.split.2)
          @[simp]
          theorem List.mem_split_iff {α : Type u} {x : α} {l : List α} :
          x l.split.1 x l.split.2 x l
          theorem List.length_split_le {α : Type u} {l : List α} {l₁ : List α} {l₂ : List α} :
          l.split = (l₁, l₂)l₁.length l.length l₂.length l.length
          theorem List.length_split_fst_le {α : Type u} (l : List α) :
          l.split.1.length l.length
          theorem List.length_split_snd_le {α : Type u} (l : List α) :
          l.split.2.length l.length
          theorem List.length_split_lt {α : Type u} {a : α} {b : α} {l : List α} {l₁ : List α} {l₂ : List α} (h : (a :: b :: l).split = (l₁, l₂)) :
          l₁.length < (a :: b :: l).length l₂.length < (a :: b :: l).length
          theorem List.perm_split {α : Type u} {l : List α} {l₁ : List α} {l₂ : List α} :
          l.split = (l₁, l₂)l.Perm (l₁ ++ l₂)
          @[irreducible]
          def List.mergeSort' {α : Type u} (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 u} (r : ααProp) [DecidableRel r] {a : α} {b : α} {l : List α} {l₁ : List α} {l₂ : List α} (h : (a :: b :: l).split = (l₁, l₂)) :
            List.mergeSort' r (a :: b :: l) = (List.mergeSort' r l₁).merge (List.mergeSort' r l₂) fun (x1 x2 : α) => decide (r x1 x2)
            @[irreducible]
            theorem List.perm_mergeSort' {α : Type u} (r : ααProp) [DecidableRel r] (l : List α) :
            (List.mergeSort' r l).Perm l
            @[simp]
            theorem List.mem_mergeSort' {α : Type u} (r : ααProp) [DecidableRel r] {l : List α} {x : α} :
            @[simp]
            theorem List.length_mergeSort' {α : Type u} (r : ααProp) [DecidableRel r] (l : List α) :
            (List.mergeSort' r l).length = l.length
            @[irreducible]
            theorem List.Sorted.merge {α : Type u} {r : ααProp} [DecidableRel r] [IsTotal α r] [IsTrans α r] {l : List α} {l' : List α} :
            List.Sorted r lList.Sorted r l'List.Sorted r (l.merge l' fun (x1 x2 : α) => decide (r x1 x2))
            @[irreducible]
            theorem List.sorted_mergeSort' {α : Type u} (r : ααProp) [DecidableRel r] [IsTotal α r] [IsTrans α r] (l : List α) :
            theorem List.mergeSort'_eq_self {α : Type u} (r : ααProp) [DecidableRel r] [IsTotal α r] [IsTrans α r] [IsAntisymm α r] {l : List α} :
            theorem List.mergeSort'_eq_insertionSort {α : Type u} (r : ααProp) [DecidableRel r] [IsTotal α r] [IsTrans α r] [IsAntisymm α r] (l : List α) :
            @[simp]
            theorem List.mergeSort'_nil {α : Type u} (r : ααProp) [DecidableRel r] :
            @[simp]
            theorem List.mergeSort'_singleton {α : Type u} (r : ααProp) [DecidableRel r] (a : α) :
            List.mergeSort' r [a] = [a]
            @[irreducible]
            theorem List.map_mergeSort' {α : Type u} {β : Type v} (r : ααProp) (s : ββProp) [DecidableRel r] [DecidableRel s] (f : αβ) (l : List α) (hl : al, bl, r a b s (f a) (f b)) :