MergeSort.agda

{-# OPTIONS --without-K --safe #-}

module MergeSort where

open import Data.Bool.Base using (Bool; true; false)
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
open import Data.Nat
  using (ℕ; zero; suc; _+_; _≤_; z≤n; s≤s; _≤?_)
open import Data.Nat.Properties
  using (≰⇒≥; ≤-reflexive; ≤-pred; m+n≤o⇒n≤o; m+n≤o⇒m≤o; +-comm; +-cancelˡ-≡; m≤m+n)
open import Data.List.Base
  using (List; []; _∷_; length; _++_)

open import Relation.Nullary
  using (Dec ; yes ; no ; does ; proof ; _because_ ; Reflects ; ofʸ ; ofⁿ)
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; refl; cong; sym; subst)

infixr 5 _∷ⁱ_

data Increasing : ℕ → List ℕ → Set where
  []ⁱ : ∀ {L} → Increasing L []
  _∷ⁱ_ : ∀ {L x xs} → L ≤ x → Increasing x xs → Increasing L (x ∷ xs)

infixr 5 _∷↭_
infixr 2 _∘↭_

data _↭_ {A : Set} : (xs ys : List A) → Set where
  ↭-swap  : ∀ {zs} → (x y : A) → (x ∷ y ∷ zs) ↭ (y ∷ x ∷ zs)
  _∘↭_ : ∀ {xs ys zs} → xs ↭ ys → ys ↭ zs → xs ↭ zs
  ↭-refl  : ∀ {xs} → xs ↭ xs
  _∷↭_  : ∀ {xs ys} → (z : A) → xs ↭ ys → (z ∷ xs) ↭ (z ∷ ys)

↭-select-elem : ∀ {A : Set} {z zs} → (ys : List A) → (ys ++ z ∷ zs) ↭ (z ∷ ys ++ zs)
↭-select-elem         []       = ↭-refl
↭-select-elem {z = z} (y ∷ ys) = (y ∷↭ ↭-select-elem ys) ∘↭ (↭-swap y z)

↭-++ˡ : ∀ {A} (zs : List A) {xs ys} → xs ↭ ys → (zs ++ xs) ↭ (zs ++ ys)
↭-++ˡ []       perm = perm
↭-++ˡ (z ∷ zs) perm = z ∷↭ (↭-++ˡ zs perm)

↭-++ʳ : ∀ {A} {zs : List A} {xs ys} → xs ↭ ys → (xs ++ zs) ↭ (ys ++ zs)
↭-++ʳ (↭-swap x y)     = ↭-swap x y
↭-++ʳ (perm₁ ∘↭ perm₂) = ↭-++ʳ perm₁ ∘↭ ↭-++ʳ perm₂
↭-++ʳ ↭-refl           = ↭-refl
↭-++ʳ (z ∷↭ perm)      = z ∷↭ ↭-++ʳ perm

--------------------------------------------------------------------------------------------------------------

data ParityView : ℕ → Set where
  Parity : ∀ p → (p ≡ 0 ⊎ p ≡ 1) → ∀ k → ParityView (k + (k + p))

+-suc : ∀ m n → m + suc n ≡ suc (m + n)
+-suc zero    n = refl
+-suc (suc m) n = cong suc (+-suc m n)

viewParity : ∀ n → ParityView n
viewParity zero = Parity 0 (inj₁ refl) 0
viewParity (suc zero) = Parity 1 (inj₂ refl) 0
viewParity (suc (suc n)) with viewParity n
... | Parity p p≡0⊎p≡1 k rewrite sym (+-suc k (k + p)) = Parity p p≡0⊎p≡1 (suc k)

--------------------------------------------------------------------------------------------------------------

data SplitView : ℕ → List ℕ → Set where
  Split : ∀ xs ys → SplitView (length xs) (xs ++ ys)

