Add prime factorization (Factoring.v) and coprimality iff lemmas

doc/changelog/02-added/306-fable-factoring.rst

@@ -0,0 +1,25 @@
+- in `Zdivisibility.v`
+
+  + lemmas `Z.coprime_mul_l_iff`, `Z.coprime_mul_r_iff`, `Z.coprime_pow_l_iff`,
+    `Z.coprime_pow_r_iff` and `Z.coprime_prime_prime`
+    (`#306 <https://github.com/coq/stdlib/pull/306>`_,
+    by Andres Erbsen and Jason Gross).
+
+- in `Factoring.v`
+
+  + new file with the prime-power factorization `ppfactor`, the sorted prime
+    factorization `factor`, the `p`-adic valuation `val`, Euler's `totient`,
+    the fundamental theorem of arithmetic (`fundamental_theorem_of_arithmetic`
+    and its `Permutation` form) and the induction principles `factor_ind` and
+    `ppfactor_ind`
+    (`#306 <https://github.com/coq/stdlib/pull/306>`_,
+    by Andres Erbsen and Jason Gross).
+
+- in `List.v`, `Sorted.v` and `Permutation.v`
+
+  + lemmas `Forall_repeat`, `repeat_inj`, `Sorted_repeat`, `StronglySorted_app`,
+    `NoDup_StronglySorted`, `HdRel_map`, `Sorted_map`,
+    `StronglySorted_Permutation_unique`, `Sorted_Permutation_unique` and
+    `fold_right_Permutation`
+    (`#306 <https://github.com/coq/stdlib/pull/306>`_,
+    by Andres Erbsen and Jason Gross).

subcomponents/zmod.v

@@ -1,6 +1,7 @@
 From subcomponents Require zarith.
 From subcomponents Require sorting.
 From subcomponents Require field.
+From Stdlib Require ZArith.Factoring.
 From Stdlib Require Zmod.Bits.
 From Stdlib Require Zmod.Zmod.
 From Stdlib Require Zmod.Zstar.

test-suite/success/Factoring.v

@@ -0,0 +1,13 @@
+From Stdlib Require Import ZArith NArith List Factoring.
+Import ListNotations.
+Local Open Scope positive_scope.
+
+Goal ppfactor 24 = [(2, 3); (3, 1)]. Proof. vm_compute. reflexivity. Qed.
+Goal ppfactor 1 = []. Proof. vm_compute. reflexivity. Qed.
+Goal ppfactor 1311 = [(3, 1); (19, 1); (23, 1)]. Proof. vm_compute. reflexivity. Qed.
+Goal ppfactor (2^16+1) = [(65537, 1)]. Proof. vm_compute. reflexivity. Qed.
+Goal factor 360 = [2; 2; 2; 3; 3; 5]. Proof. vm_compute. reflexivity. Qed.
+Goal val 2 24 = 3%N. Proof. vm_compute. reflexivity. Qed.
+Goal val 5 24 = 0%N. Proof. vm_compute. reflexivity. Qed.
+Goal totient 20 = 8. Proof. vm_compute. reflexivity. Qed.
+Goal totient 97 = 96. Proof. vm_compute. reflexivity. Qed.

theories/All.v

@@ -384,6 +384,7 @@ From Stdlib Require Export Classes.RelationPairs.
 From Stdlib Require Export Sets.Ensembles.
 From Stdlib Require Export Sets.Relations_1.
 From Stdlib Require Export Sorting.Sorted.
+From Stdlib Require Export ZArith.Factoring.
 From Stdlib Require Export Sorting.SetoidList.
 From Stdlib Require Export Structures.EqualitiesFacts.
 From Stdlib Require Export Structures.OrdersLists.

theories/Lists/List.v

@@ -3819,6 +3819,16 @@ Section Repeat.
     - now rewrite repeat_length.
   Qed.
 
+  Lemma Forall_repeat (P : A -> Prop) x n : P x -> Forall P (repeat x n).
+  Proof. intros; induction n; cbn [repeat]; constructor; trivial. Qed.
+
+  Lemma repeat_inj (x y : A) n m :
+    repeat x n = repeat y m -> n = m /\ (x = y \/ n = 0).
+  Proof.
+    revert m; induction n as [|n IH]; intros [|m]; cbn [repeat]; try discriminate; auto.
+    intros [= -> ?%IH]; intuition auto.
+  Qed.
+
 End Repeat.
 Abbreviation repeat := repeat.
 

theories/Sorting/Permutation.v

@@ -894,6 +894,11 @@ Qed.
 
 End Permutation_transp.
 
