Add Euler's criterion and quadratic reciprocity for Zmod

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).

doc/changelog/02-added/307-fable-zmod-reciprocity.rst

@@ -0,0 +1,22 @@
+- in `QuadraticReciprocity.v`
+
+  + new file with Euler's criterion for `Zstar` and `Zmod`
+    (`Zstar.euler_criterion`, `Zmod.euler_criterion`), the product of all
+    units modulo a prime (`Zstar.prod_elements_prime`), the Chinese remainder
+    decomposition of `Zmod.elements` and `Zstar.elements` for coprime moduli
+    (`CRT.Zmod.elements_mul_coprime`, `CRT.Zstar.elements_mul_coprime`) and
+    the law of quadratic reciprocity
+    (`Reciprocity.Zstar.quadratic_reciprocity'`)
+    (`#307 <https://github.com/coq/stdlib/pull/307>`_,
+    by Andres Erbsen and Jason Gross).
+
+- in `List.v`, `Finite.v`, `Permutation.v`, `Zdiv.v` and `Zdivisibility.v`
+
+  + lemmas `filter_filter`, `negb_existsb`, `existsb_as_filter`,
+    `list_prod_nil_l`, `list_prod_cons_l`, `list_prod_map_l`,
+    `list_prod_map_r`, `list_prod_map_map`, `list_prod_filter_l`,
+    `list_prod_filter_r`, `list_prod_filter_filter`, `NoDup_list_prod`,
+    `Permutation_partition`, `Z.mod_prod_mod_factor_l`,
+    `Z.mod_prod_mod_factor_r` and `Z.coprime_comm`
+    (`#307 <https://github.com/coq/stdlib/pull/307>`_,
+    by Andres Erbsen and Jason Gross).

subcomponents/zmod.v

@@ -1,6 +1,8 @@
 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.
+From Stdlib Require Zmod.QuadraticReciprocity.

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

@@ -356,6 +356,7 @@ From Stdlib Require Export Zmod.ZmodInv.
 From Stdlib Require Export Zmod.ZmodNsatz.
 From Stdlib Require Export Zmod.Zmod.
 From Stdlib Require Export Zmod.Zstar.
+From Stdlib Require Export Zmod.QuadraticReciprocity.
 From Stdlib Require Export Zmod.Bits.
 From Stdlib Require Export ZArith.Zwf.
 From Stdlib Require Export ZArith.Zquot.
@@ -384,6 +385,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/Finite.v

@@ -86,6 +86,14 @@ Proof.
  rewrite in_map_iff. intros (y & E & Y). apply Ij in E; auto; congruence.
 Qed.
 
+Lemma NoDup_list_prod [A B] l l' : NoDup l -> NoDup l' -> NoDup (@list_prod A B l l').
+Proof.
+  intros H G; induction H; intros; cbn [list_prod]; [constructor|].
+  apply NoDup_app; trivial.
+  { eapply Injective_map_NoDup, G. inversion 1; trivial. }
+  intros [] (?&[-> ->]%pair_equal_spec&?)%in_map_iff []%in_prod_iff; tauto.
+Qed.
+
 Lemma Injective_list_carac A B (d:decidable_eq A)(f:A->B) :
   Injective f <-> (forall l, NoDup l -> NoDup (map f l)).
 Proof.

theories/Lists/List.v

@@ -1702,6 +1702,24 @@ End Fold_Right_Recursor.
 
   End Bool.
 
+Lemma filter_filter [A] f g (l : list A) : filter f (filter g l) = filter (fun x => f x && g x) l.
+Proof.
+  induction l; cbn [filter]; trivial.
+  case g; cbn [filter]; case f; cbn [andb]; congruence.
+Qed.
+
+Lemma negb_existsb [A] f (l : list A) : negb (existsb f l) = forallb (fun x => negb (f x)) l.
+Proof.
+  induction l; cbn [negb orb existsb forallb]; trivial.
+  case f; rewrite ?IHl; trivial.
+Qed.
+
+Lemma existsb_as_filter [A] f (l : list A) : existsb f l = negb (length (filter f l) =? 0)%nat.
+Proof.
+  induction l; trivial.
+  cbn [existsb filter]; case f; rewrite ?IHl; trivial.
+Qed.
+
 
   (*******************************)
   (** ** Further filtering facts *)
@@ -1989,6 +2007,51 @@ End Fold_Right_Recursor.
     Proof. induction l; intros; cbn; rewrite ?IHl; trivial. Qed.
   End ListPairs.
 
+Lemma list_prod_nil_l [A B] l : @list_prod A B nil l = nil.
+Proof. trivial. Qed.
+Lemma list_prod_cons_l [A B] (x : A) l (l' : list B) :
+  list_prod (x::l) l' = map (pair x) l' ++ list_prod l l'.
+Proof. trivial. Qed.
+Lemma list_prod_map_l [A A' B] (f : A -> A') l (l' : list B) :
+  list_prod (map f l) l' = map (fun '(a, b) => (f a, b)) (list_prod l l').
+Proof.
+  induction l; rewrite ?list_prod_cons, ?map_cons, ?list_prod_cons_l,
+    ?map_app, ?map_map, ?IHl; trivial.
+Qed.
+Lemma list_prod_map_r [A B B'] (f : B -> B') (l : list A) l' :
+  list_prod l (map f l') = map (fun '(a, b) => (a, f b)) (list_prod l l').
+Proof.
+  induction l; rewrite ?list_prod_cons, ?map_cons, ?list_prod_cons_l,
+    ?map_app, ?map_map, ?IHl; trivial.
+Qed.
+Lemma list_prod_map_map [A A' B B'] (f : A -> A') (g : B -> B') l l' :
+  list_prod (map f l) (map g l') = map (fun '(x, y) => (f x, g y)) (list_prod l l').
+Proof.
+  rewrite list_prod_map_l, list_prod_map_r, ?map_map; apply map_ext.
+  intros []; trivial.
+Qed.
+Lemma list_prod_filter_l [A B] (f : A -> _) l (l' : list B) :
+  list_prod (filter f l) l' = filter (fun p => f (fst p)) (list_prod l l').
+Proof.
+  induction l; cbn [filter list_prod]; trivial.
+  rewrite filter_app, filter_map_swap; cbn [fst].
+  case f; rewrite ?filter_true, ?filter_false; cbn [list_prod map];
+  rewrite ?IHl; auto.
+Qed.
+Lemma list_prod_filter_r [A B] (f : B -> _) (l : list A) l' :
+  list_prod l (filter f l') = filter (fun p => f (snd p)) (list_prod l l').
+Proof.
+  induction l; cbn [filter list_prod]; trivial.
+  rewrite filter_app, filter_map_swap; cbn [snd].
+  rewrite ?IHl; f_equal.
+Qed.
+Lemma list_prod_filter_filter [A B] f g (l : list A) (l' : list B) :
+  list_prod (filter f l) (filter g l') = filter (fun '(x, y) => f x && g y) (list_prod l l').
+Proof.
+  rewrite list_prod_filter_l, list_prod_filter_r, ?filter_filter.
+  apply filter_ext; intros []; trivial.
+Qed.
+
 
 
 
@@ -3819,6 +3882,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,17 @@ 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.
+
+Lemma Permutation_partition [A] f (l : list A) : Permutation l (fst (partition f l) ++ snd (partition f l)).
+Proof.
+  induction l; cbn [partition]; trivial.
+  case partition eqn:?, f; cbn [fst snd app]; eauto using Permutation_cons_app.
+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]