The following document contains embedded Coq code. All the code is editable and can be run directly on the page. Once jsCoq finishes loading, you are free to experiment by stepping through the proof and viewing intermediate proof states on the right panel.
Button | Key binding | Action |
---|---|---|
F8 | Toggles the goal panel. | |
Alt+↓/↑ or Alt+N/P |
Move through the proof. | |
Alt+Enter or Ctrl+Enter (⌘ on Mac) |
Run (or go back) to the current point. | |
Ctrl+ | Hover executed statements to peek at the proof state after each step. |
As a relatively advanced showcase, we display a proof of the infinitude of primes in Coq. The proof relies on the Mathematical Components library from the MSR/Inria team led by Georges Gonthier, so our first step will be to load it:
Once the basic environment has been set up, we can proceed to the proof:
The lemma states that for any number m
,
there is a prime number larger than m
.
Coq is a constructive system, which among other things
implies that to show the existence of an object, we need to
actually provide an algorithm that will construct it.
In this case, we need to find a prime number p
that is greater than m
.
What would be a suitable p
?
Choosing p
to be the first prime divisor of m! + 1
works.
As we will shortly see, properties of divisibility will imply that
p
must be greater than m
.
Our first step is thus to use the library-provided lemma
pdivP
, which states that every number is divided by a
prime. Thus, we obtain a number p
and the corresponding
hypotheses pr_p : prime p
and p_dv_m1
,
"p divides m! + 1".
The ssreflect tactic have
provides a convenient way to
instantiate this lemma and discard the side proof obligation
1 < m! + 1
.
It remains to prove that p
is greater than m
.
We reason by
contraposition with the divisibility hypothesis, which gives us
the goal "if p ≤ m
then p
is not a prime divisor of
m! + 1
".
The goal follows from basic properties of divisibility, plus
from the fact that if p ≤ m
, then p
divides
m!
, so that for p
to divide
m! + 1
it must also divide 1,
in contradiction to p
being prime.
¡Salut!