Library examples.vector.MergesortVector

Require Import Relations Relations_1 Vector Heq.

Set Implicit Arguments.

Notations and conventions

Notation "[ ]" := vnil (at level 0).
Notation "[ a ; .. ; b ]" := (a ::: .. (b ::: []) ..) (at level 0).

Forall

Inductive Forall {A} (P:A->Prop) : forall n, vector A n -> Prop :=
| Forall_nil : Forall P vnil
| Forall_cons : forall x n (l:vector A n), 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 n (l:vector A n), Forall P l -> Forall Q l.
Proof.
  intros A P Q Himp n l H.
  induction H; constructor; firstorder.
Qed.

Preambule

Implicit Arguments Transitive [U].

Open Scope vector_scope.

Section defs.

Variable A : Type.
Variable R : A -> A -> Prop.

Locally sorted: consecutive elements of the list are ordered

  Inductive LocallySorted : forall n, vector A n -> Prop :=
    | LSorted_nil : LocallySorted vnil
    | LSorted_cons1 a : LocallySorted (a ::: vnil)
    | LSorted_consn a b n (l: vector A n) :
        LocallySorted (b ::: l) -> R a b -> LocallySorted (a ::: b ::: l).

Alternative two-step definition of being locally sorted

  Inductive HdRel a : forall n, vector A n -> Prop :=
    | HdRel_nil : HdRel a vnil
    | HdRel_cons b n (l: vector A n) : R a b -> HdRel a (b ::: l).

  Inductive Sorted : forall n, vector A n -> Prop :=
    | Sorted_nil : Sorted vnil
    | Sorted_cons a n (l: vector A n) : Sorted l -> HdRel a l -> Sorted (a ::: l).

  Lemma HdRel_inv : forall a b n (l: vector A n), HdRel a (b ::: l) -> R a b.
  Proof.
    inversion 1; auto.
  Qed.

  Lemma Sorted_inv :
    forall a n (l: vector A n), Sorted (a ::: l) -> Sorted l /\ HdRel a l.
  Proof.
    intros a n l H. inversion H. Hsubst. auto.
  Qed.

  Lemma Sorted_rect :
    forall P: forall n, vector A n -> Type,
      P _ vnil ->
      (forall a n (l:vector A n), Sorted l -> P _ l -> HdRel a l -> P _ (a ::: l)) ->
      forall n (l:vector A n), Sorted l -> P _ l.
  Proof.
    induction l; firstorder using Sorted_inv.
  Qed.

  Lemma Sorted_LocallySorted_iff : forall n (l:vector A n), Sorted l <-> LocallySorted l.
  Proof.
    split; [induction 1 as [|a l [|]] | induction 1 ].
    constructor. constructor. constructor; [ auto | eapply HdRel_inv; apply H0 ].
    constructor. constructor; constructor. constructor; [ auto | apply HdRel_cons ; auto ].
  Qed.

Strongly sorted: elements of the list are pairwise ordered

  Inductive StronglySorted : forall n, vector A n -> Prop :=
    | SSorted_nil : StronglySorted vnil
    | SSorted_cons a n (l:vector A n) : StronglySorted l -> Forall (R a) l -> StronglySorted (a ::: l).

  Lemma StronglySorted_inv : forall a n (l:vector A n), StronglySorted (a ::: l) ->
    StronglySorted l /\ Forall (R a) l.
  Proof.
    intros. inversion H. Hsubst. auto.
  Defined.

  Lemma StronglySorted_rect :
    forall P:forall n, vector A n -> Type,
      P _ vnil ->
      (forall a n (l:vector A n), StronglySorted l -> P _ l -> Forall (R a) l -> P _ (a ::: l)) ->
      forall n (l:vector A n), StronglySorted l -> P _ l.
  Proof.
    induction l. auto. firstorder using StronglySorted_inv.
  Defined.

  Lemma StronglySorted_rec :
    forall P: forall n, vector A n -> Type,
      P _ vnil ->
      (forall a n (l:vector A n), StronglySorted l -> P _ l -> Forall (R a) l -> P _ (a ::: l)) ->
      forall n (l:vector A n), StronglySorted l -> P _ l.
  Proof.
    firstorder using StronglySorted_rect.
  Defined.

  Lemma StronglySorted_Sorted : forall n (l:vector A n), StronglySorted l -> Sorted l.
  Proof.
    induction 1; constructor; trivial.
    destruct H0; constructor; trivial.
  Qed.

  Lemma Sorted_extends :
    Transitive R -> forall a n (l:vector A n), Sorted (a:::l) -> Forall (R a) l.
  Proof.
    intro. assert (forall n (l:vector A n), Sorted l -> match l with vnil => True | vcons a _ l => Forall (R a) l end).
    induction l; auto; intros.
    destruct l; constructor; trivial; apply Sorted_inv in H0; destruct H0; inversion H1; Hsubst; auto.
    apply Forall_impl with (R a0); firstorder.
    intros. apply (H0 _ (a:::l)); auto.
  Qed.

  Lemma Sorted_StronglySorted :
    Transitive R -> forall n (l:vector A n), 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 n1 (l1 : vector A n1) n2 (l2: vector A n2) : vector A (n1 + n2) :=
  match
    l1 in (vector _ n1) return (forall n2, vector A n2 -> vector A (n1 + n2))
  with
  | vnil => fun _ l2 => l2
  | vcons a1 _ l1' => fun _ l2 =>
      let fix merge_aux n2 (l2 : vector A n2) :=
        match
          l2 in (vector _ n2) return (vector A (_ + n2))
        with
        | vnil => << Svec # plus_n_O _ >> a1 ::: l1'
        | vcons a2 _ l2' =>
            if a1 <=? a2
            then a1 ::: (merge l1' (a2 ::: l2'))
            else << Svec # f_equal S (plus_Snm_nSm _ _) >> a2 ::: (merge_aux _ l2')
        end
      in merge_aux _ l2
  end n2 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.

