From 9782eda99154f3358a3694fbaacdf95acd067bb5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 11 Jan 2021 20:07:31 +0100
Subject: [PATCH] Rename `seq_S_snoc` into `seq_S` to be consistent with Coq's
 stdlib.

---
 CHANGELOG.md            | 5 +++--
 theories/list_numbers.v | 5 +++--
 2 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6f854d69..39decbe9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -40,7 +40,8 @@ Coq 8.8 and 8.9 are no longer supported.
   returns `"0"` for `N`, `Z`, and `nat`.
 - Remove duplicate `map_fmap_empty` of `fmap_empty`, and rename
   `map_fmap_empty_inv` into `fmap_empty_inv` for consistency's sake.
-- Rename `seq_S_end_app` to `seq_S_snoc`.
+- Rename `seq_S_end_app` to `seq_S`. (The lemma `seq_S` is also in Coq's stdlib
+  since Coq 8.12.)
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
@@ -57,7 +58,7 @@ s/\bQp_mult_plus_distr_l\b/Qp_mul_add_distr_r/g
 s/\bQp_mult_plus_distr_r\b/Qp_mul_add_distr_l/g
 s/\bmap_fmap_empty\b/fmap_empty/g
 s/\bmap_fmap_empty_inv\b/fmap_empty_inv/g
-s/\bseq_S_end_app\b/seq_S_snoc/g
+s/\bseq_S_end_app\b/seq_S/g
 ' $(find theories -name "*.v")
 ```
 
diff --git a/theories/list_numbers.v b/theories/list_numbers.v
index af1b5a80..8fe24c17 100644
--- a/theories/list_numbers.v
+++ b/theories/list_numbers.v
@@ -67,9 +67,10 @@ Section seq.
   Qed.
   Lemma NoDup_seq j n : NoDup (seq j n).
   Proof. apply NoDup_ListNoDup, seq_NoDup. Qed.
-  Lemma seq_S_snoc j n : seq j (S n) = seq j n ++ [j + n].
+  (* FIXME: This lemma is in the stdlib since Coq 8.12 *)
+  Lemma seq_S n j : seq j (S n) = seq j n ++ [j + n].
   Proof.
-    revert j. induction n as [|n IH]; intros j; simpl in *; f_equal; [done |].
+    revert j. induction n as [|n IH]; intros j; f_equal/=; [done |].
     by rewrite IH, Nat.add_succ_r.
   Qed.
 
-- 
GitLab