Merge PR #13804: [stdlib] [List] Add results about count_occ

Reviewed-by: anton-trunov

4 files changed, 109 insertions, 3 deletions

diff --git a/doc/changelog/10-standard-library/13582-exp_ineq.rst b/doc/changelog/10-standard-library/13582-exp_ineq.rst
index 27d89b2f8b..ff4e8db8b0 100644
--- a/doc/changelog/10-standard-library/13582-exp_ineq.rst
+++ b/doc/changelog/10-standard-library/13582-exp_ineq.rst
@@ -4,6 +4,4 @@
   Adds exp_ineq1_le, which holds for all reals (but is a <= instead of a <).
 
   (`#13582 <https://github.com/coq/coq/pull/13582>`_,
-  by Avi Shinnar and Barry Trager, with help from Laurent Théry
-
-).
+  by Avi Shinnar and Barry Trager, with help from Laurent Théry).
diff --git a/doc/changelog/10-standard-library/13804-count_occ.rst b/doc/changelog/10-standard-library/13804-count_occ.rst
new file mode 100644
index 0000000000..9354b219d8
--- /dev/null
+++ b/doc/changelog/10-standard-library/13804-count_occ.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  Lemmas about ``count_occ``: ``count_occ_app``, ``count_occ_elt_eq``, ``count_occ_elt_neq``, ``count_occ_bound``, ``count_occ_repeat_eq``, ``count_occ_repeat_neq``, ``count_occ_unique``, ``count_occ_repeat_excl``, ``count_occ_sgt``, ``Permutation_count_occ``
+  (`#13804 <https://github.com/coq/coq/pull/13804>`_,
+  by Olivier Laurent with help of Jean-Christophe Léchenet).
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index d6277b3bb5..5298f3160a 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -877,6 +877,36 @@ Section Elts.
     intros H. simpl. now destruct (eq_dec x y).
   Qed.
 
+  Lemma count_occ_app l1 l2 x :
+    count_occ (l1 ++ l2) x = count_occ l1 x + count_occ l2 x.
+  Proof.
+    induction l1 as [ | h l1 IHl1]; cbn; auto.
+    now destruct (eq_dec h x); [ rewrite IHl1 | ].
+  Qed.
+
+  Lemma count_occ_elt_eq l1 l2 x y : x = y ->
+    count_occ (l1 ++ x :: l2) y = S (count_occ (l1 ++ l2) y).
+  Proof.
+    intros ->.
+    rewrite ? count_occ_app; cbn.
+    destruct (eq_dec y y) as [Heq | Hneq];
+      [ apply Nat.add_succ_r | now contradiction Hneq ].
+  Qed.
+
+  Lemma count_occ_elt_neq l1 l2 x y : x <> y ->
+    count_occ (l1 ++ x :: l2) y = count_occ (l1 ++ l2) y.
+  Proof.
+    intros Hxy.
+    rewrite ? count_occ_app; cbn.
+    now destruct (eq_dec x y) as [Heq | Hneq]; [ contradiction Hxy | ].
+  Qed.
+
+  Lemma count_occ_bound x l : count_occ l x <= length l.
+  Proof.
+    induction l as [|h l]; cbn; auto.
+    destruct (eq_dec h x); [ apply (proj1 (Nat.succ_le_mono _ _)) | ]; intuition.
+  Qed.
+
 End Elts.
 
 (*******************************)
@@ -3242,6 +3272,54 @@ Section Repeat.
     now rewrite (IHl HF') at 1.
   Qed.
 
+  Hypothesis decA : forall x y : A, {x = y}+{x <> y}.
+
+  Lemma count_occ_repeat_eq x y n : x = y -> count_occ decA (repeat y n) x = n.
+  Proof.
+    intros ->.
+    induction n; cbn; auto.
+    destruct (decA y y); auto.
+    exfalso; intuition.
+  Qed.
+
+  Lemma count_occ_repeat_neq x y n : x <> y -> count_occ decA (repeat y n) x = 0.
+  Proof.
+    intros Hneq.
+    induction n; cbn; auto.
+    destruct (decA y x); auto.
+    exfalso; intuition.
+  Qed.
+
+  Lemma count_occ_unique x l : count_occ decA l x = length l -> l = repeat x (length l).
+  Proof.
+    induction l as [|h l]; cbn; intros Hocc; auto.
+    destruct (decA h x).
+    - f_equal; intuition.
+    - assert (Hb := count_occ_bound decA x l).
+      rewrite Hocc in Hb.
+      exfalso; apply (Nat.nle_succ_diag_l _ Hb).
+  Qed.
+
+  Lemma count_occ_repeat_excl x l :
+    (forall y, y <> x -> count_occ decA l y = 0) -> l = repeat x (length l).
+  Proof.
+    intros Hocc.
+    apply Forall_eq_repeat, Forall_forall; intros z Hin.
+    destruct (decA z x) as [Heq|Hneq]; auto.
+    apply Hocc, count_occ_not_In in Hneq; intuition.
+  Qed.
+
+  Lemma count_occ_sgt l x : l = x :: nil <->
+    count_occ decA l x = 1 /\ forall y, y <> x -> count_occ decA l y = 0.
+  Proof.
+    split.
+    - intros ->; cbn; split; intros; destruct decA; subst; intuition.
+    - intros [Heq Hneq].
+      apply count_occ_repeat_excl in Hneq.
+      rewrite Hneq, count_occ_repeat_eq in Heq; trivial.
+      now rewrite Heq in Hneq.
+  Qed.
+
 End Repeat.
 
 Lemma repeat_to_concat A n (a:A) :
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index 45fb48ad5d..2bf54baef3 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -535,6 +535,32 @@ Proof.
       now apply Permutation_cons_inv with x.
 Qed.
 
+Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}.
+
+Lemma Permutation_count_occ l1 l2 :
+  Permutation l1 l2 <-> forall x, count_occ eq_dec l1 x = count_occ eq_dec l2 x.
+Proof.
+  split.
+  - induction 1 as [ | y l1 l2 HP IHP | y z l | l1 l2 l3 HP1 IHP1 HP2 IHP2 ];
+      cbn; intros a; auto.
+    + now rewrite IHP.
+    + destruct (eq_dec y a); destruct (eq_dec z a); auto.
+    + now rewrite IHP1, IHP2.
+  - revert l2; induction l1 as [|y l1 IHl1]; cbn; intros l2 Hocc.
+    + replace l2 with (@nil A); auto.
+      symmetry; apply (count_occ_inv_nil eq_dec); intuition.
+    + assert (exists l2' l2'', l2 = l2' ++ y :: l2'') as [l2' [l2'' ->]].
+      { specialize (Hocc y).
+        destruct (eq_dec y y); intuition.
+        apply in_split, (count_occ_In eq_dec).
+        rewrite <- Hocc; apply Nat.lt_0_succ. }
+      apply Permutation_cons_app, IHl1.
+      intros z; specialize (Hocc z); destruct (eq_dec y z) as [Heq | Hneq].
+      * rewrite (count_occ_elt_eq _ _ _ Heq) in Hocc.
+        now injection Hocc.
+      * now rewrite (count_occ_elt_neq _ _ _ Hneq) in Hocc.
+   Qed.
+
 End Permutation_properties.
 
 Section Permutation_map.