Inductive Stack : nat -> Type :=
  | Snil : Stack 0
  | SconsNone m (s: Stack m) : Stack m
  | SconsSome m (s: Stack m) n (l: vector A n) : Stack (m+n)
.

Definition Sstk (n:nat) : Type := Stack n.
Notation Pstk := (_) (only parsing).

Fixpoint merge_list_to_stack m (stack: Stack m) n (l: vector A n) : Stack (m+n) :=
  match stack in Stack m return Stack (m+n) with
  | Snil => SconsSome Snil l
  | SconsNone _ stack' => SconsSome stack' l
  | SconsSome _ stack' _ l' => << Sstk # plus_assoc _ _ _ >> merge_list_to_stack stack' (merge l' l)
  end.

Fixpoint merge_stack m (stack: Stack m) : vector A m :=
  match stack in Stack m return vector A m with
  | Snil => vnil
  | SconsNone _ stack' => merge_stack stack'
  | SconsSome _ stack' _ l => << Svec # plus_comm _ _ >> merge l (merge_stack stack')
  end.

Fixpoint iter_merge m (stack : Stack m) n (l: vector A n) : vector A (m+n) :=
  match l in vector _ n return vector A (m+n) with
  | vnil => << Svec # plus_n_O _ >> merge_stack stack
  | vcons a _ l' => << Svec # sym_eq (plus_assoc _ _ _) >> iter_merge (merge_list_to_stack stack (a:::vnil)) l'
  end.

Definition sort n (l:vector A n) : vector A n := iter_merge Snil l.

The proof of correctness

Local Notation SortedB := (LocallySorted le_bool) (only parsing).

Fixpoint SortedStack m (stack: Stack m) :=
  match stack with
  | Snil => True
  | SconsNone _ stack' => SortedStack stack'
  | SconsSome _ stack' _ l => SortedB _ l /\ SortedStack stack'
  end.

Ltac invert H := inversion H; clear H.

Fixpoint flatten_stack m (stack : Stack m) : vector A m :=
  match stack in Stack m return vector A m with
  | Snil => vnil
  | SconsNone _ stack' => flatten_stack stack'
  | SconsSome _ stack' _ l => << Svec # plus_comm _ _ >> (l +++ (flatten_stack stack'))
  end.

Theorem Sorted_merge : forall n1 (l1:vector A n1) n2 (l2:vector A n2),
  SortedB _ l1 -> SortedB _ l2 -> SortedB _ (merge l1 l2).
Proof.
induction l1; induction l2; intros; simpl; auto.
  Hsimplc. auto.
  destruct (a <=? a0) as ()_eqn:Heq1.
      invert H; Hsubst.
      simpl. constructor; trivial; rewrite Heq1; constructor.
      assert (SortedB _ (merge (b:::l) (a0:::l2))) by (apply IHl1; auto).
      simpl in *. destruct (b <=? a0).
        constructor; auto. revert H. Hsimplc. intro. 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; Hsubst.
      simpl. Hsimplc. Helimc. constructor; trivial.
      assert (SortedB _ (merge (a:::l1) (b:::l))) by (apply IHl2; auto).
      simpl in *. destruct (a <=? b) as ()_eqn:Heq2.
        Hsimplc. constructor; auto.
        revert H0. Hsimplc. Helimc. intro. constructor; auto.
