diff --git a/prelude/sorting.v b/prelude/sorting.v new file mode 100644 index 0000000000000000000000000000000000000000..aca5122e060d55dd0843bf35b28c93c3e70366dd --- /dev/null +++ b/prelude/sorting.v @@ -0,0 +1,203 @@ +(* 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 iris.prelude 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.