$\newcommand{\defeq}{\mathrel{\mathop:}=}$

## 2007/11/11

### QSort in Agda, Round 2

data _≼_ : Nat -> Nat -> Set where
≼-base : {n : Nat} -> 0 ≼ n
≼-step : {m n : Nat} -> m ≼ n -> (suc m) ≼ (suc n)

≼-refl : {x : Nat} -> x ≼ x
≼-refl {0} = ≼-base
≼-refl {suc n} = ≼-step (≼-refl {n})

≼-trans : {x y z : Nat} -> x ≼ y -> y ≼ z -> x ≼ z
≼-trans {0}{_}{_} _ _ = ≼-base
≼-trans {suc x}{suc y}{suc z}
(≼-step x≼y) (≼-step y≼z) = ≼-step (≼-trans x≼y y≼z)


cmp : (m n : Nat) -> (m ≼ n) \/ (n ≼ m)
cmp 0 n = \/-IL ≼-base
cmp (suc m) 0 = \/-IR ≼-base
cmp (suc m) (suc n) with cmp m n
... | \/-IL subpf = \/-IL (≼-step subpf)
... | \/-IR subpf = \/-IR (≼-step subpf)


data BoundedAbove : List Nat -> Nat -> Set where
bdd-above-base : {n : Nat} -> BoundedAbove [] n
bdd-above-step : {n : Nat}{x : Nat}{xs : List Nat} ->
BoundedAbove xs n -> x ≼ n -> BoundedAbove (x :: xs) n

data BoundedBelow : List Nat -> Nat -> Set where
bdd-below-base : {n : Nat} -> BoundedBelow [] n
bdd-below-step : {n : Nat}{x : Nat}{xs : List Nat} ->
BoundedBelow xs n -> n ≼ x -> BoundedBelow (x :: xs) n


data IncSorted : List Nat -> Set where
inc-sorted-base : IncSorted []
inc-sorted-step  : {b x : Nat} {xs : List Nat} -> IncSorted xs ->
BoundedBelow xs b -> x ≼ b -> IncSorted (x :: xs)

data DecSorted : List Nat -> Set where
dec-sorted-base : DecSorted []
dec-sorted-step  : {b x : Nat} {xs : List Nat} -> DecSorted xs ->
BoundedAbove xs b -> b ≼ x -> DecSorted (x :: xs)


bddAbove : Nat -> List Nat -> Set
bddAbove n xs = BoundedAbove xs n

bddBelow : Nat -> List Nat -> Set
bddBelow n xs = BoundedBelow xs n


relaxUpperBound : {xs : List Nat}{m n : Nat} ->
BoundedAbove xs m -> m ≼ n -> BoundedAbove xs n
relaxUpperBound {[]}{_}{n} _ _ = bdd-above-base
relaxUpperBound {x :: xs} (bdd-above-step bdd-subpf x≼m) m≼n =
bdd-above-step (relaxUpperBound {xs} bdd-subpf m≼n) (≼-trans x≼m m≼n)

relaxLowerBound : {xs : List Nat}{m n : Nat} ->
BoundedBelow xs m -> n ≼ m -> BoundedBelow xs n
relaxLowerBound {[]}{_}{n} _ _ = bdd-below-base
relaxLowerBound {x :: xs} (bdd-below-step bdd-subpf m≼x) n≼m =
bdd-below-step (relaxLowerBound {xs} bdd-subpf n≼m) (≼-trans n≼m m≼x)


bdd-above-concat : {xs ys : List Nat}{n : Nat} -> BoundedAbove xs n ->
BoundedAbove ys n -> BoundedAbove (xs ++ ys) n
bdd-above-concat {[]}{ys} _ ys-bddabv = ys-bddabv
bdd-above-concat {x :: xs}{ys} (bdd-above-step xs-bddabv n≼x) ys-bddabv =
bdd-above-step (bdd-above-concat {xs}{ys} xs-bddabv ys-bddabv) n≼x

