remove useless hypothesis in NoDup_Permutation_bis

(thanks to new NoDup_incl_NoDup)

3 files changed, 36 insertions, 2 deletions

diff --git a/doc/changelog/10-standard-library/12119-issue12119.rst b/doc/changelog/10-standard-library/12119-issue12119.rst
new file mode 100644
index 0000000000..42672b1465
--- /dev/null
+++ b/doc/changelog/10-standard-library/12119-issue12119.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+  new lemma ``NoDup_incl_NoDup`` in ``List.v``
+  to remove useless hypothesis `NoDup l'` in ``Sorting.Permutation.NoDup_Permutation_bis``
+  (`#12119 <https://github.com/coq/coq/pull/12119>`_,
+  by Olivier Laurent).
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index f050f11170..5d5f74db44 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -2559,6 +2559,33 @@ Section ReDun.
      * now apply incl_Add_inv with a l'.
   Qed.
 
+  Lemma NoDup_incl_NoDup (l l' : list A) : NoDup l ->
+    length l' <= length l -> incl l l' -> NoDup l'.
+  Proof.
+    revert l'; induction l; simpl; intros l' Hnd Hlen Hincl.
+    - now destruct l'; inversion Hlen.
+    - assert (In a l') as Ha by now apply Hincl; left.
+      apply in_split in Ha as [l1' [l2' ->]].
+      inversion_clear Hnd as [|? ? Hnin Hnd'].
+      apply (NoDup_Add (Add_app a l1' l2')); split.
+      + apply IHl; auto.
+        * rewrite app_length.
+          rewrite app_length in Hlen; simpl in Hlen; rewrite Nat.add_succ_r in Hlen.
+          now apply Nat.succ_le_mono.
+        * apply incl_Add_inv with (u:= l1' ++ l2') in Hincl; auto.
+          apply Add_app.
+      + intros Hnin'.
+        assert (incl (a :: l) (l1' ++ l2')) as Hincl''.
+        { apply incl_tran with (l1' ++ a :: l2'); auto.
+          intros x Hin.
+          apply in_app_or in Hin as [Hin|[->|Hin]]; intuition. }
+        apply NoDup_incl_length in Hincl''; [ | now constructor ].
+        apply (Nat.nle_succ_diag_l (length l1' + length l2')).
+        rewrite_all app_length.
+        simpl in Hlen; rewrite Nat.add_succ_r in Hlen.
+        now transitivity (S (length l)).
+  Qed.
+
 End ReDun.
 
 (** NoDup and map *)
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index 86eebc6b4f..ffef8a216d 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -499,11 +499,13 @@ Proof.
        rewrite (NoDup_Add AD) in Hl'. tauto.
 Qed.
 
-Lemma NoDup_Permutation_bis l l' : NoDup l -> NoDup l' ->
+Lemma NoDup_Permutation_bis l l' : NoDup l ->
   length l' <= length l -> incl l l' -> Permutation l l'.
 Proof.
  intros. apply NoDup_Permutation; auto.
- split; auto. apply NoDup_length_incl; trivial.
+ - now apply NoDup_incl_NoDup with l.
+ - split; auto.
+   apply NoDup_length_incl; trivial.
 Qed.
 
 Lemma Permutation_NoDup l l' : Permutation l l' -> NoDup l -> NoDup l'.