A modular implementation of mergesort (the complexity is O(n.log n) in
the length of the list)
Notations and conventions
Local Notation "[ ]" := nil.
Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..).
Open Scope bool_scope.
Section MSort.
Variable A : Type.
Variable cmp : A → A → bool.
Fixpoint merge l1 l2 :=
let fix merge_aux l2 :=
match l1, l2 with
| [], _ ⇒ l2
| _, [] ⇒ l1
| a1::l1', a2::l2' ⇒
if cmp 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 cmp) (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 A))) :=
match stack with
| [] ⇒ []
| None :: stack' ⇒ flatten_stack stack'
| Some l :: stack' ⇒ l ++ flatten_stack stack'
end.
Existing Instance Permutation_app'.
Local Add Parametric Morphism (a: A) : (In a)
with signature @Permutation A ==> iff
as in_mor.
Proof. split; eapply Permutation_in; eauto using Permutation_sym. Qed.
Lemma Permutation_merge : ∀ l1 l2, Permutation (merge l1 l2) (l1++l2).
Proof.
induction l1; [by destruct l2; ins|].
induction l2; rewrite ?app_nil_r; simpl merge; try done; desf; vauto.
rewrite <- Permutation_middle; eauto.
Qed.
Lemma Permutation_merge_list_to_stack : ∀ stack l,
Permutation (flatten_stack (merge_list_to_stack stack l)) (l ++ flatten_stack stack).
Proof.
induction stack; ins; desf; ins; rewrite app_assoc.
by rewrite IHstack, Permutation_merge, (Permutation_app_comm l).
Qed.
Lemma Permutation_merge_stack : ∀ stack,
Permutation (merge_stack stack) (flatten_stack stack).
Proof.
by induction stack; ins; desf; rewrite Permutation_merge, IHstack.
Qed.
Lemma Permutation_iter_merge : ∀ l stack,
Permutation (iter_merge stack l) (flatten_stack stack ++ l).
Proof.
induction l; ins; rewrite ?app_nil_r, ?Permutation_merge_stack; ins.
by rewrite IHl, Permutation_merge_list_to_stack, <- Permutation_middle.
Qed.
Theorem sort_perm l : Permutation (sort l) l.
Proof. exact (Permutation_iter_merge l []). Qed.
Lemma Sorted_merge :
∀ l1 l2
(TOTAL: ∀ x y, In x l1 ∨ In x l2 → In y l1 ∨ In y l2 →
cmp x y = true ∨ cmp y x = true)
(S1 : Sorted l1)
(S2 : Sorted l2),
Sorted (merge l1 l2).
Proof.
induction l1; induction l2; ins; desf.
inv S1; vauto.
assert (Sorted (merge (b::l) (a0::l2))).
by apply IHl1; ins; eapply TOTAL; tauto.
by clear S1 S2 IHl1; simpls; desf; vauto.
assert (cmp a0 a).
by destruct (TOTAL a0 a); eauto; congruence.
inv S2; vauto.
assert (Sorted (merge (a::l1) (b::l))).
by apply IHl2; ins; eapply TOTAL; tauto.
clear IHl2; ins; desf; vauto.
Qed.
Lemma Sorted_merge_list_to_stack : ∀ stack l
(TOTAL: ∀ x y, In x (flatten_stack stack) ∨ In x l →
In y (flatten_stack stack) ∨ In y l →
cmp x y = true ∨ cmp y x = true),
SortedStack stack → Sorted l → SortedStack (merge_list_to_stack stack l).
Proof.
induction stack; ins; desf; ins; desf.
apply IHstack, Sorted_merge; ins; try rewrite Permutation_merge, in_app_iff in *;
eapply TOTAL; desf; eauto using in_or_app.
Qed.
Lemma Sorted_merge_stack : ∀ stack
(TOTAL: ∀ x y, In x (flatten_stack stack) →
In y (flatten_stack stack) →
cmp x y = true ∨ cmp y x = true),
SortedStack stack → Sorted (merge_stack stack).
Proof.
induction stack; ins; desf; desf; vauto.
apply Sorted_merge, IHstack; ins; eauto using in_or_app.
by rewrite Permutation_merge_stack in *; eauto using in_or_app.
by eapply TOTAL; auto using in_or_app.
by eapply IHstack; eauto; eapply TOTAL; auto using in_or_app.
Qed.
Lemma Sorted_iter_merge : ∀ stack l
(TOTAL: ∀ x y, In x (flatten_stack stack) ∨ In x l →
In y (flatten_stack stack) ∨ In y l →
cmp x y = true ∨ cmp y x = true),
SortedStack stack → Sorted (iter_merge stack l).
Proof.
intros until l; revert stack; induction l; ins.
by eapply Sorted_merge_stack; eauto.
eapply IHl, Sorted_merge_list_to_stack; ins; vauto.
rewrite Permutation_merge_list_to_stack in *; ins.
by eapply TOTAL; desf; eauto.
by eapply TOTAL; desf; eauto.
Qed.
Lemma Sorted_sort : ∀ l
(TOTAL: ∀ x y, In x l → In y l → cmp x y = true ∨ cmp y x = true),
Sorted (sort l).
Proof.
ins; apply Sorted_iter_merge; ins; desf; eauto.
Qed.
Theorem sort_sorted : ∀ (l: list A)
(TOTAL: ∀ x y, In x l → In y l → cmp x y = true ∨ cmp y x = true)
(TRANS: transitive _ cmp),
StronglySorted cmp (sort l).
Proof.
ins; eapply Sorted_StronglySorted, Sorted_LocallySorted_iff, Sorted_sort; ins.
Qed.
End MSort.
This page has been generated by coqdoc