proposition: Theorem prime_bool_spec p : prime_bool p = true <-> prime p.
proof: Proof. unfold prime_bool. rewrite orb_true_iff, !andb_true_iff, negb_true_iff, divides_bool_spec'. rewrite Nat.eqb_eq, Nat.leb_le. split. + intros [ H1 | ((H1 & H2) & H3) ]. * subst; auto. * split; try lia. destruct (euclid_2 p) as (p' & [ Hp | Hp ]). { destruct H2; exists p'; lia. } destruct p' as [ | p' ]; try (exfalso; lia). rewrite prime_bool_rec_spec in H3; try lia. intros q Hq. destruct (euclid_2 q) as (k & [ H4 | H4 ]). - destruct H2; apply divides_trans with (2 := Hq); exists k; lia. - destruct k as [ | k ]; try lia. destruct (le_lt_dec p q) as [ H5 | H5 ]. ++ apply divides_le in Hq; lia. ++ assert (k < p') as H6 by lia. destruct (H3 (p'-S k)); try lia. eq goal Hq; f_equal; lia. + intros (H1 & H2). destruct (le_lt_dec 3 p) as [ H3 | H3 ]. * right; lsplit 2; auto. - intros C; apply H2 in C; lia. - apply prime_bool_rec_spec; try lia. intros q H4 H5. apply H2 in H5; lia. * left; destruct p; try lia. destruct (H2 2); try lia. exists 0; auto. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat gcd sums)