Quicksort: inductive proof of correctness

      
      
      ;;; things is a list of length n+1
      ;;; list? is a total order on those things
      
      
      (define (quicksort things less?)
        (if (< (length things) 2)
            things
            (let ((pivot (first things))
                  (other (rest things)))
              (let-values (((below above)
                            (partition (lambda (x)
                                         (less? x pivot))
                                       other)))
                (append (quicksort below less?)
                        (list pivot)
                        (quicksort above less?))))))
    

If we sort the elements that are below the pivot, and also sort the elements in the list above, and place the pivot in between those sorted sublists, we'll get the correct result.

That correct result is computed and returned by the highlighted call to append, which completes our proof of IH(n+1).

That in turn completes of our proof of if IH(n) then IH(n+1). We didn't assume anything at all about the natural number n, so we have proved (∀ n) if IH(n) then IH(n+1).

That was the second of the two antecedents we needed to prove before we could apply the rule of inference for induction. Having proved both antecedents of that rule, we get to infer the consequent: (∀ n) IH(n).

That says quicksort returns the correct result no matter how long a list you give it.

For debugging: Click here to validate.