proposition: Lemma miller_rabin_sound l n : miller_rabin l n = false -> ~prime n.
proof: Proof. intros c pn. enough (miller_rabin l n = true) by congruence; clear c. unfold miller_rabin. destruct (n <? 2) eqn:n1. { apply Z.ltb_lt in n1. apply prime_ge_2 in pn. lia. } destruct (n =? 2) eqn:n2; auto. apply Z.eqb_neq in n2. apply Z.ltb_ge in n1. assert (bn : n > 2) by lia. clear n1 n2. rewrite andb_true_iff, Z.odd_spec. split. apply primes_are_often_odd; auto; lia. apply miller_rabin_criterion in pn; auto. destruct pn as (s & d & zs & zd & od & e & crit). destruct (remove_twos _) as (s_, d_) eqn:esd. assert (e' : remove_twos (Z.to_pos (n - 1)) = (Z.to_nat s, Z.to_pos d)). { apply remove_twos_spec; split. - exact_eq e; repeat f_equal. + rewrite Z2Pos.id; lia. + rewrite Z2Nat.id; lia. + rewrite Z2Pos.id; lia. - exact_eq od; f_equal. rewrite Z2Pos.id; lia. } rewrite esd in e'. injection e' as -> ->. rewrite Z2Pos.id; auto. rewrite forallb_forall. intros a al. destruct (_ <? _) eqn:za. apply Z.ltb_lt in za. 2:reflexivity. destruct (_ <? _) eqn:an. apply Z.ltb_lt in an. 2:reflexivity. specialize (crit a ltac:(lia)). change (implb (true && true) ?b) with b. rewrite pow_mod_help; try lia. rewrite orb_true_iff, existsb_exists, eqmb_true_iff. destruct crit as [?|(r & rs & er)]. now left. right. exists r. rewrite pow_mod_help'; try lia. rewrite eqmb_true_iff, in_Zseq. split. lia. exact_eq er; repeat f_equal. Qed.
imports: Coq(ZArith Znumtheory Lia Psatz List Bool) Coqtail(Ztools Zeqm Zlittle_fermat Zpow Zprime)