viewSplit : ∀ {n} zs → n ≤ length zs → SplitView n zs
viewSplit {zero}  zs       z≤n         = Split [] zs
viewSplit {suc n} (z ∷ zs) (s≤s n≤len) with viewSplit zs n≤len
... | Split xs ys = Split (z ∷ xs) ys

--------------------------------------------------------------------------------------------------------------

data MergeAcc : List ℕ → List ℕ → Set where
  M-emptyL : ∀ ys → MergeAcc [] ys
  M-emptyR : ∀ xs → MergeAcc xs []
  M-Cons : ∀ x y {xs ys} →
    MergeAcc xs (y ∷ ys) →
    MergeAcc (x ∷ xs) ys →
    MergeAcc (x ∷ xs) (y ∷ ys)

data MergeSortAcc : List ℕ → Set where
  MS-empty : MergeSortAcc []
  MS-one : ∀ x → MergeSortAcc (x ∷ [])
  MS-split : ∀ xs {ys} →
    (len-even : length xs ≡ length ys ⊎ 1 + length xs ≡ length ys) →
    MergeSortAcc xs →
    MergeSortAcc ys →
    MergeSortAcc (xs ++ ys)

build-merge-acc : ∀ xs ys → MergeAcc xs ys
build-merge-acc []       ys       = M-emptyL ys
build-merge-acc (x ∷ xs) []       = M-emptyR (x ∷ xs)
build-merge-acc (x ∷ xs) (y ∷ ys) =
  M-Cons x y (build-merge-acc xs (y ∷ ys))
             (build-merge-acc (x ∷ xs) ys)

length-++ : {A : Set} → (ys zs : List A) → length (ys ++ zs) ≡ length ys + length zs
length-++ []       zs = refl
length-++ (y ∷ ys) zs = cong suc (length-++ ys zs)

build-mergesort-acc : ∀ M xs → length xs ≤ M → MergeSortAcc xs
build-mergesort-acc zero    [] bnd = MS-empty
build-mergesort-acc (suc M) [] bnd = MS-empty
build-mergesort-acc (suc M) (z₁ ∷ []) bnd = MS-one z₁
build-mergesort-acc (suc M) (z₁ ∷ z₂ ∷ zs) bnd =
  split-even (z₁ ∷ z₂ ∷ zs) (s≤s (s≤s z≤n)) bnd where
  split-even : ∀ zs → 2 ≤ length zs → length zs ≤ suc M → MergeSortAcc zs
  split-even zs 2≤len-zs len-zs≤1+M with length zs in k+len-ys≡k+k+p | viewParity (length zs)
  ... | .(k + (k + p)) | Parity p p≡0⊎p≡1 k
    with viewSplit {k} zs (subst (k ≤_) (sym k+len-ys≡k+k+p) (m≤m+n k (k + p)))
  ... | Split xs ys rewrite length-++ xs ys =
    MS-split xs
             (split-len-even k+p≡len-ys)
             (build-mergesort-acc M xs (m+n≤o⇒m≤o k k+p≤M))
             (build-mergesort-acc M ys (subst (_≤ M) k+p≡len-ys k+p≤M))
    where mutual
      k+p≡len-ys : k + p ≡ length ys
      k+p≡len-ys = +-cancelˡ-≡ k (sym k+len-ys≡k+k+p)

      k+p≤M : k + p ≤ M
      k+p≤M = nonempty-split-shorter k p≡0⊎p≡1 2≤len-zs len-zs≤1+M

      split-len-even : length xs + p ≡ length ys → length xs ≡ length ys ⊎ 1 + length xs ≡ length ys
      split-len-even eq rewrite +-comm k p = Sum.map (λ where refl → eq) (λ where refl → eq) p≡0⊎p≡1

      nonempty-split-shorter : ∀ k {p M} →
        p ≡ 0 ⊎ p ≡ 1 →
        2 ≤ k + (k + p) →
        k + (k + p) ≤ suc M →
        k + p ≤ M
      nonempty-split-shorter zero    (inj₁ refl) ()       k+k+p≤1+M
      nonempty-split-shorter zero    (inj₂ refl) (s≤s ()) k+k+p≤1+M
      nonempty-split-shorter (suc j) p≡0⊎p≡1     2≤k+k+p  (s≤s j+1+j+p≤M) = m+n≤o⇒n≤o j j+1+j+p≤M

