From 0fb1c214ac9a0595762f9b3a2e6de4a82bba459d Mon Sep 17 00:00:00 2001
From: Kimaya Bedarkar <kbedarka@mpi-sws.org>
Date: Wed, 19 Feb 2025 14:22:34 +0100
Subject: [PATCH 1/3] add lemmas about seq

---
 CHANGELOG.md         |  3 ++-
 stdpp/list_numbers.v | 11 +++++++++++
 2 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 32d2f14c..e82c2830 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -12,7 +12,8 @@ API-breaking change is listed.
 - Rename `map_filter_empty_iff` to `map_empty_filter` and add
   `map_empty_filter_1` and `map_empty_filter_2`. (by Michael Sammler)
 - 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)
+ `length_zip`, `zip_nil_inv`, `lookup_zip_Some`,`lookup_zip_None`. (by Kimaya Bedarkar)
+- Add `elem_of_seq` and `seq_nil`. (by Kimaya Bedarkar)
 
 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/list_numbers.v b/stdpp/list_numbers.v
index 3333e22d..4d1b1b29 100644
--- a/stdpp/list_numbers.v
+++ b/stdpp/list_numbers.v
@@ -98,6 +98,16 @@ Section seq.
     k ∈ seq j n ↔ j ≤ k < j + n.
   Proof. rewrite elem_of_list_In, in_seq. done. Qed.
 
+  Lemma seq_nil n m:
+  seq n m = [] ↔
+  m = 0.
+  Proof. by induction n; induction m. Qed.
+
+  Lemma seq_subseteq m n1 n2 :
+    n1 ≤ n2 →
+    seq m n1 ⊆ seq m n2.
+  Proof. by intros Hle i Hi%elem_of_seq; apply elem_of_seq; lia. Qed.
+
   Lemma Forall_seq (P : nat → Prop) i n :
     Forall P (seq i n) ↔ ∀ j, i ≤ j < i + n → P j.
   Proof. rewrite Forall_forall. setoid_rewrite elem_of_seq. auto with lia. Qed.
@@ -118,6 +128,7 @@ Section seq.
     - rewrite take_nil. replace (m `min` 0) with 0 by lia. done.
     - destruct m; simpl; auto with f_equal.
   Qed.
+
 End seq.
 
 (** ** Properties of the [seqZ] function *)
-- 
GitLab


From ffcb6d4d2cde4e1ad7a189cfcd231ef32375fa8e Mon Sep 17 00:00:00 2001
From: Kimaya Bedarkar <kbedarka@mpi-sws.org>
Date: Thu, 20 Feb 2025 09:33:44 +0000
Subject: [PATCH 2/3] Apply 1 suggestion(s) to 1 file(s)

Co-authored-by: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
---
 stdpp/list_numbers.v | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/stdpp/list_numbers.v b/stdpp/list_numbers.v
index 4d1b1b29..7e79e81d 100644
--- a/stdpp/list_numbers.v
+++ b/stdpp/list_numbers.v
@@ -98,10 +98,8 @@ Section seq.
     k ∈ seq j n ↔ j ≤ k < j + n.
   Proof. rewrite elem_of_list_In, in_seq. done. Qed.
 
-  Lemma seq_nil n m:
-  seq n m = [] ↔
-  m = 0.
-  Proof. by induction n; induction m. Qed.
+  Lemma seq_nil n m : seq n m = [] ↔ m = 0.
+  Proof. by destruct m. Qed.
 
   Lemma seq_subseteq m n1 n2 :
     n1 ≤ n2 →
-- 
GitLab


From a91677691b980d0c59c8638e5b83ba7fd7debb68 Mon Sep 17 00:00:00 2001
From: Kimaya Bedarkar <kbedarka@mpi-sws.org>
Date: Thu, 20 Feb 2025 09:33:56 +0000
Subject: [PATCH 3/3] Apply 1 suggestion(s) to 1 file(s)

Co-authored-by: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
---
 stdpp/list_numbers.v | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/stdpp/list_numbers.v b/stdpp/list_numbers.v
index 7e79e81d..4489e5a8 100644
--- a/stdpp/list_numbers.v
+++ b/stdpp/list_numbers.v
@@ -101,9 +101,7 @@ Section seq.
   Lemma seq_nil n m : seq n m = [] ↔ m = 0.
   Proof. by destruct m. Qed.
 
-  Lemma seq_subseteq m n1 n2 :
-    n1 ≤ n2 →
-    seq m n1 ⊆ seq m n2.
+  Lemma seq_subseteq_mono m n1 n2 : n1 ≤ n2 → seq m n1 ⊆ seq m n2.
   Proof. by intros Hle i Hi%elem_of_seq; apply elem_of_seq; lia. Qed.
 
   Lemma Forall_seq (P : nat → Prop) i n :
-- 
GitLab