From 5f2a6b77c07004cb46379de3ccc07310094cbeec Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 5 Jul 2019 20:25:38 +0200
Subject: [PATCH] Some results about `app` and `StronglySorted`.

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

diff --git a/theories/sorting.v b/theories/sorting.v
index f01fb493..27cb04e9 100644
--- a/theories/sorting.v
+++ b/theories/sorting.v
@@ -50,6 +50,26 @@ Inductive TlRel {A} (R : relation A) (a : A) : list A → Prop :=
 Section sorted.
   Context {A} (R : relation A).
 
+  Lemma elem_of_StronglySorted_app l1 l2 x1 x2 :
+    StronglySorted R (l1 ++ l2) → x1 ∈ l1 → x2 ∈ l2 → R x1 x2.
+  Proof.
+    induction l1 as [|x1' l1 IH]; simpl; [by rewrite elem_of_nil|].
+    intros [? Hall]%StronglySorted_inv [->|?]%elem_of_cons ?; [|by auto].
+    rewrite Forall_app, !Forall_forall in Hall. naive_solver.
+  Qed.
+  Lemma StronglySorted_app_inv_l l1 l2 :
+    StronglySorted R (l1 ++ l2) → StronglySorted R l1.
+  Proof.
+    induction l1 as [|x1' l1 IH]; simpl;
+      [|inversion_clear 1]; decompose_Forall; constructor; auto.
+  Qed.
+  Lemma StronglySorted_app_inv_r l1 l2 :
+    StronglySorted R (l1 ++ l2) → StronglySorted R l2.
+  Proof.
+    induction l1 as [|x1' l1 IH]; simpl;
+      [|inversion_clear 1]; decompose_Forall; auto.
+  Qed.
+
   Lemma Sorted_StronglySorted `{!Transitive R} l :
     Sorted R l → StronglySorted R l.
   Proof. by apply Sorted.Sorted_StronglySorted. Qed.
-- 
GitLab