bdd-below-concat : {xs ys : List Nat}{n : Nat} -> BoundedBelow xs n ->
BoundedBelow ys n -> BoundedBelow (xs ++ ys) n
bdd-below-concat {[]}{ys} _ ys-bddblw = ys-bddblw
bdd-below-concat {x :: xs}{ys} (bdd-below-step xs-bddblw x≼n) ys-bddblw =
bdd-below-step (bdd-below-concat {xs}{ys} xs-bddblw ys-bddblw) x≼n

inc-sorted-concat : {xs ys : List Nat}{n : Nat} ->
IncSorted xs -> IncSorted ys -> BoundedAbove xs n ->
BoundedBelow ys n -> IncSorted (xs ++ ys)
inc-sorted-concat {[]}{ys} _ ys-sorted _ _ = ys-sorted
inc-sorted-concat {x :: xs}{ys} (inc-sorted-step xs-sorted xs-bddblw x≼b)
ys-sorted (bdd-above-step xs-bddabv x≼n) ys-bddblw =
inc-sorted-step
(inc-sorted-concat xs-sorted ys-sorted xs-bddabv ys-bddblw)
(bdd-below-concat (relaxLowerBound xs-bddblw x≼b)
(relaxLowerBound ys-bddblw x≼n))
≼-refl


qsort'' : List Nat -> List Nat ∣ IncSorted


  strong-qsort'' : {m n : Nat} -> List Nat ∣ bddAbove m ⋯ bddBelow n ->
List Nat ∣ IncSorted ⋯ bddAbove m ⋯ bddBelow n


data _∧_ (P Q : Set) : Set where
_‖_ : P -> Q -> P ∧ Q

_⋯_ : {A : Set} -> (P Q : A -> Set) -> A -> Set
_⋯_ P Q a = P a ∧ Q a

takeTailPred : {A : Set}{P Q : A -> Set} -> A ∣ P ⋯ Q -> A ∣ Q
takeTailPred (_⋮_ a (p ‖ q)) = _⋮_ a q

takeHeadPred : {A : Set}{P Q : A -> Set} -> A ∣ P ⋯ Q -> A ∣ P
takeHeadPred (_⋮_ a (p ‖ q)) = _⋮_ a p


_∧_Logic.Base 裡面的 _/\_ 意義完全一樣，但這裡定義的 constructor 是 operator form，使用上比較方便。（只做 aliasing 的話沒辦法做 pattern matching。）另外我也把 dependent pair 的 constructor 改成 operator form。（到時候命題和證明就是用一堆直線橫線和「直的橫的點點點」組成 XD。）

data _∣_ (A : Set) (P : A -> Set) : Set where
_⋮_ : (x : A) -> P x -> A ∣ P


strong-qsort'' 的前提也比 qsort'' 強（i.e., 前者的 type 並非後者的 subtype），沒辦法直接做 reduction，所以必須另外證明一個 lemma，說每個 list 都有上下界。

