An implementation of bubble sort in Agda.

BubbleSort.lagda

\begin{code}
open import Level using (_⊔_)
open import Data.Vec using (Vec; []; _∷_)
open import Data.Nat as Nat using (ℕ; zero; suc)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (∃; _×_; _,_; proj₁; proj₂)
open import Data.Empty using (⊥-elim)
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
\end{code}

\begin{code}
module BubbleSort {c ℓ₁ ℓ₂} (Ord : DecTotalOrder c ℓ₁ ℓ₂) where
\end{code}

\begin{code}
  open DecTotalOrder {{...}} using (_≤_; _≤?_; total)
  A = DecTotalOrder.Carrier Ord
\end{code}

A bounded version of the A type that is bounded at the top by ⊤ and
at the bottom by ⊥.

\begin{code}
  data  : Set c where
    ⊤   : Â
    ⊥   : Â
    ⟦_⟧ : A → Â
\end{code}

Computes the minimum of two bounded values.

\begin{code}
  infix 5 _⊓_

  _⊓_ : Â → Â → Â
  ⊤ ⊓ y = y
  ⊥ ⊓ _ = ⊥
  x ⊓ ⊤ = x
  _ ⊓ ⊥ = ⊥
  ⟦ x ⟧ ⊓ ⟦ y ⟧ with x ≤? y
  ⟦ x ⟧ ⊓ ⟦ y ⟧ | yes x≤y = ⟦ x ⟧
  ⟦ x ⟧ ⊓ ⟦ y ⟧ | no  x>y = ⟦ y ⟧
\end{code}

Lifting of the ≤-relation to bounded values Â.

\begin{code}
  infix 4 _≲_

  data _≲_ : Rel  (c ⊔ ℓ₂) where
    ⊥≲     : ∀ {x} → ⊥ ≲ x
    ≲⊤     : ∀ {x} → x ≲ ⊤
    ≤-lift : ∀ {x y} → x ≤ y → ⟦ x ⟧ ≲ ⟦ y ⟧
\end{code}

Easy constructor for when we only have a proof of y≰x.

\begin{code}
  ≰-lift : ∀ {x y} → ¬ (y ≤ x) → ⟦ x ⟧ ≲ ⟦ y ⟧
  ≰-lift {x} {y} y≰x with total x y
  ≰-lift y≰x | inj₁ x≤y = ≤-lift x≤y
  ≰-lift y≰x | inj₂ y≤x = ⊥-elim (y≰x y≤x)
\end{code}

Proof that ⊓ conserves ≲.

\begin{code}
  ⊓-conserves-≲ : ∀ {x y z} → x ≲ y → x ≲ z → x ≲ y ⊓ z
  ⊓-conserves-≲ {x} {⊤}     {_} _ q = q
  ⊓-conserves-≲ {x} {⊥}     {_} p _ = p
  ⊓-conserves-≲ {x} {⟦ _ ⟧} {⊤} p _ = p
  ⊓-conserves-≲ {x} {⟦ _ ⟧} {⊥} _ q = q
  ⊓-conserves-≲ {x} {⟦ y ⟧} {⟦ z ⟧} p q with y ≤? z
  ⊓-conserves-≲ {x} {⟦ y ⟧} {⟦ z ⟧} p _ | yes y≤z = p
  ⊓-conserves-≲ {x} {⟦ y ⟧} {⟦ z ⟧} _ q | no  y≰z = q
\end{code}

Representation a vector of length n, of which the first k elements
are still unsorted, and which has lower bound l.

\begin{code}
  data OVec : (l : Â) (n k : ℕ) → Set (c ⊔ ℓ₂) where
    []     : OVec ⊤ 0 0
    _∷_    : ∀ {l n k} → (x : A) (xs : OVec l n k) → OVec ⊥ (suc n) (suc k)
    _∷_by_ : ∀ {l n}   → (x : A) (xs : OVec l n 0) → ⟦ x ⟧ ≲ l → OVec ⟦ x ⟧ (suc n) 0
\end{code}

Converts a regular vector to a lower bound together with an n-ordered vector
with that lower bound (where the lower bound is either ⊤ or ⊥).

\begin{code}
  fromVec : ∀ {n} → Vec A n → ∃ (λ l → OVec l n n)
  fromVec [] = ⊤ , []
  fromVec (x ∷ xs) = ⊥ , x ∷ proj₂ (fromVec xs)

  fromVec-⊤or⊥ : ∀ {n} {xs : Vec A n}
    → let l = proj₁ (fromVec xs) in l ≡ ⊤ ⊎ l ≡ ⊥
  fromVec-⊤or⊥ {.0}       {[]}     = inj₁ refl
  fromVec-⊤or⊥ {.(suc _)} {x ∷ xs} = inj₂ refl
\end{code}

Converts an n-ordered vector to a regular vector.

\begin{code}
  toVec : ∀ {l n k} → OVec l n k → Vec A n
  toVec [] = []
  toVec (x ∷ xs) = x ∷ toVec xs
  toVec (x ∷ xs by _) = x ∷ toVec xs
\end{code}

Bubble performs a single "bubble" across a vector.

\begin{code}
  bubbleAcc : ∀ {l n k} (x : A) (xs : OVec l n k) → OVec (⟦ x ⟧ ⊓ l) (suc n) k
  bubbleAcc x [] = x ∷ [] by ≲⊤
  bubbleAcc x (y ∷ xs) = y ∷ bubbleAcc x xs
  bubbleAcc x (y ∷ xs by p) with x ≤? y
  ... | yes x≤y = x ∷ (y ∷ xs by p) by ≤-lift x≤y
  ... | no  x≰y = y ∷ bubbleAcc x xs by ⊓-conserves-≲ (≰-lift x≰y) p

  bubble : ∀ {l n k} → OVec l n (suc k) → ∃ (λ l → OVec l n k)
  bubble (x ∷ xs) = _ , bubbleAcc x xs
\end{code}

Iterates the bubble k times to guarantee that the entire list is
sorted, and returns a tuple with the sorted list and its lower bound.

\begin{code}
  bubblesort : ∀ {l n k} → OVec l n k → ∃ (λ l → OVec l n 0)
  bubblesort [] = ⊤ , []
  bubblesort (x ∷ xs) with bubble (x ∷ xs)
  bubblesort (x ∷ xs) | l , ys = bubblesort ys
  bubblesort (x ∷ xs by p) = ⟦ x ⟧ , x ∷ xs by p
\end{code}