diff --git a/theories/sorting.v b/theories/sorting.v index d9150c6079b15bf8da83a669852e93a26b14a755..f01fb49301dafc638672f7911b735421212cf76c 100644 --- a/theories/sorting.v +++ b/theories/sorting.v @@ -41,6 +41,11 @@ Section merge_sort. Definition merge_sort : list A → list A := merge_sort_aux []. End merge_sort. +(** Helper definition for [Sorted_reverse] below *) +Inductive TlRel {A} (R : relation A) (a : A) : list A → Prop := + | TlRel_nil : TlRel R a [] + | TlRel_cons b l : R b a → TlRel R a (l ++ [b]). + (** ** Properties of the [Sorted] and [StronglySorted] predicate *) Section sorted. Context {A} (R : relation A). @@ -112,8 +117,28 @@ Section sorted. rewrite ?Forall_fmap; eauto using Forall_impl. Qed. End fmap. + + Lemma HdRel_reverse l x : HdRel R x l → TlRel (flip R) x (reverse l). + Proof. destruct 1; rewrite ?reverse_cons; by constructor. Qed. + + Lemma Sorted_snoc l x : Sorted R l → TlRel R x l → Sorted R (l ++ [x]). + Proof. + induction 1 as [|y l Hsort IH Hhd]; intros Htl; simpl. + { repeat constructor. } + constructor. apply IH. + - inversion Htl as [|? [|??]]; simplify_list_eq; by constructor. + - destruct Hhd; constructor; [|done]. + inversion Htl as [|? [|??]]; by try discriminate_list. + Qed. End sorted. +Lemma Sorted_reverse {A} (R : relation A) l : + Sorted R l → Sorted (flip R) (reverse l). +Proof. + induction 1; rewrite ?reverse_nil, ?reverse_cons; + auto using Sorted_snoc, HdRel_reverse. +Qed. + (** ** Correctness of merge sort *) Section merge_sort_correct. Context {A} (R : relation A) `{∀ x y, Decision (R x y)}.