Mergesort.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

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

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: ∀ 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

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.

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).forall l1 l2 : list t,
LocallySorted (fun x x0 : t => x <=? x0) l1 ->
LocallySorted (fun x x0 : t => x <=? x0) l2 ->
LocallySorted (fun x x0 : t => x <=? x0) (merge l1 l2)
Proof.forall l1 l2 : list t,
LocallySorted (fun x x0 : t => x <=? x0) l1 ->
LocallySorted (fun x x0 : t => x <=? x0) l2 ->
LocallySorted (fun x x0 : t => x <=? x0) (merge l1 l2)
induction l1; induction l2; intros; simpl; auto.a:t
l1:list t
IHl1:forall l0 : list t,
LocallySorted (fun x x0 : t => x <=? x0) l1 ->
LocallySorted (fun x x0 : t => x <=? x0) l0 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge l1 l0)
a0:t
l2:list t
IHl2:LocallySorted (fun x x0 : t => x <=? x0)
  (a :: l1) ->
LocallySorted (fun x x0 : t => x <=? x0) l2 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge (a :: l1) l2)
H:LocallySorted (fun x x0 : t => x <=? x0) (a :: l1)
H0:LocallySorted (fun x x0 : t => x <=? x0)
  (a0 :: l2)
LocallySorted (fun x x0 : t => x <=? x0)
  (if a <=? a0
   then a :: merge l1 (a0 :: l2)
   else
    a0
    :: (fix merge_aux (l0 : list t) : list t :=
          match l0 with
          | [ ] => a :: l1
          | a2 :: l2' =>
              if a <=? a2
              then a :: merge l1 l0
              else a2 :: merge_aux l2'
          end) l2)
  destruct (a <=? a0) eqn:Heq1.a:t
l1:list t
IHl1:forall l0 : list t,
LocallySorted (fun x x0 : t => x <=? x0) l1 ->
LocallySorted (fun x x0 : t => x <=? x0) l0 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge l1 l0)
a0:t
l2:list t
IHl2:LocallySorted (fun x x0 : t => x <=? x0)
  (a :: l1) ->
LocallySorted (fun x x0 : t => x <=? x0) l2 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge (a :: l1) l2)
H:LocallySorted (fun x x0 : t => x <=? x0) (a :: l1)
H0:LocallySorted (fun x x0 : t => x <=? x0)
  (a0 :: l2)
Heq1:a <=? a0 = true
LocallySorted (fun x x0 : t => x <=? x0)
  (a :: merge l1 (a0 :: l2))
a:t
l1:list t
IHl1:forall l0 : list t,
LocallySorted (fun x x0 : t => x <=? x0) l1 ->
LocallySorted (fun x x0 : t => x <=? x0) l0 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge l1 l0)
a0:t
l2:list t
IHl2:LocallySorted (fun x x0 : t => x <=? x0)
  (a :: l1) ->
LocallySorted (fun x x0 : t => x <=? x0) l2 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge (a :: l1) l2)
H:LocallySorted (fun x x0 : t => x <=? x0) (a :: l1)
H0:LocallySorted (fun x x0 : t => x <=? x0)
  (a0 :: l2)
Heq1:a <=? a0 = false
LocallySorted (fun x x0 : t => x <=? x0)
  (a0
   :: (fix merge_aux (l0 : list t) : 
       list t :=
         match l0 with
         | [ ] => a :: l1
         | a2 :: l2' =>
             if a <=? a2
             then a :: merge l1 l0
             else a2 :: merge_aux l2'
         end) l2)
    invert H.a:t
IHl1:forall l0 : list t,
LocallySorted (fun x x0 : t => x <=? x0) [ ] ->
LocallySorted (fun x x0 : t => x <=? x0) l0 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge [ ] l0)
a0:t
l2:list t
IHl2:LocallySorted (fun x x0 : t => x <=? x0) [a] ->
LocallySorted (fun x x0 : t => x <=? x0) l2 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge [a] l2)
H0:LocallySorted (fun x x0 : t => x <=? x0)
  (a0 :: l2)
Heq1:a <=? a0 = true
LocallySorted (fun x x0 : t => x <=? x0)
  (a :: merge [ ] (a0 :: l2))
a, b:t
l:list t
IHl1:forall l0 : list t,
LocallySorted (fun x x0 : t => x <=? x0)
  (b :: l) ->
LocallySorted (fun x x0 : t => x <=? x0) l0 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge (b :: l) l0)
a0:t
l2:list t
IHl2:LocallySorted (fun x x0 : t => x <=? x0)
  (a :: b :: l) ->
LocallySorted (fun x x0 : t => x <=? x0) l2 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge (a :: b :: l) l2)
H0:LocallySorted (fun x x0 : t => x <=? x0)
  (a0 :: l2)
Heq1:a <=? a0 = true
H3:LocallySorted (fun x x0 : t => x <=? x0) (b :: l)
H4:is_true (a <=? b)
LocallySorted (fun x x0 : t => x <=? x0)
  (a :: merge (b :: l) (a0 :: l2))
a:t
l1:list t
IHl1:forall l0 : list t,
LocallySorted (fun x x0 : t => x <=? x0) l1 ->
LocallySorted (fun x x0 : t => x <=? x0) l0 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge l1 l0)
a0:t
l2:list t
IHl2:LocallySorted (fun x x0 : t => x <=? x0)
  (a :: l1) ->
LocallySorted (fun x x0 : t => x <=? x0) l2 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge (a :: l1) l2)
H:LocallySorted (fun x x0 : t => x <=? x0) (a :: l1)
H0:LocallySorted (fun x x0 : t => x <=? x0)
  (a0 :: l2)
Heq1:a <=? a0 = false
LocallySorted (fun x x0 : t => x <=? x0)
  (a0
   :: (fix merge_aux (l0 : list t) : 
       list t :=
         match l0 with
         | [ ] => a :: l1
         | a2 :: l2' =>
             if a <=? a2
             then a :: merge l1 l0
             else a2 :: merge_aux l2'
         end) l2)
      simpl.a:t
IHl1:forall l0 : list t,
LocallySorted (fun x x0 : t => x <=? x0) [ ] ->
LocallySorted (fun x x0 : t => x <=? x0) l0 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge [ ] l0)
a0:t
l2:list t
IHl2:LocallySorted (fun x x0 : t => x <=? x0) [a] ->
LocallySorted (fun x x0 : t => x <=? x0) l2 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge [a] l2)
H0:LocallySorted (fun x x0 : t => x <=? x0)
  (a0 :: l2)
Heq1:a <=? a0 = true
LocallySorted (fun x x0 : t => x <=? x0)
  (a :: a0 :: l2)
a, b:t
l:list t
IHl1:forall l0 : list t,
LocallySorted (fun x x0 : t => x <=? x0)
  (b :: l) ->
LocallySorted (fun x x0 : t => x <=? x0) l0 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge (b :: l) l0)
a0:t
l2:list t
IHl2:LocallySorted (fun x x0 : t => x <=? x0)
  (a :: b :: l) ->
LocallySorted (fun x x0 : t => x <=? x0) l2 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge (a :: b :: l) l2)
H0:LocallySorted (fun x x0 : t => x <=? x0)
  (a0 :: l2)
