module sorting where open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong) open import Relation.Nullary using (¬_; yes; no) open import Data.Empty using (⊥; ⊥-elim) open import Data.Nat using (ℕ; suc; zero; _≤_; z≤n ; s≤s; _≤?_) open import Data.Nat.Properties using (≤-trans; ≤-total) open import Data.Sum using (_⊎_; inj₁; inj₂) open import Data.List using (List; []; _∷_; [_]) ¬≤-flip : ∀ {x y} → ¬ (x ≤ y) → y ≤ x ¬≤-flip {x} {y} ¬x≤y with ≤-total x y ... | inj₁ x≤y = ⊥-elim (¬x≤y x≤y) ... | inj₂ y≤x = y≤x data _≤-all_ (x : ℕ) : List ℕ → Set where [] : x ≤-all [] _∷_ : {y : ℕ} → {ys : List ℕ} → x ≤ y → x ≤-all ys → x ≤-all (y ∷ ys) ≤-all-trans : ∀ x y ys → x ≤ y → y ≤-all ys → x ≤-all ys ≤-all-trans = {!!} data sorted : List ℕ → Set where [] : sorted [] _∷_ : {x : ℕ} → {xs : List ℕ} → x ≤-all xs → sorted xs → sorted (x ∷ xs) sort-ex1 : sorted (0 ∷ 2 ∷ 3 ∷ []) sort-ex1 = (z≤n ∷ (z≤n ∷ [])) ∷ (((s≤s (s≤s z≤n)) ∷ []) ∷ ([] ∷ [])) insert : ℕ → List ℕ → List ℕ insert x [] = [ x ] insert x (y ∷ xs) with x ≤? y ... | no ¬p = y ∷ insert x xs ... | yes p = x ∷ y ∷ xs isort : List ℕ → List ℕ isort [] = [] isort (x ∷ xs) = insert x (isort xs) isort-sorts : ∀ (xs : List ℕ) → sorted (isort xs) isort-sorts = {!!} -- permutation data _~_ {A : Set} : List A → List A → Set where [] : [] ~ [] _∷_ : (x : A) {xs ys : List A} → xs ~ ys → (x ∷ xs) ~ (x ∷ ys) swap : (x y : A) (xs : List A) → (x ∷ y ∷ xs) ~ (y ∷ x ∷ xs) trans : {xs ys zs : List A} → xs ~ ys → ys ~ zs → xs ~ zs ~-refl : ∀ {xs : List ℕ} → xs ~ xs ~-refl = {!!} ~-sym : ∀ {xs ys : List ℕ} → xs ~ ys → ys ~ xs ~-sym = {!!} isort-~ : (xs : List ℕ) → xs ~ (isort xs) isort-~ = {!!}