+Lemma fold_right_Permutation [A B] (f : A -> B -> B)
+  (H : forall x y z, f x (f y z) = f y (f x z)) xs ys :
+  Permutation xs ys -> forall o, fold_right f o xs = fold_right f o ys.
+Proof. induction 1; cbn [fold_right]; intuition try congruence. Qed.
+
 (* begin hide *)
 #[deprecated(since="Stdlib 9.1", use=Permutation_app_comm )]
 Abbreviation Permutation_app_swap := Permutation_app_comm (only parsing).

theories/Sorting/Sorted.v

@@ -20,7 +20,7 @@
   The two notions are equivalent if the order is transitive.
 *)
 
-From Stdlib Require Import List Relations Relations_1.
+From Stdlib Require Import List Relations Relations_1 Permutation.
 
 (* Set Universe Polymorphism. *)
 
@@ -142,6 +142,79 @@ Section defs.
 
 End defs.
 
+Local Unset Implicit Arguments.
+
+Lemma Sorted_repeat [A] R (R_refl : forall x:A, R x x) x n : Sorted R (repeat x n).
+Proof.
+  apply StronglySorted_Sorted.
+  induction n; cbn [repeat]; constructor; auto using Forall_repeat.
+Qed.
+
+#[local] Hint Constructors StronglySorted : core.
+Lemma StronglySorted_app [A] R (xs ys : list A) :
+  StronglySorted R (xs ++ ys) <->
+  Forall (fun x => Forall (R x) ys) xs /\ StronglySorted R xs /\ StronglySorted R ys.
+Proof.
+  split.
+  { intros H; remember (xs++ys); generalize dependent ys; revert xs; induction H.
+    { intros ? ? []%eq_sym%app_eq_nil; subst; eauto. }
+    intros [|x xs] ys E; cbn [app] in *; subst; eauto.
+    injection E; clear E; intros; subst.
+    specialize (IHStronglySorted xs ys eq_refl) as (?&?&?).
+    rewrite Forall_app in *; intuition eauto. }
+  { apply and_ind; induction 1; apply and_ind; trivial.
+  inversion_clear 1; cbn; constructor; eauto.
+  eapply Forall_app; eauto. }
+Qed.
+
+Lemma NoDup_StronglySorted {A} R xs (R_irrefl : forall x:A, ~R x x)
+  (H : StronglySorted R xs) : NoDup xs.
+Proof.
+  induction H; constructor; trivial.
+  intro; eapply (R_irrefl a), Forall_forall; eauto.
+Qed.
+
+Lemma HdRel_map {A B} (f : A -> B) R x xs :
+  HdRel R (f x) (map f xs) <-> HdRel (fun a b => R (f a) (f b)) x xs.
+Proof.
+  induction xs as [|??[]]; split; inversion_clear 1; cbn [map]; constructor; eauto.
+Qed.
+
+Lemma Sorted_map {A B} (f : A -> B) R xs :
+  Sorted R (map f xs) <-> Sorted (fun a b => R (f a) (f b)) xs.
+Proof.
+  induction xs as [|??[]]; split; inversion_clear 1; cbn [map];
+    constructor; try eapply HdRel_map; eauto.
+Qed.
+
+Lemma StronglySorted_Permutation_unique [A] (R : A -> A -> Prop)
+  (R_asym : forall x y, R x y -> R y x -> x = y) xs ys
+  : StronglySorted R xs -> StronglySorted R ys -> Permutation xs ys -> xs = ys.
+Proof.
+  intros H; revert ys; induction H as [|x xs Hxs IH].
+  { intros ? ? ?%Permutation_nil; congruence. }
+  intros [|y ys].
+  { intros ? ?%Permutation_sym%Permutation_nil; congruence. }
+  inversion_clear 1; intros.
+  enough (x = y) as <- by (f_equal; eauto using Permutation_cons_inv); clear IH.
+  assert (Forall (fun v => x = v \/ R x v) (y::ys)) as E. {
+    eapply Permutation_Forall; try eassumption.
+    constructor. left. trivial. eauto using Forall_impl. }
+  inversion_clear E as []; intuition try congruence.
+  assert (Forall (fun v => y = v \/ R y v) (x::xs)) as E. {
+    eapply Permutation_Forall; try symmetry; try eassumption.
+    constructor. left. trivial. eauto using Forall_impl. }
+  inversion_clear E; intuition try congruence; eauto.
+Qed.
+
+Lemma Sorted_Permutation_unique [A] (R : A -> A -> Prop)
+  (R_trans : Relations_1.Transitive R) (R_asym : forall x y, R x y -> R y x -> x = y)
+  xs ys : Sorted R xs -> Sorted R ys -> Permutation xs ys -> xs = ys.
+Proof.
+  intros. eapply StronglySorted_Permutation_unique;
+    eauto using Sorted_StronglySorted.
+Qed.
+
 #[global]
 Hint Constructors HdRel : core.
 #[global]