--------------------------------------------------------------------------------------------------------------

merge : ∀ {xs ys} → MergeAcc xs ys → List ℕ
merge (M-emptyL ys) = ys
merge (M-emptyR xs) = xs
merge (M-Cons x y accL accR) with x ≤? y
... | true  because _ = x ∷ merge accL
... | false because _ = y ∷ merge accR

mergesort′ : ∀ {xs} → MergeSortAcc xs → List ℕ
mergesort′ MS-empty   = []
mergesort′ (MS-one x) = x ∷ []
mergesort′ (MS-split xs len-even acc-xs acc-ys) =
  merge (build-merge-acc (mergesort′ acc-xs) (mergesort′ acc-ys))

mergesort : (xs : List ℕ) → List ℕ
mergesort xs = mergesort′ (build-mergesort-acc (length xs) xs (≤-reflexive refl))

merge-is-sorted : ∀ {L xs ys} → (acc : MergeAcc xs ys) →
  Increasing L xs →
  Increasing L ys →
  Increasing L (merge acc)
merge-is-sorted (M-emptyL ys) xsⁱ ysⁱ = ysⁱ
merge-is-sorted (M-emptyR xs) xsⁱ ysⁱ = xsⁱ
merge-is-sorted (M-Cons x y acc-xs acc-ys) (L≤x ∷ⁱ xsⁱ) (L≤y ∷ⁱ ysⁱ) with x ≤? y
... | yes x≤y = L≤x ∷ⁱ merge-is-sorted acc-xs xsⁱ              (x≤y ∷ⁱ ysⁱ)
... | no  x≰y = L≤y ∷ⁱ merge-is-sorted acc-ys (≰⇒≥ x≰y ∷ⁱ xsⁱ) ysⁱ

mergesort′-is-sorted : ∀ {xs} → (acc : MergeSortAcc xs) → Increasing 0 (mergesort′ acc)
mergesort′-is-sorted MS-empty   = []ⁱ
mergesort′-is-sorted (MS-one x) = z≤n ∷ⁱ []ⁱ
mergesort′-is-sorted (MS-split xs len-even acc-xs acc-ys) =
  merge-is-sorted (build-merge-acc _ _) (mergesort′-is-sorted acc-xs) (mergesort′-is-sorted acc-ys)

++-right-identity : {A : Set} → (xs : List A) → xs ++ [] ≡ xs
++-right-identity [] = refl
++-right-identity (x ∷ xs) = cong (x ∷_) (++-right-identity xs)

merge-is-permutation : ∀ {xs ys} → (acc : MergeAcc xs ys) → (xs ++ ys) ↭ merge acc
merge-is-permutation (M-emptyL ys) = ↭-refl
merge-is-permutation (M-emptyR xs) rewrite ++-right-identity xs = ↭-refl
merge-is-permutation (M-Cons x y {xs = xs} accL accR) with x ≤? y
... | true  because _ = x ∷↭ merge-is-permutation accL
... | false because _ = ↭-select-elem (x ∷ xs) ∘↭ (y ∷↭ merge-is-permutation accR)

mergesort′-is-permutation : ∀ {xs} → (acc : MergeSortAcc xs) → xs ↭ mergesort′ acc
mergesort′-is-permutation MS-empty   = ↭-refl
mergesort′-is-permutation (MS-one x) = ↭-refl
mergesort′-is-permutation (MS-split xs len-even acc-xs acc-ys) =
  ↭-++ˡ xs (mergesort′-is-permutation acc-ys) ∘↭
  ↭-++ʳ (mergesort′-is-permutation acc-xs) ∘↭
  merge-is-permutation (build-merge-acc (mergesort′ acc-xs) (mergesort′ acc-ys))

SelectionSort.agda

