Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Mergesort.v Sprache: Coq

Original von: Coq^©

(************************************************************************)
(*         *   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].

¤ Dauer der Verarbeitung: 0.5 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.