{- Computer Aided Formal Reasoning (G53CFR, G54CFR) Peter Morris Coursework 9: Quick Sort In this coursework, we're going to look at another sorting algorithm Quick Sort. The naive implementation is below: -} module ex09i where open import Data.List open import Data.Nat open import Data.Product {- Order and order are as before: -} data Order : Set where le gt : Order order : ℕ → ℕ → Order order zero n = le order (suc m) zero = gt order (suc m) (suc n) = order m n {- The key with QS is to split a list in to two parts, one part with numbers less or equal than some given pivot, and the second list with numbers greater than the pivot: -} pivot : ℕ → List ℕ → (List ℕ × List ℕ) pivot n [] = [] , [] pivot n (m ∷ ms) with pivot n ms | order m n ... | xs , ys | le = m ∷ xs , ys ... | xs , ys | gt = xs , m ∷ ys {- Sorting then involves picking a pivot from the front of the list, spliting the rest of the list, sorting the two parts and putting everything back together (note, that the pivot has to go in the _middle_ now: -} sort : List ℕ → List ℕ sort [] = [] sort (n ∷ ns) with pivot n ns ... | (xs , ys) = sort xs ++ (n ∷ sort ys) {- Sadly, again, this isn't obviously terminating (at least to Agda). So your job is to redefine QS in a structurally recursive way, in QuickSort2.agda -} ex1 : List ℕ ex1 = 5 ∷ 2 ∷ 0 ∷ 1 ∷ 4 ∷ 3 ∷ [] ex2 : List ℕ ex2 = 100 ∷ 1 ∷ 10 ∷ 1 ∷ 100 ∷ 10 ∷ []