{-# OPTIONS --without-K --safe #-}

module SelectionSort where

open import Data.Nat
  using (ℕ; zero; suc; _+_; _≤_; z≤n; s≤s; _≤?_)
open import Data.Nat.Properties
  using (≰⇒≥; ≤-trans)
open import Data.List.Base
  using (List; []; _∷_; length; _++_)

open import Relation.Nullary
  using (Dec ; yes ; no ; does ; proof ; _because_ ; Reflects ; ofʸ ; ofⁿ)
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; refl; cong)

infixr 5 _∷ⁱ_

data Increasing : ℕ → List ℕ → Set where
  []ⁱ : ∀ {L} → Increasing L []
  _∷ⁱ_ : ∀ {L x xs} → L ≤ x → Increasing x xs → Increasing L (x ∷ xs)

infixr 5 _++ᵇ_
infixr 5 _∷ᵇ_

data BoundedBelow : ℕ → List ℕ → Set where
  []ᵇ : ∀ {L} → BoundedBelow L []
  _∷ᵇ_ : ∀ {L x xs} → L ≤ x → BoundedBelow L xs → BoundedBelow L (x ∷ xs)

forgetᵇ : ∀ {L xs} → BoundedBelow L xs → List ℕ
forgetᵇ {xs = xs} bounded = xs

_++ᵇ_ : ∀ {L xs ys} → BoundedBelow L xs → BoundedBelow L ys → BoundedBelow L (xs ++ ys)
[]ᵇ       ++ᵇ ys = ys
(x ∷ᵇ xs) ++ᵇ ys = x ∷ᵇ (xs ++ᵇ ys)

relax : ∀ {L M xs} → M ≤ L → BoundedBelow L xs → BoundedBelow M xs
relax M≤L []ᵇ         = []ᵇ
relax M≤L (L≤x ∷ᵇ xs) = ≤-trans M≤L L≤x ∷ᵇ (relax M≤L xs)

data MinView : List ℕ → Set where
  Empty : MinView []
  Min : ∀ m ys zs → (prefix : BoundedBelow m ys) → (suffix : BoundedBelow m zs) → MinView (ys ++ m ∷ zs)

viewMin : ∀ xs → MinView xs
viewMin [] = Empty
viewMin (x ∷ xs) with viewMin xs
... | Empty = Min x [] [] []ᵇ []ᵇ
... | Min m ys zs ysᵇ zsᵇ with m ≤? x
... | yes m≤x = Min m (x ∷ ys) zs             (m≤x ∷ᵇ ysᵇ) zsᵇ
... | no ¬m≤x = Min x []       (ys ++ m ∷ zs) []ᵇ          (relax x≤m ysᵇ ++ᵇ x≤m ∷ᵇ relax x≤m zsᵇ)
  where x≤m = ≰⇒≥ ¬m≤x

length-++ : {A : Set} → (ys zs : List A) → length (ys ++ zs) ≡ length ys + length zs
length-++ []       zs = refl
length-++ (y ∷ ys) zs = cong suc (length-++ ys zs)

+-suc : ∀ m n → m + suc n ≡ suc (m + n)
+-suc zero    n = refl
+-suc (suc m) n = cong suc (+-suc m n)

≤-++-cons : ∀ {A : Set} {M x zs} → (ys : List A) →
  suc M ≡ length (ys ++ x ∷ zs) →
  M ≡ length (ys ++ zs)
≤-++-cons {x = x} {zs} ys len-eq
  rewrite length-++ ys (x ∷ zs)
        | length-++ ys zs
        | +-suc (length ys) (length zs)
  with len-eq
... | refl = refl

infixr 5 _∷↭_
infixr 2 _∘↭_

data _↭_ {A : Set} : (xs ys : List A) → Set where
  ↭-swap  : ∀ {zs} → (x y : A) → (x ∷ y ∷ zs) ↭ (y ∷ x ∷ zs)
  _∘↭_ : ∀ {xs ys zs} → xs ↭ ys → ys ↭ zs → xs ↭ zs
  ↭-refl  : ∀ {xs} → xs ↭ xs
  _∷↭_  : ∀ {xs ys} → (z : A) → xs ↭ ys → (z ∷ xs) ↭ (z ∷ ys)

