Merge branch 'marijnvanwezel/StronglySorted_app' into 'master'

Add lemma `StronglySorted_app_iff`

See merge request !584

CHANGELOG.md

@@ -14,6 +14,11 @@ 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)
+- Add lemmas `StronglySorted_app`, `StronglySorted_cons` and
+  `StronglySorted_app_2`. Rename lemmas
+  `elem_of_StronglySorted_app` → `StronglySorted_app_1_elem_of`,
+  `StronglySorted_app_inv_l` → `StronglySorted_app_1_l`
+  `StronglySorted_app_inv_r` → `StronglySorted_app_1_r`. (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`).
@@ -22,6 +27,9 @@ Note that the script is not idempotent, do not run it twice.
 sed -i -E -f- $(find theories -name "*.v") <<EOF
 # length
 s/\bmap_filter_empty_iff\b/map_empty_filter/g
+# StronglySorted
+s/\belem_of_StronglySorted_app\b/StronglySorted_app_1_elem_of/g
+s/\bStronglySorted_app_inv_(l|r)\b/StronglySorted_app_1_\1/g
 EOF
 ```
 

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.