Heq1:a <=? a0 = true
H3:LocallySorted (fun x x0 : t => x <=? x0) (b :: l)
H4:is_true (a <=? b)
LocallySorted (fun x x0 : t => x <=? x0)
  (a :: merge (b :: l) (a0 :: l2))
a:t
l1:list t
IHl1:forall l0 : list t,
LocallySorted (fun x x0 : t => x <=? x0) l1 ->
LocallySorted (fun x x0 : t => x <=? x0) l0 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge l1 l0)
a0:t
l2:list t
IHl2:LocallySorted (fun x x0 : t => x <=? x0)
  (a :: l1) ->
LocallySorted (fun x x0 : t => x <=? x0) l2 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge (a :: l1) l2)
H:LocallySorted (fun x x0 : t => x <=? x0) (a :: l1)
H0:LocallySorted (fun x x0 : t => x <=? x0)
  (a0 :: l2)
Heq1:a <=? a0 = false
LocallySorted (fun x x0 : t => x <=? x0)
  (a0
   :: (fix merge_aux (l0 : list t) : 
       list t :=
         match l0 with
         | [ ] => a :: l1
         | a2 :: l2' =>
             if a <=? a2
             then a :: merge l1 l0
             else a2 :: merge_aux l2'
         end) l2) constructor; trivial; rewrite Heq1; constructor.a, b:t
l:list t
IHl1:forall l0 : list t,
LocallySorted (fun x x0 : t => x <=? x0)
  (b :: l) ->
LocallySorted (fun x x0 : t => x <=? x0) l0 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge (b :: l) l0)
a0:t
l2:list t
IHl2:LocallySorted (fun x x0 : t => x <=? x0)
  (a :: b :: l) ->
LocallySorted (fun x x0 : t => x <=? x0) l2 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge (a :: b :: l) l2)
H0:LocallySorted (fun x x0 : t => x <=? x0)
  (a0 :: l2)
Heq1:a <=? a0 = true
H3:LocallySorted (fun x x0 : t => x <=? x0) (b :: l)
H4:is_true (a <=? b)
LocallySorted (fun x x0 : t => x <=? x0)
  (a :: merge (b :: l) (a0 :: l2))
a:t
l1:list t
IHl1:forall l0 : list t,
LocallySorted (fun x x0 : t => x <=? x0) l1 ->
LocallySorted (fun x x0 : t => x <=? x0) l0 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge l1 l0)
a0:t
l2:list t
IHl2:LocallySorted (fun x x0 : t => x <=? x0)
  (a :: l1) ->
LocallySorted (fun x x0 : t => x <=? x0) l2 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge (a :: l1) l2)
H:LocallySorted (fun x x0 : t => x <=? x0) (a :: l1)
H0:LocallySorted (fun x x0 : t => x <=? x0)
  (a0 :: l2)
Heq1:a <=? a0 = false
LocallySorted (fun x x0 : t => x <=? x0)
  (a0
   :: (fix merge_aux (l0 : list t) : 
       list t :=
         match l0 with
         | [ ] => a :: l1
         | a2 :: l2' =>
             if a <=? a2
             then a :: merge l1 l0
             else a2 :: merge_aux l2'
         end) l2)
      assert (Sorted (merge (b::l) (a0::l2))) by (apply IHl1; auto).a, b:t
l:list t
IHl1:forall l0 : list t,
LocallySorted (fun x x0 : t => x <=? x0)
  (b :: l) ->
LocallySorted (fun x x0 : t => x <=? x0) l0 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge (b :: l) l0)
a0:t
l2:list t
IHl2:LocallySorted (fun x x0 : t => x <=? x0)
  (a :: b :: l) ->
LocallySorted (fun x x0 : t => x <=? x0) l2 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge (a :: b :: l) l2)
H0:LocallySorted (fun x x0 : t => x <=? x0)
  (a0 :: l2)
Heq1:a <=? a0 = true
H3:LocallySorted (fun x x0 : t => x <=? x0) (b :: l)
H4:is_true (a <=? b)
H:LocallySorted (fun x x0 : t => x <=? x0)
  (merge (b :: l) (a0 :: l2))
LocallySorted (fun x x0 : t => x <=? x0)
  (a :: merge (b :: l) (a0 :: l2))
a:t
l1:list t
IHl1:forall l0 : list t,
LocallySorted (fun x x0 : t => x <=? x0) l1 ->
LocallySorted (fun x x0 : t => x <=? x0) l0 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge l1 l0)
a0:t
l2:list t
IHl2:LocallySorted (fun x x0 : t => x <=? x0)
  (a :: l1) ->
LocallySorted (fun x x0 : t => x <=? x0) l2 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge (a :: l1) l2)
H:LocallySorted (fun x x0 : t => x <=? x0) (a :: l1)
H0:LocallySorted (fun x x0 : t => x <=? x0)
  (a0 :: l2)
Heq1:a <=? a0 = false
LocallySorted (fun x x0 : t => x <=? x0)
  (a0
   :: (fix merge_aux (l0 : list t) : 
       list t :=
         match l0 with
         | [ ] => a :: l1
         | a2 :: l2' =>
             if a <=? a2
             then a :: merge l1 l0
             else a2 :: merge_aux l2'
         end) l2)
      clear H0 H3 IHl1; simpl in *.a, b:t
l:list t
a0:t
l2:list t
IHl2:LocallySorted (fun x x0 : t => x <=? x0)
  (a :: b :: l) ->
LocallySorted (fun x x0 : t => x <=? x0) l2 ->
LocallySorted (fun x x0 : t => x <=? x0)
  ((fix merge_aux (l0 : list t) : 
    list t :=
      match l0 with
      | [ ] => a :: b :: l
      | a2 :: l2' =>
          if a <=? a2
          then
           a
           :: (fix merge_aux0 
               (l1 : list t) : 
               list t :=
                 match l1 with
                 | [ ] => b :: l
                 | a1 :: l2'0 =>
                     if b <=? a1
                     then b :: merge l l1
                     else a1 :: merge_aux0 l2'0
                 end) l0
          else a2 :: merge_aux l2'
      end) l2)
Heq1:a <=? a0 = true
H4:is_true (a <=? b)
H:LocallySorted (fun x x0 : t => x <=? x0)
  (if b <=? a0
   then b :: merge l (a0 :: l2)
   else
    a0
    :: (fix merge_aux (l0 : list t) : 
        list t :=
          match l0 with
          | [ ] => b :: l
          | a2 :: l2' =>
              if b <=? a2
              then b :: merge l l0
              else a2 :: merge_aux l2'
          end) l2)
LocallySorted (fun x x0 : t => x <=? x0)
  (a
   :: (if b <=? a0
       then b :: merge l (a0 :: l2)
       else
        a0
        :: (fix merge_aux (l0 : list t) : list t :=
              match l0 with
              | [ ] => b :: l
              | a2 :: l2' =>
                  if b <=? a2
                  then b :: merge l l0
                  else a2 :: merge_aux l2'
              end) l2))
a:t
l1:list t
IHl1:forall l0 : list t,
LocallySorted (fun x x0 : t => x <=? x0) l1 ->
LocallySorted (fun x x0 : t => x <=? x0) l0 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge l1 l0)
a0:t
l2:list t
IHl2:LocallySorted (fun x x0 : t => x <=? x0)
  (a :: l1) ->
