# Sorting

```
{-# OPTIONS --allow-unsolved-metas --without-K #-}

open import Level using (Level; Lift)
import Level as L
open import Data.Nat
open import Data.Bool
open import Data.Unit
open import Data.List as List
open import Data.List.Properties using (++-assoc; ∷-injective)
open import Data.Empty
open import Data.Product as Σ hiding (swap)
open import Data.Sum as ⊎ hiding (swap)
open import Function.Base using (_∘_; flip; case_of_)
open import Relation.Binary.PropositionalEquality hiding ([_]; trans)
open import Data.List.Relation.Unary.All as All hiding (toList)
open import Relation.Unary using (_⊆_)
open import Relation.Nullary using (¬_)
open import Relation.Binary using (Decidable; Symmetric; Reflexive; Transitive)
open import Function.Definitions using (Injective; Surjective)
```

Wir betrachten einen Element-Typ `A` mit linearer Ordnung.
```
module _
  {ℓ ℓ' : Level}
  (A : Set ℓ)
  (_≤_ : A → A → Set ℓ')
  (_≤?_ : ∀ x y → x ≤ y ⊎ y ≤ x)
  (≤-trans : Transitive _≤_ )
  where

private
  variable
    ℓ'' : Level
    B : Set ℓ'
    C : Set ℓ''
    x y z : A
    xs ys zs : List A
```
## All
```
module All-redef where
  data All' (P : A → Set ℓ'') : List A → Set (ℓ'' L.⊔ ℓ) where
    [] : All' P []
    _∷_ : P x → All' P xs → All' P (x ∷ xs)

  All-map : (P Q : A → Set ℓ'') → P ⊆ Q → All' P xs → All' Q xs
  All-map P Q P⊆Q [] = []
  All-map P Q P⊆Q (Px ∷ all-P-xs) = P⊆Q Px ∷ All-map P Q P⊆Q all-P-xs

  module example (P : A → Set ℓ'') where
    
    open import Data.List.Relation.Unary.Any
    deMorgan : ¬ (Any P xs) → All (¬_ ∘ P) xs
    deMorgan {[]} ¬any = []
    deMorgan {x ∷ xs} ¬Any-P-x∷xs = ¬Px ∷ IH
      where
        ¬Px : ¬ (P x)
        ¬Px Px = ¬Any-P-x∷xs (here Px)
        IH : All (¬_ ∘ P) xs
        IH = deMorgan λ (x' : Any P xs) → ¬Any-P-x∷xs (there x')

    -- deMorgan' : All (¬_ ∘ P) xs → ¬ (Any P xs)

    -- this direction requires LEM:
    -- deMorgan : ¬ All P xs → Any (¬_ ∘ P) xs

```
## Ascending and Sorted Lists
```
data Ascending : List A → Set (ℓ L.⊔ ℓ') where
  []-asc : Ascending []
  [-]-asc : ∀ x → Ascending [ x ]
  ∷-asc : ∀ x y ys → x ≤ y → Ascending (y ∷ ys) → Ascending (x ∷ y ∷ ys)

data Sorted : List A → Set (ℓ L.⊔ ℓ') where
  []-sorted : Sorted []
  ∷-sorted : ∀ x xs → All (x ≤_) xs → Sorted xs → Sorted (x ∷ xs)

-- dot-pattern: 
-- * first match the other parameters
-- * .(TERM) means: the placeholder must necessarily be of shape TERM
Sorted⊆Ascending : Sorted ⊆ Ascending 
Sorted⊆Ascending {[]} []-sorted = []-asc
Sorted⊆Ascending {x ∷ []} _ = [-]-asc x
Sorted⊆Ascending {x ∷ y ∷ xs} (∷-sorted x .(y ∷ xs) (x≤y ∷ x≤xs) y∷xs-sorted) =
  ∷-asc x y xs x≤y (Sorted⊆Ascending y∷xs-sorted)

Ascending⊆Sorted : Ascending ⊆ Sorted 
Ascending⊆Sorted []-asc = []-sorted
Ascending⊆Sorted ([-]-asc x) = ∷-sorted x [] [] []-sorted
Ascending⊆Sorted (∷-asc x y ys x≤y y∷ys-asc) =
  case (Ascending⊆Sorted y∷ys-asc) of λ
  { y∷ys-sorted @ (∷-sorted _ _ y≤ys ys-sorted) →
  let x≤ys = All.map (≤-trans x≤y) y≤ys in
  ∷-sorted x (y ∷ ys) (x≤y ∷ x≤ys) y∷ys-sorted
  }

```
## Insertion Sort
```

module insertion-sort-separate where
  insert : A → List A → List A
  insert x [] = [ x ]
  insert x (y ∷ ys) with (x ≤? y)
  ... | inj₁ x≤y = x ∷ y ∷ ys
  ... | inj₂ y≤x = y ∷ insert x ys

  sort : List A → List A
  sort [] = []
  sort (x ∷ xs) = insert x (sort xs)

  insert-All : ∀ x xs → {P : A → Set ℓ''} → P x → All P xs → All P (insert x xs)
  insert-All x [] Px All-P-xs = Px ∷ []
  insert-All x (y ∷ ys) Px (Py ∷ All-P-ys) with (x ≤? y)
  ... | inj₁ x≤y = Px ∷ (Py ∷ All-P-ys)
  ... | inj₂ y≤x = Py ∷ insert-All x ys Px All-P-ys

  insert-sorted : ∀ x xs → Sorted xs → Sorted (insert x xs)
  insert-sorted x [] []-sorted = ∷-sorted x [] [] []-sorted
  insert-sorted x (y ∷ ys) y∷ys-sorted@(∷-sorted y ys y≤ys ys-sorted) with (x ≤? y)
  ... | inj₁ x≤y = ∷-sorted x (y ∷ ys) (x≤y ∷ All.map (≤-trans x≤y) y≤ys) y∷ys-sorted
  ... | inj₂ y≤x =
             ∷-sorted y (insert x ys)
             (insert-All x ys y≤x y≤ys)
             (insert-sorted x ys ys-sorted)

  sort-sorted : ∀ (l : List A) → Sorted (sort l)
  sort-sorted [] = []-sorted
  sort-sorted (x ∷ xs) = insert-sorted x (sort xs) IH
    where
      IH : Sorted (sort xs)
      IH = sort-sorted xs

  sort' : List A → List A
  sort' _ = []
  sort'-correct : ∀ (l : List A) → Sorted (sort' l)
  sort'-correct l = []-sorted
```
[Ende der Vorlesung am 28.05.2026]

