Skip to content

Commit c645989

Browse files
onestruggleronestruggler
authored
added insertion sort and refactored merge sort (#2751)
* added insertion sort and refactored merge sort * made insert-swap-< private
1 parent b6feb45 commit c645989

File tree

7 files changed

+355
-101
lines changed

7 files changed

+355
-101
lines changed

‎CHANGELOG.md

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -168,6 +168,10 @@ New modules
168168

169169
* `Data.List.Relation.Binary.Suffix.Propositional.Properties` showing the equivalence to right divisibility induced by the list monoid.
170170

171+
* `Data.List.Sort.InsertionSort.{agda|Base|Properties}` defines insertion sort and proves properties of insertion sort such as Sorted and Permutation properties.
172+
173+
* `Data.List.Sort.MergenSort.{agda|Base|Properties}` is a refactor of the previous `Data.List.Sort.MergenSort`.
174+
171175
* `Data.Sign.Show` to show a sign.
172176

173177
* `Relation.Binary.Morphism.Construct.Product` to plumb in the (categorical) product structure on `RawSetoid`.

‎src/Data/List/Sort/InsertionSort.agda

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- An implementation of insertion sort and its properties
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --cubical-compatible --safe #-}
8+
9+
open import Relation.Binary.Bundles using (DecTotalOrder)
10+
11+
module Data.List.Sort.InsertionSort
12+
{a ℓ₁ ℓ₂}
13+
(O : DecTotalOrder a ℓ₁ ℓ₂)
14+
where
15+
16+
open import Data.List.Sort.InsertionSort.Base O public
17+
open import Data.List.Sort.InsertionSort.Properties O using (insertionSort) public

‎src/Data/List/Sort/InsertionSort/Base.agda

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- An implementation of insertion sort
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --cubical-compatible --safe #-}
8+
9+
open import Relation.Binary.Bundles using (DecTotalOrder)
10+
11+
module Data.List.Sort.InsertionSort.Base
12+
{a ℓ₁ ℓ₂}
13+
(O : DecTotalOrder a ℓ₁ ℓ₂)
14+
where
15+
16+
open import Data.Bool.Base using (if_then_else_)
17+
open import Data.List.Base using (List; []; _∷_)
18+
open import Relation.Nullary.Decidable.Core using (does)
19+
20+
open DecTotalOrder O renaming (Carrier to A)
21+
22+
------------------------------------------------------------------------
23+
-- Definitions
24+
25+
insert : A → List A → List A
26+
insert x [] = x ∷ []
27+
insert x (y ∷ xs) = if does (x ≤? y)
28+
then x ∷ y ∷ xs
29+
else y ∷ insert x xs
30+
31+
sort : List A → List A
32+
sort [] = []
33+
sort (x ∷ xs) = insert x (sort xs)

‎src/Data/List/Sort/InsertionSort/Properties.agda

Lines changed: 155 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,155 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Properties of insertion sort
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --cubical-compatible --safe #-}
8+
9+
open import Relation.Binary.Bundles using (DecTotalOrder)
10+
11+
module Data.List.Sort.InsertionSort.Properties
12+
{a ℓ₁ ℓ₂}
13+
(O : DecTotalOrder a ℓ₁ ℓ₂)
14+
where
15+
16+
open import Data.Bool.Base using (true; false; if_then_else_)
17+
open import Data.List.Base using (List; []; _∷_)
18+
open import Data.List.Relation.Binary.Pointwise using ([]; _∷_; decidable; setoid)
19+
open import Data.List.Relation.Binary.Permutation.Propositional
20+
import Data.List.Relation.Binary.Permutation.Propositional.Properties as Perm
21+
open import Data.List.Relation.Unary.Linked using ([]; [-]; _∷_)
22+
open import Relation.Binary.Bundles using (Setoid)
23+
open import Relation.Binary.Definitions using (Decidable)
24+
open import Relation.Binary.Properties.DecTotalOrder O using (≰⇒≥)
25+
open import Relation.Nullary.Decidable.Core using (does; yes; no)
26+
open import Relation.Nullary.Negation.Core using (contradiction)
27+
28+
open DecTotalOrder O renaming (Carrier to A; trans to ≤-trans)
29+
using (totalOrder; _≤?_; _≤_; module Eq; _≈_; ≤-respʳ-≈; ≤-respˡ-≈; antisym)
30+
31+
open import Data.List.Relation.Binary.Equality.Setoid Eq.setoid
32+
using (_≋_; ≋-refl; ≋-sym; ≋-trans)
33+
open import Data.List.Relation.Unary.Sorted.TotalOrder totalOrder using (Sorted)
34+
open import Data.List.Sort.Base totalOrder using (SortingAlgorithm)
35+
open import Data.List.Sort.InsertionSort.Base O
36+
import Relation.Binary.Reasoning.Setoid (setoid Eq.setoid) as ≋-Reasoning
37+
38+
------------------------------------------------------------------------
39+
-- Permutation property
40+
41+
insert-↭ : ∀ x xs → insert x xs ↭ x ∷ xs
42+
insert-↭ x [] = ↭-refl
43+
insert-↭ x (y ∷ xs) with does (x ≤? y)
44+
... | true = ↭-refl
45+
... | false = begin
46+
y ∷ insert x xs ↭⟨ prep y (insert-↭ x xs) ⟩
47+
y ∷ x ∷ xs ↭⟨ swap y x refl ⟩
48+
x ∷ y ∷ xs ∎
49+
where open PermutationReasoning
50+
51+
insert-cong-↭ : ∀ {x xs ys} → xs ↭ ys → insert x xs ↭ x ∷ ys
52+
insert-cong-↭ {x} {xs} {ys} eq = begin
53+
insert x xs ↭⟨ insert-↭ x xs ⟩
54+
x ∷ xs ↭⟨ prep x eq ⟩
55+
x ∷ ys ∎
56+
where open PermutationReasoning
57+
58+
sort-↭ : ∀ (xs : List A) → sort xs ↭ xs
59+
sort-↭ [] = ↭-refl
60+
sort-↭ (x ∷ xs) = insert-cong-↭ (sort-↭ xs)
61+
62+
------------------------------------------------------------------------
63+
-- Sorted property
64+
65+
insert-↗ : ∀ x {xs} → Sorted xs → Sorted (insert x xs)
66+
insert-↗ x [] = [-]
67+
insert-↗ x ([-] {y}) with x ≤? y
68+
... | yes x≤y = x≤y ∷ [-]
69+
... | no x≰y = ≰⇒≥ x≰y ∷ [-]
70+
insert-↗ x (_∷_ {y} {z} {ys} y≤z z≤ys) with x ≤? y
71+
... | yes x≤y = x≤y ∷ y≤z ∷ z≤ys
72+
... | no x≰y with ih ← insert-↗ x z≤ys | x ≤? z
73+
... | yes _ = ≰⇒≥ x≰y ∷ ih
74+
... | no _ = y≤z ∷ ih
75+
76+
sort-↗ : ∀ xs → Sorted (sort xs)
77+
sort-↗ [] = []
78+
sort-↗ (x ∷ xs) = insert-↗ x (sort-↗ xs)
79+
80+
------------------------------------------------------------------------
81+
-- Algorithm
82+
83+
insertionSort : SortingAlgorithm
84+
insertionSort = record
85+
{ sort = sort
86+
; sort-↭ = sort-↭
87+
; sort-↗ = sort-↗
88+
}
89+
90+
------------------------------------------------------------------------
91+
-- Congruence properties
92+
93+
insert-congʳ : ∀ z {xs ys} → xs ≋ ys → insert z xs ≋ insert z ys
94+
insert-congʳ z [] = ≋-refl
95+
insert-congʳ z (_∷_ {x} {y} {xs} {ys} x∼y eq) with z ≤? x | z ≤? y
96+
... | yes _ | yes _ = Eq.refl ∷ x∼y ∷ eq
97+
... | no z≰x | yes z≤y = contradiction (≤-respʳ-≈ (Eq.sym x∼y) z≤y) z≰x
98+
... | yes z≤x | no z≰y = contradiction (≤-respʳ-≈ x∼y z≤x) z≰y
99+
... | no _ | no _ = x∼y ∷ insert-congʳ z eq
100+
101+
insert-congˡ : ∀ {x y} xs → x ≈ y → insert x xs ≋ insert y xs
102+
insert-congˡ {x} {y} [] eq = eq ∷ []
103+
insert-congˡ {x} {y} (z ∷ xs) eq with x ≤? z | y ≤? z
104+
... | yes _ | yes _ = eq ∷ ≋-refl
105+
... | no x≰z | yes y≤z = contradiction (≤-respˡ-≈ (Eq.sym eq) y≤z) x≰z
106+
... | yes x≤z | no y≰z = contradiction (≤-respˡ-≈ eq x≤z) y≰z
107+
... | no _ | no _ = Eq.refl ∷ insert-congˡ xs eq
108+
109+
insert-cong : ∀ {x y xs ys} → x ≈ y → xs ≋ ys → insert x xs ≋ insert y ys
110+
insert-cong {y = y} {xs} eq₁ eq₂ = ≋-trans (insert-congˡ xs eq₁) (insert-congʳ y eq₂)
111+
112+
sort-cong : ∀ {xs ys} → xs ≋ ys → sort xs ≋ sort ys
113+
sort-cong [] = []
114+
sort-cong (x∼y ∷ eq) = insert-cong x∼y (sort-cong eq)
115+
116+
private
117+
insert-swap-≤ : ∀ {x y} xs → x ≤ y → insert x (insert y xs) ≋ insert y (insert x xs)
118+
insert-swap-≤ {x} {y} [] x≤y with x ≤? y
119+
... | no xy = contradiction x≤y xy
120+
... | yes xy with y ≤? x
121+
... | yes yx = Eq.sym eq ∷ eq ∷ [] where eq = antisym yx xy
122+
... | no _ = ≋-refl
123+
insert-swap-≤ {x} {y} (z ∷ xs) x≤y with y ≤? z
124+
insert-swap-≤ {x} {y} (z ∷ xs) x≤y | yes yz with x ≤? y
125+
insert-swap-≤ {x} {y} (z ∷ xs) x≤y | yes yz | yes xy with x ≤? z
126+
insert-swap-≤ {x} {y} (z ∷ xs) x≤y | yes yz | yes xy | yes xz with y ≤? x
127+
insert-swap-≤ {x} {y} (z ∷ xs) x≤y | yes yz | yes xy | yes xz | yes yx =
128+
Eq.sym eq ∷ eq ∷ ≋-refl where eq = antisym yx xy
129+
insert-swap-≤ {x} {y} (z ∷ xs) x≤y | yes yz | yes xy | yes xz | no yx with y ≤? z
130+
insert-swap-≤ {x} {y} (z ∷ xs) x≤y | yes yz | yes xy | yes xz | no yx | yes yz' = ≋-refl
131+
insert-swap-≤ {x} {y} (z ∷ xs) x≤y | yes yz | yes xy | yes xz | no yx | no yz' = contradiction yz yz'
132+
insert-swap-≤ {x} {y} (z ∷ xs) x≤y | yes yz | yes xy | no xz = contradiction (≤-trans xy yz) xz
133+
insert-swap-≤ {x} {y} (z ∷ xs) x≤y | yes yz | no xy = contradiction x≤y xy
134+
insert-swap-≤ {x} {y} (z ∷ xs) x≤y | no yz with x ≤? z
135+
insert-swap-≤ {x} {y} (z ∷ xs) x≤y | no yz | yes xz with y ≤? x
136+
insert-swap-≤ {x} {y} (z ∷ xs) x≤y | no yz | yes xz | yes yx = contradiction (≤-trans yx xz) yz
137+
insert-swap-≤ {x} {y} (z ∷ xs) x≤y | no yz | yes xz | no yx with y ≤? z
138+
insert-swap-≤ {x} {y} (z ∷ xs) x≤y | no yz | yes xz | no yx | yes yz' = contradiction yz' yz
139+
insert-swap-≤ {x} {y} (z ∷ xs) x≤y | no yz | yes xz | no yx | no yz' = ≋-refl
140+
insert-swap-≤ {x} {y} (z ∷ xs) x≤y | no yz | no xz with y ≤? z
141+
insert-swap-≤ {x} {y} (z ∷ xs) x≤y | no yz | no xz | yes yz' = contradiction yz' yz
142+
insert-swap-≤ {x} {y} (z ∷ xs) x≤y | no yz | no xz | no yz' = Eq.refl ∷ (insert-swap-≤ xs x≤y)
143+
144+
insert-swap : ∀ x y xs → insert x (insert y xs) ≋ insert y (insert x xs)
145+
insert-swap x y xs with x ≤? y
146+
... | yes x≤y = insert-swap-≤ xs x≤y
147+
... | no x≰y = ≋-sym (insert-swap-≤ xs (≰⇒≥ x≰y))
148+
149+
insert-swap-cong : ∀ {x y x′ y′ xs ys} → x ≈ x′ → y ≈ y′ → xs ≋ ys →
150+
insert x (insert y xs) ≋ insert y′ (insert x′ ys)
151+
insert-swap-cong {x} {y} {x′} {y′} {xs} {ys} eq₁ eq₂ eq₃ = begin
152+
insert x (insert y xs) ≈⟨ insert-cong eq₁ (insert-cong eq₂ eq₃) ⟩
153+
insert x′ (insert y′ ys) ≈⟨ insert-swap x′ y′ ys ⟩
154+
insert y′ (insert x′ ys) ∎
155+
where open ≋-Reasoning

‎src/Data/List/Sort/MergeSort.agda

Lines changed: 2 additions & 101 deletions
Original file line numberDiff line numberDiff line change
@@ -15,104 +15,5 @@ open import Relation.Binary.Bundles using (DecTotalOrder)
1515
module Data.List.Sort.MergeSort
1616
{a ℓ₁ ℓ₂} (O : DecTotalOrder a ℓ₁ ℓ₂) where
1717

18-
open import Data.Bool.Base using (true; false)
19-
open import Data.List.Base
20-
using (List; []; _∷_; merge; length; map; [_]; concat; _++_)
21-
open import Data.List.Properties using (length-partition; ++-assoc; concat-map-[_])
22-
open import Data.List.Relation.Unary.Linked using ([]; [-])
23-
import Data.List.Relation.Unary.Sorted.TotalOrder.Properties as Sorted
24-
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
25-
import Data.List.Relation.Unary.All.Properties as All
26-
open import Data.List.Relation.Binary.Permutation.Propositional
27-
import Data.List.Relation.Binary.Permutation.Propositional.Properties as Perm
28-
open import Data.Maybe.Base using (just)
29-
open import Data.Nat.Base using (_<_; _>_; z<s; s<s)
30-
open import Data.Nat.Induction
31-
open import Data.Nat.Properties using (m<n⇒m<1+n)
32-
open import Data.Product.Base as Product using (_,_)
33-
open import Function.Base using (_∘_)
34-
open import Relation.Nullary.Negation.Core using (¬_)
35-
open import Relation.Nullary.Decidable.Core using (does)
36-
37-
open DecTotalOrder O renaming (Carrier to A)
38-
39-
open import Data.List.Sort.Base totalOrder
40-
open import Data.List.Relation.Unary.Sorted.TotalOrder totalOrder hiding (head)
41-
open import Relation.Binary.Properties.DecTotalOrder O using (≰⇒≥; ≰-respˡ-≈)
42-
43-
open PermutationReasoning
44-
45-
------------------------------------------------------------------------
46-
-- Definition
47-
48-
mergePairs : List (List A) → List (List A)
49-
mergePairs (xs ∷ ys ∷ yss) = merge _≤?_ xs ys ∷ mergePairs yss
50-
mergePairs xss = xss
51-
52-
private
53-
length-mergePairs : ∀ xs ys yss → let zss = xs ∷ ys ∷ yss in
54-
length (mergePairs zss) < length zss
55-
length-mergePairs _ _ [] = s<s z<s
56-
length-mergePairs _ _ (xs ∷ []) = s<s (s<s z<s)
57-
length-mergePairs _ _ (xs ∷ ys ∷ yss) = s<s (m<n⇒m<1+n (length-mergePairs xs ys yss))
58-
59-
mergeAll : (xss : List (List A)) → Acc _<_ (length xss) → List A
60-
mergeAll [] _ = []
61-
mergeAll (xs ∷ []) _ = xs
62-
mergeAll xss@(xs ∷ ys ∷ yss) (acc rec) = mergeAll
63-
(mergePairs xss) (rec (length-mergePairs xs ys yss))
64-
65-
sort : List A → List A
66-
sort xs = mergeAll (map [_] xs) (<-wellFounded-fast _)
67-
68-
------------------------------------------------------------------------
69-
-- Permutation property
70-
71-
mergePairs-↭ : ∀ xss → concat (mergePairs xss) ↭ concat xss
72-
mergePairs-↭ [] = ↭-refl
73-
mergePairs-↭ (xs ∷ []) = ↭-refl
74-
mergePairs-↭ (xs ∷ ys ∷ xss) = begin
75-
merge _ xs ys ++ concat (mergePairs xss) ↭⟨ Perm.++⁺ (Perm.merge-↭ _ xs ys) (mergePairs-↭ xss) ⟩
76-
(xs ++ ys) ++ concat xss ≡⟨ ++-assoc xs ys (concat xss) ⟩
77-
xs ++ ys ++ concat xss ∎
78-
79-
mergeAll-↭ : ∀ xss (rec : Acc _<_ (length xss)) → mergeAll xss rec ↭ concat xss
80-
mergeAll-↭ [] _ = ↭-refl
81-
mergeAll-↭ (xs ∷ []) _ = ↭-sym (Perm.++-identityʳ xs)
82-
mergeAll-↭ (xs ∷ ys ∷ xss) (acc rec) = begin
83-
mergeAll (mergePairs (xs ∷ ys ∷ xss)) _ ↭⟨ mergeAll-↭ (mergePairs (xs ∷ ys ∷ xss)) _ ⟩
84-
concat (mergePairs (xs ∷ ys ∷ xss)) ↭⟨ mergePairs-↭ (xs ∷ ys ∷ xss) ⟩
85-
concat (xs ∷ ys ∷ xss) ∎
86-
87-
sort-↭ : ∀ xs → sort xs ↭ xs
88-
sort-↭ xs = begin
89-
mergeAll (map [_] xs) _ ↭⟨ mergeAll-↭ (map [_] xs) _ ⟩
90-
concat (map [_] xs) ≡⟨ concat-map-[ xs ] ⟩
91-
xs ∎
92-
93-
------------------------------------------------------------------------
94-
-- Sorted property
95-
96-
mergePairs-↗ : ∀ {xss} → All Sorted xss → All Sorted (mergePairs xss)
97-
mergePairs-↗ [] = []
98-
mergePairs-↗ (xs↗ ∷ []) = xs↗ ∷ []
99-
mergePairs-↗ (xs↗ ∷ ys↗ ∷ xss↗) = Sorted.merge⁺ O xs↗ ys↗ ∷ mergePairs-↗ xss↗
100-
101-
mergeAll-↗ : ∀ {xss} (rec : Acc _<_ (length xss)) →
102-
All Sorted xss → Sorted (mergeAll xss rec)
103-
mergeAll-↗ rec [] = []
104-
mergeAll-↗ rec (xs↗ ∷ []) = xs↗
105-
mergeAll-↗ (acc rec) (xs↗ ∷ ys↗ ∷ xss↗) = mergeAll-↗ _ (mergePairs-↗ (xs↗ ∷ ys↗ ∷ xss↗))
106-
107-
sort-↗ : ∀ xs → Sorted (sort xs)
108-
sort-↗ xs = mergeAll-↗ _ (All.map⁺ (All.universal (λ _ → [-]) xs))
109-
110-
------------------------------------------------------------------------
111-
-- Algorithm
112-
113-
mergeSort : SortingAlgorithm
114-
mergeSort = record
115-
{ sort = sort
116-
; sort-↭ = sort-↭
117-
; sort-↗ = sort-↗
118-
}
18+
open import Data.List.Sort.MergeSort.Base O public
19+
open import Data.List.Sort.MergeSort.Properties O using (mergeSort) public

‎src/Data/List/Sort/MergeSort/Base.agda

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- An implementation of merge sort
5+
------------------------------------------------------------------------
6+
7+
-- Unless you are need a particular property of MergeSort, you should
8+
-- import and use the sorting algorithm from `Data.List.Sort` instead
9+
-- of this file.
10+
11+
{-# OPTIONS --cubical-compatible --safe #-}
12+
13+
open import Relation.Binary.Bundles using (DecTotalOrder)
14+
15+
module Data.List.Sort.MergeSort.Base
16+
{a ℓ₁ ℓ₂} (O : DecTotalOrder a ℓ₁ ℓ₂) where
17+
18+
open import Data.List.Base
19+
using (List; []; _∷_; merge; length; map; [_])
20+
21+
open import Data.Nat.Base using (_<_; _>_; z<s; s<s)
22+
open import Data.Nat.Induction
23+
open import Data.Nat.Properties using (m<n⇒m<1+n)
24+
25+
open DecTotalOrder O renaming (Carrier to A)
26+
27+
------------------------------------------------------------------------
28+
-- Definition
29+
30+
mergePairs : List (List A) → List (List A)
31+
mergePairs (xs ∷ ys ∷ yss) = merge _≤?_ xs ys ∷ mergePairs yss
32+
mergePairs xss = xss
33+
34+
private
35+
length-mergePairs : ∀ xs ys yss → let zss = xs ∷ ys ∷ yss in
36+
length (mergePairs zss) < length zss
37+
length-mergePairs _ _ [] = s<s z<s
38+
length-mergePairs _ _ (xs ∷ []) = s<s (s<s z<s)
39+
length-mergePairs _ _ (xs ∷ ys ∷ yss) = s<s (m<n⇒m<1+n (length-mergePairs xs ys yss))
40+
41+
mergeAll : (xss : List (List A)) → Acc _<_ (length xss) → List A
42+
mergeAll [] _ = []
43+
mergeAll (xs ∷ []) _ = xs
44+
mergeAll xss@(xs ∷ ys ∷ yss) (acc rec) = mergeAll
45+
(mergePairs xss) (rec (length-mergePairs xs ys yss))
46+
47+
sort : List A → List A
48+
sort xs = mergeAll (map [_] xs) (<-wellFounded-fast _)

0 commit comments

Comments
 (0)