LocallySorted (fun x x0 : t => x <=? x0) l2 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge (a :: l1) l2)
H:LocallySorted (fun x x0 : t => x <=? x0) (a :: l1)
H0:LocallySorted (fun x x0 : t => x <=? x0)
  (a0 :: l2)
Heq1:a <=? a0 = false
LocallySorted (fun x x0 : t => x <=? x0)
  (a0
   :: (fix merge_aux (l0 : list t) : 
       list t :=
         match l0 with
         | [ ] => a :: l1
         | a2 :: l2' =>
             if a <=? a2
             then a :: merge l1 l0
             else a2 :: merge_aux l2'
         end) l2)
      destruct (b <=? a0); constructor; auto || rewrite Heq1; constructor.a:t
l1:list t
IHl1:forall l0 : list t,
LocallySorted (fun x x0 : t => x <=? x0) l1 ->
LocallySorted (fun x x0 : t => x <=? x0) l0 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge l1 l0)
a0:t
l2:list t
IHl2:LocallySorted (fun x x0 : t => x <=? x0)
  (a :: l1) ->
LocallySorted (fun x x0 : t => x <=? x0) l2 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge (a :: l1) l2)
H:LocallySorted (fun x x0 : t => x <=? x0) (a :: l1)
H0:LocallySorted (fun x x0 : t => x <=? x0)
  (a0 :: l2)
Heq1:a <=? a0 = false
LocallySorted (fun x x0 : t => x <=? x0)
  (a0
   :: (fix merge_aux (l0 : list t) : list t :=
         match l0 with
         | [ ] => a :: l1
         | a2 :: l2' =>
             if a <=? a2
             then a :: merge l1 l0
             else a2 :: merge_aux l2'
         end) l2)
    assert (a0 <=? a) by
      (destruct (leb_total a0 a) as [H'|H']; trivial || (rewrite Heq1 in H'; inversion H')).a:t
l1:list t
IHl1:forall l0 : list t,
LocallySorted (fun x x0 : t => x <=? x0) l1 ->
LocallySorted (fun x x0 : t => x <=? x0) l0 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge l1 l0)
a0:t
l2:list t
IHl2:LocallySorted (fun x x0 : t => x <=? x0)
  (a :: l1) ->
LocallySorted (fun x x0 : t => x <=? x0) l2 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge (a :: l1) l2)
H:LocallySorted (fun x x0 : t => x <=? x0) (a :: l1)
H0:LocallySorted (fun x x0 : t => x <=? x0)
  (a0 :: l2)
Heq1:a <=? a0 = false
H1:is_true (a0 <=? a)
LocallySorted (fun x x0 : t => x <=? x0)
  (a0
   :: (fix merge_aux (l0 : list t) : list t :=
         match l0 with
         | [ ] => a :: l1
         | a2 :: l2' =>
             if a <=? a2
             then a :: merge l1 l0
             else a2 :: merge_aux l2'
         end) l2)
    invert H0.a:t
l1:list t
IHl1:forall l2 : list t,
LocallySorted (fun x x0 : t => x <=? x0) l1 ->
LocallySorted (fun x x0 : t => x <=? x0) l2 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge l1 l2)
a0:t
IHl2:LocallySorted (fun x x0 : t => x <=? x0)
  (a :: l1) ->
LocallySorted (fun x x0 : t => x <=? x0) [ ] ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge (a :: l1) [ ])
H:LocallySorted (fun x x0 : t => x <=? x0) (a :: l1)
Heq1:a <=? a0 = false
H1:is_true (a0 <=? a)
LocallySorted (fun x x0 : t => x <=? x0)
  (a0 :: a :: l1)
a:t
l1:list t
IHl1:forall l2 : list t,
LocallySorted (fun x x0 : t => x <=? x0) l1 ->
LocallySorted (fun x x0 : t => x <=? x0) l2 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge l1 l2)
a0, b:t
l:list t
IHl2:LocallySorted (fun x x0 : t => x <=? x0)
  (a :: l1) ->
LocallySorted (fun x x0 : t => x <=? x0)
  (b :: l) ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge (a :: l1) (b :: l))
H:LocallySorted (fun x x0 : t => x <=? x0) (a :: l1)
Heq1:a <=? a0 = false
H1:is_true (a0 <=? a)
H4:LocallySorted (fun x x0 : t => x <=? x0) (b :: l)
H5:is_true (a0 <=? b)
LocallySorted (fun x x0 : t => x <=? x0)
  (a0
   :: (if a <=? b
       then a :: merge l1 (b :: l)
       else
        b
        :: (fix merge_aux 
            (l2 : list t) : 
            list t :=
              match l2 with
              | [ ] => a :: l1
              | a2 :: l2' =>
                  if a <=? a2
                  then a :: merge l1 l2
                  else a2 :: merge_aux l2'
              end) l))
      constructor; trivial.a:t
l1:list t
IHl1:forall l2 : list t,
LocallySorted (fun x x0 : t => x <=? x0) l1 ->
LocallySorted (fun x x0 : t => x <=? x0) l2 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge l1 l2)
a0, b:t
l:list t
IHl2:LocallySorted (fun x x0 : t => x <=? x0)
  (a :: l1) ->
LocallySorted (fun x x0 : t => x <=? x0)
  (b :: l) ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge (a :: l1) (b :: l))
H:LocallySorted (fun x x0 : t => x <=? x0) (a :: l1)
Heq1:a <=? a0 = false
H1:is_true (a0 <=? a)
H4:LocallySorted (fun x x0 : t => x <=? x0) (b :: l)
H5:is_true (a0 <=? b)
LocallySorted (fun x x0 : t => x <=? x0)
  (a0
   :: (if a <=? b
       then a :: merge l1 (b :: l)
       else
        b
        :: (fix merge_aux (l2 : list t) : list t :=
              match l2 with
              | [ ] => a :: l1
              | a2 :: l2' =>
                  if a <=? a2
                  then a :: merge l1 l2
                  else a2 :: merge_aux l2'
              end) l))
      assert (Sorted (merge (a::l1) (b::l))) by auto using IHl1.a:t
l1:list t
IHl1:forall l2 : list t,
LocallySorted (fun x x0 : t => x <=? x0) l1 ->
LocallySorted (fun x x0 : t => x <=? x0) l2 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge l1 l2)
a0, b:t
l:list t
IHl2:LocallySorted (fun x x0 : t => x <=? x0)
  (a :: l1) ->
LocallySorted (fun x x0 : t => x <=? x0)
  (b :: l) ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge (a :: l1) (b :: l))
H:LocallySorted (fun x x0 : t => x <=? x0) (a :: l1)
Heq1:a <=? a0 = false
H1:is_true (a0 <=? a)
H4:LocallySorted (fun x x0 : t => x <=? x0) (b :: l)
H5:is_true (a0 <=? b)
H0:LocallySorted (fun x x0 : t => x <=? x0)
  (merge (a :: l1) (b :: l))
LocallySorted (fun x x0 : t => x <=? x0)
  (a0
   :: (if a <=? b
       then a :: merge l1 (b :: l)
       else
        b
        :: (fix merge_aux (l2 : list t) : list t :=
              match l2 with
              | [ ] => a :: l1
              | a2 :: l2' =>
                  if a <=? a2
                  then a :: merge l1 l2
                  else a2 :: merge_aux l2'
              end) l))
      clear IHl2; simpl in *.a:t
