From fc86dae9ebe50c7a9afb115c336b5d105a78498c Mon Sep 17 00:00:00 2001 From: thery Date: Sun, 13 Oct 2024 01:52:44 +0200 Subject: [PATCH] a is unbounded --- euler.v | 41 +++++++++++++++++++++-------------------- 1 file changed, 21 insertions(+), 20 deletions(-) diff --git a/euler.v b/euler.v index 1c56be4..b405b64 100644 --- a/euler.v +++ b/euler.v @@ -17,12 +17,12 @@ apply/eqP; elim/big_rec2: _ => // i m n _ /eqP nEm. by rewrite modnMml -modnMmr nEm modnMmr. Qed. -Definition res_quad p a := has (fun i => (i * i) %% p == a) (iota 0 p). +Definition res_quad p a := has (fun i => i * i == a %[mod p]) (iota 0 p). Compute res_quad 7 4. Lemma res_quadP a p : - reflect (exists i : 'I_p, (i * i) %% p = a) (res_quad p a). + reflect (exists i : 'I_p, i * i = a %[mod p]) (res_quad p a). Proof. apply: (iffP hasP) => [[x /[!mem_iota] [/andP[_ xLp] /eqP xxE]]|[x xxE]]. by exists (Ordinal xLp). @@ -30,7 +30,7 @@ by exists (val x); [rewrite mem_iota /= | apply/eqP]. Qed. Lemma res_quadPn a p : - reflect (forall i : 'I_p, (i * i) %% p != a) (~~ (res_quad p a)). + reflect (forall i : 'I_p, i * i != a %[mod p]) (~~ (res_quad p a)). Proof. apply: (iffP hasPn) => [xxE i| xxE i /[!mem_iota] /= iI]. by apply: xxE; rewrite mem_iota /=. @@ -38,21 +38,22 @@ by apply: (xxE (Ordinal iI)). Qed. Lemma fact_sqr_exp a p : - prime p -> 0 < a < p -> ~~ res_quad p a -> (p.-1`!) = a ^ p.-1./2 %[mod p]. + prime p -> ~~ (p %| a) -> ~~ res_quad p a -> (p.-1`!) = a ^ p.-1./2 %[mod p]. Proof. -move=> pP aLp aR. +move=> pP pNDa aR. have -> : p.-1`! = \prod_(i in 'F_p | i != 0%R) i. apply: etrans (_ : \prod_(i in 'F_p | i != 0 :> nat) i = _); last first. by apply: eq_bigl => i. rewrite /= Fp_cast //. rewrite fact_prod big_add1 /= big_mkord. - case: p {aLp aR}pP => //= p pP. + case: p {pNDa aR}pP => //= p pP. by rewrite [RHS]big_mkcond /= big_ord_recl /= mul1n. pose a' : 'F_p := inZp a. +have a'E : a' = a %% p :> nat by rewrite /= Fp_cast. have a'_neq0 : a' != 0%R. - apply/eqP=> /val_eqP /=. - rewrite Fp_cast // modn_small; first by case: (a) aLp. - by case/andP: aLp. + apply/eqP/val_eqP; rewrite [val a']a'E /=. + by have /negPf := pNDa; rewrite /dvdn => ->. +rewrite -modnXm -a'E. pose f (i : 'F_p) : 'F_p := (a' / i)%R. have f_eq0 : f 0%R = 0%R by rewrite /f GRing.invr0 GRing.mulr0. have fM (i : 'F_p) : i != ord0 -> (f i * i = a')%R. @@ -65,7 +66,7 @@ have fI_neq0 (i : 'F_p) : i != 0%R -> f i != i. have /res_quadPn/(_ (Ordinal iL)) /= := aR. have /val_eqP := fM _ i_neq0; rewrite fiE /=. rewrite ![X in _ %% X]Fp_cast //= => /eqP->. - by rewrite modn_small ?eqxx // Fp_cast; case/andP: aLp. + by rewrite Fp_cast // eqxx. have fB : {on [pred i | i != ord0], bijective f}. by exists f => j _; apply: fI. pose can (i : 'F_p) := if i < (f i) then i else f i. @@ -92,14 +93,11 @@ apply: etrans (_ : \prod_(j in 'F_p | j < f j) (j * f j) = _ %[mod p]). rewrite /can; case: leqP; last by case: (i =P j); rewrite andbF. case: (f i =P j); rewrite ?andbF // => <-. by rewrite fI eqxx andbF. -apply: etrans (_ : \prod_(j in 'F_p | j < f j) a = _ %[mod p]). +apply: etrans (_ : \prod_(j in 'F_p | j < f j) a' = _ %[mod p]). rewrite -modn_prodm; congr (_ %% _); apply: eq_bigr => i /andP[_ iLfi]. have i_neq0 : i != 0%R. by apply/eqP=> i_eq0; rewrite i_eq0 f_eq0 ltnn in iLfi. - have /val_eqP/eqP := fM i i_neq0. - have -> : val a' = a. - by rewrite /= modn_small // Fp_cast; case/andP: aLp. - move=> <- //=; rewrite mulnC. + rewrite -(fM i i_neq0) mulnC. by congr (_ %% _); rewrite Fp_cast. congr (_ %% _). rewrite prod_nat_const. @@ -130,25 +128,28 @@ by case: eqP => // ->; rewrite f_eq0 ltnn. Qed. Lemma euler_criterion a p : - prime p -> 0 < a < p -> + prime p -> ~~ (p %| a) -> a ^ p.-1./2 = (if res_quad p a then 1 else p.-1) %[mod p]. Proof. -move=> pP aLp. +move=> pP pNDa. have p_gt0 : 0 < p by apply: prime_gt0. have [/res_quadP[i Hi]|Hrn] := boolP (res_quad p a); last first. rewrite -fact_sqr_exp //. apply/eqP; rewrite -(eqn_modDr 1) !addn1 prednK //. have /dvdnP[k->] : (p %| (p.-1)`!.+1) by rewrite -Wilson // prime_gt1. by rewrite modnn modnMl. -rewrite -modnXm -Hi modn_mod modnXm mulnn -expnM mul2n. +rewrite -modnXm -Hi modnXm mulnn -expnM mul2n. have [pO|/(prime_oddPn pP) pE2]:= boolP (odd p); last first. by rewrite [in X in _ ^ X]pE2 /= expn0. -have i_gt0 : 0 < i by case: i Hi aLp => [] [] //= _ <-; rewrite mod0n. +have i_gt0 : 0 < i. + case: i Hi pNDa => [] [] //= _. + by rewrite /dvdn => <- /[!mod0n]. rewrite even_halfK; last by case: (p) pP pO. apply/eqP; rewrite eqn_mod_dvd //; last by rewrite expn_gt0 i_gt0. rewrite -(Gauss_dvdr _ (_ : coprime _ i)); last first. rewrite prime_coprime //; apply/negP => /dvdnP [k iE]. - by rewrite -Hi iE mulnA modnMl in aLp. + rewrite iE mulnA modnMl in Hi. + by case/negP: pNDa; rewrite /dvdn -Hi. rewrite mulnBr muln1 -expnS prednK //. rewrite -eqn_mod_dvd //; first by apply/eqP/fermat_little. by apply: leq_pexp2l (_ : 1 <= p).