```
module ↭-redef where -- \lr~
  infix 3 _↭_
  data _↭_ : List A → List A → Set ℓ where
    refl : xs ↭ xs
    prep : ∀ x → ys ↭ zs → (x ∷ ys) ↭ (x ∷ zs)
    swap-const : ∀ x y → x ∷ y ∷ zs ↭ y ∷ x ∷ zs 
    trans : xs ↭ ys → ys ↭ zs → xs ↭ zs

  test : A → Set ℓ
  test x = [] ↭ (x ∷ [])

  ↭-sym : xs ↭ ys → ys ↭ xs
  ↭-sym refl = refl
  ↭-sym (prep x perm) = prep x (↭-sym perm)
  ↭-sym (swap-const x y) = swap-const y x
  ↭-sym (trans p1 p2) = trans (↭-sym p2) (↭-sym p1)

  swap : ∀ x y {ws} → zs ↭ ws → x ∷ y ∷ zs ↭ y ∷ x ∷ ws
  swap x y zs↭ws = trans (swap-const x y) (prep y (prep x zs↭ws))

open import Data.List.Relation.Binary.Permutation.Propositional

record SortingAlgorithm : Set (ℓ L.⊔ ℓ') where
  field
    f : List A → List A
    permutes : f xs ↭ xs
    sorted : Sorted (f xs)

module insertion-sort-permutes where
  open insertion-sort-separate
  insert-permutes : ∀ x ys → insert x ys ↭ x ∷ ys
  insert-permutes x [] = refl
  insert-permutes x (y ∷ ys) with (x ≤? y)
  ... | inj₁ x≤y = refl
  ... | inj₂ y≤x = begin
    y ∷ insert x ys ↭⟨ prep y (insert-permutes x ys) ⟩
    y ∷ x ∷ ys      ↭⟨ swap y x refl ⟩
    x ∷ y ∷ ys
    ∎
    where open PermutationReasoning

  sort-permutes : ∀ xs → sort xs ↭ xs
  sort-permutes [] = refl
  sort-permutes (x ∷ xs) =
    -- trans (insert-permutes x (sort xs))
    --       (prep x (sort-permutes xs))
    begin
    sort (x ∷ xs)        ≡⟨⟩
    insert x (sort xs)   ↭⟨ insert-permutes x (sort xs) ⟩
    x ∷ sort xs   ↭⟨ prep x (sort-permutes xs) ⟩
    x ∷ xs
    ∎
    where open PermutationReasoning

InsertionSort : SortingAlgorithm
InsertionSort = record
  { f = insertion-sort-separate.sort
  ; permutes = insertion-sort-permutes.sort-permutes _
  ; sorted = λ {xs} → insertion-sort-separate.sort-sorted xs
  }
```

