Merge PR #12799: [stdlib] [List] Additional statements about List.repeat

Reviewed-by: anton-trunov

3 files changed, 54 insertions, 0 deletions

diff --git a/doc/changelog/10-standard-library/12799-list-repeat.rst b/doc/changelog/10-standard-library/12799-list-repeat.rst
new file mode 100644
index 0000000000..adfc48f67b
--- /dev/null
+++ b/doc/changelog/10-standard-library/12799-list-repeat.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  New lemmas about ``repeat`` in ``List`` and ``Permutation``: ``repeat_app``, ``repeat_eq_app``, ``repeat_eq_cons``, ``repeat_eq_elt``, ``Forall_eq_repeat``, ``Permutation_repeat``
+  (`#12799 <https://github.com/coq/coq/pull/12799>`_,
+  by Olivier Laurent).
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index c3c69f46f3..e0eae7c287 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -3157,6 +3157,44 @@ Section Repeat.
     - f_equal; apply IHn.
   Qed.
 
+  Lemma repeat_app x n m :
+    repeat x (n + m) = repeat x n ++ repeat x m.
+  Proof.
+    induction n as [|n IHn]; simpl; auto.
+    now rewrite IHn.
+  Qed.
+
+  Lemma repeat_eq_app x n l1 l2 :
+    repeat x n = l1 ++ l2 -> repeat x (length l1) = l1 /\ repeat x (length l2) = l2.
+  Proof.
+    revert n; induction l1 as [|a l1 IHl1]; simpl; intros n Hr; subst.
+    - repeat split; now rewrite repeat_length.
+    - destruct n; inversion Hr as [ [Heq Hr0] ]; subst.
+      now apply IHl1 in Hr0 as [-> ->].
+  Qed.
+
+  Lemma repeat_eq_cons x y n l :
+    repeat x n = y :: l -> x = y /\ repeat x (pred n) = l.
+  Proof.
+    intros Hr.
+    destruct n; inversion_clear Hr; auto.
+  Qed.
+
+  Lemma repeat_eq_elt x y n l1 l2 :
+    repeat x n = l1 ++ y :: l2 -> x = y /\ repeat x (length l1) = l1 /\ repeat x (length l2) = l2.
+  Proof.
+    intros Hr; apply repeat_eq_app in Hr as [Hr1 Hr2]; subst.
+    apply repeat_eq_cons in Hr2; intuition.
+  Qed.
+
+  Lemma Forall_eq_repeat x l :
+    Forall (eq x) l -> l = repeat x (length l).
+  Proof.
+    induction l as [|a l IHl]; simpl; intros HF; auto.
+    inversion_clear HF as [ | ? ? ? HF']; subst.
+    now rewrite (IHl HF') at 1.
+  Qed.
+
 End Repeat.
 
 Lemma repeat_to_concat A n (a:A) :
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index 026cf32ceb..2f445c341a 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -522,6 +522,18 @@ Proof.
   repeat red; eauto using Permutation_NoDup.
 Qed.
 
+Lemma Permutation_repeat x n l :
+  Permutation l (repeat x n) -> l = repeat x n.
+Proof.
+  revert n; induction l as [|y l IHl] ; simpl; intros n HP; auto.
+  - now apply Permutation_nil in HP; inversion HP.
+  - assert (y = x) as Heq by (now apply repeat_spec with n, (Permutation_in _ HP); left); subst.
+    destruct n; simpl; simpl in HP.
+    + symmetry in HP; apply Permutation_nil in HP; inversion HP.
+    + f_equal; apply IHl.
+      now apply Permutation_cons_inv with x.
+Qed.
+
 End Permutation_properties.
 
 Section Permutation_map.