Forgot to commit prelude/sorting, this fixes 6dbe0c27.

theories/sorting.v

+(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* This file is distributed under the terms of the BSD license. *)
+(** Merge sort. Adapted from the implementation of Hugo Herbelin in the Coq
+standard library, but without using the module system. *)
+From Coq Require Export Sorted.
+From stdpp Require Export orders list.
+
+Section merge_sort.
+  Context {A} (R : relation A) `{∀ x y, Decision (R x y)}.
+
+  Fixpoint list_merge (l1 : list A) : list A → list A :=
+    fix list_merge_aux l2 :=
+    match l1, l2 with
+    | [], _ => l2
+    | _, [] => l1
+    | x1 :: l1, x2 :: l2 =>
+       if decide_rel R x1 x2 then x1 :: list_merge l1 (x2 :: l2)
+       else x2 :: list_merge_aux l2
+    end.
+  Global Arguments list_merge !_ !_ /.
+
+  Local Notation stack := (list (option (list A))).
+  Fixpoint merge_list_to_stack (st : stack) (l : list A) : stack :=
+    match st with
+    | [] => [Some l]
+    | None :: st => Some l :: st
+    | Some l' :: st => None :: merge_list_to_stack st (list_merge l' l)
+    end.
+  Fixpoint merge_stack (st : stack) : list A :=
+    match st with
+    | [] => []
+    | None :: st => merge_stack st
+    | Some l :: st => list_merge l (merge_stack st)
+    end.
+  Fixpoint merge_sort_aux (st : stack) (l : list A) : list A :=
+    match l with
+    | [] => merge_stack st
+    | x :: l => merge_sort_aux (merge_list_to_stack st [x]) l
+    end.
+  Definition merge_sort : list A → list A := merge_sort_aux [].
+End merge_sort.
+
+(** ** Properties of the [Sorted] and [StronglySorted] predicate *)
+Section sorted.
+  Context {A} (R : relation A).
+
+  Lemma Sorted_StronglySorted `{!Transitive R} l :
+    Sorted R l → StronglySorted R l.
+  Proof. by apply Sorted.Sorted_StronglySorted. Qed.
+  Lemma StronglySorted_unique `{!AntiSymm (=) R} l1 l2 :
+    StronglySorted R l1 → StronglySorted R l2 → l1 ≡ₚ l2 → l1 = l2.
+  Proof.
+    intros Hl1; revert l2. induction Hl1 as [|x1 l1 ? IH Hx1]; intros l2 Hl2 E.
+    { symmetry. by apply Permutation_nil. }
+    destruct Hl2 as [|x2 l2 ? Hx2].
+    { by apply Permutation_nil in E. }
+    assert (x1 = x2); subst.
+    { rewrite Forall_forall in Hx1, Hx2.
+      assert (x2 ∈ x1 :: l1) as Hx2' by (by rewrite E; left).
+      assert (x1 ∈ x2 :: l2) as Hx1' by (by rewrite <-E; left).
+      inversion Hx1'; inversion Hx2'; simplify_eq; auto. }
+    f_equal. by apply IH, (inj (x2 ::)).
+  Qed.
+  Lemma Sorted_unique `{!Transitive R, !AntiSymm (=) R} l1 l2 :
+    Sorted R l1 → Sorted R l2 → l1 ≡ₚ l2 → l1 = l2.
+  Proof. auto using StronglySorted_unique, Sorted_StronglySorted. Qed.
+
+  Global Instance HdRel_dec x `{∀ y, Decision (R x y)} l :
+    Decision (HdRel R x l).
+  Proof.
+   refine
+    match l with
+    | [] => left _
+    | y :: l => cast_if (decide (R x y))
+    end; abstract first [by constructor | by inversion 1].
+  Defined.
+  Global Instance Sorted_dec `{∀ x y, Decision (R x y)} : ∀ l,
+    Decision (Sorted R l).
+  Proof.
+   refine
+    (fix go l :=
+    match l return Decision (Sorted R l) with
+    | [] => left _
+    | x :: l => cast_if_and (decide (HdRel R x l)) (go l)
+    end); clear go; abstract first [by constructor | by inversion 1].
+  Defined.
+  Global Instance StronglySorted_dec `{∀ x y, Decision (R x y)} : ∀ l,
+    Decision (StronglySorted R l).
+  Proof.
+   refine
+    (fix go l :=
+    match l return Decision (StronglySorted R l) with
+    | [] => left _
+    | x :: l => cast_if_and (decide (Forall (R x) l)) (go l)
+    end); clear go; abstract first [by constructor | by inversion 1].
+  Defined.
+
+  Context {B} (f : A → B).
+  Lemma HdRel_fmap (R1 : relation A) (R2 : relation B) x l :
+    (∀ y, R1 x y → R2 (f x) (f y)) → HdRel R1 x l → HdRel R2 (f x) (f <$> l).
+  Proof. destruct 2; constructor; auto. Qed.
+  Lemma Sorted_fmap (R1 : relation A) (R2 : relation B) l :
+    (∀ x y, R1 x y → R2 (f x) (f y)) → Sorted R1 l → Sorted R2 (f <$> l).
+  Proof. induction 2; simpl; constructor; eauto using HdRel_fmap. Qed.
+  Lemma StronglySorted_fmap (R1 : relation A) (R2 : relation B) l :
+    (∀ x y, R1 x y → R2 (f x) (f y)) →
+    StronglySorted R1 l → StronglySorted R2 (f <$> l).
+  Proof.
+    induction 2; csimpl; constructor;
+      rewrite ?Forall_fmap; eauto using Forall_impl.
+  Qed.
+End sorted.
+
+(** ** Correctness of merge sort *)
+Section merge_sort_correct.
+  Context  {A} (R : relation A) `{∀ x y, Decision (R x y)} `{!Total R}.
+
+  Lemma list_merge_cons x1 x2 l1 l2 :
+    list_merge R (x1 :: l1) (x2 :: l2) =
+      if decide (R x1 x2) then x1 :: list_merge R l1 (x2 :: l2)
+      else x2 :: list_merge R (x1 :: l1) l2.
+  Proof. done. Qed.
+  Lemma HdRel_list_merge x l1 l2 :
+    HdRel R x l1 → HdRel R x l2 → HdRel R x (list_merge R l1 l2).
+  Proof.
+    destruct 1 as [|x1 l1 IH1], 1 as [|x2 l2 IH2];
+      rewrite ?list_merge_cons; simpl; repeat case_decide; auto.
+  Qed.
+  Lemma Sorted_list_merge l1 l2 :
+    Sorted R l1 → Sorted R l2 → Sorted R (list_merge R l1 l2).
+  Proof.
+    intros Hl1. revert l2. induction Hl1 as [|x1 l1 IH1];
+      induction 1 as [|x2 l2 IH2]; rewrite ?list_merge_cons; simpl;
+      repeat case_decide;
+      constructor; eauto using HdRel_list_merge, HdRel_cons, total_not.
+  Qed.
+  Lemma merge_Permutation l1 l2 : list_merge R l1 l2 ≡ₚ l1 ++ l2.
+  Proof.
+    revert l2. induction l1 as [|x1 l1 IH1]; intros l2;
+      induction l2 as [|x2 l2 IH2]; rewrite ?list_merge_cons; simpl;
+      repeat case_decide; auto.
+    - by rewrite (right_id_L [] (++)).
+    - by rewrite IH2, Permutation_middle.
+  Qed.
+
+  Local Notation stack := (list (option (list A))).
+  Inductive merge_stack_Sorted : stack → Prop :=
+    | merge_stack_Sorted_nil : merge_stack_Sorted []
+    | merge_stack_Sorted_cons_None st :
+       merge_stack_Sorted st → merge_stack_Sorted (None :: st)
+    | merge_stack_Sorted_cons_Some l st :
+       Sorted R l → merge_stack_Sorted st → merge_stack_Sorted (Some l :: st).
+  Fixpoint merge_stack_flatten (st : stack) : list A :=
+    match st with
+    | [] => []
+    | None :: st => merge_stack_flatten st
+    | Some l :: st => l ++ merge_stack_flatten st
+    end.
+
+  Lemma Sorted_merge_list_to_stack st l :
+    merge_stack_Sorted st → Sorted R l →
+    merge_stack_Sorted (merge_list_to_stack R st l).
+  Proof.
+    intros Hst. revert l.
+    induction Hst; repeat constructor; naive_solver auto using Sorted_list_merge.
+  Qed.
+  Lemma merge_list_to_stack_Permutation st l :
+    merge_stack_flatten (merge_list_to_stack R st l) ≡ₚ
+      l ++ merge_stack_flatten st.
+  Proof.
+    revert l. induction st as [|[l'|] st IH]; intros l; simpl; auto.
+    by rewrite IH, merge_Permutation, (assoc_L _), (comm (++) l).
+  Qed.
+  Lemma Sorted_merge_stack st :
+    merge_stack_Sorted st → Sorted R (merge_stack R st).
+  Proof. induction 1; simpl; auto using Sorted_list_merge. Qed.
+  Lemma merge_stack_Permutation st : merge_stack R st ≡ₚ merge_stack_flatten st.
+  Proof.
+    induction st as [|[] ? IH]; intros; simpl; auto.
+    by rewrite merge_Permutation, IH.
+  Qed.
+  Lemma Sorted_merge_sort_aux st l :
+    merge_stack_Sorted st → Sorted R (merge_sort_aux R st l).
+  Proof.
+    revert st. induction l; simpl;
+      auto using Sorted_merge_stack, Sorted_merge_list_to_stack.
+  Qed.
+  Lemma merge_sort_aux_Permutation st l :
+    merge_sort_aux R st l ≡ₚ merge_stack_flatten st ++ l.
+  Proof.
+    revert st. induction l as [|?? IH]; simpl; intros.
+    - by rewrite (right_id_L [] (++)), merge_stack_Permutation.
+    - rewrite IH, merge_list_to_stack_Permutation; simpl.
+      by rewrite Permutation_middle.
+  Qed.
+  Lemma Sorted_merge_sort l : Sorted R (merge_sort R l).
+  Proof. apply Sorted_merge_sort_aux. by constructor. Qed.
+  Lemma merge_sort_Permutation l : merge_sort R l ≡ₚ l.
+  Proof. unfold merge_sort. by rewrite merge_sort_aux_Permutation. Qed.
+  Lemma StronglySorted_merge_sort `{!Transitive R} l :
+    StronglySorted R (merge_sort R l).
+  Proof. auto using Sorted_StronglySorted, Sorted_merge_sort. Qed.
+End merge_sort_correct.