From 7f43d3f22994b25d91105deb6749b23376c70f7e Mon Sep 17 00:00:00 2001
From: Marijn van Wezel <marijnvanwezel@gmail.com>
Date: Mon, 27 Jan 2025 12:26:34 +0100
Subject: [PATCH 1/4] Add lemma `StronglySorted_app`

---
 CHANGELOG.md    |  4 ++++
 stdpp/sorting.v | 49 ++++++++++++++++++++++++++++++++++++-------------
 2 files changed, 40 insertions(+), 13 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index e82c2830..b7136e10 100644
--- a/CHANGELOG.md
+++ b/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`).
diff --git a/stdpp/sorting.v b/stdpp/sorting.v
index c5d4d95f..f888675e 100644
--- a/stdpp/sorting.v
+++ b/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.
-- 
GitLab


From 55e93ffd7e07e425e51d13e11edb2f681f574924 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 24 Feb 2025 14:42:46 +0100
Subject: [PATCH 2/4] Renames and make use of `set_solver` to shorten proof.

---
 stdpp/sorting.v | 50 +++++++++++++++++++------------------------------
 1 file changed, 19 insertions(+), 31 deletions(-)

diff --git a/stdpp/sorting.v b/stdpp/sorting.v
index f888675e..57f050a7 100644
--- a/stdpp/sorting.v
+++ b/stdpp/sorting.v
@@ -1,7 +1,7 @@
 (** Merge sort. Adapted from the implementation of Hugo Herbelin in the Coq
 standard library, but without using the module system. *)
 From Coq Require Export Sorted.
-From stdpp Require Export orders list.
+From stdpp Require Export orders list sets.
 From stdpp Require Import options.
 
 Section merge_sort.
@@ -48,48 +48,36 @@ Inductive TlRel {A} (R : relation A) (a : A) : list A → Prop :=
 Section sorted.
   Context {A} (R : relation A).
 
-  Lemma StronglySorted_app_iff l1 l2 :
-    StronglySorted R (l1 ++ l2) ↔ 
+  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; 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.
+    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 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_iff. Qed.
-  Lemma elem_of_StronglySorted_app l1 l2 x1 x2 :
+  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_iff. naive_solver. Qed.
-  Lemma StronglySorted_app_inv_l l1 l2 :
+  Proof. rewrite StronglySorted_app. naive_solver. Qed.
+  Lemma StronglySorted_app_1_l l1 l2 :
     StronglySorted R (l1 ++ l2) → StronglySorted R l1.
-  Proof. rewrite StronglySorted_app_iff. naive_solver. 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. rewrite StronglySorted_app_iff. naive_solver. Qed.
+  Proof. rewrite StronglySorted_app. naive_solver. Qed.
 
   Lemma Sorted_StronglySorted `{!Transitive R} l :
     Sorted R l → StronglySorted R l.
-- 
GitLab


From 80ff9d7b2a9f45f8e76a4ae1c8fc001f7b591ad6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 24 Feb 2025 14:48:57 +0100
Subject: [PATCH 3/4] Tweak CHANGELOG.

---
 CHANGELOG.md | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index b7136e10..a685028c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -15,9 +15,11 @@ API-breaking change is listed.
  `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)
+- 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`).
@@ -26,6 +28,8 @@ 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
+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
 ```
 
-- 
GitLab


From 7d1f381e7ee2c7183954bed59b44cb70143af4ca Mon Sep 17 00:00:00 2001
From: marijnvanwezel <marijnvanwezel@gmail.com>
Date: Tue, 25 Feb 2025 18:20:44 +0100
Subject: [PATCH 4/4] Tweak imports

---
 CHANGELOG.md    | 2 +-
 stdpp/sorting.v | 3 ++-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a685028c..516c417e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -14,7 +14,6 @@ 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 lemmas `StronglySorted_app`, `StronglySorted_cons` and
   `StronglySorted_app_2`. Rename lemmas
   `elem_of_StronglySorted_app` → `StronglySorted_app_1_elem_of`,
@@ -28,6 +27,7 @@ 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
diff --git a/stdpp/sorting.v b/stdpp/sorting.v
index 57f050a7..f1f787f2 100644
--- a/stdpp/sorting.v
+++ b/stdpp/sorting.v
@@ -1,7 +1,8 @@
 (** Merge sort. Adapted from the implementation of Hugo Herbelin in the Coq
 standard library, but without using the module system. *)
 From Coq Require Export Sorted.
-From stdpp Require Export orders list sets.
+From stdpp Require Export orders list.
+From stdpp Require Import sets.
 From stdpp Require Import options.
 
 Section merge_sort.
-- 
GitLab