l1:list t
IHl1:forall l2 : list t,
LocallySorted (fun x x0 : t => x <=? x0) l1 ->
LocallySorted (fun x x0 : t => x <=? x0) l2 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge l1 l2)
a0, b:t
l:list t
H:LocallySorted (fun x x0 : t => x <=? x0) (a :: l1)
Heq1:a <=? a0 = false
H1:is_true (a0 <=? a)
H4:LocallySorted (fun x x0 : t => x <=? x0) (b :: l)
H5:is_true (a0 <=? b)
H0:LocallySorted (fun x x0 : t => x <=? x0)
  (if a <=? b
   then a :: merge l1 (b :: l)
   else
    b
    :: (fix merge_aux (l2 : list t) : 
        list t :=
          match l2 with
          | [ ] => a :: l1
          | a2 :: l2' =>
              if a <=? a2
              then a :: merge l1 l2
              else a2 :: merge_aux l2'
          end) l)
LocallySorted (fun x x0 : t => x <=? x0)
  (a0
   :: (if a <=? b
       then a :: merge l1 (b :: l)
       else
        b
        :: (fix merge_aux (l2 : list t) : list t :=
              match l2 with
              | [ ] => a :: l1
              | a2 :: l2' =>
                  if a <=? a2
                  then a :: merge l1 l2
                  else a2 :: merge_aux l2'
              end) l))
      destruct (a <=? b); constructor; auto.
Qed.

Theorem Permuted_merge : forall l1 l2, Permutation (l1++l2) (merge l1 l2).forall l1 l2 : list t,
Permutation (l1 ++ l2) (merge l1 l2)
Proof.forall l1 l2 : list t,
Permutation (l1 ++ l2) (merge l1 l2)
  induction l1; simpl merge; intro.l2:list t
Permutation ([ ] ++ l2)
  ((fix merge_aux (l0 : list t) : list t := l0) l2)
a:t
l1:list t
IHl1:forall l0 : list t,
Permutation (l1 ++ l0) (merge l1 l0)
l2:list t
Permutation ((a :: l1) ++ l2)
  ((fix merge_aux (l0 : list t) : list t :=
      match l0 with
      | [ ] => a :: l1
      | a2 :: l2' =>
          if a <=? a2
          then a :: merge l1 l0
          else a2 :: merge_aux l2'
      end) l2)
    assert (forall l, (fix merge_aux (l0 : list t) : list t := l0) l = l)
    as -> by (destruct l; trivial). (* Technical lemma *)l2:list t
Permutation ([ ] ++ l2) l2
a:t
l1:list t
IHl1:forall l0 : list t,
Permutation (l1 ++ l0) (merge l1 l0)
l2:list t
Permutation ((a :: l1) ++ l2)
  ((fix merge_aux (l0 : list t) : list t :=
      match l0 with
      | [ ] => a :: l1
      | a2 :: l2' =>
          if a <=? a2
          then a :: merge l1 l0
          else a2 :: merge_aux l2'
      end) l2)
    apply Permutation_refl.a:t
l1:list t
IHl1:forall l0 : list t,
Permutation (l1 ++ l0) (merge l1 l0)
l2:list t
Permutation ((a :: l1) ++ l2)
  ((fix merge_aux (l0 : list t) : list t :=
      match l0 with
      | [ ] => a :: l1
      | a2 :: l2' =>
          if a <=? a2
          then a :: merge l1 l0
          else a2 :: merge_aux l2'
      end) l2)
  induction l2.a:t
l1:list t
IHl1:forall l2 : list t,
Permutation (l1 ++ l2) (merge l1 l2)
Permutation ((a :: l1) ++ [ ]) (a :: l1)
a:t
l1:list t
IHl1:forall l0 : list t,
Permutation (l1 ++ l0) (merge l1 l0)
a0:t
l2:list t
IHl2:Permutation ((a :: l1) ++ l2)
  ((fix merge_aux (l0 : list t) : 
    list t :=
      match l0 with
      | [ ] => a :: l1
      | a2 :: l2' =>
          if a <=? a2
          then a :: merge l1 l0
          else a2 :: merge_aux l2'
      end) l2)
Permutation ((a :: l1) ++ a0 :: l2)
  (if a <=? a0
   then a :: merge l1 (a0 :: l2)
   else
    a0
    :: (fix merge_aux (l0 : list t) : 
        list t :=
          match l0 with
          | [ ] => a :: l1
          | a2 :: l2' =>
              if a <=? a2
              then a :: merge l1 l0
              else a2 :: merge_aux l2'
          end) l2)
    rewrite app_nil_r.a:t
l1:list t
IHl1:forall l2 : list t,
Permutation (l1 ++ l2) (merge l1 l2)
Permutation (a :: l1) (a :: l1)
a:t
l1:list t
IHl1:forall l0 : list t,
Permutation (l1 ++ l0) (merge l1 l0)
a0:t
l2:list t
IHl2:Permutation ((a :: l1) ++ l2)
  ((fix merge_aux (l0 : list t) : 
    list t :=
      match l0 with
      | [ ] => a :: l1
      | a2 :: l2' =>
          if a <=? a2
          then a :: merge l1 l0
          else a2 :: merge_aux l2'
      end) l2)
Permutation ((a :: l1) ++ a0 :: l2)
  (if a <=? a0
   then a :: merge l1 (a0 :: l2)
   else
    a0
    :: (fix merge_aux (l0 : list t) : 
        list t :=
          match l0 with
          | [ ] => a :: l1
          | a2 :: l2' =>
              if a <=? a2
              then a :: merge l1 l0
              else a2 :: merge_aux l2'
          end) l2) apply Permutation_refl.a:t
l1:list t
IHl1:forall l0 : list t,
Permutation (l1 ++ l0) (merge l1 l0)
a0:t
l2:list t
IHl2:Permutation ((a :: l1) ++ l2)
  ((fix merge_aux (l0 : list t) : 
    list t :=
      match l0 with
      | [ ] => a :: l1
      | a2 :: l2' =>
          if a <=? a2
          then a :: merge l1 l0
          else a2 :: merge_aux l2'
      end) l2)
Permutation ((a :: l1) ++ a0 :: l2)
  (if a <=? a0
   then a :: merge l1 (a0 :: l2)
   else
    a0
    :: (fix merge_aux (l0 : list t) : list t :=
          match l0 with
          | [ ] => a :: l1
          | a2 :: l2' =>
              if a <=? a2
              then a :: merge l1 l0
              else a2 :: merge_aux l2'
          end) l2)
    destruct (a <=? a0).a:t
l1:list t
IHl1:forall l0 : list t,
Permutation (l1 ++ l0) (merge l1 l0)
a0:t
l2:list t
IHl2:Permutation ((a :: l1) ++ l2)
  ((fix merge_aux (l0 : list t) : 
    list t :=
      match l0 with
      | [ ] => a :: l1
      | a2 :: l2' =>
          if a <=? a2
          then a :: merge l1 l0
          else a2 :: merge_aux l2'
      end) l2)
Permutation ((a :: l1) ++ a0 :: l2)
  (a :: merge l1 (a0 :: l2))