↭-select-elem : ∀ {A : Set} {z zs} → (ys : List A) → (ys ++ z ∷ zs) ↭ (z ∷ ys ++ zs)
↭-select-elem         []       = ↭-refl
↭-select-elem {z = z} (y ∷ ys) = (y ∷↭ ↭-select-elem ys) ∘↭ (↭-swap y z)

mutual
  sort : (xs : List ℕ) → List ℕ
  sort xs = sort′ (length xs) xs refl

  sort′ : (M : ℕ) → (xs : List ℕ) → (M ≡ length xs) → List ℕ
  sort′ zero    [] len-eq = []
  sort′ (suc M) xs len-eq with viewMin xs
  ... | Empty = []
  ... | Min m ys zs _ _ =
    m ∷ sort′ M (ys ++ zs) (≤-++-cons ys len-eq)

  sort-is-sorted : ∀ xs → Increasing 0 (sort xs)
  sort-is-sorted xs = sort′-is-sorted (length xs) (bounded-by-zero xs) refl
    where bounded-by-zero : ∀ ys → BoundedBelow 0 ys
          bounded-by-zero []       = []ᵇ
          bounded-by-zero (x ∷ ys) = z≤n ∷ᵇ bounded-by-zero ys

  sort′-is-sorted : ∀ {L xs} M → BoundedBelow L xs → ∀ bnd → Increasing L (sort′ M xs bnd)
  sort′-is-sorted zero    []ᵇ len-eq = []ⁱ
  sort′-is-sorted (suc M) xsᵇ len-eq with viewMin (forgetᵇ xsᵇ)
  ... | Empty = []ⁱ
  ... | Min m _ _ ysᵇ zsᵇ =
    lookup (forgetᵇ ysᵇ) xsᵇ ∷ⁱ sort′-is-sorted M (ysᵇ ++ᵇ zsᵇ) (≤-++-cons (forgetᵇ ysᵇ) len-eq)
    where lookup : ∀ {L zs} ys′ → BoundedBelow L (ys′ ++ m ∷ zs) → L ≤ m
          lookup []         (L≤m  ∷ᵇ xsᵇ) = L≤m
          lookup (y′ ∷ ys′) (L≤y′ ∷ᵇ xsᵇ) = lookup ys′ xsᵇ

  sort-is-permutation : ∀ xs → xs ↭ sort xs
  sort-is-permutation xs = sort′-is-permutation (length xs) xs refl

  sort′-is-permutation : ∀ M xs bnd → xs ↭ sort′ M xs bnd
  sort′-is-permutation zero    [] len-eq = ↭-refl
  sort′-is-permutation (suc M) xs len-eq with viewMin xs
  ... | Empty = ↭-refl
  ... | Min m ys zs _ _ =
    ↭-select-elem ys ∘↭ (m ∷↭ sort′-is-permutation M (ys ++ zs) (≤-++-cons ys len-eq))

--------------------------------------------------------------------------------------------------------------

open import Data.Bool.Base using (Bool; true; false)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat
  using (_≟_)
open import Data.Nat.Properties
  using (≟-diag; ≤-reflexive)

open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Data.List.Relation.Unary.Any as ListAny
  using (Any; here; there)
open import Data.List.Membership.Propositional
  using (_∈_)

min : ℕ → ℕ → ℕ
min y x with y ≤? x
... | true  because _ = y
... | false because _ = x

smallest : ℕ → List ℕ → ℕ
smallest y [] = y
smallest y (x ∷ xs) = smallest (min y x) xs

rm : ℕ → List ℕ → List ℕ
rm y [] = []
rm y (x ∷ xs) with y ≟ x
... | true  because _ = xs
... | false because _ = x ∷ rm y xs

