val merge'_stable: #a:eqtype -> (l: list a{Cons? l}) -> (r: list a{Cons? r}) -> k:(a -> Tot int) ->
  Lemma (requires (sorted l k /\ sorted r k))
        (ensures stable (l@r) (merge' l r k) k)
val merge'_stable: #a:eqtype -> (l: list a{Cons? l}) -> (r: list a{Cons? r}) -> k:(a -> Tot int) ->
  Lemma (requires (sorted l k /\ sorted r k))
        (ensures stable (l@r) (merge' l r k) k)
let merge'_stable #a l r k = merge'_filter_eq_inv l r k
(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module MergeSort2
(**
  @author: A Manning
  @summary: This module implements a generic merge sort and proves it's stability.
  A great deal of inspiration taken from
  http://research.microsoft.com/en-us/um/people/leino/papers/krml241.pdf.
  Verifies in ~8s for me.
 **)

open FStar.List.Tot
open GenericSort
open GenericStability
(*
  The key function k will appear frequently here.
*)

(** First define the merge function without any properties.**)
val merge': #a:eqtype -> (l1:list a) -> (l2:list a) -> k:(a -> Tot int) -> Tot (list a)
let rec merge' #a l1 l2 k = match (l1, l2) with
  | [], _ -> l2
  | _, [] -> l1
  | h1::tl1, h2::tl2 ->
    if k h1 <= k h2
    then h1::(merge' tl1 l2 k)
    else h2::(merge' l1 tl2 k)

(** merging l and r returns a permutation of l and r **)
val merge'_permutation: #a:eqtype ->
  (l1:list a) ->
  (l2:list a) ->
  k:(a -> Tot int) ->
  Lemma(ensures permutation_2 (merge' l1 l2 k) l1 l2)
let rec merge'_permutation #a l1 l2 k = match (l1, l2) with
  | [], _ -> ()
  | _, [] -> ()
  | h1::tl1, h2::tl2 ->
    if k h1 <= k h2
    then (merge'_permutation tl1 l2 k)
    else (merge'_permutation l1 tl2 k)

(** merging two sorted lists returns a sorted list **)
val merge'_sorted: #a:eqtype ->
  (l1:list a) ->
  (l2:list a) ->
  k:(a -> Tot int) ->
  Lemma (requires (sorted l1 k /\ sorted l2 k))
        (ensures sorted (merge' l1 l2 k) k)
let rec merge'_sorted #a l1 l2 k = match (l1, l2) with
  | [], _ -> ()
  | _, [] -> ()
  | h1::tl1, h2::tl2 ->
    if k h1 <= k h2
    then (merge'_sorted tl1 l2 k)
    else (merge'_sorted l1 tl2 k)

(** filtering (l appended to r) wrt x is equivalent to merging l and r, then filtering wrt x **)
val merge'_filter_eq_inv: #a:eqtype -> (l: list a{Cons? l}) -> (r: list a{Cons? r}) -> k:(a -> Tot int) ->
  Lemma (requires (sorted l k /\ sorted r k))
        (ensures (forall x. Cons? l /\ Cons? r /\ (filter_eq x (l@r) k = filter_eq x (merge' l r k) k)))
let rec merge'_filter_eq_inv #a l r k =
  if k (hd r) < k (hd l) then begin
    stable_lift l r k;
    if (tl r) = [] then ()
    else begin
      merge'_filter_eq_inv l (tl r) k;
      filter_eq_append [hd r] (merge' l (tl r) k) k
    end
  end
  else if (tl l) = [] then ()
  else begin
    merge'_filter_eq_inv (tl l) r k;
    filter_eq_append [hd l] (merge' (tl l) r k) k
  end

(** merge is stable **)
val merge'_stable: #a:eqtype -> (l: list a{Cons? l}) -> (r: list a{Cons? r}) -> k:(a -> Tot int) ->
  Lemma (requires (sorted l k /\ sorted r k))
/
prims.fst.checked GenericStability.fst.checked GenericSort.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
MergeSort2.fst
l: Prims.list a {Cons? l} -> r: Prims.list a {Cons? r} -> k: (_: a -> Prims.int)
  -> FStar.Pervasives.Lemma (requires GenericSort.sorted l k /\ GenericSort.sorted r k)
      (ensures GenericStability.stable (l @ r) (MergeSort2.merge' l r k) k)
Prims.eqtype Prims.list Prims.b2t Prims.uu___is_Cons Prims.int MergeSort2.merge'_filter_eq_inv Prims.unit
let merge'_stable #a l r k =
  
merge'_filter_eq_inv l r k