a:t
l1:list t
IHl1:forall l0 : list t,
Permutation (l1 ++ l0) (merge l1 l0)
a0:t
l2:list t
IHl2:Permutation ((a :: l1) ++ l2)
  ((fix merge_aux (l0 : list t) : 
    list t :=
      match l0 with
      | [ ] => a :: l1
      | a2 :: l2' =>
          if a <=? a2
          then a :: merge l1 l0
          else a2 :: merge_aux l2'
      end) l2)
Permutation ((a :: l1) ++ a0 :: l2)
  (a0
   :: (fix merge_aux (l0 : list t) : 
       list t :=
         match l0 with
         | [ ] => a :: l1
         | a2 :: l2' =>
             if a <=? a2
             then a :: merge l1 l0
             else a2 :: merge_aux l2'
         end) l2)
      constructor; apply IHl1.a:t
l1:list t
IHl1:forall l0 : list t,
Permutation (l1 ++ l0) (merge l1 l0)
a0:t
l2:list t
IHl2:Permutation ((a :: l1) ++ l2)
  ((fix merge_aux (l0 : list t) : 
    list t :=
      match l0 with
      | [ ] => a :: l1
      | a2 :: l2' =>
          if a <=? a2
          then a :: merge l1 l0
          else a2 :: merge_aux l2'
      end) l2)
Permutation ((a :: l1) ++ a0 :: l2)
  (a0
   :: (fix merge_aux (l0 : list t) : list t :=
         match l0 with
         | [ ] => a :: l1
         | a2 :: l2' =>
             if a <=? a2
             then a :: merge l1 l0
             else a2 :: merge_aux l2'
         end) l2)
      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).forall (stack : list (option (list t))) (l : list t),
SortedStack stack ->
LocallySorted (fun x x0 : t => x <=? x0) l ->
SortedStack (merge_list_to_stack stack l)
Proof.forall (stack : list (option (list t))) (l : list t),
SortedStack stack ->
LocallySorted (fun x x0 : t => x <=? x0) l ->
SortedStack (merge_list_to_stack stack l)
  induction stack as [|[|]]; intros; simpl.l:list t
H:SortedStack [ ]
H0:LocallySorted (fun x x0 : t => x <=? x0) l
LocallySorted (fun x x0 : t => x <=? x0) l /\ True
l:list t
stack:list (option (list t))
IHstack:forall l1 : list t,
SortedStack stack ->
LocallySorted (fun x x0 : t => x <=? x0) l1 ->
SortedStack (merge_list_to_stack stack l1)
l0:list t
H:SortedStack (Some l :: stack)
H0:LocallySorted (fun x x0 : t => x <=? x0) l0
SortedStack (merge_list_to_stack stack (merge l l0))
stack:list (option (list t))
IHstack:forall l0 : list t,
SortedStack stack ->
LocallySorted (fun x x0 : t => x <=? x0) l0 ->
SortedStack (merge_list_to_stack stack l0)
l:list t
H:SortedStack (None :: stack)
H0:LocallySorted (fun x x0 : t => x <=? x0) l
LocallySorted (fun x x0 : t => x <=? x0) l /\
SortedStack stack
    auto.l:list t
stack:list (option (list t))
IHstack:forall l1 : list t,
SortedStack stack ->
LocallySorted (fun x x0 : t => x <=? x0) l1 ->
SortedStack (merge_list_to_stack stack l1)
l0:list t
H:SortedStack (Some l :: stack)
H0:LocallySorted (fun x x0 : t => x <=? x0) l0
SortedStack (merge_list_to_stack stack (merge l l0))
stack:list (option (list t))
IHstack:forall l0 : list t,
SortedStack stack ->
LocallySorted (fun x x0 : t => x <=? x0) l0 ->
SortedStack (merge_list_to_stack stack l0)
l:list t
H:SortedStack (None :: stack)
H0:LocallySorted (fun x x0 : t => x <=? x0) l
LocallySorted (fun x x0 : t => x <=? x0) l /\
SortedStack stack
    apply IHstack.l:list t
stack:list (option (list t))
IHstack:forall l1 : list t,
SortedStack stack ->
LocallySorted (fun x x0 : t => x <=? x0) l1 ->
SortedStack (merge_list_to_stack stack l1)
l0:list t
H:SortedStack (Some l :: stack)
H0:LocallySorted (fun x x0 : t => x <=? x0) l0
SortedStack stack
l:list t
stack:list (option (list t))
IHstack:forall l1 : list t,
SortedStack stack ->
LocallySorted (fun x x0 : t => x <=? x0) l1 ->
SortedStack (merge_list_to_stack stack l1)
l0:list t
H:SortedStack (Some l :: stack)
H0:LocallySorted (fun x x0 : t => x <=? x0) l0
LocallySorted (fun x x0 : t => x <=? x0) (merge l l0)
stack:list (option (list t))
IHstack:forall l0 : list t,
SortedStack stack ->
LocallySorted (fun x x0 : t => x <=? x0) l0 ->
SortedStack (merge_list_to_stack stack l0)
l:list t
H:SortedStack (None :: stack)
H0:LocallySorted (fun x x0 : t => x <=? x0) l
LocallySorted (fun x x0 : t => x <=? x0) l /\
SortedStack stack destruct H as (_,H1).l:list t
stack:list (option (list t))
IHstack:forall l1 : list t,
SortedStack stack ->
LocallySorted (fun x x0 : t => x <=? x0) l1 ->
SortedStack (merge_list_to_stack stack l1)
l0:list t
H1:SortedStack stack
H0:LocallySorted (fun x x0 : t => x <=? x0) l0
SortedStack stack
l:list t
stack:list (option (list t))
IHstack:forall l1 : list t,
SortedStack stack ->
LocallySorted (fun x x0 : t => x <=? x0) l1 ->
SortedStack (merge_list_to_stack stack l1)
l0:list t
H:SortedStack (Some l :: stack)
H0:LocallySorted (fun x x0 : t => x <=? x0) l0
LocallySorted (fun x x0 : t => x <=? x0) (merge l l0)
stack:list (option (list t))
IHstack:forall l0 : list t,
SortedStack stack ->
LocallySorted (fun x x0 : t => x <=? x0) l0 ->
SortedStack (merge_list_to_stack stack l0)
l:list t
H:SortedStack (None :: stack)
H0:LocallySorted (fun x x0 : t => x <=? x0) l
LocallySorted (fun x x0 : t => x <=? x0) l /\
SortedStack stack fold SortedStack in H1.l:list t
stack:list (option (list t))
IHstack:forall l1 : list t,
SortedStack stack ->
LocallySorted (fun x x0 : t => x <=? x0) l1 ->
SortedStack (merge_list_to_stack stack l1)
l0:list t
H1:SortedStack stack
H0:LocallySorted (fun x x0 : t => x <=? x0) l0
SortedStack stack
l:list t
stack:list (option (list t))
IHstack:forall l1 : list t,
SortedStack stack ->
LocallySorted (fun x x0 : t => x <=? x0) l1 ->
SortedStack (merge_list_to_stack stack l1)
l0:list t
H:SortedStack (Some l :: stack)
H0:LocallySorted (fun x x0 : t => x <=? x0) l0
LocallySorted (fun x x0 : t => x <=? x0) (merge l l0)
stack:list (option (list t))
IHstack:forall l0 : list t,
SortedStack stack ->
LocallySorted (fun x x0 : t => x <=? x0) l0 ->
SortedStack (merge_list_to_stack stack l0)
l:list t
H:SortedStack (None :: stack)
H0:LocallySorted (fun x x0 : t => x <=? x0) l
LocallySorted (fun x x0 : t => x <=? x0) l /\
SortedStack stack auto.l:list t
stack:list (option (list t))
IHstack:forall l1 : list t,
SortedStack stack ->
LocallySorted (fun x x0 : t => x <=? x0) l1 ->
SortedStack (merge_list_to_stack stack l1)
l0:list t
H:SortedStack (Some l :: stack)
H0:LocallySorted (fun x x0 : t => x <=? x0) l0
LocallySorted (fun x x0 : t => x <=? x0) (merge l l0)
stack:list (option (list t))
IHstack:forall l0 : list t,
SortedStack stack ->
LocallySorted (fun x x0 : t => x <=? x0) l0 ->
SortedStack (merge_list_to_stack stack l0)
l:list t
H:SortedStack (None :: stack)
H0:LocallySorted (fun x x0 : t => x <=? x0) l
LocallySorted (fun x x0 : t => x <=? x0) l /\
SortedStack stack
      apply Sorted_merge; auto; destruct H; auto.stack:list (option (list t))
