Documentation

Init.Data.List.Sort.Basic

Definition of merge and mergeSort. #

These definitions are intended for verification purposes, and are replaced at runtime by efficient versions in Init.Data.List.Sort.Impl.

@[irreducible]
def List.merge {α : Type u_1} (xs : List α) (ys : List α) (le : autoParam (ααBool) _auto✝) :
List α

O(min |l| |r|). Merge two lists using le as a switch.

This version is not tail-recursive, but it is replaced at runtime by mergeTR using a @[csimp] lemma.

Equations
  • [].merge ys le = ys
  • xs.merge [] le = xs
  • (x :: xs_2).merge (y :: ys_2) le = if le x y = true then x :: xs_2.merge (y :: ys_2) le else y :: (x :: xs_2).merge ys_2 le
Instances For
    @[simp]
    theorem List.nil_merge {α : Type u_1} {le : ααBool} (ys : List α) :
    [].merge ys le = ys
    @[simp]
    theorem List.merge_right {α : Type u_1} {le : ααBool} (xs : List α) :
    xs.merge [] le = xs
    def List.splitInTwo {α : Type u_1} {n : Nat} (l : { l : List α // l.length = n }) :
    { l : List α // l.length = (n + 1) / 2 } × { l : List α // l.length = n / 2 }

    Split a list in two equal parts. If the length is odd, the first part will be one element longer.

    Equations
    Instances For
      @[irreducible]
      def List.mergeSort {α : Type u_1} (xs : List α) (le : autoParam (ααBool) _auto✝) :
      List α

      Simplified implementation of stable merge sort.

      This function is designed for reasoning about the algorithm, and is not efficient. (It particular it uses the non tail-recursive merge function, and so can not be run on large lists, but also makes unnecessary traversals of lists.) It is replaced at runtime in the compiler by mergeSortTR₂ using a @[csimp] lemma.

      Because we want the sort to be stable, it is essential that we split the list in two contiguous sublists.

      Equations
      Instances For
        def List.enumLE {α : Type u_1} (le : ααBool) (a : Nat × α) (b : Nat × α) :

        Given an ordering relation le : α → α → Bool, construct the reverse lexicographic ordering on Nat × α. which first compares the second components using le, but if these are equivalent (in the sense le a.2 b.2 && le b.2 a.2) then compares the first components using .

        This function is only used in stating the stability properties of mergeSort.

        Equations
        Instances For