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
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.
- Cass Alexandru, Henning Urbat, Thorsten Wißmann: Intrinsically correct algorithms and recursive coalgebras