In jedem der obigen Beweise zu `insert` (bzw. `sort`) mussten wir die Induktive
Struktur `insert` (bzw. `sort`) duplizieren.

## Intrinsically Correct Insertion Sort

```
All-↭ : {P : A → Set ℓ''} → All P xs → xs ↭ ys → All P ys
All-↭ all-P-xs refl = all-P-xs
All-↭ (px ∷ all-P-xs) (prep x p) = px ∷ (All-↭ all-P-xs p)
All-↭ (px ∷ py ∷ all-P-xs) (swap x y p) =
  py ∷ px ∷ All-↭ all-P-xs p
All-↭ all-P-xs (trans p1 p2) =
  All-↭ (All-↭ all-P-xs p1) p2

module intrinsically-correct where
  insert : ∀ x ys → Sorted ys → ∃[ zs ](Sorted zs × (x ∷ ys) ↭ zs)
  insert x [] ys-sorted =
         [ x ]
         , (∷-sorted x [] [] ys-sorted)
         , refl
  insert x (y ∷ zs) y∷zs-sorted@(∷-sorted y zs y≤zs zs-sorted)
        with (x ≤? y)
  ... | inj₁ x≤y =
        (x ∷ y ∷ zs)
        , ∷-sorted x (y ∷ zs)
                   (x≤y ∷ All.map (≤-trans x≤y) y≤zs)
                   y∷zs-sorted
        , refl
  ... | inj₂ y≤x =
        let
          ws , ws-sorted , x∷zs↭ws = insert x zs zs-sorted
          helper : All (_≤_ y) (x ∷ zs)
          helper = y≤x ∷ y≤zs
        in
        (y ∷ ws)
        , ∷-sorted y ws (All-↭ helper x∷zs↭ws) ws-sorted
        , (begin
           x ∷ y ∷ zs ↭⟨ swap x y refl ⟩
           y ∷ x ∷ zs ↭⟨ prep y x∷zs↭ws ⟩
           y ∷ ws
          ∎)
        where open PermutationReasoning

  sort : ∀ xs → ∃[ ys  ] (Sorted ys × xs ↭ ys)
  sort [] = [] , ([]-sorted , refl)
  sort (x ∷ xs) =
    let
      ys , ys-sorted , xs↭ys  = sort xs
      zs , zs-sorted , x∷ys↭zs = insert x ys ys-sorted
    in
    zs , zs-sorted , (begin
      x ∷ xs ↭⟨ prep x xs↭ys ⟩
      x ∷ ys ↭⟨ x∷ys↭zs ⟩
      zs
    ∎)
    where open PermutationReasoning

InsertionSort-intrinsic : SortingAlgorithm
InsertionSort-intrinsic = record
    { f = proj₁ ∘ sort
    ; permutes = λ {xs} → ↭-sym (proj₂ (proj₂ (sort xs)))
    ; sorted = λ {xs} → (proj₁ (proj₂ (sort xs)))
    }
    where open intrinsically-correct
```
[Ende der Vorlesung am 01. Juni 2026]

## Definition von Permutation
```
_ : ∀ (a b : A) → (a ∷ b ∷ []) ↭ (a ∷ b ∷ [])
_ = λ a b → trans (swap a b refl) (swap b a refl)

infix 3 _∼_
data _∼_ : List A → List A → Set ℓ where
  []~[] : [] ∼ []
  ∷∼ : ∀ x xs ys zs → xs ∼ ys ++ zs
       → (x ∷ xs) ∼ (ys ++ [ x ] ++ zs)

pattern _∷[_∼⟨_⟩_++_] x xs xs~ys++zs ys zs = ∷∼ x xs ys zs xs~ys++zs
```

```diagram
x ∷ xs
│    │∼
│    🯜
│ ys++zs
│ ╭──┴──────────╮
╰─│──────╮      │
  │      │      │
  🯜      🯜      🯜
 ys ++ [ x ] ++ zs
```