Qed.

Theorem Permuted_merge : forall n1 (l1:vector A n1) n2 (l2:vector A n2), VPermutation (l1+++l2) (merge l1 l2).
Proof.
  induction l1; simpl merge; intro.
    assert (forall n (l:vector A n), (fix merge_aux n0 (l0 : vector A n0) : vector A n0 := l0) _ l = l)
    by (destruct l; trivial).     apply VPermutation_refl.
  induction l2.
    simpl. Hsimpl. Hrewritec <- (vapp_nil_end l1). apply VPermutation_refl.
    destruct (a <=? a0).
      constructor; apply IHl1.
      simpl. Hsimplc. apply VPermutation_sym, (VPermutation_cons_app (a:::l1)), VPermutation_sym, IHl2.
Qed.

Theorem Sorted_merge_list_to_stack : forall m (stack:Stack m) n (l:vector A n),
  SortedStack stack -> SortedB _ l -> SortedStack (merge_list_to_stack stack l).
Proof.
  induction stack; intros; simpl; auto.
    Hsimplc. apply IHstack. destruct H; auto.
      apply Sorted_merge; auto; destruct H; auto.
Qed.

Theorem Permuted_merge_list_to_stack : forall m (stack: Stack m) n (l:vector A n),
  VPermutation (l +++ (flatten_stack stack)) (flatten_stack (merge_list_to_stack stack l)).
Proof.
  induction stack; simpl; intros.
    Hsimplc. apply VPermutation_refl.
    Hsimplc. apply VPermutation_refl.
    Hsimplc. Helimc. rewrite (Hrw (vass_app _ _ _)); Hsimplc.
    eapply VPermutation_trans.
      apply VPermutation_app_tail.
      eapply VPermutation_trans.
        apply VPermutation_app_swap.
      apply Permuted_merge.
    apply IHstack.
Qed.

Theorem Sorted_merge_stack : forall m (stack:Stack m),
  SortedStack stack -> SortedB _ (merge_stack stack).
Proof.
induction stack; simpl; intros.
  constructor; auto.
  auto.
  Hsimplc. apply Sorted_merge; tauto.
Qed.

Theorem Permuted_merge_stack : forall m (stack:Stack m),
  VPermutation (flatten_stack stack) (merge_stack stack).
Proof.
induction stack; simpl.
  apply VPermutation_refl.
  assumption.
  Hsimplc. apply VPermutation_trans with _ (l +++ (merge_stack stack)).
    apply VPermutation_app_head; trivial.
    apply Permuted_merge.
Qed.

Theorem Sorted_iter_merge : forall m (stack:Stack m) n (l:vector A n),
  SortedStack stack -> SortedB _ (iter_merge stack l).
Proof.
  intros m stack n l H; induction l in m, stack, H |- *; simpl.
    Hsimplc. auto using Sorted_merge_stack.
    Hsimplc. assert (SortedB _ (a:::vnil)) by constructor.
    auto using Sorted_merge_list_to_stack.
Qed.

Theorem Permuted_iter_merge : forall n (l:vector A n) m (stack: Stack m),
  VPermutation ((flatten_stack stack) +++ l) (iter_merge stack l).
Proof.
  induction l; simpl; intros.
    rewrite (Hrw (sym_Heq (vapp_nil_end _))); Hsimplc. apply Permuted_merge_stack.
    change (a:::l) with (a ::: vnil +++ l).
    rewrite (Hrw (vass_app _ (a:::vnil) l)). simpl. Hsimplc.
    eapply VPermutation_trans.
      apply VPermutation_app_tail.
    eapply VPermutation_trans.
    apply VPermutation_app_swap.
    apply Permuted_merge_list_to_stack.
    apply IHl.
Qed.

Theorem Sorted_sort : forall n (l:vector A n), SortedB _ (sort l).
Proof.
intros. apply (Sorted_iter_merge Snil). constructor.
Qed.

Corollary LocallySorted_sort : forall n (l:vector A n), Sorted le_bool (sort l).
Proof. intros; eapply Sorted_LocallySorted_iff, Sorted_sort; auto. Qed.

Theorem Permuted_sort : forall n (l:vector A n), VPermutation l (sort l).
Proof.
intros. apply (Permuted_iter_merge l Snil).
Qed.

Corollary StronglySorted_sort : forall n (l:vector A n),
  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:::vnil).

Print SimpleMergeExample.