Some results about `app` and `StronglySorted`.

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.