smallest-elem : ∀ y xs → smallest y xs ∈ xs ⊎ smallest y xs ≡ y
smallest-elem y [] = inj₂ refl
smallest-elem y (x ∷ xs) with smallest-elem (min y x) xs
... | inj₁ smallest∈xs = inj₁ (there smallest∈xs)
... | inj₂ smallest≡min with y ≤? x
... | true  because _ = inj₂ smallest≡min
... | false because _ = inj₁ (here smallest≡min)

rm-len : ∀ {y xs} → y ∈ xs → length xs ≡ suc (length (rm y xs))
rm-len {y} {x ∷ xs} y∈x∷xs with y ≟ x
... | yes y≡x = refl
... | no  y≢x with y∈x∷xs
... | here y≡x = ⊥-elim (y≢x y≡x)
... | there y∈l = cong suc (rm-len y∈l)

rm-smallest-len : ∀ x xs → length xs ≡ length (rm (smallest x xs) (x ∷ xs))
rm-smallest-len x xs with smallest x xs ≟ x
... | yes smallest≡x rewrite ≟-diag smallest≡x = refl
... | no  smallest≢x with smallest-elem x xs
... | inj₁ smallest∈xs = rm-len smallest∈xs
... | inj₂ smallest≡x = ⊥-elim (smallest≢x smallest≡x)

ss′ : ∀ M (xs : List ℕ) → M ≡ length xs → List ℕ
ss′ zero    []       len-eq = []
ss′ (suc M) (x ∷ xs) refl =
  smallest x xs ∷
  ss′ M
      (rm (smallest x xs) (x ∷ xs))
      (rm-smallest-len x xs)

forget≤ : ∀ {L n} → L ≤ n → ℕ
forget≤ {n = n} L≤n = n

bounded-smallest : ∀ {L y xs} → L ≤ y → BoundedBelow L xs → L ≤ smallest y xs
bounded-smallest L≤y []ᵇ = L≤y
bounded-smallest L≤y (L≤x ∷ᵇ xsᵇ) with forget≤ L≤y ≤? forget≤ L≤x
... | true  because _ = bounded-smallest L≤y xsᵇ
... | false because _ = bounded-smallest L≤x xsᵇ

smallest-smaller : ∀ y xs → smallest y xs ≤ y
smallest-smaller y [] = ≤-reflexive refl
smallest-smaller y (x ∷ xs) with y ≤? x
... | yes y≤x = smallest-smaller y xs
... | no  y≰x = ≤-trans (smallest-smaller x xs) (≰⇒≥ y≰x)

smallest-bounded : ∀ y xs → BoundedBelow (smallest y xs) xs
smallest-bounded y [] = []ᵇ
smallest-bounded y (x ∷ xs) with y ≤? x
... | yes y≤x = ≤-trans (smallest-smaller y xs) y≤x ∷ᵇ smallest-bounded y xs
... | no  y≰x = smallest-smaller x xs ∷ᵇ smallest-bounded x xs

rm-bounded : ∀ {L xs} y → BoundedBelow L xs → BoundedBelow L (rm y xs)
rm-bounded y []ᵇ = []ᵇ
rm-bounded y (L≤x ∷ᵇ xsᵇ) with y ≟ forget≤ L≤x
... | true  because _ = xsᵇ
... | false because _ = L≤x ∷ᵇ rm-bounded y xsᵇ

ss′-is-sorted : ∀ {xs L} M → BoundedBelow L xs → (len-eq : M ≡ length xs) → Increasing L (ss′ M xs len-eq)
ss′-is-sorted          zero    []ᵇ          len-eq = []ⁱ
ss′-is-sorted {x ∷ xs} (suc M) (L≤x ∷ᵇ xsᵇ) refl =
  bounded-smallest L≤x xsᵇ ∷ⁱ
  ss′-is-sorted M
                (rm-bounded (smallest x xs) (smallest-smaller x xs ∷ᵇ smallest-bounded x xs))
                (rm-smallest-len x xs)