From 8dfc99835b180664ce4a458e96ce5151a7441bb5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 27 Jun 2019 22:51:50 +0200
Subject: [PATCH] Prove `Sorted_reverse`.

---
 theories/sorting.v | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

diff --git a/theories/sorting.v b/theories/sorting.v
index d9150c60..f01fb493 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)}.
-- 
GitLab