Add lemma `StronglySorted_app_iff`

This merge request adds the lemma StronglySorted_app_iff (and the corollary StronglySorted_app), and rewrites the existing *_app lemmas as a corollary of StronglySorted_app_iff.

stdpp/sorting.v

@@ -2,6 +2,7 @@
 standard library, but without using the module system. *)
 From Coq Require Export Sorted.
 From stdpp Require Export orders list.
+From stdpp Require Import sets.
 From stdpp Require Import options.
 
 Section merge_sort.
@@ -48,25 +49,36 @@ 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.
+  Lemma StronglySorted_cons l x :
+    StronglySorted R (x :: l) ↔
+      Forall (R x) l ∧ StronglySorted R l.
+  Proof. split; [inv 1|constructor]; naive_solver. Qed.
+
+  Lemma StronglySorted_app l1 l2 :
+    StronglySorted R (l1 ++ l2) ↔
+      (∀ x1 x2, x1 ∈ l1 → x2 ∈ l2 → R x1 x2) ∧
+      StronglySorted R l1 ∧
+      StronglySorted R l2.
   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.
+    induction l1 as [|x1' l1 IH]; simpl.
+    - set_solver by eauto using SSorted_nil.
+    - rewrite !StronglySorted_cons, IH, !Forall_forall. set_solver.
   Qed.
-  Lemma StronglySorted_app_inv_l l1 l2 :
+  Lemma StronglySorted_app_2 l1 l2 :
+    (∀ x1 x2, x1 ∈ l1 → x2 ∈ l2 → R x1 x2) →
+    StronglySorted R l1 →
+    StronglySorted R l2 →
+    StronglySorted R (l1 ++ l2).
+  Proof. by rewrite StronglySorted_app. Qed.
+  Lemma StronglySorted_app_1_elem_of l1 l2 x1 x2 :
+    StronglySorted R (l1 ++ l2) → x1 ∈ l1 → x2 ∈ l2 → R x1 x2.
+  Proof. rewrite StronglySorted_app. naive_solver. Qed.
+  Lemma StronglySorted_app_1_l l1 l2 :
     StronglySorted R (l1 ++ l2) → StronglySorted R l1.
-  Proof.
-    induction l1 as [|x1' l1 IH]; simpl;
-      [|inv 1]; decompose_Forall; constructor; auto.
-  Qed.
-  Lemma StronglySorted_app_inv_r l1 l2 :
+  Proof. rewrite StronglySorted_app. naive_solver. Qed.
+  Lemma StronglySorted_app_1_r l1 l2 :
     StronglySorted R (l1 ++ l2) → StronglySorted R l2.
-  Proof.
-    induction l1 as [|x1' l1 IH]; simpl;
-      [|inv 1]; decompose_Forall; auto.
-  Qed.
+  Proof. rewrite StronglySorted_app. naive_solver. Qed.
 
   Lemma Sorted_StronglySorted `{!Transitive R} l :
     Sorted R l → StronglySorted R l.