proposition: Theorem miller_rabin_criterion (p : Z) : p > 2 -> prime p -> exists s d : Z, 0 < s /\ 0 < d /\ Z.Odd d /\ p - 1 = 2 ^ s * d /\ forall a, 0 < a < p -> a ^ d ≡ 1 [p] \/ exists r, 0 <= r < s /\ a ^ (2 ^ r * d) ≡ -1 [p].
proof: Proof. intros p3 pp. pose proof primes_are_often_odd p ltac:(lia) pp as op. destruct (factoring_out_prime_at_least_once 2 (p - 1)) as (s & d & psd & d2 & s1). - apply prime_2. - lia. - destruct op as (k & ->). exists k. lia. - assert (0 < d). { enough (~d = 0 /\ ~d < 0) by lia. split; intros d0. - apply d2. exists 0. lia. - enough (2 ^ s * d < 0) by lia. apply Z.mul_pos_neg. 2:lia. apply Z.pow_pos_nonneg; lia. } exists s, d. repeat split; try lia. + apply Odd_div, d2. + intros a zap. pose proof Fermat's_little_theorem_Z_pZ p a pp zap as f. rewrite psd in f. clear psd. apply eqm_divide in f; try now apply prime_not_0. change (a ^ (2 ^ s * d) ≡ 1 [p]) in f. assert (s0 : 0 <= s) by lia. revert s s0 s1 f. match goal with |- forall s, 0 <= s -> ?G => apply (Z.right_induction (fun s => G)) end. intros ? ? ->; tauto. lia. intros s s0 IHs s0_ asp. apply miller_rabin_step in asp; lia || auto. destruct asp as [e | e]. * destruct (Z.eq_dec s 0) as [-> | s1]. -- left. exact_eq e. repeat f_equal. lia. -- destruct (IHs ltac:(lia) e) as [ ? | (r & lr & E)]; auto. right. exists r. split; lia || auto. * right. exists s. split; lia || auto. Qed.
imports: Coq(ZArith Znumtheory Lia Psatz List Bool) Coqtail(Ztools Zeqm Zlittle_fermat Zpow Zprime)