Skip to content

Instantly share code, notes, and snippets.

@jfdm

jfdm/Flag.idr

Created October 2, 2023 10:48
Show Gist options
  • Save jfdm/4b4b60226e68c2612ce474e95b833a5d to your computer and use it in GitHub Desktop.
Save jfdm/4b4b60226e68c2612ce474e95b833a5d to your computer and use it in GitHub Desktop.
Download ZIP
Merge Sort in Idris...or 'a' solution to the dutch flag problem.
Raw
Flag.idr
module Flag
import Control.Relation
import Control.WellFounded
import Data.Nat
import Data.DPair
import Data.List
import Data.List.Views
%default total
lengthSuc : (xs : List a) -> (y : a) -> (ys : List a) ->
length (xs ++ (y :: ys)) = S (length (xs ++ ys))
lengthSuc [] _ _ = Refl
lengthSuc (x :: xs) y ys = cong S (lengthSuc xs y ys)
lengthLT : (xs : List a) -> (ys : List a) ->
LTE (length xs) (length (ys ++ xs))
lengthLT xs [] = reflexive {x = length xs}
lengthLT xs (x :: ys) = lteSuccRight (lengthLT _ _)
smallerLeft : (ys : List a) -> (y : a) -> (zs : List a) ->
LTE (S (S (length ys))) (S (length (ys ++ (y :: zs))))
smallerLeft [] y zs = LTESucc (LTESucc LTEZero)
smallerLeft (z :: ys) y zs = LTESucc (smallerLeft ys _ _)
smallerRight : (ys : List a) -> (zs : List a) ->
LTE (S (S (length zs))) (S (length (ys ++ (y :: zs))))
smallerRight ys zs = rewrite lengthSuc ys y zs in
(LTESucc (LTESucc (lengthLT _ _)))
data Merge : (f : a -> a -> Type)
-> (xs,ys,zs : List a)
-> Type
where
EmptyR : Merge f Nil ys ys
EmptyL : Merge f xs Nil xs
GoLT : {0 f : a -> a -> Type}
-> (prf : f x y)
-> (rest : Merge f xs (y::ys) zs)
-> Merge f (x::xs) (y::ys) (x::zs)
GoGTE : {0 f : a -> a -> Type}
-> (prf : f x y -> Void)
-> (rest : Merge f (x::xs) ys zs)
-> Merge f (x::xs) (y::ys) (y::zs)
export
merge : (cmp : (x,y : a) -> Dec (f x y))
-> (xs : List a)
-> (ys : List a)
-> DPair (List a)
(Merge f xs ys)
merge cmp [] []
= ([] ** EmptyR)
merge cmp [] (x :: xs)
= (x :: xs ** EmptyR)
merge cmp (x :: xs) []
= (x :: xs ** EmptyL)
merge cmp (x :: xs) (y :: ys) with (cmp x y)
merge cmp (x :: xs) (y :: ys) | (Yes pH) with (assert_total $ merge cmp xs (y::ys))
merge cmp (x :: xs) (y :: ys) | (Yes pH) | (zs ** pT)
= (x :: zs ** GoLT pH pT)
merge cmp (x :: xs) (y :: ys) | (No contra) with (assert_total $ merge cmp (x::xs) ys)
merge cmp (x :: xs) (y :: ys) | (No contra) | (zs ** pT)
= (y :: zs ** GoGTE contra pT)
public export
data MergeSort : (f : a -> a -> Type)
-> (xs,ys : List a)
-> Type where
MergeSortNil : MergeSort f Nil Nil
MergeSortOne : (x : a) -> MergeSort f [x] [x]
MergeSortPair : (xs, ys, as, bs, cs : List a) -- Explicit, don't erase
-> (lrec : Lazy (MergeSort f xs as))
-> (rrec : Lazy (MergeSort f ys bs))
-> (doM : Merge f as bs cs)
-> MergeSort f (xs ++ ys) cs
public export
mergeSort : (cmp : (x,y : a) -> Dec (f x y))
-> (xs : List a)
-> DPair (List a)
(MergeSort f xs)
mergeSort cmp xs with (sizeAccessible xs)
mergeSort cmp xs | acc with (split xs)
mergeSort cmp [] | acc | SplitNil
= ([] ** MergeSortNil)
mergeSort cmp [x] | acc | (SplitOne x)
= ([x] ** MergeSortOne x)
mergeSort cmp (x :: ys ++ (y :: zs)) | acc | (SplitPair x ys y zs) with (assert_total $ mergeSort cmp (x::ys))
mergeSort cmp (x :: ys ++ (y :: zs)) | acc | (SplitPair x ys y zs) | lefts with (assert_total $ mergeSort cmp (y::zs))
mergeSort cmp (x :: ys ++ (y :: zs)) | acc | (SplitPair x ys y zs) | (as ** prfL) | (bs ** prfR) with (merge cmp as bs)
mergeSort cmp (x :: ys ++ (y :: zs)) | acc | (SplitPair x ys y zs) | (as ** prfL) | (bs ** prfR) | (cs ** prfM) = (cs ** MergeSortPair
(x::ys)
(y::zs)
as
bs
cs
prfL
prfR
prfM
)
data Kleur = Rode | Blauw | Wit
data GT : (a,b : Kleur) -> Type where
RW : GT Rode Wit
RB : GT Rode Blauw
WB : GT Wit Blauw
Uninhabited (Flag.GT x x) where
uninhabited RW impossible
Uninhabited (GT Blauw Rode) where uninhabited _ impossible
Uninhabited (GT Blauw Wit) where uninhabited _ impossible
Uninhabited (GT Wit Rode) where uninhabited _ impossible
gt : (a,b : Kleur) -> Dec (GT a b)
gt Rode Rode = No absurd
gt Rode Blauw = Yes RB
gt Rode Wit = Yes RW
gt Blauw Rode = No absurd
gt Blauw Blauw = No absurd
gt Blauw Wit = No absurd
gt Wit Rode
= No absurd
gt Wit Blauw
= Yes WB
gt Wit Wit
= No absurd
xs : List Kleur
xs = [Blauw, Wit, Blauw, Wit, Rode, Rode, Wit, Blauw]
Raw
repl.txt
λΠ> mergeSort gt xs
([Rode, Rode, Wit, Wit, Wit, Blauw, Blauw, Blauw] **
MergeSortPair [Blauw, Wit, Blauw, Wit] [Rode, Rode, Wit, Blauw] [Wit, Wit, Blauw, Blauw] [Rode,
Rode,
Wit,
Blauw] [Rode,
Rode,
Wit,
Wit,
Wit,
Blauw,
Blauw,
Blauw] (Delay (MergeSortPair [Blauw,
Wit] [Blauw,
Wit] [Wit,
Blauw] [Wit,
Blauw] [Wit,
Wit,
Blauw,
Blauw] (Delay (MergeSortPair [Blauw] [Wit] [Blauw] [Wit] [Wit,
Blauw] (Delay (MergeSortOne Blauw)) (Delay (MergeSortOne Wit)) (GoGTE absurd EmptyL))) (Delay (MergeSortPair [Blauw] [Wit] [Blauw] [Wit] [Wit,
Blauw] (Delay (MergeSortOne Blauw)) (Delay (MergeSortOne Wit)) (GoGTE absurd EmptyL))) (GoGTE absurd (GoLT WB (GoGTE absurd EmptyL))))) (Delay (MergeSortPair [Rode,
Rode] [Wit,
Blauw] [Rode,
Rode] [Wit,
Blauw] [Rode,
Rode,
Wit,
Blauw] (Delay (MergeSortPair [Rode] [Rode] [Rode] [Rode] [Rode,
Rode] (Delay (MergeSortOne Rode)) (Delay (MergeSortOne Rode)) (GoGTE absurd EmptyL))) (Delay (MergeSortPair [Wit] [Blauw] [Wit] [Blauw] [Wit,
Blauw] (Delay (MergeSortOne Wit)) (Delay (MergeSortOne Blauw)) (GoLT WB EmptyR))) (GoLT RW (GoLT RW EmptyR)))) (GoGTE absurd (GoGTE absurd (GoGTE absurd (GoLT WB (GoLT WB (GoGTE absurd EmptyL)))))))
λΠ> fst $ mergeSort gt xs
[Rode, Rode, Wit, Wit, Wit, Blauw, Blauw, Blauw]
λΠ>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment