Skip to content

Instantly share code, notes, and snippets.

@davidad
Last active June 25, 2019 13:45
Show Gist options
  • Save davidad/a07686394ffb948f8cff56c48ab982c0 to your computer and use it in GitHub Desktop.
Save davidad/a07686394ffb948f8cff56c48ab982c0 to your computer and use it in GitHub Desktop.
Coq formalization of the infinitude of primes
Require Import Arith Decidable Euclid Psatz Wf_nat.
Definition divides a b := exists k, b = k * a.
Definition prime p := 2 <= p /\ forall k, divides k p -> (k = 1 \/ k = p).
Lemma dec_divides k n: decidable (divides k n).
Proof with intuition.
case (le_gt_dec k 0)...
- case (le_gt_dec n 0).
+ left; exists 0...
+ right... destruct H.
absurd (n = 0); nia.
- pose proof modulo k g n.
destruct H, e, H, x.
+ left; exists x0...
+ right... destruct H1.
absurd ((x1 * k) = (x0 * k + (S x))); try congruence.
case (le_dec x1 x0); nia.
Qed.
Lemma has_prime_divisor {n}: (n > 1) -> exists k, divides k n /\ prime k.
Proof with intuition.
intros.
assert (has_unique_least_element le (fun k => divides k n /\ 2 <= k)).
- apply dec_inh_nat_subset_has_unique_least_element...
+ refine (dec_and _ _ (dec_divides _ _) (dec_le _ _)).
+ exists n...
- do 4 destruct H0.
unfold prime; exists x...
case (le_gt_dec 2 k); destruct H4.
+ right; apply eq_sym, (H1 k)...
* clear - H0 H4; destruct H0.
exists (x0 * x1); nia.
* pose proof (H2 x' (conj H6 H7)).
enough (k <= x); transitivity x...
clear - H3 H4.
assert (x0 > 0); nia.
+ left; clear - H3 H4 g; nia.
Qed.
Lemma divides_fact {n x}: (x <= n /\ x > 1) -> divides x (fact n).
Proof with intuition.
intro H; destruct H; induction H.
- case_eq x...
+ absurd (x > 1)...
+ exists (fact n).
simpl fact at 1; ring.
- destruct IHle.
exists ((S m) * x0).
cbn [fact]; rewrite H1; ring.
Qed.
Theorem primes_infinite : forall n, exists p, p > n /\ prime p.
Proof with intuition.
intro n.
pose (z := 1 + (fact n)).
assert (HZ: z > 1) by (pose proof (lt_O_fact n); intuition).
enough ((exists x, prime x /\ x > 1 /\ divides x z) /\
(forall x, x > n \/ ~ x > n) /\
(forall x, ~(x > 1 /\ divides x z /\ ~ x > n))) by firstorder.
repeat split...
- decompose [ex and] (has_prime_divisor HZ).
exists x...
destruct H1...
- apply dec_gt...
- destruct H.
assert (H3: exists m, m > 0 /\ z = 1 + (m*x)).
+ apply not_gt in H2.
pose proof (divides_fact (conj H2 H0)).
destruct H1 as [m]; clear - H1; exists m...
pose proof (lt_O_fact n); nia.
+ decompose [ex and] H3.
absurd (x0 * x = 1 + x1 * x); try congruence.
clear - H0; case (le_dec x0 x1); nia.
Qed.
Check primes_infinite.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment