# 日々の流転

## 2009-08-31 [長年日記]

### λ. Agda2でクイックソート

LLTV後の飲み会でranhaさんが、クイックソートの停止性をAgda2の停止性チェッカに説得できないというような事を話していた(参考: 修行失敗 - Yet Another Ranha (2009-08-27))ので、Agdaさんを説得してみた。 基本的には length (filter p xs) ≦ length xs の証明Wellfounded induction in Agda2 で書いたのを組み合わせただけなんだけど、Agda2のライブラリの使い方を調べるのが面倒くさかったよ……

```module Quicksort where

open import Data.Bool
open import Data.Nat
open import Data.List
open import Relation.Binary using (Rel)
import Induction.WellFounded as WF
open WF using (Acc; acc)
open WF _<′_ using () renaming (Acc to <-Acc)
open import Induction.Nat using (<-allAcc)

R : ∀ {A} → Rel (List A)
R {A} xs ys = length xs <′ length ys

R-allAcc : ∀ {A} xs → Acc (R {A}) xs
R-allAcc xs = f xs (<-allAcc (length xs))
where
f : ∀ xs → <-Acc (length xs) → Acc R xs
f xs (acc rs) = acc (λ ys h → f ys (rs (length ys) h))

s≤′s : ∀ {m n} → (m ≤′ n) → suc m ≤′ suc n
s≤′s ≤′-refl = ≤′-refl
s≤′s (≤′-step h) = ≤′-step (s≤′s h)

length-filter
: ∀ {A} → (f : A → Bool) → (xs : List A)
→ length (filter f xs) ≤′ length xs
length-filter f [] = ≤′-refl
length-filter f (x ∷ xs) with f x
... | true  = s≤′s (length-filter f xs)
... | false = ≤′-step (length-filter f xs)

length-filter′
: ∀ {A} → (f : A → Bool) → (x : A) → (xs : List A)
→ length (filter f xs) <′ length (x ∷ xs)
length-filter′ f x xs = s≤′s (length-filter f xs)

quicksort′
: ∀ {A} → (A → A → Bool) → (xs : List A)
→ ((ys : List A) → R ys xs → List A) → List A
quicksort′ _≤?_ [] f = []
quicksort′ _≤?_ (x ∷ xs) f = f ys ys-lem ++ [ x ] ++ f zs zs-lem
where
ys = filter (λ y → y ≤? x) xs
zs = filter (λ y → not (y ≤? x)) xs
ys-lem : R ys (x ∷ xs)
ys-lem = length-filter′ (λ y → y ≤? x) x xs
zs-lem : R zs (x ∷ xs)
zs-lem = length-filter′ (λ y → not (y ≤? x)) x xs

quicksort : ∀ {A} → (A → A → Bool) → List A → List A
quicksort {A} _≤?_ = wfRec (λ _ → List A) (quicksort′ _≤?_)
where open WF.All R R-allAcc```

Tags: agda