From 9fc63eecb78da9710d76d71e32cef53067cca50f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 17 Sep 2026 14:40:57 +0000 Subject: [PATCH 1/2] Add prime factorization (Factoring.v) and coprimality iff lemmas Factoring.v comes from Andres Erbsen's WIP ZmodSqrt branch (andres-erbsen/stdlib@5bd6d0db, theories/ZArith/Factoring.v). It defines the p-adic valuation `val`, the prime-power factorization `ppfactor`, the sorted prime factorization `factor` and Euler's `totient` on positive numbers, all computable, and proves the fundamental theorem of arithmetic together with the induction principles `factor_ind` and `ppfactor_ind`. The two unfinished scratch lemmas of the WIP (`in_ppfactor`, `val_ext`) are left out. Zdivisibility.v gains `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`, which the same WIP used. The generic list lemmas it needed go to their natural homes: `Forall_repeat` and `repeat_inj` in List.v; `Sorted_repeat`, `StronglySorted_app`, `NoDup_StronglySorted`, `HdRel_map`, `Sorted_map`, `StronglySorted_Permutation_unique` and `Sorted_Permutation_unique` in Sorted.v (which now requires Permutation); `fold_right_Permutation` in Permutation.v. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm --- .../02-added/306-fable-factoring.rst | 25 + subcomponents/zmod.v | 1 + test-suite/success/Factoring.v | 13 + theories/All.v | 1 + theories/Lists/List.v | 10 + theories/Sorting/Permutation.v | 5 + theories/Sorting/Sorted.v | 75 +- theories/ZArith/Factoring.v | 664 ++++++++++++++++++ theories/ZArith/Zdivisibility.v | 27 + 9 files changed, 820 insertions(+), 1 deletion(-) create mode 100644 doc/changelog/02-added/306-fable-factoring.rst create mode 100644 test-suite/success/Factoring.v create mode 100644 theories/ZArith/Factoring.v diff --git a/doc/changelog/02-added/306-fable-factoring.rst b/doc/changelog/02-added/306-fable-factoring.rst new file mode 100644 index 0000000000..f92f7dd63c --- /dev/null +++ b/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 `_, + 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 `_, + 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 `_, + by Andres Erbsen and Jason Gross). diff --git a/subcomponents/zmod.v b/subcomponents/zmod.v index ef281ee3db..addffe4e3c 100644 --- a/subcomponents/zmod.v +++ b/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. diff --git a/test-suite/success/Factoring.v b/test-suite/success/Factoring.v new file mode 100644 index 0000000000..9a79739302 --- /dev/null +++ b/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. diff --git a/theories/All.v b/theories/All.v index 0c3d3131e4..815ef5f1e1 100644 --- a/theories/All.v +++ b/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. diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 0af438550e..206fd0ae60 100644 --- a/theories/Lists/List.v +++ b/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. diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index d781adc7a9..f3ad02c576 100644 --- a/theories/Sorting/Permutation.v +++ b/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). diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v index 289a70c538..5f414dd1e8 100644 --- a/theories/Sorting/Sorted.v +++ b/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] diff --git a/theories/ZArith/Factoring.v b/theories/ZArith/Factoring.v new file mode 100644 index 0000000000..a070c20565 --- /dev/null +++ b/theories/ZArith/Factoring.v @@ -0,0 +1,664 @@ +From Corelib Require Import Program.Wf. +From Stdlib Require Import List Sorted Permutation Lists.Finite. Import ListNotations. +From Stdlib Require Import Zdivisibility ZArith Lia. +#[local] Open Scope positive_scope. +#[local] Coercion Z.pos : positive >-> Z. +#[local] Coercion N.pos : positive >-> N. +#[local] Coercion Z.of_N : N >-> Z. + +#[local] Lemma fst_pair [A B] a b : fst (@pair A B a b) = a. Proof. reflexivity. Qed. +#[local] Lemma snd_pair [A B] a b : snd (@pair A B a b) = b. Proof. reflexivity. Qed. + +Module Pos. + Definition of_N n : positive := match n with N.pos n => n | _ => xH end. + + Definition lt_dec a b : {a Lt} with + | Lt => left eq_refl | _ => right _ + end); abstract discriminate. + Defined. + + Lemma lt_wf : well_founded Pos.lt. + Proof. + unshelve eapply Morphisms_Prop.well_founded_morphism. + { exact (fun a b => N.lt a b). } + { repeat intro; hnf; lia. } + { eapply measure_wf with (R:=N.lt), N.lt_wf_0. } + Qed. + + Lemma gt_wf c : well_founded (fun a b : positive => b < a <= c). + Proof. + unshelve eapply Morphisms_Prop.well_founded_morphism. + { exact (fun a b => (b < a <= c)%N). } + { repeat intro; hnf; lia. } + { eapply measure_wf with (R:=(fun a b => (b < a <= c)%N)), N.gt_wf. } + Qed. + + Lemma divide_1_r a : (a | 1) <-> a = 1. + Proof. split. { inversion_clear 1. nia. } { intros []. exists 1. nia. } Qed. + + + Definition pow_N p n := + match n with + | N0 => xH + | Npos q => Pos.pow p q + end. + + Lemma Npos_pow_N p n : N.pos (Pos.pow_N p n) = N.pow p n. + Proof. cbv [pow_N]; case n; trivial. Qed. + + Definition pow_pred p q := Pos.pow_N p (Pos.pred_N q). + + Lemma Npos_pow_pred p q : N.pos (Pos.pow_pred p q) = N.pow p (Pos.pred_N q). + Proof. cbv [pow_pred pow_N]; case Pos.pred_N; trivial. Qed. +End Pos. + +Module N. + #[local] Open Scope N_scope. + Definition lt_dec a b : {a Lt} with + | Lt => left eq_refl | _ => right _ + end); abstract discriminate. + Defined. + + Lemma pos_of_N n : N.pos (Pos.of_N n) = N.max 1 n. + Proof. case n; cbn; lia. Qed. + + Lemma pos_of_N_pos n : N.lt 0 n -> N.pos (Pos.of_N n) = n. + Proof. case n; cbn; lia. Qed. + + Lemma pos_mul a b : N.pos (a * b) = N.mul a b. Proof. lia. Qed. + + Lemma divide_pos_pos (a b : positive) : N.divide a b <-> Pos.divide a b. + Proof. + split. + { destruct 1 as [x ?]. assert (0 < x)%N by nia. exists (Z.to_pos x). nia. } + { destruct 1 as [x ?]. assert (0 < x)%N by nia. exists (Z.to_pos x). nia. } + Qed. + + Lemma div_eucl_as_div_mod a b : N.div_eucl a b = (a / b, a mod b). + Proof. apply surjective_pairing. Qed. + + Lemma pos_div_eucl_pos_as_div_mod a (b : positive) : N.pos_div_eucl a b = (a / b, a mod b). + Proof. rewrite <- div_eucl_as_div_mod; trivial. Qed. +End N. + +Module Z. + Lemma pos_of_N n : Z.pos (Pos.of_N n) = Z.max 1 (Z.of_N n). + Proof. case n; cbn; lia. Qed. + + Import ZifyClasses. + #[global] Instance Op_Pos_of_N : UnOp Pos.of_N. + Proof. refine ({| TUOp x := Z.max 1 x ; TUOpInj x := _ |}). exact (pos_of_N x). Defined. + Add Zify UnOp Op_Pos_of_N. + + Lemma pos_of_N_pos (n : N) : Z.lt 0 n -> Z.pos (Pos.of_N n) = n. + Proof. lia. Qed. + + Lemma divide_pos_pos (a b : positive) : Z.divide a b <-> Pos.divide a b. + Proof. + split. + { destruct 1 as [x ?]. assert (0 < x)%Z by nia. exists (Z.to_pos x). nia. } + { destruct 1 as [x ?]. assert (0 < x)%Z by nia. exists (Z.to_pos x). nia. } + Qed. +End Z. + +(* ** [val p n] finds largest k s.t. [p^k] divides [n] *) + +#[local] Open Scope N_scope. + +#[local] Definition val_subterm p n (val : forall m, Pos.lt m n -> N) : N := + match N.pos_div_eucl n p with + | (N.pos m, 0) => if Pos.lt_dec m n then N.succ (val m ltac:(trivial)) else 0 + | _ => 0 + end. +Definition val (p : positive) : positive -> N := + Fix (Acc_intro_generator 64 Pos.lt_wf) _ (val_subterm p). + +Lemma val_step p n : val p n = ltac:( + let y := eval cbv beta delta [val_subterm] in (val_subterm p n (fun y _ => val p y)) in + exact y). +Proof. + cbv [val val_subterm]. + rewrite Init.Wf.Fix_eq; [reflexivity|]; intros. + repeat match goal with |- context[match ?x with _ => _ end] => destruct x end; + repeat (eapply H || f_equal || trivial). +Qed. + +Lemma val_1_r p : val p 1 = 0. +Proof. repeat (case p as []; trivial). Qed. + +Lemma val_1_l n : val 1 n = 0. +Proof. + rewrite val_step, N.pos_div_eucl_pos_as_div_mod, N.div_1_r, N.mod_1_r. + case Pos.lt_dec; lia. +Qed. + +Lemma val_0_iff' (p n : positive) : val p n = 0 <-> (p = xH \/ n mod p <> 0). +Proof. + rewrite val_step, N.pos_div_eucl_pos_as_div_mod. + repeat match goal with |- context[match ?x with _ => _ end] => destruct x eqn:? end; + zify; Z.to_euclidean_division_equations; nia. +Qed. + +Lemma val_0_iff p n (H : p <> xH) : val p n = 0 <-> n mod p <> 0. +Proof. rewrite val_0_iff'; lia. Qed. + +Lemma val_0_iff_divide p n (H : p <> xH) : val p n = 0 <-> ~ (p | n). +Proof. rewrite val_0_iff, N.Lcm0.mod_divide; trivial; reflexivity. Qed. + +Lemma val_mul p n (H : p <> xH) : val p (Pos.mul p n) = N.succ (val p n). +Proof. + rewrite val_step, N.pos_div_eucl_pos_as_div_mod. + rewrite N.pos_mul, N.mul_comm, N.div_mul, N.Div0.mod_mul by lia. + case Pos.lt_dec; nia. +Qed. + +Lemma val_mul_pow (p k n : positive) (H : p <> xH) : val p (p ^ k * n) = k + val p n. +Proof. + induction k using Pos.peano_ind; + rewrite ?Pos.pow_1_r, ?Pos.pow_succ_r, <-?Pos.mul_assoc, ?val_mul; lia. +Qed. + +Lemma divide_val (p n : positive) : (p ^ val p n | n). +Proof. + induction n using (well_founded_induction Pos.lt_wf); rewrite val_step; cbv [id]. + assert ((p ^ 0 | n)). { rewrite N.pow_0_r. apply N.divide_1_l. } + repeat match goal with |- context[match ?x with _ => _ end] => destruct x eqn:? end; trivial. + epose proof N.pos_div_eucl_spec _ _ as E. rewrite Heqp0 in E; subst; rewrite E. + rewrite N.pow_succ_r, ?N.add_0_r, N.mul_comm; try eapply N.mul_divide_cancel_r; eauto; lia. +Qed. + +Lemma divide'_val (p n : positive) : ( Pos.of_N (p ^ val p n) | n)%positive. +Proof. + case (divide_val p n) as [q Hq]. exists (Pos.of_N q). + enough (q * p ^ val p n = Pos.of_N q * Pos.of_N (p ^ val p n))%N by nia. + rewrite ?N.pos_of_N_pos; lia. +Qed. + +Lemma le_val_iff k p n (H : p <> xH) : k <= val p n <-> ( p^k | n ). +Proof. + split. + { case (divide_val p n) as [q ->]. exists (q*p^(val p n - k)). + rewrite <-N.mul_assoc, <-N.pow_add_r, N.sub_add; trivial. } + { inversion 1 as [[|q] ?]; case k as [|k] in *; try lia. + assert (n = q * p ^ k)%positive as -> by lia. + rewrite Pos.mul_comm, val_mul_pow; try lia. } +Qed. + +Lemma powdivide_as_val (p : positive) k (n : positive) : + (p^k | n) <-> (p = xH \/ k <= val p n). +Proof. + case (Pos.eq_dec p xH) as [->|]; + rewrite ?N.pow_1_l, ?le_val_iff by trivial; intuition apply N.divide_1_l. +Qed. + +Lemma val_iff k p n (H : p <> xH) : val p n = k <-> (p^k|n) /\ ~(p^N.succ k|n). +Proof. rewrite !powdivide_as_val; lia. Qed. + +Lemma divide_as_val (p : positive) (n : positive) : + (p | n) <-> (p = xH \/ 1 <= val p n). +Proof. rewrite <-(N.pow_1_r p). rewrite powdivide_as_val; lia. Qed. + +Lemma ndivide_val (p n : positive) (H : p <> xH) k (Hk : val p n < k) : ~ ( p ^ k | n). +Proof. rewrite <-le_val_iff; try lia. Qed. + +Lemma ndivide_val_succ (p n : positive) (H : p <> xH) : ~ ( p * p ^ val p n | n). +Proof. rewrite <-N.pow_succ_r, <-le_val_iff; try lia. Qed. + +Lemma ndivide_val_div (p n : positive) (H : p <> xH) : ~ ( p | n / p ^ val p n ). +Proof. + intros [x X]; case (divide_val p n) as [q Hq]. + rewrite Hq, N.div_mul in X by lia; rewrite X in Hq. + eapply (ndivide_val_succ p n); trivial; exists x; lia. +Qed. + +(** * Factorization into prime powers *) + +#[local] Open Scope positive_scope. + +Definition ppfactor_lt := MR Pos.lt (uncurry Pos.sub). + +Lemma ppfactor_wf : well_founded ppfactor_lt. +Proof. apply measure_wf, Pos.lt_wf. Qed. + +Definition ppfactor_subterm (n_i : positive * positive) (ppfactor : forall m_j, ppfactor_lt m_j n_i -> list (positive * positive)) + : list (positive * positive). +Proof. +simple refine ( + let n := fst n_i in let i := Pos.succ (snd n_i) in + if Pos.lt_dec n (i*i) then if Pos.eqb 1 n then [] else [(n, 1)] else + let k := val i n in + let j := if N.odd i then Pos.succ i else i in + if N.eq_dec 0 k then ppfactor (n, j) _ + else (i, Pos.of_N k) :: ppfactor (Pos.of_N (n/i^k), j) _); +clear ppfactor; abstract ( + cbv [ppfactor_lt MR uncurry]; subst n; destruct n_i as [n i']; cbn [fst snd] in *; try solve + [ subst i; case N.odd in *; lia + | case (divide'_val i n) as [q Eq]; case N.odd in *; zify; Z.div_mod_to_equations; nia]). +Defined. + +Definition ppfactor_rec : positive * positive -> list (positive * positive) := + Fix (Acc_intro_generator 64 ppfactor_wf) _ ppfactor_subterm. + +Lemma ppfactor_rec_step p : ppfactor_rec p = ltac:( + let y := eval cbv beta delta [ppfactor_subterm] in (ppfactor_subterm p (fun y _ => ppfactor_rec y)) in + exact y). +Proof. + cbv [ppfactor_rec ppfactor_subterm]. + rewrite Init.Wf.Fix_eq; [reflexivity|]; intros. + repeat match goal with |- context[match ?x with _ => _ end] => destruct x end; + repeat (eapply H || f_equal || trivial). +Defined. + +Definition ppfactor p := ppfactor_rec (p, 1). + +(* +Compute ppfactor 24. +Compute ppfactor 1311. +Compute ppfactor (2^16-1). +Compute ppfactor (2^16+1). +Time Compute ppfactor (2^32-1). (* 0.003s *) +Time Compute ppfactor (2^32+1). (* 0.02s *) +Time Compute ppfactor (2^31+1). (* 0.3s *) +Time Compute ppfactor (2^31-1). (* 0.6s *) +Time Compute ppfactor (2^46-1). (* 3.2s *) +*) + +Lemma fold_right_nil [A B] (f : B -> A -> A) a : fold_right f a nil = a. +Proof. reflexivity. Qed. + +Lemma fold_right_cons [A B] (f : B -> A -> A) a x xs : + fold_right f a (x::xs) = f x (fold_right f a xs). Proof. reflexivity. Qed. + +#[local] Abbreviation Π := (fold_right Pos.mul 1). + +Lemma prod_app ps qs : Π (ps ++ qs) = Π ps * Π qs. +Proof. induction ps; cbn [fold_right app]; rewrite ?IHps, ?Pos.mul_assoc, ?Pos.mul_1_l; trivial. Qed. + +Lemma prod_concat ps : Π (concat ps) = Π (map Π ps). +Proof. induction ps; cbn [fold_right concat map]; rewrite ?prod_app; congruence. Qed. + +Lemma prod_repeat q c : Π (repeat q (Pos.to_nat c)) = q ^ c. +Proof. + induction c using Pos.peano_ind; trivial. + rewrite ?Pos2Nat.inj_succ, ?Pos.pow_succ_r; cbn [repeat fold_right]; congruence. +Qed. + +Lemma divide_in_prod ps : Forall (fun p => (p | Π ps)) ps. +Proof. + induction ps; cbn [fold_right concat map]; constructor; trivial. + { apply Pos.divide_mul_l. exists 1. lia. } + { eapply Forall_impl; eauto; cbv beta; intros q [y ->]; exists (a*y); lia. } +Qed. + +Lemma prod_ppfactor_rec p i : Π (map (uncurry Pos.pow) (ppfactor_rec (p, i))) = p. +Proof. + change p with (fst (p, i)) at 2; + induction (p, i) as [[p' i']IH] using (well_founded_induction ppfactor_wf); + clear i p; rename p' into p; rewrite ppfactor_rec_step; cbn [fst snd]. + set (Pos.succ i') as i. + set (if N.odd _ then _ else _) as j; assert (i' < j) by (case N.odd in *; subst i; lia). + repeat match goal with |- context[match ?x with _ => _ end] => destruct x eqn:? end; + repeat (cbn [uncurry (* map -- Qed timeout *)]; rewrite ?fold_right_nil, ?fold_right_cons, ?map_cons); + rewrite ?IH; cbn [fst snd]; + try rapply ppfactor_subterm_subproof; try rapply ppfactor_subterm_subproof0; trivial; + try apply Pos.eqb_eq in Heqb; try lia. + case (divide_val i p) as [q Hq]. + rewrite Hq, N.div_mul, Pos.mul_comm by lia. + enough (Pos.of_N q * i ^ Pos.of_N (val i p) = p)%N by lia; + rewrite ?N.pos_of_N_pos; lia. +Qed. + +Lemma prod_ppfactor p : Π (map (uncurry Pos.pow) (ppfactor p)) = p. +Proof. apply prod_ppfactor_rec. Qed. + +Lemma Private_ppfactor_rec_correct + (n i : positive) (ps := map fst (ppfactor_rec (n, i))) : + (forall d, 1 < d -> (d | fst (n, i)) -> Pos.succ (snd (n, i)) <= d)%Z -> + StronglySorted Pos.lt ps /\ Forall (fun p => Z.prime (Z.pos p) /\ ( snd (n, i) < p <= fst (n, i))) ps. +Proof. + induction (n, i) as [[n' i']IH] using (well_founded_induction ppfactor_wf); + clear n i; rename n' into n; subst ps; rewrite ppfactor_rec_step; cbn [fst snd]. + intros I; case Pos.lt_dec as []. (* base case *) + { case (Pos.eqb_spec 1 n) as []; repeat split; cbn [map fst]; + intuition eauto using SSorted_cons, SSorted_nil; + try apply Forall_cons; try apply Forall_nil; split. + { split; [lia|]; intros a?[b ?]. + pose proof I a ltac:(lia) ltac:(exists b; lia). + pose proof I b ltac:(nia) ltac:(exists a; lia). nia. } + { pose proof (I n ltac:(lia) ltac:(reflexivity)); lia. } } + set (Pos.succ i') as i in *. (* bound variables *) + set (if N.odd _ then _ else _) as j'; + assert (j' = i'+1 \/ j'=i'+2) by (case N.odd in *; subst i; lia). + case (divide'_val i n) as [q Hq]. + set (val i n) as k in *. + assert (q = Pos.of_N (n / i ^ k)). { zify; Z.div_mod_to_equations; nia. } + assert (forall d, (1 < d)%Z -> (d | n) -> d <> i -> (Pos.succ j' <= d))%Z as I_. + { intros a ? [b ab] ?. pose proof (I a ltac:(lia) ltac:(exists b; trivial)). + case N.odd eqn:E; [|lia]. rewrite <-N.even_succ, N.even_spec in E. + case E as [j]. enough (a <> Pos.succ i) by lia; intro. + unshelve epose proof (I 2 _ ltac:(exists (b*j)%Z)); lia. } + case N.eq_dec as []; rewrite ?map_cons. + { case (IH (n, j') ltac:(try rapply ppfactor_subterm_subproof; trivial)) as (A&B); + clear IH; cbn [fst snd] in *. (* recursive case withot division *) + { intros; apply I_; trivial. (* invariant preserved: i wasn't a ppfactor *) + intros ->; case (proj1 (val_0_iff_divide i n ltac:(lia)) ltac:(lia)). + case H2 as [b ?]; exists (Z.to_N b); lia. } + eapply conj, Forall_impl; eauto; intuition lia. } + (* recursive case with division *) eassert (I' : _); try + case (IH (Pos.of_N (n / i ^ k), j') ltac:(rapply ppfactor_subterm_subproof0; trivial) I') as (A&B); + clear IH; rewrite ?fst_pair, ?snd_pair in * (* cbn -> Qed timeout *). + { (* invariant restored: i is no longer a facter *) + intros ? ? Hb; apply I_; trivial; case Hb as [b]. { exists (b*i^k)%Z; nia. } + intros->. subst k. apply (ndivide_val_succ i n); [|exists (Z.to_N b)];nia. } + eassert (O : _ ); [|split; constructor; [trivial|exact O|split;[|nia]| ] ]. + { (* range of recursive ppfactors *) epose proof divide_in_prod _ as D; + erewrite (prod_ppfactor_rec (Pos.of_N (n / i ^ k)) j'), Forall_map in D. + eapply Forall_map in B. epose proof Forall_and B D as F; cbv beta in *. + eapply Forall_map, Forall_impl, F; clear A D F; intros [f e] ([]&x&Hx); + cbv [fst snd uncurry] in *. + unshelve epose proof I f _ _; try nia. + exists (Pos.of_N (i ^ k)*x*(f^Pos.pred_N e))%N. + enough (f^e = f * f ^ Pos.pred_N e)%N by nia. + replace (N.pos e) with (N.succ (N.pred e)) by lia. + rewrite N.pow_succ_r'; f_equal; lia. } + { (* found a ppfactor *) split; try lia. + intros a ? [b]. unshelve epose proof I a _ ltac:(exists (q*a^(k-1)*b^k)%Z); try nia. + enough (i ^ k = (a * a ^ (k - 1)) * b ^ k :> Z)%Z by lia. + rewrite <-Z.pow_succ_r, Z.sub_1_r, Z.succ_pred, <-Z.pow_mul_l by lia; f_equal; lia. } + { eapply Forall_impl, B; intuition nia. } +Qed. + +Lemma Sorted_ppfactor n : Sorted Pos.lt (map fst (ppfactor n)). +Proof. eapply StronglySorted_Sorted, Private_ppfactor_rec_correct; cbn [fst snd]; lia. Qed. + +Lemma NoDup_ppfactor n : NoDup (ppfactor n). +Proof. + eapply NoDup_StronglySorted with (R:=fun a b=>fst a Z.prime (Z.pos p)). + +Lemma fst_ppfactor n : Forall (fun p => prime p /\ 2 <= p <= n) (map fst (ppfactor n)). +Proof. eapply Forall_impl, Private_ppfactor_rec_correct; cbn [fst snd]; intuition lia. Qed. + +Lemma prime_ppfactor n : Forall prime (map fst (ppfactor n)). +Proof. eapply Forall_impl, fst_ppfactor; cbv beta; intuition idtac. Qed. + +Lemma range_ppfactor n : Forall (fun p => 2 <= p <= n) (map fst (ppfactor n)). +Proof. eapply Forall_impl, fst_ppfactor; cbv beta; intuition idtac. Qed. + +Lemma ppfactor_inj a b (H : ppfactor a = ppfactor b) : a = b. +Proof. rewrite <-(prod_ppfactor a), <-(prod_ppfactor b); congruence. Qed. + +(** * Factorization into primes *) + +#[local] Abbreviation expand := (flat_map (fun '(p, k) => repeat p (Pos.to_nat k))). +Definition factor n := expand (ppfactor n). + +#[local] Lemma prod_expand xs : Π (expand xs) = Π (map (uncurry Pos.pow) xs). +Proof. + erewrite flat_map_concat_map, prod_concat, map_map, map_ext; trivial. + intros []; apply prod_repeat. +Qed. + +Lemma prod_factor n : Π (factor n) = n. +Proof. rewrite <-prod_ppfactor, <-prod_expand; trivial. Qed. + +#[local] Lemma Forall_expand [A] (P : A -> Prop) xs : + Forall P (expand xs) <-> Forall P (map fst xs). +Proof. + rewrite flat_map_concat_map, Forall_concat, !Forall_map, !Forall_forall. + split; intros H [] I; specialize (H _ I); cbn [fst] in *; + eauto using Forall_repeat. + destruct repeat eqn:? in H. + { apply (f_equal (@length _)) in Heql; rewrite repeat_length in Heql; + cbn [length] in Heql; lia. } + eapply repeat_eq_cons in Heql; intuition subst. inversion_clear H; trivial. +Qed. + +Lemma prime_factor n : Forall prime (factor n). +Proof. eapply Forall_expand, Forall_impl, prime_ppfactor; eauto. Qed. + +Lemma range_factor n : Forall (fun p => 2 <= p <= n) (factor n). +Proof. eapply Forall_expand, Forall_impl, range_ppfactor; eauto. Qed. + +Lemma Sorted_factor n : Sorted Pos.le (factor n). +Proof. + pose proof Sorted_ppfactor n as H. + eapply Sorted_StronglySorted in H; try rapply Pos.lt_trans. + cbv [factor]; set (ppfactor n) as pps in *; clearbody pps. + induction pps as [|[p k]]; cbn [repeat flat_map]; trivial. + inversion_clear H as [| x y Hsort Hlt ]. + eapply StronglySorted_Sorted, StronglySorted_app; repeat split; + try eapply Sorted_StronglySorted; try rapply Pos.le_trans; + eauto using Sorted_repeat, Pos.le_refl. + eapply Forall_forall; intros ? ->%repeat_spec. + eapply Forall_forall; intros q [[] [H ->%repeat_spec]]%in_flat_map. + eapply Forall_forall in Hlt; [|eapply in_map, H]; eauto using Pos.lt_le_incl. +Qed. + +Lemma factor_inj a b (H : factor a = factor b) : a = b. +Proof. rewrite <-(prod_factor a), <-(prod_factor b); congruence. Qed. + +(** Euler's totient function *) + +Definition totientpp p e := Pos.pow_pred p e * Pos.pred p. +Definition totient n := Π (map (uncurry totientpp) (ppfactor n)). + +(* +Compute totient 1. +Compute totient 9. +Compute totient 20. +Compute totient 80. +Compute totient 90. +Compute totient 352. +Time Compute totient (2^46-1). +*) + +(** * Fundamental theorem of arithmetic *) + +Lemma prime_product_1 ps : Forall prime ps -> Π ps = 1 -> ps = nil. +Proof. + destruct 1; cbn; intuition idtac. + eapply Z.prime_ge_2 in H. + nia. +Qed. + +Lemma prime_divisor_of_prime_product : + forall p qs, prime p -> Forall prime qs -> (p | Π qs)%Z -> In p qs. +Proof. + induction 2 as [|q qs]; cbn [fold_right]; intros. + { apply Z.prime_ge_2 in H; apply Z.divide_1_r_abs in H0; lia. } + rewrite Pos2Z.inj_mul in *. + case (Pos.eq_dec p q) as [->|]. { eauto using in_eq. } + eapply or_intror, IHForall, Z.gauss, Z.coprime_prime_prime; eauto; lia. +Qed. + +Lemma prime_divisor_of_prime_power_product q pps (Hq : prime q) + (Hp : Forall prime (map fst pps)) (Hd : (q | Π (map (uncurry Pos.pow) pps))%Z) + : In q (map fst pps). +Proof. + unshelve epose proof prime_divisor_of_prime_product q (expand pps) _ _ _ as H; + rewrite ?prod_expand; try apply Forall_expand; trivial. + rewrite in_flat_map in H; case H as ([p k]&?&->%repeat_spec). + apply in_map_iff; exists (p, k); eauto. +Qed. + +Lemma fundamental_theorem_of_arithmetic_Permutation' ps : + Forall prime ps -> forall qs, Forall prime qs -> Π ps = Π qs -> Permutation ps qs. +Proof. + induction 1 as [|p ps]; cbn [fold_right]; intros. + { eapply prime_product_1 in H; subst; trivial; lia. } + epose proof prime_divisor_of_prime_product p qs ltac:(trivial) ltac:(trivial) ltac:(exists(Π ps);lia). + eapply in_split in H3; case H3 as (qs0&qs1&?); subst qs. + eapply perm_trans, Permutation_middle; try apply perm_skip, IHForall. + { eapply Permutation_Forall in H1; try (symmetry; eapply Permutation_middle); + inversion_clear H1; trivial. } + { pose proof Z.prime_ge_2 _ H. + symmetry in H2; erewrite fold_right_Permutation in H2; + try (symmetry; eapply Permutation_middle); cbn [fold_right] in *; nia. } +Qed. + +Lemma fundamental_theorem_of_arithmetic_Permutation (a : positive) ps : + Forall prime ps -> Π ps = a -> Permutation ps (factor a). +Proof. + intros;eapply fundamental_theorem_of_arithmetic_Permutation'; + rewrite ?prod_factor; eauto using prime_factor. +Qed. + +Lemma fundamental_theorem_of_arithmetic (a : positive) ps : + Sorted Pos.le ps -> Forall prime ps -> Π ps = a -> ps = factor a. +Proof. + intros; eapply (Sorted_Permutation_unique Pos.le); + try eapply fundamental_theorem_of_arithmetic_Permutation; + eauto using Sorted_factor; cbv [Relations_1.Transitive]; lia. +Qed. + +Lemma factor_complete p n : prime p -> (p | n) -> In p (factor n). +Proof. + intros Hp [n' Hq]. + unshelve epose proof fundamental_theorem_of_arithmetic_Permutation n (p::factor n') _ _; + rewrite ?fold_right_cons, ?prod_factor; auto using prime_factor; try lia. + eauto using Permutation_in, in_eq. +Qed. + +Lemma factor_prime p (H : prime p) : factor p = [p]. +Proof. + symmetry; eapply fundamental_theorem_of_arithmetic; + auto; apply Pos.mul_1_r. +Qed. + +Lemma factor_prime_power p (H : prime p) k : + factor (p^k) = repeat p (Pos.to_nat k). +Proof. + symmetry; eapply fundamental_theorem_of_arithmetic; + auto using Sorted_repeat, Forall_repeat, Pos.le_refl, prod_repeat. +Qed. + +Lemma NoDup_ppfactor' n : NoDup (map (uncurry Pos.pow) (ppfactor n)). +Proof. + eapply Injective_map_NoDup_in, NoDup_ppfactor. + intros [p e] [q k]; cbn [uncurry]; intros A B E. + eapply Forall_forall in A; try eapply Forall_map, prime_ppfactor. + eapply Forall_forall in B; try eapply Forall_map, prime_ppfactor. + eapply (f_equal factor) in E; rewrite 2factor_prime_power in E by trivial. + eapply repeat_inj in E; intuition subst; f_equal; lia. +Qed. + +Lemma factor_mul_Permutation a b : Permutation (factor (a*b)) (factor a ++ factor b). +Proof. + rewrite <-(prod_factor a) at 1; rewrite <-(prod_factor b) at 1; + specialize (prime_factor b); specialize (prime_factor a). + intros. symmetry. eapply fundamental_theorem_of_arithmetic_Permutation. + { eapply Forall_app; eauto. } { rewrite ?prod_app, ?prod_factor; trivial. } +Qed. + +Lemma divide_factor n : Forall (fun d => (d | n)) (factor n). +Proof. + rewrite <-(prod_factor n); rewrite prod_factor at 1. + generalize (factor n) as xs; induction xs; + rewrite ?fold_right_nil, ?fold_right_cons; constructor. + { exists (Π xs). lia. } + { eapply Forall_impl, IHxs; intros x [y ?]; exists (a*y); lia. } +Qed. + +Lemma in_factor p n : In p (factor n) <-> prime p /\ (p | n). +Proof. + pose proof proj1 (Forall_forall _ _) (prime_factor n). + pose proof proj1 (Forall_forall _ _) (divide_factor n). + intuition auto using factor_complete. +Qed. + +Lemma disjoint_factor_coprime (a b : positive) (H : Pos.gcd a b = 1) + p (Ha : In p (factor a)) (Hb : In p (factor b)) : False. +Proof. + apply (f_equal Z.pos) in H; rewrite Pos2Z.inj_gcd in H. + pose proof (proj1 (Forall_forall _ _) (range_factor _)) _ Ha; cbv beta in *. + apply (proj1 (Forall_forall _ _) (divide_factor _)), Z.divide_Zpos in Ha. + apply (proj1 (Forall_forall _ _) (divide_factor _)), Z.divide_Zpos in Hb. + epose proof Z.gcd_greatest _ _ _ Ha Hb as D; rewrite H in *. + apply Z.divide_1_r in D; lia. +Qed. + +#[local] Opaque Z.gcd. + +Lemma factor_ind (P : positive -> Prop) + (init : P 1) + (step : forall n p, P n -> prime p -> + (forall q, prime q -> Z.divide q n -> q <= p) -> P (n * p)) + : forall n, P n. +Proof. + intros n; revert step; revert init. + rewrite <-(prod_factor n). + specialize (Sorted_factor n); cbv zeta. + specialize (prime_factor n); cbv zeta. + specialize (range_factor n); cbv zeta. + set (factor n) as ps; clearbody ps. + induction ps as [|p ps] using rev_ind; cbn; trivial. + rewrite prod_app; cbn [map fold_right]; rewrite Pos.mul_1_r. + intros [A H']%Forall_app [B H]%Forall_app C ? ?; inversion_clear H. + eapply Sorted_StronglySorted in C; try exact Pos.le_trans. + eapply StronglySorted_app in C; case C as (?&C&?). + eapply step; eauto; try eapply IHps; eauto using StronglySorted_Sorted. + intros q ? ?%prime_divisor_of_prime_product; eauto. + eapply Forall_forall in H; eauto. inversion_clear H; eauto. +Qed. + +Lemma N_factor_ind (P : N -> Prop) + (zero : P N0) + (init : P (N.pos 1)) + (step : forall n p, P n -> prime p -> + (forall q, prime q -> Z.divide q n -> q <= p) -> P (n * p)%N) + : forall n, P n. +Proof. + unshelve epose proof factor_ind (fun p => P p) _ _; cbv beta; eauto. + { intros. rewrite N.pos_mul; eauto. } + destruct n; eauto. +Qed. + +Lemma Z_factor_ind (P : Z -> Prop) + (zero : P Z0) + (init : P (Z.pos 1)) + (step : forall n p, P n -> prime p -> + (forall q, prime q -> Z.divide q n -> q <= p) -> P (n * p)%Z) + (opp : forall n : positive, P n -> P (Z.neg n)) + : forall n, P n. +Proof. + unshelve epose proof factor_ind (fun p => P p) _ _; cbv beta; eauto. + { intros. rewrite Pos2Z.inj_mul; eauto. } + destruct n; eauto. +Qed. + +Lemma ppfactor_ind (P : positive -> Prop) + (init : P 1) + (step : forall n p k, P n -> prime p -> Z.gcd n p = xH -> + (forall q, prime q -> Z.divide q n -> q < p) -> P (n * p ^ k)) + : forall n, P n. +Proof. + intros n; revert step; revert init. + rewrite <-(prod_ppfactor n). + specialize (Sorted_ppfactor n); cbv zeta. + specialize (prime_ppfactor n); cbv zeta. + specialize (range_ppfactor n); cbv zeta. + set (ppfactor n) as pps; clearbody pps. + induction pps as [|[p k]] using rev_ind; cbn; trivial. + rewrite map_app, map_cons; cbn [map]. + rewrite map_app, map_cons, prod_app; cbn [map fold_right uncurry]. + rewrite Pos.mul_1_r. + intros H H0 H1 **. + eapply Forall_app in H; case H as [? [[] _]%Forall_cons_iff]; cbn [fst snd] in *. + eapply Forall_app in H0; case H0 as [? [? _]%Forall_cons_iff]; cbn [fst snd] in *. + eapply Sorted_StronglySorted in H1; try exact Pos.lt_trans. + eapply StronglySorted_app in H1; case H1 as (?&?&?). + eapply step; eauto using Forall_app. + eapply IHpps; eauto using Forall_app; + try split; eauto using StronglySorted_Sorted. + { rewrite Z.gcd_comm. apply Z.coprime_prime_l; trivial. + intros X%prime_divisor_of_prime_power_product; trivial. + eapply Forall_forall in H1; eauto; inversion H1; lia. } + { intros q Hq Hd%prime_divisor_of_prime_power_product; trivial. + eapply Forall_forall in H1; eauto; inversion H1; trivial. } +Qed. diff --git a/theories/ZArith/Zdivisibility.v b/theories/ZArith/Zdivisibility.v index 1a3cfef4d0..e620986e27 100644 --- a/theories/ZArith/Zdivisibility.v +++ b/theories/ZArith/Zdivisibility.v @@ -90,6 +90,30 @@ Qed. Lemma coprime_pow_l a b n : 0 <= n -> coprime a b -> coprime (a ^ n) b. Proof. symmetry. apply coprime_pow_r; try symmetry; trivial. Qed. +Lemma coprime_mul_r_iff a b c : coprime a (b * c) <-> coprime a b /\ coprime a c. +Proof. + split; [|intros []; auto using coprime_mul_r]. + cbv [coprime]; intros H; split; + apply Z.divide_1_r_nonneg; auto using Z.gcd_nonneg; rewrite <-H; + apply Z.gcd_greatest; auto using Z.gcd_divide_l; + [apply Z.divide_mul_l|apply Z.divide_mul_r]; apply Z.gcd_divide_r. +Qed. + +Lemma coprime_mul_l_iff a b c : coprime (a * b) c <-> coprime a c /\ coprime b c. +Proof. + split; [|intros []; auto using coprime_mul_l]. + intros H; symmetry in H; apply coprime_mul_r_iff in H; intuition symmetry; trivial. +Qed. + +Lemma coprime_pow_r_iff a b n (Hn : 0 < n) : coprime a (b ^ n) <-> coprime a b. +Proof. + rewrite <-(Z.succ_pred n), Z.pow_succ_r, coprime_mul_r_iff by lia. + split; [intros []; trivial|]; intros; split; trivial; apply coprime_pow_r; trivial; lia. +Qed. + +Lemma coprime_pow_l_iff a b n (Hn : 0 < n) : coprime (a ^ n) b <-> coprime a b. +Proof. split; intros; symmetry; apply (coprime_pow_r_iff _ _ _ Hn); symmetry; trivial. Qed. + Definition prime p := 1 < p /\ forall n, 1 < n < p -> ~ (n|p). Existing Class prime. @@ -171,6 +195,9 @@ Proof. split; intros; subst; auto using Z.divide_refl, divide_prime_prime. Qed. +Lemma coprime_prime_prime p q (Hp : prime p) (Hq : prime q) (H : p <> q) : coprime p q. +Proof. apply coprime_prime_l; trivial; intros ?%divide_prime_prime; auto. Qed. + Theorem divide_prime_pp p q n (Hp : prime p) (Hq : prime q) (Hn : 0 <= n) : (p | q^n) -> p = q. Proof. From b27026e74d7313fb3b1c1f8c38b7f446c7ed4a3d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 17 Sep 2026 14:47:31 +0000 Subject: [PATCH 2/2] Add Euler's criterion and quadratic reciprocity for Zmod QuadraticReciprocity.v is the fully proved part of Andres Erbsen's WIP ZmodSqrt branch (andres-erbsen/stdlib@5bd6d0db, theories/Zmod/ZmodSqrt.v): the Chinese-remainder decomposition of `Zmod.elements` and `Zstar.elements` for coprime moduli, the product of all units modulo a prime (`prod_elements_prime`), Euler's criterion for `Zstar` and `Zmod`, and the law of quadratic reciprocity for odd primes (`quadratic_reciprocity'`). The square-root algorithms and their partially proved correctness lemmas are not included. The generic lemmas it needs move to their homes: `filter_filter`, `negb_existsb`, `existsb_as_filter` and the `list_prod` lemmas in List.v, `NoDup_list_prod` in Finite.v, `Permutation_partition` in Permutation.v, `Z.mod_prod_mod_factor_l/r` in Zdiv.v and `Z.coprime_comm` in Zdivisibility.v. The WIP's `Permutation_filter` already exists on master as a `Proper` instance. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm --- .../02-added/307-fable-zmod-reciprocity.rst | 22 + subcomponents/zmod.v | 1 + theories/All.v | 1 + theories/Lists/Finite.v | 8 + theories/Lists/List.v | 63 ++ theories/Sorting/Permutation.v | 6 + theories/ZArith/Zdiv.v | 6 + theories/ZArith/Zdivisibility.v | 3 + theories/Zmod/QuadraticReciprocity.v | 891 ++++++++++++++++++ 9 files changed, 1001 insertions(+) create mode 100644 doc/changelog/02-added/307-fable-zmod-reciprocity.rst create mode 100644 theories/Zmod/QuadraticReciprocity.v diff --git a/doc/changelog/02-added/307-fable-zmod-reciprocity.rst b/doc/changelog/02-added/307-fable-zmod-reciprocity.rst new file mode 100644 index 0000000000..1d3048a4db --- /dev/null +++ b/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 `_, + 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 `_, + by Andres Erbsen and Jason Gross). diff --git a/subcomponents/zmod.v b/subcomponents/zmod.v index addffe4e3c..fc5e6a3da9 100644 --- a/subcomponents/zmod.v +++ b/subcomponents/zmod.v @@ -5,3 +5,4 @@ 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. diff --git a/theories/All.v b/theories/All.v index 815ef5f1e1..cc5c118c5d 100644 --- a/theories/All.v +++ b/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. diff --git a/theories/Lists/Finite.v b/theories/Lists/Finite.v index b2fb5b87fb..dee25a34f8 100644 --- a/theories/Lists/Finite.v +++ b/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. diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 206fd0ae60..8b4a5e05b6 100644 --- a/theories/Lists/List.v +++ b/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. + diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index f3ad02c576..345803b962 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -899,6 +899,12 @@ Lemma fold_right_Permutation [A B] (f : A -> B -> B) 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). diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index ac1de41d9f..aecfd53d74 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -811,6 +811,12 @@ Proof. ring_simplify; trivial. Qed. +Lemma mod_prod_mod_factor_l x a b : x mod (a*b) mod a = x mod a. +Proof. apply mod_mod_divide; exists b; ring. Qed. + +Lemma mod_prod_mod_factor_r x a b : x mod (a*b) mod b = x mod b. +Proof. apply mod_mod_divide; exists a; ring. Qed. + Lemma mod_opp_mod_opp a b : - (-a mod b) mod b = a mod b. Proof. eapply cong_iff_0. diff --git a/theories/ZArith/Zdivisibility.v b/theories/ZArith/Zdivisibility.v index e620986e27..04d27c142d 100644 --- a/theories/ZArith/Zdivisibility.v +++ b/theories/ZArith/Zdivisibility.v @@ -49,6 +49,9 @@ Definition coprime_Bezout a b := proj2 (Bezout_coprime_iff a b). #[global] Instance Symmetric_coprime : RelationClasses.Symmetric coprime. Proof. cbv [coprime]; intros ? ? ?; rewrite Z.gcd_comm; trivial. Qed. +Lemma coprime_comm a b : coprime a b <-> coprime b a. +Proof. cbv [coprime]; rewrite Z.gcd_comm; reflexivity. Qed. + Lemma coprime_0_l_iff z : coprime 0 z <-> Z.abs z = 1. Proof. cbv [coprime]. rewrite Z.gcd_0_l. reflexivity. Qed. diff --git a/theories/Zmod/QuadraticReciprocity.v b/theories/Zmod/QuadraticReciprocity.v new file mode 100644 index 0000000000..0c8bf9c947 --- /dev/null +++ b/theories/Zmod/QuadraticReciprocity.v @@ -0,0 +1,891 @@ +From Stdlib Require Import ZArith ZModOffset Zdiv Zdivisibility Lia. +From Stdlib Require Import Bool.Bool Lists.List Lists.Finite Sorting.Permutation. +Import ListNotations. +From Stdlib Require Import Zmod.ZmodDef Zmod.ZstarDef Zmod.Zmod Zmod.Zstar. + +#[local] Lemma andb_implied_r a b : (a = true -> b = true) -> a && b = a. +Proof. case a, b; trivial. intros H. case H; trivial. Qed. + +#[local] Open Scope Z_scope. +#[local] Coercion Z.pos : positive >-> Z. +#[local] Coercion N.pos : positive >-> N. +#[local] Coercion Z.of_N : N >-> Z. +#[local] Coercion ZmodDef.Zmod.to_Z : Zmod >-> Z. +#[local] Coercion Zstar.to_Zmod : Zstar.Zstar >-> Zmod.Zmod. + +#[local] Lemma Private_odd_prime (p : Z) : Z.prime p -> 3 <= p -> p mod 2 = 1. +Proof. + case (Z.mod_pos_bound p 2 eq_refl) as [[]%Zle_lt_or_eq ?]; trivial. + { intros _ _; eapply Z.le_antisymm; + solve [ eapply Z.lt_pred_le + eapply Zlt_succ_le; trivial ]. } + intros [? A] B. + case (A 2). { split. exact eq_refl. eapply Z.le_succ_l; trivial. } + apply Z.mod_divide. inversion 1. congruence. +Qed. +#[local] Abbreviation odd_prime := Private_odd_prime (only parsing). + +Module CRT. +Module Zmod. +Import ZmodDef.Zmod ZmodBase.Zmod. +Lemma elements_mul_coprime (a b : positive) (H : Z.coprime a b) : + Permutation (elements (a * b)) + (map (fun xy : Zmod _ * Zmod _ => Zmod.of_Z (a*b) (Z.combinecong a b (fst xy) (snd xy))) + (list_prod (elements a) (elements b))). +Proof. + eapply NoDup_Permutation_bis; try apply NoDup_elements; rewrite ?length_map, ?length_prod, ?length_elements; try lia. + intros xy G; rewrite in_map_iff; exists (of_Z _ xy, of_Z _ xy); cbn [fst snd]. + split; cycle 1. { apply List.in_prod; apply in_elements; lia. } + apply to_Z_inj; rewrite !to_Z_of_Z, Z.combinecong_mod_l, Z.combinecong_mod_r. + symmetry; rewrite <-2mod_to_Z at 1; f_equal. + apply Z.combinecong_complete_coprime_nonneg_nonneg; trivial; lia. +Qed. +End Zmod. + +Module Zstar. +Import ZstarDef.Zstar ZstarBase.Zstar. + +Lemma elements_mul_coprime (a b : positive) (H : Z.coprime a b) : + Permutation (elements (a * b)) + (map (fun xy : Zstar _ * Zstar _ => of_Zmod (Zmod.of_Z (a*b) (Z.combinecong a b (fst xy) (snd xy)))) + (list_prod (elements a) (elements b))). +Proof. + pose proof Zmod.elements_mul_coprime a b H as P. + eapply (Permutation_filter (fun x : Zmod (a*b) => Z.gcd x (a*b) =? 1)) in P. + eapply (Permutation_map (@of_Zmod (a*b))) in P. + rewrite <-Pos2Z.inj_mul in P; rewrite P; clear P. + symmetry; rewrite <-map_map with (g:=of_Zmod), filter_map_swap; Morphisms.f_equiv. + erewrite <-map_ext, <-map_map with (f := fun xy : Zstar _ * Zstar _ => (fst xy : Zmod _, snd xy : Zmod _)); [ eapply f_equal | intros; exact eq_refl ]. + cbv [elements]. + do 2 (case Z.eqb_spec; try lia); intros. + erewrite list_prod_map_map, map_map, list_prod_filter_filter; + erewrite map_ext_in, map_id, filter_ext; trivial; intros [x y]; cbn [fst snd]. + { case (Z.combinecong_sound_coprime a b x y ltac:(trivial)) as [Hx Hy]. + apply eq_true_iff_eq; rewrite andb_true_iff, !Z.eqb_eq. + rewrite Zmod.to_Z_of_Z, Pos2Z.inj_mul. + setoid_rewrite Z.coprime_mul_r_iff. + rewrite <-(Z.coprime_mod_l_iff _ a), <-(Z.coprime_mod_l_iff _ b). + rewrite Z.mod_prod_mod_factor_l, Z.mod_prod_mod_factor_r, Hx, Hy. + rewrite Z.coprime_mod_l_iff, Z.coprime_mod_l_iff. reflexivity. } + { intros [?[?%Z.eqb_eq ?%Z.eqb_eq]%andb_true_iff]%filter_In. + rewrite !to_Zmod_of_Zmod; trivial. } +Qed. + +Lemma length_elements_mul_coprime (a b : positive) (H : Z.coprime a b) : + length (elements (a*b)) = (length (elements a) * length (elements b))%nat. +Proof. erewrite elements_mul_coprime, ?length_map, ?length_prod; trivial; lia. Qed. + +Lemma length_elements_semiprime (p q : positive) + (Hp : Z.prime p) (Hq : Z.prime q) (H : p <> q) : + length (elements (p*q)) = Z.to_nat ((p-1)*(q-1)). +Proof. + rewrite length_elements_mul_coprime, 2length_elements_prime; + try apply Z.coprime_prime_prime; trivial; nia. +Qed. +End Zstar. +End CRT. + +Module Zstar. +Import ZstarDef.Zstar ZstarBase.Zstar. + +Lemma square_roots_opp_prime {p : positive} (Hp : Z.prime p) (x y : Zstar p) : + pow x 2 = pow y 2 <-> (x = y \/ x = opp y). +Proof. + rewrite <-3 to_Zmod_inj_iff, 2to_Zmod_pow, to_Zmod_opp. + rewrite (Zmod.square_roots_opp_prime Hp); reflexivity. +Qed. + +Lemma square_roots_1_prime (p : positive) (Hp : Z.prime p) (x : Zstar p) : + pow x 2 = one <-> (x = one \/ x = opp one). +Proof. + rewrite <-3to_Zmod_inj_iff, to_Zmod_pow, to_Zmod_opp, to_Zmod_1. + rewrite (Zmod.square_roots_1_prime Hp); reflexivity. +Qed. + +#[local] Notation "∏ xs" := (prod xs) (at level 40). + +Local Infix "*" := mul. +Local Infix "/" := div. + +(* TODO: move? Local? *) +Definition of_bool m (b : bool) : Zstar m := if b then one else opp one. +Lemma of_bool_negb m b : of_bool m (negb b) = opp (of_bool m b). +Proof. case b; cbn [of_bool negb]; rewrite ?opp_opp; trivial. Qed. +Lemma of_bool_1_iff (m : positive) b : of_bool m b = one <-> b = true \/ m <= 2. +Proof. + pose proof @opp_1_neq_1 m. + pose proof @wlog_eq_Zstar_3_pos m one (opp one) ltac:(lia). + case (Z.leb_spec 3 m); case b; cbn [of_bool]; intuition (congruence || lia). +Qed. +Lemma of_bool_m1_iff (m : positive) b : of_bool m b = (opp one) <-> b = false \/ m <= 2. +Proof. + pose proof @opp_1_neq_1 m. + pose proof @wlog_eq_Zstar_3_pos m one (opp one) ltac:(lia). + case (Z.leb_spec 3 m); case b; cbn [of_bool]; intuition (congruence || lia). +Qed. +Lemma of_bool_1_iff_ge3 m b (Hm : Pos.le 3 m) : of_bool m b = one <-> b = true. +Proof. rewrite of_bool_1_iff; intuition (congruence || lia). Qed. +Lemma of_bool_m1_iff_ge3 m b (Hm : Pos.le 3 m) : of_bool m b = opp one <-> b = false. +Proof. rewrite of_bool_m1_iff; intuition (congruence || lia). Qed. + +Lemma abs_of_bool m b : abs (of_bool m b) = one. +Proof. cbv [of_bool]; case b; rewrite ?abs_opp, ?abs_1; trivial. Qed. +Lemma inv_of_bool m b : inv (of_bool m b) = of_bool m b. +Proof. cbv [of_bool]; case b; rewrite ?inv_opp, ?inv_1; trivial. Qed. + +Lemma to_Z_true {m : positive} (H : 2 <= m) : Zmod.to_Z (of_bool m true) = 1. +Proof. cbv [of_bool]. rewrite to_Zmod_1, Zmod.to_Z_1, Z.mod_small; lia. Qed. + +Lemma to_Z_false {m : positive} : Zmod.to_Z (of_bool m false) = m-1. +Proof. + case (Pos.eq_dec m 1) as [->|]; trivial. + case (Pos.eq_dec m 2) as [->|]; trivial. + cbv [of_bool]. + rewrite to_Zmod_opp, Zmod.to_Z_opp, to_Zmod_1, Zmod.to_Z_1, (Z.mod_diveq (-1)); + rewrite ?(Z.mod_small 1); try lia. +Qed. + +Lemma signed_true {m : positive} (H : 3 <= m) : Zmod.signed (of_bool m true) = 1. +Proof. cbv [of_bool]. rewrite to_Zmod_1, Zmod.signed_1; trivial. Qed. + +Lemma signed_false {m : positive} (H : 2 <= m) : Zmod.signed (of_bool m false) = -1. +Proof. + case (Pos.eq_dec m 2) as [->|]; trivial. cbv [of_bool]. + rewrite to_Zmod_opp, Zmod.signed_opp, to_Zmod_1, Zmod.signed_1 by lia. + rewrite Z.smod_small; trivial. zify; Z.to_euclidean_division_equations; nia. +Qed. + +#[local] Lemma euler_criterion_subproof {p : positive} (Hp : Z.prime p) (a : Zstar p) : + ∏ elements p = + of_bool _ (negb (existsb (fun x => eqb (pow x 2) a) (elements p))) * pow a ((p-1)/2). +Proof. + apply wlog_eq_Zstar_3_pos; try lia; intro Hp'. + + (* Tripartite categorization *) + rewrite existsb_as_filter, negb_involutive. + set (roots := filter (fun x : Zstar p => eqb (pow x 2) a) (elements p)). + set (smalls := filter (fun x : Zstar p => x div a x pow x 2 =? a)). + erewrite (Permutation_partition (fun x : Zstar _ => x Z <-> a/x = x :> Z). + { intros x; rewrite !Zmod.to_Z_inj_iff, !to_Zmod_inj_iff. + erewrite <-(mul_cancel_l_iff x _ x), mul_div_r_same_r. split; congruence. } + erewrite (filter_ext (fun _ => _ && _) (fun x : Zstar _ => x _ && _) (fun x => div a x div a x) smalls)); + [|rewrite HPP in HP; clear HPP]. + { apply Permutation.NoDup_Permutation; intros; trivial. + { eapply Injective_map_NoDup; trivial. + (* TODO: div_inj, inv_inj *) + intros ? ? E. + rewrite <-2mul_inv_r in E. + eapply mul_cancel_l, (f_equal inv) in E. + rewrite 2 inv_inv in E. + trivial. } + cbv [smalls larges]. + rewrite in_map_iff; repeat setoid_rewrite filter_In. + repeat setoid_rewrite N.ltb_lt. + assert (Hdiv : forall x y z : Zstar p, div z y = x <-> z = mul x y); [|setoid_rewrite Hdiv]. + { split; intros; subst. + { rewrite <-mul_inv_r, <-!mul_assoc, mul_inv_same_l, mul_1_r; auto. } + { rewrite div_mul_l, div_same, mul_1_r; trivial. } } + split. + { intros []. exists (div a x). rewrite mul_div_r_same_r, div_div_r_same. intuition apply in_elements. } + { intros (y&A&?&?). rewrite A in *. rewrite mul_comm. + rewrite div_mul_l, div_same, mul_1_r in *. intuition apply in_elements. } } + erewrite prod_Permutation, prod_app by eapply HP. + erewrite (prod_Permutation (smalls++_) (flat_map (fun x => [x;a/x]) smalls)); cycle 1. + { generalize (div a) as f; generalize smalls as xs; generalize (Zstar p) as A; clear. + induction xs; cbn [map flat_map app]; intros; econstructor. + erewrite <-Permutation_middle; eauto. } + erewrite prod_flat_map, map_ext, map_const, (prod_repeat a); cycle 1. + { intros x. cbn [prod fold_right]. rewrite mul_1_r, mul_div_r_same_r; trivial. } + + (* Counting elements *) + assert (length (elements p) = length roots + 2*length smalls)%nat as HL. + { erewrite Permutation.Permutation_length, !length_app, !length_map by eauto; lia. } + assert (Z.of_nat (length smalls) = (p-1-Z.of_nat (length roots))/2)%Z as ->. + { pose proof length_elements_prime p Hp. + zify; Z.to_euclidean_division_equations; lia. } + + (* Casework on [length roots] using [NoDup roots] *) + destruct roots as [|x roots'] eqn:A. (* no roots *) + { cbn [prod fold_right length Nat.eqb of_bool]; rewrite ?mul_1_l, Z.sub_0_r; trivial. } + assert (Hx: In x roots). { rewrite A. left. split. } apply filter_In, proj2 in Hx. + destruct roots' as [|y roots''] eqn:B. (* 1 *) + { unshelve ecase (opp_distinct_odd _ _ x); try lia; auto using odd_prime. + assert (In (opp x) roots) as AA. + { apply filter_In, conj; try apply in_elements. rewrite pow_opp_2; trivial. } + rewrite A in AA; inversion AA as [|AAA]; trivial; inversion AAA. } + (* 2 <= *) + assert (Hy: In y roots). { rewrite A. right. left. split. } apply filter_In, proj2 in Hy. + rewrite eqb_eq in *. + assert (y = opp x) as ->. + { case (proj1 (square_roots_opp_prime Hp y x)); trivial. + { congruence. } + { intros ->. inversion_clear NDroots as [|? ? X]; case X; left; trivial. } } + destruct roots'' as [|z roots''']; cycle 1. (* 3 <= *) + { assert (Hz: In z roots). { rewrite A. right. right. left. split. } apply filter_In, proj2 in Hz. + rewrite ?eqb_eq in *. + { case (proj1 (square_roots_opp_prime Hp z x)) as [->| ->]. + { congruence. } + { inversion_clear NDroots as [|? ? X]; case X; right; left; split. } + { inversion_clear NDroots as [|? ? ? X]. + inversion_clear X as [|? ? Y]; case Y; left; split. } } } + (* 2 roots *) + cbn [prod fold_right length Nat.eqb of_bool]; + repeat rewrite ?mul_1_r, ?mul_1_l, ?mul_opp_l, ?mul_opp_r. + rewrite <-pow_2_r, Hx, <-pow_succ_r. f_equal. f_equal. + zify; Z.to_euclidean_division_equations; lia. +Qed. + +(** One direction of Wilson's theorem *) +Theorem prod_elements_prime {p : positive} (Hp : Z.prime p) : ∏ elements p = opp one. +Proof. + rewrite (euler_criterion_subproof Hp one). + rewrite (proj2 (existsb_exists _ _)), pow_1_l, mul_1_r; cbn [of_bool negb]; trivial. + exists one; rewrite ?pow_1_l, ?eqb_eq ; auto using in_elements. +Qed. + +Lemma euler_criterion_existsb {p : positive} a (Hp : Z.prime p) : + pow a ((p-1)/2) = of_bool p (existsb (fun x => eqb (pow x 2) a) (elements p)). +Proof. + pose proof euler_criterion_subproof Hp a as H. + rewrite prod_elements_prime in H by trivial. + apply (f_equal opp) in H; rewrite ?of_bool_negb, ?mul_opp_l, ?opp_opp in H. + case existsb in *; cbn [of_bool] in *; + rewrite H, ?mul_opp_l, ?opp_opp, ?mul_1_l; trivial. +Qed. + +Theorem euler_criterion {p : positive} (a : Zstar p) (Hp : Z.prime p): + pow a ((p-1)/2) = one <-> exists x, pow x 2 = a. +Proof. + split. + { case (Pos.leb_spec 3 p) as []; cycle 1. + { exists one. apply wlog_eq_Zstar_3_pos; lia. } + rewrite euler_criterion_existsb, of_bool_1_iff, existsb_exists by trivial. + intros [[x [_ Hx%eqb_eq]]|]; try lia; eauto. } + { intros [x Hx]; eapply euler_criterion_square; eauto. } +Qed. + +Lemma euler_criterion_nonsquare {p : positive} (Hp : Z.prime p) + (a : Zstar p) (Ha : forall x, pow x 2 <> a) : pow a ((p-1)/2) = opp one. +Proof. + rewrite euler_criterion_existsb by trivial. + case existsb eqn:H; trivial; exfalso. + apply existsb_exists in H; case H as [x [_ H%eqb_eq]]. + case (Ha x); trivial. +Qed. + +Lemma euler_criterion_neq_one {p : positive} (Hp : Z.prime p) + (a : Zstar p) (H : pow a ((p-1)/2) <> one) : forall x, pow x 2 <> a. +Proof. + rewrite euler_criterion in H by trivial; intros x Hx; case H; eauto. +Qed. + +Lemma euler_criterion_m1 {p : positive} (Hp : Z.prime p) (Hp' : 3 <= p) + (a : Zstar p) (H : pow a ((p-1)/2) = opp one) : forall x, pow x 2 <> a. +Proof. + apply euler_criterion_neq_one; trivial; rewrite H; apply opp_1_neq_1; trivial. +Qed. +End Zstar. + +Module Zmod. +Import ZstarBase ZmodDef.Zmod ZmodBase.Zmod Zmod. +Local Infix "*" := mul. +Local Infix "^" := pow. + +Theorem euler_criterion_square_nz {p : positive} (Hp : Z.prime p) + (a sqrt_a : Zmod p) (Ha : pow sqrt_a 2 = a) (Hnz : a <> zero) : + pow a ((p-1)/2) = one. +Proof. + assert (sqrt_a <> zero). { intros ->; rewrite pow_0_l in *; congruence. } + rewrite <-to_Z_0_iff in *; pose proof to_Z_range a; pose proof to_Z_range sqrt_a. + assert (Z.coprime a p). { symmetry; apply Z.coprime_prime_small; trivial; lia. } + assert (Z.coprime sqrt_a p). { symmetry; apply Z.coprime_prime_small; trivial; lia. } + unshelve epose proof + (E := Zstar.euler_criterion_square Hp (Zstar.of_Zmod a) (Zstar.of_Zmod sqrt_a) _). + { apply Zstar.to_Zmod_inj; rewrite Zstar.to_Zmod_pow, 2Zstar.to_Zmod_of_Zmod; trivial. } + apply (f_equal Zstar.to_Zmod) in E. + rewrite Zstar.to_Zmod_pow, Zstar.to_Zmod_of_Zmod, Zstar.to_Zmod_1 in E; trivial. +Qed. + +Theorem euler_criterion_square {p : positive} (Hp : Z.prime p) + (a sqrt_a : Zmod p) (Ha : pow sqrt_a 2 = a) : + a = zero \/ pow a ((p-1)/2) = one. +Proof. + pose proof euler_criterion_square_nz Hp _ _ Ha. + case (eqb_spec a zero); intuition idtac. +Qed. + +Theorem euler_criterion {p : positive} a (Hp : Z.prime p) : + (a = zero \/ a ^ ((p - 1) / 2) = one) <-> exists x : Zmod p, pow x 2 = a. +Proof. + split; cycle 1. + { intros []; eauto using euler_criterion_square. } + intros []. + { subst. exists zero. trivial. } + pose proof (Z.prime_ge_2 _ Hp) as Hp'; pose proof one_neq_zero (m:=p) ltac:(lia). + case (Pos.eq_dec p 2) as [->|]. { + pose proof in_elements a ltac:(lia) as C; case C as [<-| [<-| [] ] ]; + [exists zero|exists one]; trivial. } + assert (((p - 1) / 2) <> 0)%Z by (zify; Z.div_mod_to_equations; nia). + assert (a <> zero). { intros ->; rewrite pow_0_l in *. congruence. lia. } + rewrite <-to_Z_0_iff in H2; pose proof to_Z_range a. + assert (Z.coprime a p). { symmetry; apply Z.coprime_prime_small; trivial; lia. } + case (proj1 (@Zstar.euler_criterion p (Zstar.of_Zmod a) Hp)) as [x Hx]. + { apply Zstar.to_Zmod_inj. + rewrite Zstar.to_Zmod_pow, Zstar.to_Zmod_of_Zmod, Zstar.to_Zmod_1; trivial. } + { exists x. apply (f_equal Zstar.to_Zmod) in Hx. + rewrite Zstar.to_Zmod_pow, Zstar.to_Zmod_of_Zmod in Hx; trivial. } +Qed. + +End Zmod. + +Module Reciprocity. Module Zstar. +Import ZmodDef. +Import ZmodDef.Zmod ZmodBase.Zmod CRT.Zmod QuadraticReciprocity.Zmod. +Import ZstarDef.Zstar ZstarBase.Zstar CRT.Zstar QuadraticReciprocity.Zstar. +#[local] Notation "∏ xs" := (prod xs) (at level 40). + +Module Z. +Lemma pow_m1_l : forall n, 0 <= n -> Z.pow (-1) n = if Z.odd n then -1 else 1. +Proof. + eapply Wf_Z.natlike_ind; trivial; intros. + rewrite Z.pow_succ_r, Z.odd_succ, <-Z.negb_odd by trivial. + case Z.odd in *; cbv [negb]; lia. +Qed. +End Z. + +#[local] Lemma mul_signed_subgroups_abs (p q : positive) (Hp : p mod 2 = 1) (Hq : q mod 2 = 1) x y : + abs x = abs y :> Zstar (p*q) -> Z.smodulo x p * Z.smodulo x q = Z.smodulo y p * Z.smodulo y q. +Proof. + intros []%eq_abs_iff; [congruence|subst y]. + rewrite to_Zmod_opp, to_Z_opp. + symmetry. + rewrite <-Z.smod_mod, Z.mod_mod_divide, Z.smod_mod by (exists q; lia). + rewrite <-(Z.smod_mod _ q), Z.mod_mod_divide, Z.smod_mod by (exists p; lia). + rewrite <-(Z.smod_idemp_opp _ p), <-(Z.smod_idemp_opp _ q). + pose proof Z.smod_pos_bound x p ltac:(lia). + pose proof Z.smod_pos_bound x q ltac:(lia). + rewrite !(Z.smod_small (- _)); (zify; Z.to_euclidean_division_equations; nia). +Qed. + +Lemma square_prod_positives {p : positive} (prime_p : Z.prime p) (odd_p : 3 <= p) : + pow (∏ positives p) 2 = opp (pow (opp one) ((p - 1) / 2)). +Proof. + rewrite pow_2_r. + pose proof prod_elements_prime prime_p as H. + rewrite elements_by_sign in H by lia. + rewrite negatives_as_positives_odd in H by auto using odd_prime. + apply (f_equal opp) in H; rewrite ?opp_opp in H. + rewrite prod_app, prod_opp, prod_rev, (mul_comm (pow _ _)), mul_assoc, <-mul_opp_r in H. + rewrite length_rev, length_positives_prime in H by trivial. + replace (Z.of_nat (N.to_nat (Pos.pred_N p / 2))) with ((p - 1) / 2) in H by lia. + apply (f_equal (fun x => mul x (inv (opp (pow (opp one) ((p - 1) / 2)))))) in H. + rewrite Z2Nat.id in H by (Z.div_mod_to_equations; lia). + rewrite <-?mul_assoc, mul_inv_same_r, mul_1_r in H. + rewrite mul_1_l, inv_opp, inv_pow_m1 in H; exact H. +Qed. + +#[local] Lemma prod_snd_abspairs + {p q : positive} {prime_p : Z.prime p} {prime_q : Z.prime q} (odd_p : 3 <= p) {odd_q : 3 <= q} {coprime_p_q : Z.coprime p q} : + ∏ map snd (list_prod (elements p) (positives q)) = + (-1)^((p-1)/2) * (-1)^((q-1)/2*((p-1)/2)) mod q :> Z. +Proof. + rewrite List.snd_list_prod, prod_concat, map_repeat, prod_repeat. + rewrite length_elements_prime, Z2Nat.id by (trivial || Z.div_mod_to_equations; lia). + replace (p-1) with (2 * ((p-1)/2)) at 1; cycle 1. + { pose proof odd_prime _ prime_p odd_p. (zify; Z.to_euclidean_division_equations; nia). } + rewrite pow_mul_r, square_prod_positives, <-mul_m1_l, pow_mul_l, <-pow_mul_r by trivial. + rewrite ?to_Zmod_mul, ?to_Zmod_pow, ?to_Zmod_opp, ?to_Zmod_1. + rewrite ?to_Z_mul, ?to_Z_pow_nonneg_r, ?to_Z_opp, ?to_Z_1, ?Z.mod_pow_l, ?Zmult_mod_idemp_l, ?Zmult_mod_idemp_r, ?(Z.mod_small 1); + trivial; try (Z.to_euclidean_division_equations; nia). +Qed. + +#[local] Lemma prod_fst_abspairs + {p q : positive} {prime_p : Z.prime p} {prime_q : Z.prime q} (odd_p : 3 <= p) {odd_q : 3 <= q} {coprime_p_q : Z.coprime p q} : + ∏ map fst (list_prod (elements p) (positives q)) = (-1)^((q-1)/2) mod p :> Z. +Proof. + erewrite List.fst_list_prod, prod_flat_map, map_ext, prod_pow, prod_elements_prime; trivial. + 2: { intros. instantiate (1:=((q-1)/2)). + rewrite prod_repeat, length_positives_prime; trivial; f_equal. + zify; Z.to_euclidean_division_equations; nia. } + rewrite to_Zmod_pow, to_Zmod_opp, to_Zmod_1. + rewrite to_Z_pow_nonneg_r, to_Z_opp, to_Z_1, Z.mod_pow_l, ?(Z.mod_small 1); trivial; + Z.to_euclidean_division_equations; nia. +Qed. + +#[local] Abbreviation combine p q := + (fun xy : Zstar _ * Zstar _ => Zstar.of_Zmod (Zmod.of_Z (p*q)%positive (Z.combinecong p%positive q%positive (fst xy) (snd xy)))). + +Lemma prod_combinecong + {p q : positive} {Hp : 3 <= p} {Hq : 3 <= q} {coprime_p_q : Z.coprime p q} (ps : list (Zstar p * Zstar q)) : + ∏ (map (combine p q)) ps = + Zstar.of_Zmod (Zmod.of_Z (p*q) (Z.combinecong p q (∏ map fst ps) (∏ map snd ps))). +Proof. + induction ps as [|[x y]]; cbn [fst snd map]; rewrite ?prod_nil, ?prod_cons; [|rewrite IHps; clear IHps]. + { erewrite <-Z.combinecong_complete_coprime_nonneg_nonneg with (a:=1); + repeat (rewrite ?Z.mod_small, ?to_Zmod_1, ?to_Z_1; + trivial; try (Z.to_euclidean_division_equations; nia)). } + rewrite ?to_Zmod_mul, ?to_Z_mul. + symmetry; erewrite <-Z.combinecong_complete_coprime_nonneg_nonneg with + (a:=(Z.combinecong p q x y) * (Z.combinecong p q (∏ map fst ps) (∏ map snd ps))) + by (trivial; try lia; rewrite <-Zmult_mod_idemp_r, <-Zmult_mod_idemp_l, + ?(proj1 (Z.combinecong_sound_coprime _ _ _ _ coprime_p_q)), + ?(proj2 (Z.combinecong_sound_coprime _ _ _ _ coprime_p_q)), + ?Zmult_mod_idemp_r, ?Zmult_mod_idemp_l, ?Zmod_mod; trivial). + rewrite of_Z_mod, of_Z_mul, of_Zmod_mul; trivial; + rewrite to_Z_of_Z, Z.coprime_mod_l_iff, ?Pos2Z.inj_mul; apply Z.coprime_mul_r; + rewrite <-Z.coprime_mod_l_iff, + ?(proj1 (Z.combinecong_sound_coprime _ _ _ _ coprime_p_q)), + ?(proj2 (Z.combinecong_sound_coprime _ _ _ _ coprime_p_q)), ?Z.coprime_mod_l_iff; + auto using to_Zmod_range. +Qed. + +Lemma abs_prod_abs m xs : @abs m (∏ map abs xs) = abs (∏ xs). +Proof. + induction xs; cbn [map]; rewrite ?prod_nil, ?prod_cons; trivial. + rewrite <-abs_mul_abs_r, IHxs, abs_mul_abs_abs; trivial. +Qed. + +Lemma abs_prod_positives_semiprime + {p q : positive} {prime_p : Z.prime p} {prime_q : Z.prime q} (odd_p : 3 <= p) {odd_q : 3 <= q} {coprime_p_q : Z.coprime p q} : + abs (∏ positives (p*q)) = abs (∏ map (combine p q) (list_prod (elements p) (positives q))). +Proof. + intros. + pose (absq (x : Zstar (p*q)) := if 0 q) by (cbv [Z.coprime] in *; intro; subst; rewrite Z.gcd_diag in *; lia). + rewrite length_positives_prime, length_positives_odd, length_elements_semiprime by + (trivial; Z.to_euclidean_division_equations; lia). + zify. rewrite Nat2Z.inj_div in *. zify. Z.to_euclidean_division_equations. nia. } + setoid_rewrite in_map_iff. + intros ? (?&[]&?). + exists (of_Zmod (of_Z p (absq x)), of_Zmod (of_Z q (absq x))); cbn [fst snd]. + rewrite in_prod_iff, in_positives; [|lia]. + pose proof coprime_to_Zmod x as C; apply Z.coprime_mul_r_iff in C; case C as []. + pose proof coprime_to_Zmod (absq x) as C;apply Z.coprime_mul_r_iff in C; case C as []. + repeat rewrite ?to_Zmod_of_Zmod, ?to_Z_of_Z, ?signed_of_Z, + ?Z.combinecong_mod_l, ?Z.combinecong_mod_r, ?Z.coprime_mod_l_iff; trivial; []. + (intuition auto using in_elements); [|]; cycle 1. + { cbv [absq]; case (Z.ltb_spec 0 (Z.smodulo x q)) as []; trivial. + rewrite to_Zmod_opp, to_Z_opp, <-Z.smod_mod, Z.mod_mod_divide, Z.smod_mod, <-Z.smod_idemp_opp by + (exists p; lia). + pose proof Z.smod_pos_bound x q ltac:(lia). + case (Z.eqb_spec (Z.smodulo x q) 0) as [E|]. + { apply (f_equal (fun x => x mod q)) in E; rewrite Z.mod_smod, Zmod_0_l in E. + rewrite <-Z.coprime_mod_l_iff, E, Z.coprime_0_l_iff in *. lia. } + rewrite Z.smod_small; try lia. + pose proof odd_prime q prime_q odd_q as Hq'; Z.to_euclidean_division_equations; nia. } + erewrite <-Z.combinecong_complete_coprime_nonneg_nonneg by (trivial; lia). + rewrite of_Z_mod, of_Z_to_Z, of_Zmod_to_Zmod; trivial. +Qed. + +Lemma add_seq a b c : map (Nat.add a) (seq b c) = seq (a+b) c. +Proof. + revert b; induction c; intros; + cbn [seq map]; rewrite ?IHc, ?Nat.add_succ_r; trivial. +Qed. + +Lemma add_seq_0_l a b : map (Nat.add a) (seq 0 b) = seq a b. +Proof. rewrite add_seq, Nat.add_0_r; trivial. Qed. + +#[local] Open Scope nat_scope. +Lemma filter_0mod_seq_0_mul : (forall m, m <> 0 -> forall n, + filter (fun i => i mod m =? 0) (seq 0 (n * m)) = map (Nat.mul m) (seq 0 n))%nat. +Proof. + intros until n; induction n; intros; trivial; []. + rewrite Nat.mul_succ_l, Nat.add_comm, seq_app, filter_app, Nat.add_0_l. + case m as [|pred_m] eqn:pred_m_eq at 2; [contradiction|]; cbn [seq filter]. + rewrite Nat.Div0.mod_0_l, Nat.eqb_refl. + erewrite filter_ext_in, filter_false; cycle 1. + { intros ??%in_seq; apply Nat.eqb_neq; intros [[]X]%Nat.Div0.mod_divides; nia. } + cbn [map "++"]; rewrite Nat.mul_0_r; f_equal. + erewrite <-add_seq_0_l, filter_map_swap, filter_ext, IHn; cycle 1. + { intros. rewrite <-Nat.Div0.add_mod_idemp_l, Nat.Div0.mod_same, Nat.add_0_l; trivial. } + symmetry. rewrite <-add_seq_0_l, 2map_map; apply map_ext; lia. +Qed. + +Lemma filter_cong_seq_mul_mul k m (Hm : m <> 0) : forall n s, + filter (fun i => i mod m =? k mod m) (seq (s*m) (n*m)) = map (fun i => i*m + k mod m) (seq s n). +Proof. + induction n; trivial; intros. + rewrite Nat.mul_succ_l, Nat.add_comm, seq_app, filter_app, <-Nat.mul_succ_l, IHn. + enough (filter _ _ = [_]) as -> by exact eq_refl. + pose proof Nat.mod_bound_pos k m ltac:(lia) ltac:(lia). + replace m with ((k mod m) + (1 + (m-(k mod m+1)))) at 2 by lia. + rewrite ?seq_app, ?filter_app. + erewrite filter_ext_in, filter_false, filter_ext_in, filter_true, filter_ext_in, filter_false; + trivial; intros i ?%in_seq; try apply Nat.eqb_eq; try apply Nat.eqb_neq; assert (s = i / m); + zify; rewrite ?Nat2Z.inj_div, ?Nat2Z.inj_mod in *; Z.to_euclidean_division_equations; nia. +Qed. + +Lemma filter_cong_seq k m (Hm : m <> 0) n s : + filter (fun i => i mod m =? k mod m) (seq s n) = + filter (fun i : nat => i mod m =? k mod m) (seq s (n mod m)) ++ + map (Nat.add (s mod m + n mod m + (k mod m + m - s mod m + m - n mod m) mod m)) + (map (Nat.mul m) (seq (s / m) (n / m))). +Proof. + match goal with |- _ = ?R => set R end. + pose proof Nat.mod_bound_pos s m ltac:(lia) ltac:(lia). + pose proof Nat.mod_bound_pos n m ltac:(lia) ltac:(lia). + rewrite (Nat.div_mod n m), Nat.add_comm, seq_app, (Nat.mul_comm m) by lia. + rewrite (Nat.div_mod s m) at 2 by lia. + rewrite <-Nat.add_assoc, Nat.add_comm, <-add_seq by lia. + rewrite filter_app, filter_map_swap. + + unshelve erewrite (Nat.mul_comm m), (filter_ext _ _ _ (seq (_*m) _)), (filter_cong_seq_mul_mul (k mod m+m-s mod m + m - n mod m)) by lia; shelve_unifiable. + { intros i; apply eq_true_iff_eq; rewrite 2Nat.eqb_eq; split; intros R. + { rewrite <-R; clear R. + apply Nat2Z.inj_iff; repeat rewrite ?Nat2Z.inj_mod, ?Nat2Z.inj_mul, ?Nat2Z.inj_add, ?Nat2Z.inj_sub by lia. + repeat match goal with + |- context[Z.of_nat ?x] => is_var x; let x' := fresh x "'" in rename x into x'; + set (Z.of_nat x') as x + end. + rewrite <-Z.mod_add with (a:=Z.sub _ _) (b:=-2%Z) by lia. + replace ((s mod m + n mod m + i) mod m + m - s mod m + m - n mod m + - (2) * m)%Z + with ((s mod m + n mod m + i) mod m - (s mod m + n mod m))%Z by lia. + rewrite Zminus_mod_idemp_l. f_equal. lia. } + { rewrite <-Nat.Div0.add_mod_idemp_r, R by lia; clear R; rewrite !Nat.Div0.add_mod_idemp_r, ?Zmod_mod. + apply Nat2Z.inj_iff; repeat rewrite ?Nat2Z.inj_mod, ?Nat2Z.inj_mul, ?Nat2Z.inj_add, ?Nat2Z.inj_sub by lia. + repeat match goal with + |- context[Z.of_nat ?x] => is_var x; let x' := fresh x "'" in rename x into x'; + set (Z.of_nat x') as x + end. + rewrite <-Z.mod_add with (a:=Z.add _ _) (b:=-2%Z) by lia. + replace (s mod m + n mod m + (k mod m + m - s mod m + m - n mod m) + - (2) * m)%Z + with (k mod m)%Z by lia. + apply Z.mod_mod; lia. } } + + erewrite map_map, map_ext, <-map_map with + (f:=Nat.mul m) + (g:=Nat.add(s mod m + n mod m + ((k mod m + m - s mod m + m - n mod m) mod m))). + 2:{ intros i; cbv beta. lia. } + + epose proof fun x => filter_In (fun i : nat => i mod m =? k mod m) x (seq s (n mod m)). + setoid_rewrite in_seq in H1. + + exact eq_refl. +Qed. +Local Close Scope nat_scope. + +#[local] Lemma coprime_prime_r a p (H : Z.prime p) : Z.coprime a p <-> a mod p <> 0. +Proof. + rewrite Z.coprime_comm. etransitivity. { apply Z.coprime_prime_l_iff; trivial. } + pose proof Z.not_prime_0. + rewrite Z.mod_divide; intuition subst; contradiction. +Qed. + +#[local] Lemma mul_eq_1_iff a b : a*b = 1 <-> a = 1 /\ b = 1 \/ a = -1 /\ b = -1. +Proof. pose proof Z.eq_mul_1 a b; nia. Qed. +#[local] Lemma filter_filter {A} f g l : + @filter A f (filter g l) = filter (fun a => f a && g a) l. +Proof. induction l; cbn; auto. case g; cbn; case f; cbn; rewrite ?IHl; auto. Qed. +Lemma seq_mul_r s n c : seq s (n*c) = flat_map (fun i => seq (s + i*c) c) (seq O n). +Proof. + revert s; induction n; intros; rewrite ?flat_map_nil_l, ?Nat.add_0_r; trivial. + cbn [Nat.mul]; rewrite Nat.add_comm, seq_app. + rewrite seq_S, flat_map_app, IHn; cbn [flat_map]; rewrite app_nil_r; trivial. +Qed. +Lemma seq_0_mur n c : seq O (n*c) = flat_map (fun i => seq (i*c) c) (seq O n). +Proof. apply seq_mul_r. Qed. +Lemma prod_map_filter {A} {m} (f : A -> Zstar m) g (xs : list A) : + ∏ map f (filter g xs) = div (∏ map f xs) (∏ map f (filter (fun x => negb (g x)) xs)). +Proof. + induction xs; cbn [map filter]; rewrite ?prod_nil, ?prod_cons, ?div_same; trivial. + case g; cbn [negb map]; rewrite ?prod_cons, !IHxs, ?div_mul_l; trivial. + rewrite <-!mul_inv_r, ?inv_mul, ?mul_assoc, ?(mul_comm (f a)), ?mul_assoc; f_equal. + rewrite <-?mul_assoc, mul_inv_same_r, mul_1_r; trivial. +Qed. +#[local] Lemma to_Zmod_prod {m} xs : @to_Zmod m (∏ xs) = fold_right Zmod.mul Zmod.one (map to_Zmod xs). +Proof. induction xs; cbn [map fold_right]; rewrite ?prod_nil, ?prod_cons, ?to_Zmod_1, ?to_Zmod_mul, ?IHxs; auto. Qed. +#[local] Lemma of_Zmod_prod {m} xs (Hm : 0 < m) : Forall (fun x : Zmod m => Z.coprime x m) xs -> @of_Zmod m (fold_right Zmod.mul Zmod.one xs) = ∏ (map of_Zmod xs). +Proof. + intros H. apply wlog_eq_Zstar_3_pos; trivial; intro Hm'. + induction H; cbn [fold_right map]; rewrite ?prod_nil, ?prod_cons, ?of_Zmod_1, ?of_Zmod_mul, ?IHForall; auto. + clear H IHForall x; induction H0; cbn [fold_right]; + rewrite ?to_Z_1, ?to_Z_mul, ?Z.coprime_mod_l_iff, ?Z.coprime_mul_l_iff; + auto using Z.coprime_1_l. +Qed. +Lemma prod_positives_semiprime + {p q : positive} {prime_p : Z.prime p} {prime_q : Z.prime q} (odd_p : 3 <= p) {odd_q : 3 <= q} {coprime_p_q : Z.coprime p q} : + Z.smodulo (∏ positives (p*q)) p = (-1)^((q-1)/2) * Z.smodulo (q^((p-1)/2)) p. +Proof. + assert (tl_seq : forall start len, tl (seq start len) = seq (S start) (len-1)). + { destruct len; rewrite ?Nat.sub_1_r; trivial. } + assert ( + map_add_seq: forall len start shift : nat, map (Nat.add shift) (seq start len) = seq (shift + start) len + ). + { clear; induction len; cbn [seq map]; intros; rewrite ?IHlen, ?Nat.add_succ_r; trivial. } + assert ( + seq_as_0_l : forall len start shift : nat, seq start len = map (Nat.add start) (seq O len) + ). + { clear -map_add_seq; intros. rewrite map_add_seq, Nat.add_0_r; trivial. } + assert ( +div_mul_same_r: + forall {m : positive} (x y z : Zstar m), div (mul y x) (mul z x) = div y z + ). + { clear; intros. + repeat rewrite <-?mul_inv_r, ?inv_mul, ?(mul_comm x), <-?mul_assoc. + rewrite mul_inv_same_l, mul_1_r; trivial. } + + assert (div_abs1_r : forall m (x y : Zstar m), abs y = one -> div x y = mul x y). + { clear; intros m x y H. + rewrite <-abs_1 in H; eapply eq_sym, eq_abs_iff in H; case H as [->| ->]; + rewrite <-?mul_inv_r, ?inv_opp, ?inv_1; trivial. } + + pose proof odd_prime p prime_p odd_p as Hp'. + pose proof odd_prime q prime_q odd_q as Hq'. + rewrite Z.coprime_comm in coprime_p_q. + + assert ((p / 2) < p) by (Z.div_mod_to_equations; nia). + + rewrite <-(Z.smod_smod_divide _ (Pos.mul p q)), smod_unsigned by (exists q; lia). + + (* injecting product into [Zmod p] *) + rewrite <-signed_of_Z, <-(to_Zmod_of_Zmod (of_Z _ _)); cycle 1. + { rewrite to_Z_of_Z, <-smod_unsigned, <-Z.mod_smod, Z.smod_smod_divide, Z.mod_smod, Z.coprime_mod_l_iff + by (exists q; lia). + pose proof coprime_to_Zmod (∏ positives (p * q)) as Hc; + apply Z.coprime_mul_r_iff in Hc; case Hc as []; trivial. } + + cbv [positives]. + erewrite to_Zmod_prod, map_map, map_ext_in, map_id; cbv beta. + 2: { intros ? [_ E]%filter_In. apply Z.eqb_eq in E. + rewrite to_Zmod_of_Zmod by assumption; exact eq_refl. } + + rewrite <-(@of_Z_mod p), <-(Z.mod_smod _ p). + rewrite <-(@smod_unsigned (p*q)), Z.smod_smod_divide, Z.mod_smod by (exists q; lia). + rewrite <-Zmod.mod_to_Z. + assert (forall xs, fold_right Zmod.mul Zmod.one xs mod (p*q)%positive = fold_right Z.mul 1 (map to_Z xs) mod (p*q)%positive) as ->. + { clear -odd_p odd_q. induction xs; cbn [fold_right map]; rewrite ?to_Z_1, ?to_Z_mul, ?Zmod_mod by lia; trivial. + rewrite <-Z.mul_mod_idemp_r by lia. + set ((unsigned (fold_right _ _ _) mod _)) in *. + rewrite IHxs. + rewrite Z.mul_mod_idemp_r by lia; trivial. } + rewrite Z.mod_mod_divide, of_Z_mod by (exists q; lia). + eassert (forall xs, of_Z _ (fold_right Z.mul 1 xs) = fold_right Zmod.mul Zmod.one (map (of_Z _) xs)) as ->. + { clear. induction xs; cbn [fold_right map]; rewrite ?of_Z_mul, ?IHxs; trivial. } + + rewrite !map_map. + rewrite of_Zmod_prod, ?map_map; try lia; cycle 1. + { eapply Forall_map, Forall_forall; intros ? [? E%Z.eqb_eq]%filter_In. + apply Z.coprime_mul_r_iff in E; case E as []. + rewrite to_Z_of_Z, Z.coprime_mod_l_iff by (exists q; lia); trivial. } + + (* inclusion-exclusion principle for [Zmod (p * q)] *) + erewrite filter_ext, <-filter_filter; cbv beta; cycle 1. + { instantiate (1:=fun x => Z.gcd x p =? 1). instantiate (1:=fun x => Z.gcd x q =? 1). + intros x. apply eq_true_iff_eq. + rewrite andb_true_iff, !Z.eqb_eq, and_comm; apply Z.coprime_mul_r_iff. } + + cbv [Zmod.positives]. + rewrite 2 filter_map_swap, ?map_map. + rewrite prod_map_filter, filter_filter. + erewrite (filter_ext_in (fun k => andb _ _) (fun k => (Z.of_nat k mod q) =? 0)); cycle 1. + { intros ? G; apply in_seq in G. + rewrite (proj2 (Z.ltb_lt _ _)) in G by lia; cbn [Z.b2z] in G. + eapply eq_true_iff_eq. rewrite andb_true_iff, <-eq_true_not_negb_iff, 3Z.eqb_eq. + rewrite !to_Z_of_Z, <-!(Z.gcd_mod_l (Z.of_nat a mod (p * q))), + !Z.mod_mod_divide, !Z.gcd_mod_l by ((exists q + exists p); lia). + repeat setoid_rewrite (Z.coprime_comm (Z.of_nat a)). + rewrite !Z.coprime_prime_l_iff by trivial. + case (Z.BoolSpec_divide q (Z.of_nat a)); intuition idtac; + rewrite !Z.mod_divide in *; try trivial; try contradiction; try lia. + case (Z.lcm_least p q (Z.of_nat a)) as [d ?]; trivial. + cbv [Z.coprime] in coprime_p_q. + rewrite Z.gcd_comm, Z.gcd_1_lcm_mul, Z.abs_eq in coprime_p_q by lia; rewrite coprime_p_q in *. + assert (0 < d) by lia. zify; Z.div_mod_to_equations; nia. } + + eassert ( let f := _ in let n := _ in filter f (seq 1 n) = filter f (seq 0 (S n))) as ->. + { cbn [seq filter]. rewrite to_Z_0. setoid_rewrite Z.gcd_0_l. rewrite (proj2 (Z.eqb_neq _ _)); trivial; lia. } + rewrite (proj2 (Z.ltb_lt _ _)) by lia; cbn [Z.b2z]. + eassert (S _ = (Pos.to_nat p * Z.to_nat (q / 2) + S (Z.to_nat (p/2)))%nat) + as -> by (Z.div_mod_to_equations; nia); rewrite Nat.mul_comm. + + (* filtering numerator *) + erewrite List.filter_ext; cycle 1. + { intros k. + rewrite to_Z_of_Z, <-Z.gcd_mod_l, Z.mod_mod_divide by (exists q; lia). + exact eq_refl. } + + rewrite seq_app, seq_mul_r, List.flat_map_concat_map. + repeat rewrite <-?List.concat_filter_map, ?map_app, ?concat_map, ?map_map, ?filter_app. + cbn [Nat.add]. + + erewrite List.map_ext; cycle 1. + { intros i. + replace (Pos.to_nat p) with (S (Pos.to_nat p-1)) at 2 by lia. + cbn [List.seq List.filter]. + rewrite Nat2Z.inj_mul, positive_nat_Z, Z_mod_mult, Z.gcd_0_l, (proj2 (Z.eqb_neq _ _)) by lia. + erewrite filter_ext_in, filter_true; [exact eq_refl|]; intros j ?%in_seq; cbv beta. + rewrite Z.gcd_mod_l, Z.gcd_comm. + apply Z.eqb_eq, Z.coprime_prime_l_iff; trivial. + rewrite <-Z.mod_divide, (Z.mod_diveq (Z.of_nat i)); lia. } + + cbn [List.seq List.filter]. + rewrite Nat2Z.inj_mul, positive_nat_Z, Z_mod_mult, Z.gcd_0_l, (proj2 (Z.eqb_neq _ _)) by lia. + erewrite filter_ext_in, filter_true; cycle 1. + { intros j ?%in_seq; cbv beta. + rewrite Z.gcd_mod_l, Z.gcd_comm. + apply Z.eqb_eq, Z.coprime_prime_l_iff; trivial. + rewrite <-Z.mod_divide, (Z.mod_diveq (Z.of_nat (Z.to_nat (q/2)))); lia. } + + (* multiplying numerator *) + rewrite prod_app, prod_concat, map_map. + erewrite map_ext_in, (map_const (opp one)), prod_repeat, length_seq, Z2Nat.id; revgoals. + { intros i **. + rewrite <-Nat.add_1_l, Nat.add_comm. rewrite <-map_add_seq, map_map. + erewrite map_ext_in; cycle 1. + { intros k Hk; apply in_seq in Hk. + rewrite to_Z_of_Z, <-of_Z_mod, Z.mod_mod_divide by (exists q; lia). + rewrite Nat2Z.inj_add, Nat2Z.inj_mul, positive_nat_Z, Z.add_comm. + rewrite Z.mod_add, of_Z_mod by lia. exact eq_refl. } + rewrite <-map_map. rewrite <-tl_seq. + rewrite <-tl_map. + eassert (map _ _ = Zmod.elements p) as -> by trivial. + pose proof to_Zmod_elements_prime p ltac:(trivial). + eassert (map of_Zmod _ = Zstar.elements p) as ->. + { erewrite <-to_Zmod_elements_prime, map_map, map_ext_in, map_id; trivial; intros. + rewrite of_Zmod_to_Zmod. trivial. } + rewrite prod_elements_prime by trivial. exact eq_refl. } + { clear -odd_q; Z.div_mod_to_equations; nia. } + + erewrite <-Nat.add_1_r, <-map_add_seq, map_map, map_ext_in; cycle 1. + { intros k **; cbv beta. rapply f_equal. + rewrite to_Z_of_Z, <-of_Z_mod, Z.mod_mod_divide by (exists q; lia). + rewrite Nat2Z.inj_add, Nat2Z.inj_mul, positive_nat_Z, Z.add_comm, Z2Nat.id by + (clear -odd_p; Z.div_mod_to_equations; nia). + rewrite Z.mod_add, of_Z_mod by lia; trivial. } + + (* filtering denominator *) + eassert (filter _ (seq 1 _) = map (Nat.mul (Z.to_nat q)) (seq 1 (Z.to_nat (p/2)))) as ->. + { erewrite filter_ext with (g:=fun x => (x mod Pos.to_nat q =? 0 mod Z.to_nat q)%nat); cycle 1. + { intros i; eapply eq_true_iff_eq. + rewrite Nat.Div0.mod_0_l. + rewrite Z.eqb_eq, Nat.eqb_eq, <-Nat2Z.inj_iff, Nat2Z.inj_mod; lia. } + rewrite filter_cong_seq by lia. + rewrite Nat.Div0.mod_0_l, Nat.add_0_l, !(Nat.mod_small 1), !(Nat.div_small 1) by lia. + assert (2 * (Z.to_nat ((Z.abs (p * q) - 1) / 2) mod Z.to_nat q) <= Z.to_nat q)%nat. + { repeat rewrite ?Nat2Z.inj_le, ?Nat2Z.inj_mod, ?Nat2Z.inj_mul by lia. + rewrite (Z.mod_diveq (p/2)); zify; Z.to_euclidean_division_equations; nia. } + erewrite filter_ext_in, filter_false; cycle 1; cbn [List.app]. + { intros i ?%in_seq; apply Nat.eqb_neq; intros [d X]%Nat.Lcm0.mod_divide. + subst i; destruct d; try nia. } + rewrite map_ext_in with (g:=Nat.add (Z.to_nat q)), map_map; cycle 1. + { intros iq [i [? Hi%in_seq]]%in_map_iff; subst iq. + repeat rewrite <-?Nat2Z.inj_iff, ?Z2Nat.id, ?Nat2Z.inj_mod, ?Nat2Z.inj_div, ?Nat2Z.inj_add, ?Nat2Z.inj_sub, ?Nat2Z.inj_mul; [|(zify; Z.to_euclidean_division_equations; nia)..]. + rewrite Zminus_mod_idemp_r. + rewrite <-Z.mod_add with (a:=Z.sub _ _) (b:=-2%Z) by lia. + eassert (_+-2*q = - (1 + (Z.abs (p*q)-1)/2)) as -> by lia. + rewrite Z_mod_nz_opp_full by + (rewrite (Z.mod_diveq (p/2)); zify; Z.to_euclidean_division_equations; nia). + enough ((1 + (Z.abs (p * q) - 1) / 2) mod q = 1 + ((Z.abs (p * q) - 1) / 2) mod q) by lia. + rewrite <-Z.add_mod_idemp_r by lia. rewrite Z.mod_small; trivial. + rewrite (Z.mod_diveq (p/2)); zify; Z.to_euclidean_division_equations; nia. + } + rewrite map_ext with (g:=fun i => Nat.mul (Z.to_nat q) (S i)), <-map_map, seq_shift by nia. + f_equal. f_equal. repeat rewrite <-?Nat2Z.inj_iff, ?Z2Nat.id, ?Nat2Z.inj_div; + zify; Z.to_euclidean_division_equations; nia. } + + (* multiplying denominator *) + erewrite map_map, (map_ext_in (fun x : nat => of_Zmod (of_Z p (to_Z _)))); cycle 1. + { intros ? L%in_seq. + rewrite to_Z_of_Z, <-of_Z_mod, Z.mod_mod_divide by (exists q; lia). + rewrite Nat2Z.inj_mul, Z2Nat.id, of_Z_mod, of_Z_mul by lia. + rewrite of_Zmod_mul; cycle 1. + { rewrite to_Z_of_Z, Z.coprime_mod_l_iff; trivial. } + { rewrite to_Z_of_Z, Z.coprime_mod_l_iff, Z.coprime_comm. + apply Z.coprime_prime_small; trivial; lia. } + exact eq_refl. } + rewrite <-map_map with (g := mul _), prod_map_mul, length_map, length_seq. + + (* cancellation *) + rewrite div_mul_same_r, Z2Nat.id by (zify; Z.div_mod_to_equations; lia). + eassert ((p / 2) = (p-1)/2) as -> by (zify; Z.div_mod_to_equations; lia). + eassert ((q / 2) = (q-1)/2) as -> by (zify; Z.div_mod_to_equations; lia). + rewrite div_abs1_r by (rewrite euler_criterion_existsb, abs_of_bool; trivial). + + pose proof (@euler_criterion_existsb p (of_Zmod (of_Z _ q)) ltac:(trivial)) as Heul. + apply to_Zmod_inj_iff, signed_inj_iff in Heul; revert Heul. + + (* zification *) + rewrite ?to_Zmod_mul, ?to_Zmod_pow, ?to_Zmod_opp, ?to_Zmod_1. + rewrite signed_mul, ?signed_pow_nonneg_r, ?signed_opp_small, ?signed_1 by + (rewrite ?signed_1; zify; Z.div_mod_to_equations; lia). + rewrite to_Zmod_of_Zmod by (rewrite to_Z_of_Z, Z.coprime_mod_l_iff; trivial). + rewrite signed_of_Z, Z.smod_pow_l. + intro Heul. + rewrite 2Z.smod_small; trivial. + + all : clear -Heul odd_p odd_q Hp' Hq'; rewrite ?Z.pow_m1_l; repeat (case Z.odd; [|]); + try solve [simpl Z.mul; rewrite ?(Z.gcd_opp_l 1), Z.gcd_1_l; trivial]; + try (zify; Z.to_euclidean_division_equations; nia). + all : destruct existsb in *; rewrite ?signed_true, ?signed_false in * by lia. + all : rewrite Heul; clear Heul. + all : rewrite Z.smod_small; try (zify; Z.to_euclidean_division_equations; nia). +Qed. + +Lemma quadratic_reciprocity' + (p q : positive) (prime_p : Z.prime p) (prime_q : Z.prime q) (odd_p : 3 <= p) (odd_q : 3 <= q) (coprime_p_q : Z.gcd p q = 1) : + Z.smodulo (q ^ ((p - 1) / 2)) p * Z.smodulo (p ^ ((q - 1) / 2)) q = + (-1) ^ ((q - 1) / 2 * ((p - 1) / 2)). +Proof. + pose proof odd_prime p prime_p odd_p as Hp'. + pose proof odd_prime q prime_q odd_q as Hq'. + + unshelve epose proof abs_prod_positives_semiprime(p:=p)(q:=q) _ as H; trivial. + unshelve erewrite prod_combinecong, prod_snd_abspairs, prod_fst_abspairs in H; trivial. + progress rewrite ?Z.combinecong_mod_l, ?Z.combinecong_mod_r in H. + apply mul_signed_subgroups_abs, eq_sym in H; trivial. + progress replace (Z.smodulo (∏ positives (p*q)) q) with (Z.smodulo (∏ positives (q*p)) q) in H + by (rewrite Z.mul_comm; trivial). + erewrite 2@prod_positives_semiprime in H by (trivial || rewrite Z.coprime_comm; trivial). + + rewrite !to_Zmod_of_Zmod, !to_Z_of_Z in H. + 2: rewrite to_Z_of_Z, Z.coprime_mod_l_iff; apply Z.coprime_mul_r_iff; + split; rewrite <-Z.coprime_mod_l_iff; + rewrite (proj1 (Z.combinecong_sound_coprime _ _ _ _ coprime_p_q)) + || rewrite (proj2 (Z.combinecong_sound_coprime _ _ _ _ coprime_p_q)); rewrite Z.coprime_mod_l_iff. + rewrite <-(Z.smod_mod _ p), Z.mod_mod_divide, + (proj1 (Z.combinecong_sound_coprime _ _ _ _ coprime_p_q)), Z.smod_mod in H by (exists q; lia). + rewrite <-(Z.smod_mod _ q), Z.mod_mod_divide, + (proj2 (Z.combinecong_sound_coprime _ _ _ _ coprime_p_q)), Z.smod_mod in H by (exists p; lia). + + rewrite ?(Z.smod_small ((-1)^_)), ?(Z.smod_small ((-1)^_*(-1)^_)) in H. + enough ((-1) ^ ((p - 1) / 2) * (-1) ^ ((q - 1) / 2) <> 0) by nia. + all : clear -odd_p odd_q Hp' Hq'; rewrite ?Z.pow_m1_l; repeat (case Z.odd; [|]); + try solve [simpl Z.mul; rewrite ?(Z.coprime_opp_l 1); trivial using Z.coprime_1_l]; + try (zify; Z.to_euclidean_division_equations; nia). +Qed. + +End Zstar. + +End Reciprocity.