proposition: Theorem merge_sort_correct: sort_correct A le (merge_sort (fun x y => bool_decide (x <= y))).
proof: Proof. Proof with auto with lists. intro l; functional induction (merge_sort (fun x y => bool_decide (x <= y)) l) ... - split... - split ... - destruct IHl0, IHl1. split ... apply (merge_LocallySorted (merge_sort (fun x y => bool_decide (x <= y)) l1) (merge_sort (fun x y => bool_decide (x <= y)) l2)); trivial. transitivity (l1++l2). generalize (split_permutation (_x :: _x0 :: _x1)). rewrite e0. intro;symmetry... transitivity ((merge_sort (fun x y => bool_decide (x <= y)) l1) ++ (merge_sort (fun x y => bool_decide (x <= y)) l2)). rewrite <- H0, <- H2 ... apply merge_permutation; trivial. Qed.
imports: Coq(List Wf_nat Recdef Compare_dec Arith Peano_dec Lia RelationClasses Sorting.Sorted Sorting.Permutation) hydras(DecPreOrder DecPreOrder_Instances Sort_spec)