IHstack:forall l0 : list t,
SortedStack stack ->
LocallySorted (fun x x0 : t => x <=? x0) l0 ->
SortedStack (merge_list_to_stack stack l0)
l:list t
H:SortedStack (None :: stack)
H0:LocallySorted (fun x x0 : t => x <=? x0) l
LocallySorted (fun x x0 : t => x <=? x0) l /\
SortedStack stack
      auto.
Qed.

Theorem Permuted_merge_list_to_stack : forall stack l,
  Permutation (l ++ flatten_stack stack) (flatten_stack (merge_list_to_stack stack l)).forall (stack : list (option (list t))) (l : list t),
Permutation (l ++ flatten_stack stack)
  (flatten_stack (merge_list_to_stack stack l))
Proof.forall (stack : list (option (list t))) (l : list t),
Permutation (l ++ flatten_stack stack)
  (flatten_stack (merge_list_to_stack stack l))
  induction stack as [|[]]; simpl; intros.l:list t
Permutation (l ++ [ ]) (l ++ [ ])
l:list t
stack:list (option (list t))
IHstack:forall l1 : list t,
Permutation (l1 ++ flatten_stack stack)
  (flatten_stack
     (merge_list_to_stack stack l1))
l0:list t
Permutation (l0 ++ l ++ flatten_stack stack)
  (flatten_stack
     (merge_list_to_stack stack (merge l l0)))
stack:list (option (list t))
IHstack:forall l0 : list t,
Permutation (l0 ++ flatten_stack stack)
  (flatten_stack
     (merge_list_to_stack stack l0))
l:list t
Permutation (l ++ flatten_stack stack)
  (l ++ flatten_stack stack)
    reflexivity.l:list t
stack:list (option (list t))
IHstack:forall l1 : list t,
Permutation (l1 ++ flatten_stack stack)
  (flatten_stack
     (merge_list_to_stack stack l1))
l0:list t
Permutation (l0 ++ l ++ flatten_stack stack)
  (flatten_stack
     (merge_list_to_stack stack (merge l l0)))
stack:list (option (list t))
IHstack:forall l0 : list t,
Permutation (l0 ++ flatten_stack stack)
  (flatten_stack
     (merge_list_to_stack stack l0))
l:list t
Permutation (l ++ flatten_stack stack)
  (l ++ flatten_stack stack)
    rewrite app_assoc.l:list t
stack:list (option (list t))
IHstack:forall l1 : list t,
Permutation (l1 ++ flatten_stack stack)
  (flatten_stack
     (merge_list_to_stack stack l1))
l0:list t
Permutation ((l0 ++ l) ++ flatten_stack stack)
  (flatten_stack
     (merge_list_to_stack stack (merge l l0)))
stack:list (option (list t))
IHstack:forall l0 : list t,
Permutation (l0 ++ flatten_stack stack)
  (flatten_stack
     (merge_list_to_stack stack l0))
l:list t
Permutation (l ++ flatten_stack stack)
  (l ++ flatten_stack stack)
    etransitivity.l:list t
stack:list (option (list t))
IHstack:forall l1 : list t,
Permutation (l1 ++ flatten_stack stack)
  (flatten_stack
     (merge_list_to_stack stack l1))
l0:list t
Permutation ((l0 ++ l) ++ flatten_stack stack) ?y
l:list t
stack:list (option (list t))
IHstack:forall l1 : list t,
Permutation (l1 ++ flatten_stack stack)
  (flatten_stack
     (merge_list_to_stack stack l1))
l0:list t
Permutation ?y
  (flatten_stack
     (merge_list_to_stack stack (merge l l0)))
stack:list (option (list t))
IHstack:forall l0 : list t,
Permutation (l0 ++ flatten_stack stack)
  (flatten_stack
     (merge_list_to_stack stack l0))
l:list t
Permutation (l ++ flatten_stack stack)
  (l ++ flatten_stack stack)
      apply Permutation_app_tail.l:list t
stack:list (option (list t))
IHstack:forall l1 : list t,
Permutation (l1 ++ flatten_stack stack)
  (flatten_stack
     (merge_list_to_stack stack l1))
l0:list t
Permutation (l0 ++ l) ?l'
l:list t
stack:list (option (list t))
IHstack:forall l1 : list t,
Permutation (l1 ++ flatten_stack stack)
  (flatten_stack
     (merge_list_to_stack stack l1))
