# Quicksort for lists

Content created by Egbert Rijke, Fredrik Bakke and Victor Blanchi.

Created on 2023-05-03.

module lists.quicksort-lists where

Imports
open import elementary-number-theory.inequality-natural-numbers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.strong-induction-natural-numbers

open import foundation.coproduct-types
open import foundation.identity-types
open import foundation.unit-type
open import foundation.universe-levels

open import lists.concatenation-lists
open import lists.lists

open import order-theory.decidable-total-orders


## Idea

Quicksort is a sorting algorithm on lists that works by selecting a pivoting element, dividing the list into elements smaller than the pivoting element and elements greater than the pivoting element, and sorting those two lists by again applying the quicksort algorithm.

## Definition

module _
{l1 l2 : Level} (X : Decidable-Total-Order l1 l2)
where

helper-quicksort-list-divide-leq :
(x : type-Decidable-Total-Order X) →
(y : type-Decidable-Total-Order X) →
leq-or-strict-greater-Decidable-Poset X x y →
list (type-Decidable-Total-Order X) →
list (type-Decidable-Total-Order X)
helper-quicksort-list-divide-leq x y (inl p) l = l
helper-quicksort-list-divide-leq x y (inr p) l = cons y l

quicksort-list-divide-leq :
type-Decidable-Total-Order X → list (type-Decidable-Total-Order X) →
list (type-Decidable-Total-Order X)
quicksort-list-divide-leq x nil = nil
quicksort-list-divide-leq x (cons y l) =
helper-quicksort-list-divide-leq
( x)
( y)
( is-leq-or-strict-greater-Decidable-Total-Order X x y)
( quicksort-list-divide-leq x l)

helper-quicksort-list-divide-strict-greater :
(x : type-Decidable-Total-Order X) →
(y : type-Decidable-Total-Order X) →
leq-or-strict-greater-Decidable-Poset X x y →
list (type-Decidable-Total-Order X) →
list (type-Decidable-Total-Order X)
helper-quicksort-list-divide-strict-greater x y (inl p) l = cons y l
helper-quicksort-list-divide-strict-greater x y (inr p) l = l

quicksort-list-divide-strict-greater :
type-Decidable-Total-Order X → list (type-Decidable-Total-Order X) →
list (type-Decidable-Total-Order X)
quicksort-list-divide-strict-greater x nil = nil
quicksort-list-divide-strict-greater x (cons y l) =
helper-quicksort-list-divide-strict-greater
( x)
( y)
( is-leq-or-strict-greater-Decidable-Total-Order X x y)
( quicksort-list-divide-strict-greater x l)

private
helper-inequality-length-quicksort-list-divide-leq :
(x : type-Decidable-Total-Order X) →
(y : type-Decidable-Total-Order X) →
(p : leq-or-strict-greater-Decidable-Poset X x y) →
(l : list (type-Decidable-Total-Order X)) →
length-list (helper-quicksort-list-divide-leq x y p l) ≤-ℕ
length-list (cons y l)
helper-inequality-length-quicksort-list-divide-leq x y (inl _) l =
succ-leq-ℕ (length-list l)
helper-inequality-length-quicksort-list-divide-leq x y (inr _) l =
refl-leq-ℕ (length-list (cons y l))

inequality-length-quicksort-list-divide-leq :
(x : type-Decidable-Total-Order X) →
(l : list (type-Decidable-Total-Order X)) →
length-list (quicksort-list-divide-leq x l) ≤-ℕ length-list l
inequality-length-quicksort-list-divide-leq x nil = star
inequality-length-quicksort-list-divide-leq x (cons y l) =
transitive-leq-ℕ
( length-list (quicksort-list-divide-leq x (cons y l)))
( length-list (cons y (quicksort-list-divide-leq x l)))
( length-list (cons y l))
( inequality-length-quicksort-list-divide-leq x l)
( helper-inequality-length-quicksort-list-divide-leq
( x)
( y)
( is-leq-or-strict-greater-Decidable-Total-Order X x y)
( quicksort-list-divide-leq x l))

helper-inequality-length-quicksort-list-divide-strict-greater :
(x : type-Decidable-Total-Order X) →
(y : type-Decidable-Total-Order X) →
(p : leq-or-strict-greater-Decidable-Poset X x y) →
(l : list (type-Decidable-Total-Order X)) →
length-list (helper-quicksort-list-divide-strict-greater x y p l) ≤-ℕ
length-list (cons y l)
helper-inequality-length-quicksort-list-divide-strict-greater
( x)
( y)
( inl _)
( l) =
refl-leq-ℕ (length-list (cons y l))
helper-inequality-length-quicksort-list-divide-strict-greater
( x)
( y)
( inr _)
( l) =
succ-leq-ℕ (length-list l)

inequality-length-quicksort-list-divide-strict-greater :
(x : type-Decidable-Total-Order X) →
(l : list (type-Decidable-Total-Order X)) →
length-list (quicksort-list-divide-strict-greater x l) ≤-ℕ length-list l
inequality-length-quicksort-list-divide-strict-greater x nil = star
inequality-length-quicksort-list-divide-strict-greater x (cons y l) =
transitive-leq-ℕ
( length-list (quicksort-list-divide-strict-greater x (cons y l)))
( length-list (cons y (quicksort-list-divide-strict-greater x l)))
( length-list (cons y l))
( inequality-length-quicksort-list-divide-strict-greater x l)
( helper-inequality-length-quicksort-list-divide-strict-greater
( x)
( y)
( is-leq-or-strict-greater-Decidable-Total-Order X x y)
( quicksort-list-divide-strict-greater x l))

base-quicksort-list :
(l : list (type-Decidable-Total-Order X)) → zero-ℕ ＝ length-list l →
list (type-Decidable-Total-Order X)
base-quicksort-list nil x = nil

inductive-step-quicksort-list :
(k : ℕ) →
□-≤-ℕ
( λ n →
(l : list (type-Decidable-Total-Order X)) →
n ＝ length-list l → list (type-Decidable-Total-Order X))
( k) →
(l : list (type-Decidable-Total-Order X)) →
succ-ℕ k ＝ length-list l → list (type-Decidable-Total-Order X)
inductive-step-quicksort-list k sort (cons x l) p =
concat-list
( sort
( length-list (quicksort-list-divide-leq x l))
( transitive-leq-ℕ
( length-list (quicksort-list-divide-leq x l))
( length-list l)
( k)
( leq-eq-ℕ (length-list l) k (is-injective-succ-ℕ (inv p)))
( inequality-length-quicksort-list-divide-leq x l))
( quicksort-list-divide-leq x l)
( refl))
( cons
( x)
( sort
( length-list (quicksort-list-divide-strict-greater x l))
( transitive-leq-ℕ
( length-list (quicksort-list-divide-strict-greater x l))
( length-list l)
( k)
( leq-eq-ℕ (length-list l) k (is-injective-succ-ℕ (inv p)))
( inequality-length-quicksort-list-divide-strict-greater x l))
( quicksort-list-divide-strict-greater x l)
( refl)))

quicksort-list :
list (type-Decidable-Total-Order X) →
list (type-Decidable-Total-Order X)
quicksort-list l =
strong-ind-ℕ
( λ n →
(l : list (type-Decidable-Total-Order X)) → n ＝ length-list l →
list (type-Decidable-Total-Order X))
( base-quicksort-list)
( inductive-step-quicksort-list)
( length-list l)
( l)
( refl)