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
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
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).
quicksort returns the correct result
no matter how long a list you give it.