l0:list t
Permutation (?l' ++ flatten_stack stack)
  (flatten_stack
     (merge_list_to_stack stack (merge l l0)))
stack:list (option (list t))
IHstack:forall l0 : list t,
Permutation (l0 ++ flatten_stack stack)
  (flatten_stack
     (merge_list_to_stack stack l0))
l:list t
Permutation (l ++ flatten_stack stack)
  (l ++ flatten_stack stack)
      etransitivity.l:list t
stack:list (option (list t))
IHstack:forall l1 : list t,
Permutation (l1 ++ flatten_stack stack)
  (flatten_stack
     (merge_list_to_stack stack l1))
l0:list t
Permutation (l0 ++ l) ?y
l:list t
stack:list (option (list t))
IHstack:forall l1 : list t,
Permutation (l1 ++ flatten_stack stack)
  (flatten_stack
     (merge_list_to_stack stack l1))
l0:list t
Permutation ?y ?l'
l:list t
stack:list (option (list t))
IHstack:forall l1 : list t,
Permutation (l1 ++ flatten_stack stack)
  (flatten_stack
     (merge_list_to_stack stack l1))
l0:list t
Permutation (?l' ++ flatten_stack stack)
  (flatten_stack
     (merge_list_to_stack stack (merge l l0)))
stack:list (option (list t))
IHstack:forall l0 : list t,
Permutation (l0 ++ flatten_stack stack)
  (flatten_stack
     (merge_list_to_stack stack l0))
l:list t
Permutation (l ++ flatten_stack stack)
  (l ++ flatten_stack stack)
        apply Permutation_app_comm.l:list t
stack:list (option (list t))
IHstack:forall l1 : list t,
Permutation (l1 ++ flatten_stack stack)
  (flatten_stack
     (merge_list_to_stack stack l1))
l0:list t
Permutation (l ++ l0) ?l'
l:list t
stack:list (option (list t))
IHstack:forall l1 : list t,
Permutation (l1 ++ flatten_stack stack)
  (flatten_stack
     (merge_list_to_stack stack l1))
l0:list t
Permutation (?l' ++ flatten_stack stack)
  (flatten_stack
     (merge_list_to_stack stack (merge l l0)))
stack:list (option (list t))
IHstack:forall l0 : list t,
Permutation (l0 ++ flatten_stack stack)
  (flatten_stack
     (merge_list_to_stack stack l0))
l:list t
Permutation (l ++ flatten_stack stack)
  (l ++ flatten_stack stack)
      apply Permuted_merge.l:list t
stack:list (option (list t))
IHstack:forall l1 : list t,
Permutation (l1 ++ flatten_stack stack)
  (flatten_stack
     (merge_list_to_stack stack l1))
l0:list t
Permutation (merge l l0 ++ flatten_stack stack)
  (flatten_stack
     (merge_list_to_stack stack (merge l l0)))
stack:list (option (list t))
IHstack:forall l0 : list t,
Permutation (l0 ++ flatten_stack stack)
  (flatten_stack
     (merge_list_to_stack stack l0))
l:list t
Permutation (l ++ flatten_stack stack)
  (l ++ flatten_stack stack)
    apply IHstack.stack:list (option (list t))
IHstack:forall l0 : list t,
Permutation (l0 ++ flatten_stack stack)
  (flatten_stack
     (merge_list_to_stack stack l0))
l:list t
Permutation (l ++ flatten_stack stack)
  (l ++ flatten_stack stack)
    reflexivity.
Qed.

Theorem Sorted_merge_stack : forall stack,
  SortedStack stack -> Sorted (merge_stack stack).forall stack : list (option (list t)),
SortedStack stack ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge_stack stack)
Proof.forall stack : list (option (list t)),
SortedStack stack ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge_stack stack)
induction stack as [|[|]]; simpl; intros.H:True
LocallySorted (fun x x0 : t => x <=? x0) [ ]
l:list t
stack:list (option (list t))
IHstack:SortedStack stack ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge_stack stack)
H:LocallySorted (fun x x0 : t => x <=? x0) l /\
SortedStack stack
LocallySorted (fun x x0 : t => x <=? x0)
  (merge l (merge_stack stack))
stack:list (option (list t))
IHstack:SortedStack stack ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge_stack stack)
H:SortedStack stack
LocallySorted (fun x x0 : t => x <=? x0)
  (merge_stack stack)
  constructor; auto.l:list t
stack:list (option (list t))
IHstack:SortedStack stack ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge_stack stack)
H:LocallySorted (fun x x0 : t => x <=? x0) l /\
SortedStack stack
LocallySorted (fun x x0 : t => x <=? x0)
  (merge l (merge_stack stack))
stack:list (option (list t))
IHstack:SortedStack stack ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge_stack stack)
H:SortedStack stack
LocallySorted (fun x x0 : t => x <=? x0)
  (merge_stack stack)
  apply Sorted_merge; tauto.stack:list (option (list t))
IHstack:SortedStack stack ->
LocallySorted (fun x x0 : t => x <=? x0)
  (merge_stack stack)
H:SortedStack stack
LocallySorted (fun x x0 : t => x <=? x0)
  (merge_stack stack)
  auto.
Qed.

Theorem Permuted_merge_stack : forall stack,
  Permutation (flatten_stack stack) (merge_stack stack).forall stack : list (option (list t)),
Permutation (flatten_stack stack) (merge_stack stack)
Proof.forall stack : list (option (list t)),
Permutation (flatten_stack stack) (merge_stack stack)
induction stack as [|[]]; simpl.Permutation [ ] [ ]
l:list t
stack:list (option (list t))
IHstack:Permutation (flatten_stack stack)
  (merge_stack stack)
Permutation (l ++ flatten_stack stack)
  (merge l (merge_stack stack))
stack:list (option (list t))
IHstack:Permutation (flatten_stack stack)
  (merge_stack stack)
Permutation (flatten_stack stack) (merge_stack stack)
  trivial.l:list t
stack:list (option (list t))
IHstack:Permutation (flatten_stack stack)
  (merge_stack stack)
Permutation (l ++ flatten_stack stack)
  (merge l (merge_stack stack))
stack:list (option (list t))
IHstack:Permutation (flatten_stack stack)
  (merge_stack stack)
Permutation (flatten_stack stack) (merge_stack stack)
  transitivity (l ++ merge_stack stack).l:list t
stack:list (option (list t))
IHstack:Permutation (flatten_stack stack)
  (merge_stack stack)
Permutation (l ++ flatten_stack stack)
  (l ++ merge_stack stack)
l:list t
stack:list (option (list t))
IHstack:Permutation (flatten_stack stack)
  (merge_stack stack)
Permutation (l ++ merge_stack stack)
  (merge l (merge_stack stack))
stack:list (option (list t))
IHstack:Permutation (flatten_stack stack)
  (merge_stack stack)
Permutation (flatten_stack stack) (merge_stack stack)
    apply Permutation_app_head; trivial.l:list t
stack:list (option (list t))
IHstack:Permutation (flatten_stack stack)
  (merge_stack stack)
Permutation (l ++ merge_stack stack)
  (merge l (merge_stack stack))
stack:list (option (list t))
IHstack:Permutation (flatten_stack stack)
  (merge_stack stack)
Permutation (flatten_stack stack) (merge_stack stack)
    apply Permuted_merge.stack:list (option (list t))
IHstack:Permutation (flatten_stack stack)
  (merge_stack stack)
Permutation (flatten_stack stack) (merge_stack stack)
  assumption.
Qed.

Theorem Sorted_iter_merge : forall stack l,
  SortedStack stack -> Sorted (iter_merge stack l).forall (stack : list (option (list t))) (l : list t),
SortedStack stack ->
LocallySorted (fun x x0 : t => x <=? x0)
  (iter_merge stack l)
Proof.forall (stack : list (option (list t))) (l : list t),
SortedStack stack ->
LocallySorted (fun x x0 : t => x <=? x0)
  (iter_merge stack l)
  intros stack l H; induction l in stack, H |- *; simpl.stack:list (option (list t))
H:SortedStack stack
LocallySorted (fun x x0 : t => x <=? x0)
  (merge_stack stack)
stack:list (option (list t))
a:t
l:list t
H:SortedStack stack
IHl:forall stack0 : list (option (list t)),
SortedStack stack0 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (iter_merge stack0 l)
LocallySorted (fun x x0 : t => x <=? x0)
  (iter_merge (merge_list_to_stack stack [a]) l)
    auto using Sorted_merge_stack.stack:list (option (list t))
a:t
l:list t
H:SortedStack stack
IHl:forall stack0 : list (option (list t)),
SortedStack stack0 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (iter_merge stack0 l)
LocallySorted (fun x x0 : t => x <=? x0)
  (iter_merge (merge_list_to_stack stack [a]) l)
    assert (Sorted [a]) by constructor.stack:list (option (list t))
