-
Notifications
You must be signed in to change notification settings - Fork 0
/
MergeSort3.agda
93 lines (77 loc) · 3.2 KB
/
MergeSort3.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
{-# OPTIONS --sized-types #-}
open import Data.Sum renaming (_⊎_ to _∨_)
module MergeSort3 {A : Set}
(_≤_ : A → A → Set)
(tot≤ : (a b : A) → a ≤ b ∨ b ≤ a) where
open import Level hiding (suc)
open import Size
open import Data.List
open import Function
open import Algebra
open import Algebra.Structures
open import Data.Bool hiding (_≟_;_∨_)
open import Data.Empty
open import Induction
open import Induction.Lexicographic
open import Data.Unit
open import Data.Product
open import Data.Nat hiding (_≤?_;_⊔_;_≟_) renaming (_≤_ to _≤n_)
open import Data.Nat.Properties
open import Relation.Nullary.Decidable
open import Relation.Binary.PropositionalEquality as PropEq renaming ([_] to [_]i)
data Sorted : List A → Set where
nils : Sorted []
singls : (x : A)
-- -----------
→ Sorted [ x ]
conss : (x y : A)(ys : List A) → x ≤ y → Sorted (y ∷ ys)
-- --------------------------------------------------------------
→ Sorted (x ∷ y ∷ ys)
data Bound (A : Set) : Set where
bot : Bound A
val : A → Bound A
data LeB : Bound A → Bound A → Set where
lebx : {b : Bound A} → LeB bot b
lexy : {a b : A} → a ≤ b → LeB (val a) (val b)
data OList : {ι : Size} → Bound A → Set where
onil : {ι : Size}{l : Bound A}
-- --------------------------------
→ OList {↑ ι} l
:< : {ι : Size}{l : Bound A}(x : A){l≤x : LeB l (val x)} → OList {ι} (val x)
-- -----------------------------------------------------------------------------------------------
→ OList {↑ ι} l
forgetO : {l : Bound A} → OList l → List A
forgetO onil = []
forgetO (:< x xs) = x ∷ forgetO xs
lemma-sort : {l : Bound A}(xs : OList l) → Sorted (forgetO xs)
lemma-sort onil = nils
lemma-sort (:< x onil) = singls x
lemma-sort (:< x (:< y {lexy x≤y} xs))
= conss x y (forgetO xs) x≤y (lemma-sort (:< y {lexy x≤y} xs))
data ListN : {ι : Size} → Set where
[] : {ι : Size} → ListN {↑ ι}
_∷_ : {ι : Size} → A → ListN {ι} → ListN {↑ ι}
forgetN : ListN → List A
forgetN [] = []
forgetN (x ∷ xs) = x ∷ forgetN xs
deal : {ι : Size}(xs : ListN {ι}) → ListN {ι} × ListN {ι}
deal [] = ([] , [])
deal (x ∷ []) = (x ∷ [] , [])
deal (x ∷ y ∷ xs) with deal xs
... | ys , zs = (x ∷ ys , y ∷ zs)
merge : {ι ι′ : Size}{l : Bound A} → OList {ι} l → OList {ι′} l → OList l
merge onil l = l
merge l onil = l
merge (:< x {l≤x = l≤x} xs)
(:< y {l≤x = l≤y} ys)
with tot≤ x y
... | inj₁ x≤y = (:< x {l≤x = l≤x} (merge xs (:< y {l≤x = lexy x≤y} ys)))
... | inj₂ y≤x = (:< y {l≤x = l≤y} (merge (:< x {l≤x = lexy y≤x} xs) ys))
mergeSort : {ι : Size} → ListN {↑ ι} → OList bot
mergeSort [] = onil
mergeSort (x ∷ []) = :< x {l≤x = lebx} onil
mergeSort (x ∷ (y ∷ xs)) with deal xs
... | (ys , zs) = merge (mergeSort (x ∷ ys)) (mergeSort (y ∷ zs))
-- Verify Correctness against Sorted specification
lemma-mergeSort-sorted : (xs : ListN) → Sorted (forgetO (mergeSort xs))
lemma-mergeSort-sorted = lemma-sort ∘ mergeSort