lemma3 : (xs : List Nat) ->
∃ (\n -> List Nat ∣ equalTo xs ⋯ bddAbove n ⋯ bddBelow 0)
lemma3 [] = ∃-I 0 (_⋮_ [] (refl ‖ bdd-above-base ‖ bdd-below-base))
lemma3 (x :: xs) with lemma3 xs
lemma3 (x :: xs) | ∃-I n (_⋮_ xs' (eq-pf ‖ bdd-above-pf ‖ bdd-below-pf))
with cmp x n
lemma3 (x :: xs) | ∃-I n (_⋮_ xs' (eq-pf ‖ bdd-above-pf ‖ bdd-below-pf))
| \/-IL x≼n =
∃-I n (x :: xs ⋮
(refl {_}{x :: xs} ‖
bdd-above-step
(subst (\ys -> BoundedAbove ys n) (sym eq-pf) bdd-above-pf)
x≼n ‖
bdd-below-step
(subst (\ys -> BoundedBelow ys 0) (sym eq-pf) bdd-below-pf)
(≼-base {x})))
lemma3 (x :: xs) | ∃-I n (_⋮_ xs' (eq-pf ‖ bdd-above-pf ‖ bdd-below-pf))
| \/-IR n≼x =
∃-I x (x :: xs ⋮
(refl {_}{x :: xs} ‖
bdd-above-step
(relaxUpperBound
(subst (\ys -> BoundedAbove ys n)
(sym eq-pf) bdd-above-pf) n≼x)
(≼-refl {x})  ‖
bdd-below-step
(subst (\ys -> BoundedBelow ys 0) (sym eq-pf) bdd-below-pf)
(≼-base {x})))


qsort'' 的本體就可以寫出來了。

qsort'' : List Nat -> List Nat ∣ IncSorted
qsort'' xs =
(takeHeadPred ○ strong-qsort'' ○ takeTailPred) (takeProof (lemma3 xs))


qsort'' = takeHeadPred ○ strong-qsort'' ○ takeTailPred ○ takeProof ○ lemma3


takeWitness : {A : Set}{P : A -> Set} -> ∃ P -> A
takeWitness (∃-I wit pf) = wit

takeProof : {A : Set}{P : A -> Set} -> (ex : ∃ P) -> P (takeWitness ex)
takeProof (∃-I wit pf) = pf


partition'' : {m n : Nat} -> (p : Nat) ->
List Nat ∣ bddAbove m ⋯ bddBelow n ->
(List Nat ∣ bddAbove p ⋯ bddBelow n) ×
(List Nat ∣ bddAbove m ⋯ bddBelow p)
partition'' p ([] ⋮ upperBoundPf ‖ lowerBoundPf) =
< [] ⋮ bdd-above-base {p} ‖ lowerBoundPf ,
[] ⋮ upperBoundPf ‖ bdd-below-base {p} >
partition'' p (x :: xs ⋮ bdd-above-step xs-bddabv x≼m ‖
bdd-below-step xs-bddblw n≼x)
with partition'' p (xs ⋮ xs-bddabv ‖ xs-bddblw) | cmp x p
... | < ys ⋮ ys-bddabv ‖ ys-bddblw , zs&pfs > | \/-IL x≼p =
< x :: ys ⋮ bdd-above-step ys-bddabv x≼p ‖
bdd-below-step ys-bddblw n≼x ,
zs&pfs >
... | < ys&pfs , zs ⋮ zs-bddabv ‖ zs-bddblw > | \/-IR p≼x =
< ys&pfs ,
x :: zs ⋮ bdd-above-step zs-bddabv x≼m ‖
bdd-below-step zs-bddblw p≼x >


strong-qsort'' : {m n : Nat} -> List Nat ∣ bddAbove m ⋯ bddBelow n ->
List Nat ∣ IncSorted ⋯ bddAbove m ⋯ bddBelow n
strong-qsort'' ([] ⋮ bddabv ‖ bddblw) =
[] ⋮ inc-sorted-base ‖ bddabv ‖ bddblw
strong-qsort'' (x :: xs ⋮ bdd-above-step xs-bddabv x≼m ‖
bdd-below-step xs-bddblw n≼x)
with partition'' x (xs ⋮ xs-bddabv ‖ xs-bddblw)
... | < left , right > with strong-qsort'' left | strong-qsort'' right
strong-qsort'' (x :: xs ⋮ bdd-above-step xs-bddabv x≼m ‖
bdd-below-step xs-bddblw n≼x) | < left , right >
| ys ⋮ ys-sorted ‖ ys-bddabv ‖ ys-bddblw
| zs ⋮ zs-sorted ‖ zs-bddabv ‖ zs-bddblw =
ys ++ x :: zs ⋮
(inc-sorted-concat
ys-sorted (inc-sorted-step zs-sorted zs-bddblw ≼-refl)
ys-bddabv (bdd-below-step zs-bddblw ≼-refl)) ‖
(bdd-above-concat
(relaxUpperBound ys-bddabv x≼m) (bdd-above-step zs-bddabv x≼m)) ‖
(bdd-below-concat
ys-bddblw (bdd-below-step (relaxLowerBound zs-bddblw n≼x) n≼x))


--

Labels: ,