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
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** A modular implementation of mergesort (the complexity is O(n.log n) in
the length of the list) *)
(* Initial author: Hugo Herbelin, Oct 2009 *)
Require Import List Setoid Permutation Sorted Orders.
(** Notations and conventions *)
Local Notation "[ ]" := nil.
Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..).
Open Scope bool_scope.
Local Coercion is_true : bool >-> Sortclass.
(** The main module defining [mergesort] on a given boolean
order [<=?]. We require minimal hypotheses : this boolean
order should only be total: [forall x y, (x<=?y) \/ (y<=?x)].
Transitivity is not mandatory, but without it one can
only prove [LocallySorted] and not [StronglySorted].
*)
Module Sort (Import X:Orders.TotalLeBool').
Fixpoint merge l1 l2 :=
let fix merge_aux l2 :=
match l1, l2 with
| [], _ => l2
| _, [] => l1
| a1::l1', a2::l2' =>
if a1 <=? a2 then a1 :: merge l1' l2 else a2 :: merge_aux l2'
end
in merge_aux l2.
(** We implement mergesort using an explicit stack of pending mergings.
Pending merging are represented like a binary number where digits are
either None (denoting 0) or Some list to merge (denoting 1). The n-th
digit represents the pending list to be merged at level n, if any.
Merging a list to a stack is like adding 1 to the binary number
represented by the stack but the carry is propagated by merging the
lists. In practice, when used in mergesort, the n-th digit, if non 0,
carries a list of length 2^n. For instance, adding singleton list
[3] to the stack Some [4]::Some [2;6]::None::Some [1;3;5;5]
reduces to propagate the carry [3;4] (resulting of the merge of [3]
and [4]) to the list Some [2;6]::None::Some [1;3;5;5], which reduces
to propagating the carry [2;3;4;6] (resulting of the merge of [3;4] and
[2;6]) to the list None::Some [1;3;5;5], which locally produces
Some [2;3;4;6]::Some [1;3;5;5], i.e. which produces the final result
None::None::Some [2;3;4;6]::Some [1;3;5;5].
For instance, here is how [6;2;3;1;5] is sorted:
<<
operation stack list
iter_merge [] [6;2;3;1;5]
= append_list_to_stack [ + [6]] [2;3;1;5]
-> iter_merge [[6]] [2;3;1;5]
= append_list_to_stack [[6] + [2]] [3;1;5]
= append_list_to_stack [ + [2;6];] [3;1;5]
-> iter_merge [[2;6];] [3;1;5]
= append_list_to_stack [[2;6]; + [3]] [1;5]
-> merge_list [[2;6];[3]] [1;5]
= append_list_to_stack [[2;6];[3] + [1] [5]
= append_list_to_stack [[2;6] + [1;3];] [5]
= append_list_to_stack [ + [1;2;3;6];;] [5]
-> merge_list [[1;2;3;6];;] [5]
= append_list_to_stack [[1;2;3;6];; + [5]] []
-> merge_stack [[1;2;3;6];;[5]]
= [1;2;3;5;6]
>>
The complexity of the algorithm is n*log n, since there are
2^(p-1) mergings to do of length 2, 2^(p-2) of length 4, ..., 2^0
of length 2^p for a list of length 2^p. The algorithm does not need
explicitly cutting the list in 2 parts at each step since it the
successive accumulation of fragments on the stack which ensures
that lists are merged on a dichotomic basis.
*)
Fixpoint merge_list_to_stack stack l :=
match stack with
| [] => [Some l]
| None :: stack' => Some l :: stack'
| Some l' :: stack' => None :: merge_list_to_stack stack' (merge l' l)
end.
Fixpoint merge_stack stack :=
match stack with
| [] => []
| None :: stack' => merge_stack stack'
| Some l :: stack' => merge l (merge_stack stack')
end.
Fixpoint iter_merge stack l :=
match l with
| [] => merge_stack stack
| a::l' => iter_merge (merge_list_to_stack stack [a]) l'
end.
Definition sort := iter_merge [].
(** The proof of correctness *)
Local Notation Sorted := (LocallySorted leb) (only parsing).
Fixpoint SortedStack stack :=
match stack with
| [] => True
| None :: stack' => SortedStack stack'
| Some l :: stack' => Sorted l /\ SortedStack stack'
end.
Local Ltac invert H := inversion H; subst; clear H.
Fixpoint flatten_stack (stack : list (option (list t))) :=
match stack with
| [] => []
| None :: stack' => flatten_stack stack'
| Some l :: stack' => l ++ flatten_stack stack'
end.
Theorem Sorted_merge : forall l1 l2,
Sorted l1 -> Sorted l2 -> Sorted (merge l1 l2).
Proof.
induction l1; induction l2; intros; simpl; auto.
destruct (a <=? a0) eqn:Heq1.
invert H.
simpl. constructor; trivial; rewrite Heq1; constructor.
assert (Sorted (merge (b::l) (a0::l2))) by (apply IHl1; auto).
clear H0 H3 IHl1; simpl in *.
destruct (b <=? a0); constructor; auto || rewrite Heq1; constructor.
assert (a0 <=? a) by
(destruct (leb_total a0 a) as [H'|H']; trivial || (rewrite Heq1 in H'; inversion H')).
invert H0.
constructor; trivial.
assert (Sorted (merge (a::l1) (b::l))) by auto using IHl1.
clear IHl2; simpl in *.
destruct (a <=? b); constructor; auto.
Qed.
Theorem Permuted_merge : forall l1 l2, Permutation (l1++l2) (merge l1 l2).
Proof.
induction l1; simpl merge; intro.
assert (forall l, (fix merge_aux (l0 : list t) : list t := l0) l = l)
as -> by (destruct l; trivial). (* Technical lemma *)
apply Permutation_refl.
induction l2.
rewrite app_nil_r. apply Permutation_refl.
destruct (a <=? a0).
constructor; apply IHl1.
apply Permutation_sym, Permutation_cons_app, Permutation_sym, IHl2.
Qed.
Theorem Sorted_merge_list_to_stack : forall stack l,
SortedStack stack -> Sorted l -> SortedStack (merge_list_to_stack stack l).
Proof.
induction stack as [|[|]]; intros; simpl.
auto.
apply IHstack. destruct H as (_,H1). fold SortedStack in H1. auto.
apply Sorted_merge; auto; destruct H; auto.
auto.
Qed.
Theorem Permuted_merge_list_to_stack : forall stack l,
Permutation (l ++ flatten_stack stack) (flatten_stack (merge_list_to_stack stack l)).
Proof.
induction stack as [|[]]; simpl; intros.
reflexivity.
rewrite app_assoc.
etransitivity.
apply Permutation_app_tail.
etransitivity.
apply Permutation_app_comm.
apply Permuted_merge.
apply IHstack.
reflexivity.
Qed.
Theorem Sorted_merge_stack : forall stack,
SortedStack stack -> Sorted (merge_stack stack).
Proof.
induction stack as [|[|]]; simpl; intros.
constructor; auto.
apply Sorted_merge; tauto.
auto.
Qed.
Theorem Permuted_merge_stack : forall stack,
Permutation (flatten_stack stack) (merge_stack stack).
Proof.
induction stack as [|[]]; simpl.
trivial.
transitivity (l ++ merge_stack stack).
apply Permutation_app_head; trivial.
apply Permuted_merge.
assumption.
Qed.
Theorem Sorted_iter_merge : forall stack l,
SortedStack stack -> Sorted (iter_merge stack l).
Proof.
intros stack l H; induction l in stack, H |- *; simpl.
auto using Sorted_merge_stack.
assert (Sorted [a]) by constructor.
auto using Sorted_merge_list_to_stack.
Qed.
Theorem Permuted_iter_merge : forall l stack,
Permutation (flatten_stack stack ++ l) (iter_merge stack l).
Proof.
induction l; simpl; intros.
rewrite app_nil_r. apply Permuted_merge_stack.
change (a::l) with ([a]++l).
rewrite app_assoc.
etransitivity.
apply Permutation_app_tail.
etransitivity.
apply Permutation_app_comm.
apply Permuted_merge_list_to_stack.
apply IHl.
Qed.
Theorem Sorted_sort : forall l, Sorted (sort l).
Proof.
intro; apply Sorted_iter_merge. constructor.
Qed.
Corollary LocallySorted_sort : forall l, Sorted.Sorted leb (sort l).
Proof. intro; eapply Sorted_LocallySorted_iff, Sorted_sort; auto. Qed.
Theorem Permuted_sort : forall l, Permutation l (sort l).
Proof.
intro; apply (Permuted_iter_merge l []).
Qed.
Corollary StronglySorted_sort : forall l,
Transitive leb -> StronglySorted leb (sort l).
Proof. auto using Sorted_StronglySorted, LocallySorted_sort. Qed.
End Sort.
(** An example *)
Module NatOrder <: TotalLeBool.
Definition t := nat.
Fixpoint leb x y :=
match x, y with
| 0, _ => true
| _, 0 => false
| S x', S y' => leb x' y'
end.
Infix "<=?" := leb (at level 35).
Theorem leb_total : forall a1 a2, a1 <=? a2 \/ a2 <=? a1.
Proof.
induction a1; destruct a2; simpl; auto.
Qed.
End NatOrder.
Module Import NatSort := Sort NatOrder.
Example SimpleMergeExample := Eval compute in sort [5;3;6;1;8;6;0].
|
