Library examples.vector.MergesortList
A modular implementation of mergesort (the complexity is O(n.log n) in
the length of the list)
Require Import Relations Relations_1 List.
Set Implicit Arguments.
Notations and conventions
Notation "[ ]" := nil (at level 0).
Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) (at level 0).
Forall
Inductive Forall {A} (P:A->Prop) : list A -> Prop :=
| Forall_nil : Forall P nil
| Forall_cons : forall x l, P x -> Forall P l -> Forall P (x::l).
Hint Constructors Forall.
Lemma Forall_impl : forall A (P Q : A -> Prop), (forall a, P a -> Q a) ->
forall l, Forall P l -> Forall Q l.
Proof.
intros A P Q Himp l H.
induction H; firstorder.
Qed.
Preambule
Implicit Arguments Transitive [U].
Section defs.
Variable A : Type.
Variable R : A -> A -> Prop.
Locally sorted: consecutive elements of the list are ordered
Inductive LocallySorted : list A -> Prop :=
| LSorted_nil : LocallySorted []
| LSorted_cons1 a : LocallySorted [a]
| LSorted_consn a b l :
LocallySorted (b :: l) -> R a b -> LocallySorted (a :: b :: l).
Alternative two-step definition of being locally sorted
Inductive HdRel a : list A -> Prop :=
| HdRel_nil : HdRel a []
| HdRel_cons b l : R a b -> HdRel a (b :: l).
Inductive Sorted : list A -> Prop :=
| Sorted_nil : Sorted []
| Sorted_cons a l : Sorted l -> HdRel a l -> Sorted (a :: l).
Lemma HdRel_inv : forall a b l, HdRel a (b :: l) -> R a b.
Proof.
inversion 1; auto.
Qed.
Lemma Sorted_inv :
forall a l, Sorted (a :: l) -> Sorted l /\ HdRel a l.
Proof.
intros a l H; inversion H; auto.
Qed.
Lemma Sorted_rect :
forall P:list A -> Type,
P [] ->
(forall a l, Sorted l -> P l -> HdRel a l -> P (a :: l)) ->
forall l:list A, Sorted l -> P l.
Proof.
induction l; firstorder using Sorted_inv.
Qed.
Lemma Sorted_LocallySorted_iff : forall l, Sorted l <-> LocallySorted l.
Proof.
split; [induction 1 as [|a l [|]]| induction 1].
apply LSorted_nil. apply LSorted_cons1. apply LSorted_consn; auto. eapply HdRel_inv; apply H1.
apply Sorted_nil. apply Sorted_cons; [apply Sorted_nil | apply HdRel_nil]. apply Sorted_cons; [ auto | apply HdRel_cons ; auto ].
Qed.
Strongly sorted: elements of the list are pairwise ordered
Inductive StronglySorted : list A -> Prop :=
| SSorted_nil : StronglySorted []
| SSorted_cons a l : StronglySorted l -> Forall (R a) l -> StronglySorted (a :: l).
Lemma StronglySorted_inv : forall a l, StronglySorted (a :: l) ->
StronglySorted l /\ Forall (R a) l.
Proof.
intros; inversion H; auto.
Defined.
Lemma StronglySorted_rect :
forall P:list A -> Type,
P [] ->
(forall a l, StronglySorted l -> P l -> Forall (R a) l -> P (a :: l)) ->
forall l, StronglySorted l -> P l.
Proof.
induction l; firstorder using StronglySorted_inv.
Defined.
Lemma StronglySorted_rec :
forall P:list A -> Type,
P [] ->
(forall a l, StronglySorted l -> P l -> Forall (R a) l -> P (a :: l)) ->
forall l, StronglySorted l -> P l.
Proof.
firstorder using StronglySorted_rect.
Qed.
Lemma StronglySorted_Sorted : forall l, StronglySorted l -> Sorted l.
Proof.
induction 1 as [|? ? ? ? HForall]; constructor; trivial.
destruct HForall; constructor; trivial.
Qed.
Lemma Sorted_extends :
Transitive R -> forall a l, Sorted (a::l) -> Forall (R a) l.
Proof.
intros. change match a :: l with [] => True | a :: l => Forall (R a) l end.
induction H0 as [|? ? ? ? H1]; [trivial|].
destruct H1; constructor; trivial.
eapply Forall_impl; [|eassumption].
firstorder.
Qed.
Lemma Sorted_StronglySorted :
Transitive R -> forall l, Sorted l -> StronglySorted l.
Proof.
induction 2; constructor; trivial.
apply Sorted_extends; trivial.
constructor; trivial.
Qed.
End defs.
Hint Constructors HdRel: sorting.
Hint Constructors Sorted: sorting.
Open Scope bool_scope.
Local Coercion eq_true : bool >-> Sortclass.
A total relation
Module Type TotalOrder.
Parameter A : Type.
Parameter le_bool : A -> A -> bool.
Infix "<=?" := le_bool (at level 35).
Axiom le_bool_total : forall a1 a2, a1 <=? a2 \/ a2 <=? a1.
End TotalOrder.
The main module defining mergesort on a given total order.
We require minimal hypotheses
Module Sort (Import X:TotalOrder).
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
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 SortedB := (LocallySorted le_bool) (only parsing).
Fixpoint SortedStack stack :=
match stack with
| [] => True
| None :: stack' => SortedStack stack'
| Some l :: stack' => SortedB l /\ SortedStack stack'
end.
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.
Theorem Sorted_merge : forall l1 l2,
SortedB l1 -> SortedB l2 -> SortedB (merge l1 l2).
Proof.
induction l1; induction l2; intros; simpl; auto.
destruct (a <=? a0) as ()_eqn:Heq1.
invert H.
simpl. constructor; trivial; rewrite Heq1; constructor.
assert (SortedB (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 (le_bool_total a0 a) as [H'|H']; trivial || (rewrite Heq1 in H'; inversion H')).
invert H0.
constructor; trivial.
assert (SortedB (merge (a::l1) (b::l))) by auto using IHl1.
clear IHl2; simpl in *.
destruct (a <=? b) as ()_eqn:Heq2;
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 A) : list A := l0) l = l)
as -> by (destruct l; trivial). apply Permutation_refl.
induction l2.
rewrite <- app_nil_end. 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 -> SortedB 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.
apply Permutation_refl. rewrite ass_app.
eapply Permutation_trans. apply Permutation_app_tail.
eapply Permutation_trans. apply Permutation_app_swap.
apply Permuted_merge.
apply IHstack.
apply Permutation_refl. Qed.
Theorem Sorted_merge_stack : forall stack,
SortedStack stack -> SortedB (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.
apply Permutation_refl.
apply Permutation_trans with (l ++ merge_stack stack).
apply Permutation_app_head; trivial.
apply Permuted_merge.
assumption.
Qed.
Theorem Sorted_iter_merge : forall stack l,
SortedStack stack -> SortedB (iter_merge stack l).
Proof.
intros stack l H; induction l in stack, H |- *; simpl.
auto using Sorted_merge_stack.
assert (SortedB [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_end. apply Permuted_merge_stack.
change (a::l) with ([a]++l).
rewrite ass_app.
eapply Permutation_trans.
apply Permutation_app_tail.
eapply Permutation_trans.
apply Permutation_app_swap.
apply Permuted_merge_list_to_stack.
apply IHl.
Qed.
Theorem Sorted_sort : forall l, SortedB (sort l).
Proof.
intro; apply Sorted_iter_merge. constructor.
Qed.
Corollary LocallySorted_sort : forall l, Sorted le_bool (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 le_bool -> StronglySorted le_bool (sort l).
Proof. auto using Sorted_StronglySorted, LocallySorted_sort. Qed.
End Sort.
An example
Module NatOrder.
Definition A := nat.
Fixpoint le_bool x y :=
match x, y with
| 0, _ => true
| S x', 0 => false
| S x', S y' => le_bool x' y'
end.
Infix "<=?" := le_bool (at level 35).
Theorem le_bool_total : forall a1 a2, a1 <=? a2 \/ a2 <=? a1.
Proof.
induction a1; destruct a2; simpl; auto using is_eq_true.
Qed.
End NatOrder.
Module Import NatSort := Sort NatOrder.
Example SimpleMergeExample := Eval compute in sort [5;3;6;1;8;6;0].
Print SimpleMergeExample.