Add lemma `StronglySorted_app`

CHANGELOG.md

@@ -14,6 +14,10 @@ API-breaking change is listed.
 - Add lemma about `zip_with`: `lookup_zip_with_None` and add lemmas for `zip`:
  `length_zip`, `zip_nil_inv`, `lookup_zip_Some`,`lookup_zip_None`. (by Kimaya Bedarkar)
 - Add `elem_of_seq` and `seq_nil`. (by Kimaya Bedarkar)
+  `length_zip`, `zip_nil_inv`, `lookup_zip_Some`,`lookup_zip_None`. (by Kimaya Bedarkar)
+- Add lemma `StronglySorted_app`. (by Marijn van Wezel)
+- Add lemmas `StronglySorted_app_iff` and `StronglySorted_app`. (by Marijn van
+  Wezel)
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).

stdpp/sorting.v

@@ -48,25 +48,48 @@ 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_app_iff 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; split.
+    - intros Hs. repeat split; [|constructor|naive_solver].
+      by setoid_rewrite elem_of_nil.
+    - naive_solver.
+    - intros [Hs Hall]%StronglySorted_inv. split.
+      * intros ? ? Hinl1 Hinl2.
+        apply elem_of_cons in Hinl1 as [Hinl1|Hinl1].
+        + subst. apply Forall_app in Hall as [_ Hall].
+          rewrite Forall_forall in Hall. by apply Hall.
+        + apply IH in Hs as (HR & ? & ?). by apply HR.
+      * repeat split; [apply SSorted_cons|]; apply IH in Hs.
+        + naive_solver.
+        + apply Forall_app in Hall; naive_solver.
+        + naive_solver.
+    - intros (HR & [? ?]%StronglySorted_inv & ?). apply SSorted_cons.
+      * apply IH; [|done..]. repeat split; [|done..].
+        intros; apply HR; [|done]. apply elem_of_cons. naive_solver.
+      * rewrite Forall_app; split; [done|].
+        rewrite Forall_forall. intros; apply HR; [|done].
+        apply elem_of_cons. naive_solver.
   Qed.
+  Lemma StronglySorted_app 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_iff. Qed.
+  Lemma elem_of_StronglySorted_app l1 l2 x1 x2 :
+    StronglySorted R (l1 ++ l2) → x1 ∈ l1 → x2 ∈ l2 → R x1 x2.
+  Proof. rewrite StronglySorted_app_iff. 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;
-      [|inv 1]; decompose_Forall; constructor; auto.
-  Qed.
+  Proof. rewrite StronglySorted_app_iff. naive_solver. Qed. 
   Lemma StronglySorted_app_inv_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_iff. naive_solver. Qed.
 
   Lemma Sorted_StronglySorted `{!Transitive R} l :
     Sorted R l → StronglySorted R l.