Documentation

Init.Data.List.Sort.Impl

Replacing merge and mergeSort at runtime with tail-recursive and faster versions. #

We replace merge with mergeTR using a @[csimp] lemma.

We replace mergeSort in two steps:

There is no public API in this file; it solely exists to implement the @[csimp] lemmas affecting runtime behaviour.

Future work #

The current runtime implementation could be further improved in a number of ways, e.g.:

Because the theory developed for mergeSort is independent of the runtime implementation, as long as such improvements are carefully validated by benchmarking, they can be done without changing the theory, as long as a @[csimp] lemma is provided.

def List.MergeSort.Internal.mergeTR {α : Type u_1} (l₁ : List α) (l₂ : List α) (le : ααBool) :
List α

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

Equations
Instances For
    @[irreducible]
    def List.MergeSort.Internal.mergeTR.go {α : Type u_1} (le : ααBool) :
    List αList αList αList α
    Equations
    Instances For
      theorem List.MergeSort.Internal.mergeTR_go_eq :
      ∀ {α : Type u_1} {le : ααBool} {l₁ l₂ acc : List α}, List.MergeSort.Internal.mergeTR.go le l₁ l₂ acc = acc.reverse ++ l₁.merge l₂ le
      def List.MergeSort.Internal.splitRevAt {α : Type u_1} (n : Nat) (l : List α) :
      List α × List α

      Variant of splitAt, that does not reverse the first list, i.e splitRevAt n l = ((l.take n).reverse, l.drop n).

      This exists solely as an optimization for mergeSortTR and mergeSortTR₂, and should not be used elsewhere.

      Equations
      Instances For
        def List.MergeSort.Internal.splitRevAt.go {α : Type u_1} :
        List αNatList αList α × List α

        Auxiliary for splitAtRev: splitAtRev.go xs n acc = ((take n xs).reverse ++ acc, drop n xs).

        Equations
        Instances For
          theorem List.MergeSort.Internal.splitRevAt_go {α : Type u_1} (xs : List α) (n : Nat) (acc : List α) :
          List.MergeSort.Internal.splitRevAt.go xs n acc = ((List.take n xs).reverse ++ acc, List.drop n xs)
          def List.MergeSort.Internal.mergeSortTR {α : Type u_1} (l : List α) (le : autoParam (ααBool) _auto✝) :
          List α

          An intermediate speed-up for mergeSort. This version uses the tail-recurive mergeTR function as a subroutine.

          This is not the final version we use at runtime, as mergeSortTR₂ is faster. This definition is useful as an intermediate step in proving the @[csimp] lemma for mergeSortTR₂.

          Equations
          Instances For
            @[irreducible]
            def List.MergeSort.Internal.mergeSortTR.run {α : Type u_1} (le : autoParam (ααBool) _auto✝) {n : Nat} :
            { l : List α // l.length = n }List α
            Equations
            Instances For
              def List.MergeSort.Internal.splitRevInTwo {α : 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, reversing the first part. If the length is odd, the first part will be one element longer.

              Equations
              Instances For
                def List.MergeSort.Internal.splitRevInTwo' {α : Type u_1} {n : Nat} (l : { l : List α // l.length = n }) :
                { l : List α // l.length = n / 2 } × { l : List α // l.length = (n + 1) / 2 }

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

                Equations
                Instances For
                  def List.MergeSort.Internal.mergeSortTR₂ {α : Type u_1} (l : List α) (le : autoParam (ααBool) _auto✝) :
                  List α

                  Faster version of mergeSortTR, which avoids unnecessary list reversals.

                  Equations
                  Instances For
                    @[irreducible]
                    def List.MergeSort.Internal.mergeSortTR₂.run {α : Type u_1} (le : autoParam (ααBool) _auto✝) {n : Nat} :
                    { l : List α // l.length = n }List α
                    Equations
                    Instances For
                      @[irreducible]
                      def List.MergeSort.Internal.mergeSortTR₂.run' {α : Type u_1} (le : autoParam (ααBool) _auto✝) {n : Nat} :
                      { l : List α // l.length = n }List α
                      Equations
                      Instances For
                        theorem List.MergeSort.Internal.splitRevInTwo'_fst {α : Type u_1} {n : Nat} (l : { l : List α // l.length = n }) :
                        (List.MergeSort.Internal.splitRevInTwo' l).fst = (List.splitInTwo l.val.reverse, ).snd.val,
                        theorem List.MergeSort.Internal.splitRevInTwo'_snd {α : Type u_1} {n : Nat} (l : { l : List α // l.length = n }) :
                        (List.MergeSort.Internal.splitRevInTwo' l).snd = (List.splitInTwo l.val.reverse, ).fst.val.reverse,
                        theorem List.MergeSort.Internal.splitRevInTwo_fst {α : Type u_1} {n : Nat} (l : { l : List α // l.length = n }) :
                        (List.MergeSort.Internal.splitRevInTwo l).fst = (List.splitInTwo l).fst.val.reverse,
                        theorem List.MergeSort.Internal.splitRevInTwo_snd {α : Type u_1} {n : Nat} (l : { l : List α // l.length = n }) :
                        @[irreducible]
                        theorem List.MergeSort.Internal.mergeSortTR_run_eq_mergeSort {α : Type u_1} {le : ααBool} {n : Nat} (l : { l : List α // l.length = n }) :
                        @[irreducible]
                        theorem List.MergeSort.Internal.mergeSortTR₂_run_eq_mergeSort {α : Type u_1} {le : ααBool} {n : Nat} (l : { l : List α // l.length = n }) :
                        @[irreducible]
                        theorem List.MergeSort.Internal.mergeSortTR₂_run'_eq_mergeSort {α : Type u_1} {l' : List α} {le : ααBool} {n : Nat} (l : { l : List α // l.length = n }) (w : l' = l.val.reverse) :