```
module examples (a b : A) (a≢b : a ≢ b) where
  ↭-not-unique : Σ[ p ∈ (a ∷ b ∷ [] ↭ a ∷ b ∷ []) ]
                 (∃[ p' ] (p ≢ p'))
  ↭-not-unique = refl , (trans (swap a b refl) (swap b a refl)) , (λ ())
  -- ∼-not-unique : ∀ {ws} (p p' : (a ∷ b ∷ [] ∼ ws)) → p ≡ p'
  -- ∼-not-unique (x ∷[ xs ∼⟨ xs~ys++zs ⟩ ys ++ zs ]) p' =
  --   {!p!}

↭-++ : (x ∷ (ys ++ zs)) ↭ (ys ++ [ x ] ++ zs)
↭-++ {ys = []} = refl
↭-++ {ys = y ∷ ys} = trans (swap _ _ refl) (prep y ↭-++)

∼⊆↭ : xs ∼ ys → xs ↭ ys
∼⊆↭ []~[] = refl
∼⊆↭ (x ∷[ xs ∼⟨ p ⟩ ys ++ zs ]) =
  trans (prep x (∼⊆↭ p)) ↭-++

∼-reflexive : xs ∼ xs
∼-reflexive {xs = []} = []~[]
∼-reflexive {xs = x ∷ xs} =
  x ∷[ xs ∼⟨ ∼-reflexive ⟩ [] ++ xs ]


∼-extract-assumption : Set _
∼-extract-assumption = ∀ {ws ys x zs} →
  ys ++ [ x ] ++ zs ∼ ws
  → ∃[ us ] ∃[ vs ]
    (ws ≡ us ++ [ x ] ++ vs)
    × (ys ++ zs ∼ us ++ vs)

module Incomplete-Transitivity-Proof (∼-extract : ∼-extract-assumption) where
  -- For non-empty lists and two permutations p and p', starting with
  -- the list `x ∷ xs`, we have:
  -- ys = []:
  -- 
  -- x ∷ xs
  -- │   │∼
  -- │   🯜
  -- │   ys ++ zs
  -- │  ╭───┴───────────╮
  -- │  │               │
  -- ╰──│──────╮        │
  --    │      │        │
  --    🯜      🯜        🯜
  --    ys    ++ [ x ] ++ zs
  --    ╰────────┬────────╯
  --             │
  --             🯜
  --             ws ≡ us ++ [ x ] ++ vs
  
  ∼-transitive : xs ∼ ys → ys ∼ zs → xs ∼ zs
  ∼-transitive []~[] []~[] = []~[]
  ∼-transitive {zs = ws} (x ∷[ xs ∼⟨ xs∼ys++zs ⟩ ys ++ zs ]) p'
    with (∼-extract p')
  ... | us , vs , (refl , ys++zs∼us++vs) =
    x ∷[ xs ∼⟨ ∼-transitive xs∼ys++zs ys++zs∼us++vs ⟩ us ++ vs ]
  
  ∼-prep : ∀ x → xs ∼ ys → (x ∷ xs) ∼ (x ∷ ys)
  ∼-prep {xs} {ys} x p = x ∷[ xs ∼⟨ p ⟩ [] ++ ys ]
  
  ↭⊆∼ : xs ↭ ys → xs ∼ ys
  ↭⊆∼ refl = ∼-reflexive
  ↭⊆∼ (prep {xs} {ys} x p) = ∼-prep x (↭⊆∼ p)
  ↭⊆∼ (swap {xs} {ys} x y p) =
    x ∷[ y ∷ xs ∼⟨ ∼-prep y (↭⊆∼ p) ⟩ [ y  ] ++ ys ]
  ↭⊆∼ (trans p p') = ∼-transitive (↭⊆∼ p) (↭⊆∼ p')
```
[Ende der Vorlesung am 08.06.2026]
```

record _++_⟶_++_ (xs ys vs ws : List A) : Set ℓ where
  -- describe that list concatenation ++ is moved
  -- along the subword δ
  field
    δ : List A
    --   ┌──────┬────────────┐
    -- 1 │  xs  │        ys  │
    --   ├──────┼─────┬──────┤
    -- 2 │  xs  │  δ  │  ws  │
    --   ├──────┴─────┼──────┤
    -- 3 │  vs        │  ws  │
    --   └────────────┴──────┘
    prefix-δ : xs ++ δ ≡ vs -- line 2 vs line 3
    suffix-δ : ys ≡ δ ++ ws -- line 1 vs line 2

  ∷-prep : ∀ x → (x ∷ xs) ++ ys ⟶ (x ∷ vs) ++ ws
  ∷-prep x = record
    { δ = δ
    ; prefix-δ = cong (x ∷_) prefix-δ
    ; suffix-δ = suffix-δ
    }
  original-equation : xs ++ ys ≡ vs ++ ws
  original-equation = begin
    xs ++ ys ≡⟨ cong (xs ++_) suffix-δ ⟩
    xs ++ (δ ++ ws) ≡⟨ ++-assoc xs δ ws ⟨
    (xs ++ δ) ++ ws ≡⟨ cong (_++ ws) prefix-δ ⟩
    vs ++ ws
    ∎
    where open ≡-Reasoning

open import Data.List.Properties using (∷-injective)

++-split : ∀ xs vs {ws} →
           xs ++ ys ≡ vs ++ ws
           →    xs ++ ys ⟶ vs ++ ws
                ⊎  vs ++ ws ⟶ xs ++ ys

++-split [] vs eq = inj₁ (record { δ = vs ; prefix-δ = refl ; suffix-δ = eq })
++-split xs@(_ ∷ _) [] eq = inj₂ (record { δ = xs ; prefix-δ = refl ; suffix-δ = sym eq })
++-split (x ∷ xs) (v ∷ vs) eq with (∷-injective eq)
... | refl , eq' = ⊎.map
      (λ - → _++_⟶_++_.∷-prep - x)
      (λ - → _++_⟶_++_.∷-prep - x)
      (++-split xs vs eq')

∼-sym-++-assoc : ∀ {us} vs {ws} {xs} → xs ∼ us ++ vs ++ ws → xs ∼ (us ++ vs) ++ ws
∼-sym-++-assoc {us} vs {ws} {xs} = subst (_ ∼_) (sym (++-assoc us vs ws))

∼-++-assoc : ∀ {us} vs {ws} {xs} → xs ∼ (us ++ vs) ++ ws → xs ∼ us ++ (vs ++ ws)
∼-++-assoc {us} vs {ws} {xs} = subst (_ ∼_) (++-assoc us vs ws)



∼-extract : ∀ {ws ys x zs} → ys ++ [ x ] ++ zs ∼ ws → ∃[ us ] ∃[ vs ] (ws ≡ us ++ [ x ] ++ vs) × (ys ++ zs ∼ us ++ vs)
∼-extract {ys = []} (x ∷[ xs ∼⟨ p ⟩ ys ++ zs ]) =
  ys , (zs , (refl , p))
∼-extract {ys = y ∷ ys} {x = x} {zs = zs} (y ∷[ .(ys ++ x ∷ zs) ∼⟨ p ⟩ vs ++ ws ])
  with (∼-extract p)
... | prefix , suffix , eq1 , eq2
  with (++-split vs prefix eq1)
... | inj₁ record { δ = δ ; prefix-δ = refl ; suffix-δ = refl } =
      vs ++ y ∷ δ , suffix
      , sym (++-assoc vs (y ∷ δ) (x ∷ suffix))
      , ∼-sym-++-assoc (y ∷ δ) (y ∷[ ys ++ zs ∼⟨ ∼-++-assoc {vs} δ eq2 ⟩ vs ++ (δ ++ suffix) ])

... | inj₂ record { δ = [] ; prefix-δ = refl ; suffix-δ = refl } =
      prefix ++ [ y ] , suffix
      , (begin
        (prefix ++ []) ++ [ y ] ++ x ∷ suffix ≡⟨ ++-assoc _ [ y ] _ ⟨
        ((prefix ++ []) ++ [ y ]) ++ x ∷ suffix ≡⟨ cong (_++ _) (++-assoc prefix [] [ y ]) ⟩
        (prefix ++ [ y ]) ++ x ∷ suffix ∎)
      , ∼-sym-++-assoc [ y ] (y ∷[ ys ++ zs ∼⟨ eq2 ⟩ prefix ++ suffix ])
      where open ≡-Reasoning

... | inj₂ record { δ = (.x ∷ δ) ; prefix-δ = refl ; suffix-δ = refl } =
      prefix , δ ++ y ∷ ws
      , ++-assoc prefix (x ∷ δ) (y ∷ ws)
      , ∼-++-assoc {prefix} δ
        (y ∷[ (ys ++ zs) ∼⟨ ∼-sym-++-assoc {prefix} δ eq2 ⟩ (prefix ++ δ) ++ ws ])

open Incomplete-Transitivity-Proof ∼-extract
```
[Ende der Vorlesung am 11. Juni 2026]

## Stdlib
```
import Data.List.Relation.Unary.Linked using (Linked)
-- ^- Ascending = Linked _≤_
import Data.List.Sort.Base using (SortingAlgorithm)
```

## Aktuelles aus der Forschung:

* Cass Alexandru, Vikraman Choudhury, Jurriaan Rot, Niels van der Weide: [Intrinsically Correct Sorting in Cubical Agda](https://dl.acm.org/doi/10.1145/3703595.3705873).
* Cass Alexandru, Henning Urbat, Thorsten Wißmann: [Intrinsically correct algorithms and recursive coalgebras](https://arxiv.org/abs/2512.10748)