a:t
l:list t
H:SortedStack stack
IHl:forall stack0 : list (option (list t)),
SortedStack stack0 ->
LocallySorted (fun x x0 : t => x <=? x0)
  (iter_merge stack0 l)
H0:LocallySorted (fun x x0 : t => x <=? x0) [a]
LocallySorted (fun x x0 : t => x <=? x0)
  (iter_merge (merge_list_to_stack stack [a]) l)
    auto using Sorted_merge_list_to_stack.
Qed.

Theorem Permuted_iter_merge : forall l stack,
  Permutation (flatten_stack stack ++ l) (iter_merge stack l).forall (l : list t) (stack : list (option (list t))),
Permutation (flatten_stack stack ++ l)
  (iter_merge stack l)
Proof.forall (l : list t) (stack : list (option (list t))),
Permutation (flatten_stack stack ++ l)
  (iter_merge stack l)
  induction l; simpl; intros.stack:list (option (list t))
Permutation (flatten_stack stack ++ [ ])
  (merge_stack stack)
a:t
l:list t
IHl:forall stack0 : list (option (list t)),
Permutation (flatten_stack stack0 ++ l)
  (iter_merge stack0 l)
stack:list (option (list t))
Permutation (flatten_stack stack ++ a :: l)
  (iter_merge (merge_list_to_stack stack [a]) l)
    rewrite app_nil_r.stack:list (option (list t))
Permutation (flatten_stack stack) (merge_stack stack)
a:t
l:list t
IHl:forall stack0 : list (option (list t)),
Permutation (flatten_stack stack0 ++ l)
  (iter_merge stack0 l)
stack:list (option (list t))
Permutation (flatten_stack stack ++ a :: l)
  (iter_merge (merge_list_to_stack stack [a]) l) apply Permuted_merge_stack.a:t
l:list t
IHl:forall stack0 : list (option (list t)),
Permutation (flatten_stack stack0 ++ l) (iter_merge stack0 l)
stack:list (option (list t))
Permutation (flatten_stack stack ++ a :: l)
  (iter_merge (merge_list_to_stack stack [a]) l)
    change (a::l) with ([a]++l).a:t
l:list t
IHl:forall stack0 : list (option (list t)),
Permutation (flatten_stack stack0 ++ l) (iter_merge stack0 l)
stack:list (option (list t))
Permutation (flatten_stack stack ++ [a] ++ l)
  (iter_merge (merge_list_to_stack stack [a]) l)
    rewrite app_assoc.a:t
l:list t
IHl:forall stack0 : list (option (list t)),
Permutation (flatten_stack stack0 ++ l) (iter_merge stack0 l)
stack:list (option (list t))
Permutation ((flatten_stack stack ++ [a]) ++ l)
  (iter_merge (merge_list_to_stack stack [a]) l)
    etransitivity.a:t
l:list t
IHl:forall stack0 : list (option (list t)),
Permutation (flatten_stack stack0 ++ l) (iter_merge stack0 l)
stack:list (option (list t))
Permutation ((flatten_stack stack ++ [a]) ++ l) ?y
a:t
l:list t
IHl:forall stack0 : list (option (list t)),
Permutation (flatten_stack stack0 ++ l)
  (iter_merge stack0 l)
stack:list (option (list t))
Permutation ?y
  (iter_merge (merge_list_to_stack stack [a]) l)
      apply Permutation_app_tail.a:t
l:list t
IHl:forall stack0 : list (option (list t)),
Permutation (flatten_stack stack0 ++ l) (iter_merge stack0 l)
stack:list (option (list t))
Permutation (flatten_stack stack ++ [a]) ?l'
a:t
l:list t
IHl:forall stack0 : list (option (list t)),
Permutation (flatten_stack stack0 ++ l)
  (iter_merge stack0 l)
stack:list (option (list t))
Permutation (?l' ++ l)
  (iter_merge (merge_list_to_stack stack [a]) l)
    etransitivity.a:t
l:list t
IHl:forall stack0 : list (option (list t)),
Permutation (flatten_stack stack0 ++ l) (iter_merge stack0 l)
stack:list (option (list t))
Permutation (flatten_stack stack ++ [a]) ?y
a:t
l:list t
IHl:forall stack0 : list (option (list t)),
Permutation (flatten_stack stack0 ++ l)
  (iter_merge stack0 l)
stack:list (option (list t))
Permutation ?y ?l'
a:t
l:list t
IHl:forall stack0 : list (option (list t)),
Permutation (flatten_stack stack0 ++ l)
  (iter_merge stack0 l)
stack:list (option (list t))
Permutation (?l' ++ l)
  (iter_merge (merge_list_to_stack stack [a]) l)
    apply Permutation_app_comm.a:t
l:list t
IHl:forall stack0 : list (option (list t)),
Permutation (flatten_stack stack0 ++ l) (iter_merge stack0 l)
stack:list (option (list t))
Permutation ([a] ++ flatten_stack stack) ?l'
a:t
l:list t
IHl:forall stack0 : list (option (list t)),
Permutation (flatten_stack stack0 ++ l)
  (iter_merge stack0 l)
stack:list (option (list t))
Permutation (?l' ++ l)
  (iter_merge (merge_list_to_stack stack [a]) l)
    apply Permuted_merge_list_to_stack.a:t
l:list t
IHl:forall stack0 : list (option (list t)),
Permutation (flatten_stack stack0 ++ l) (iter_merge stack0 l)
stack:list (option (list t))
Permutation
  (flatten_stack (merge_list_to_stack stack [a]) ++ l)
  (iter_merge (merge_list_to_stack stack [a]) l)
    apply IHl.
Qed.

Theorem Sorted_sort : forall l, Sorted (sort l).forall l : list t,
LocallySorted (fun x x0 : t => x <=? x0) (sort l)
Proof.forall l : list t,
LocallySorted (fun x x0 : t => x <=? x0) (sort l)
intro; apply Sorted_iter_merge.l:list t
SortedStack [ ] constructor.
Qed.

Corollary LocallySorted_sort : forall l, Sorted.Sorted leb (sort l).forall l : list t,
Sorted.Sorted (fun x x0 : t => x <=? x0) (sort l)
Proof.forall l : list t,
Sorted.Sorted (fun x x0 : t => x <=? x0) (sort l) intro; eapply Sorted_LocallySorted_iff, Sorted_sort; auto. Qed.

Theorem Permuted_sort : forall l, Permutation l (sort l).forall l : list t, Permutation l (sort l)
Proof.forall l : list t, Permutation l (sort l)
intro; apply (Permuted_iter_merge l []).
Qed.

Corollary StronglySorted_sort : forall l,
  Transitive leb -> StronglySorted leb (sort l).forall l : list t,
Transitive (fun x x0 : t => x <=? x0) ->
StronglySorted (fun x x0 : t => x <=? x0) (sort l)
Proof.forall l : list t,
Transitive (fun x x0 : t => x <=? x0) ->
StronglySorted (fun x x0 : t => x <=? x0) (sort l) 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.forall a1 a2 : nat, a1 <=? a2 \/ a2 <=? a1
  Proof.forall a1 a2 : nat, a1 <=? a2 \/ a2 <=? a1
    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].