Welcome to the JsCoq technology demo! JsCoq is an interactive, web-based environment for the Coq Theorem prover, developed at the Centre de Recherche en Informatique of MINES ParisTech (former École de Mines de Paris).
JsCoq is open source. If you find any problem or want to make any contribution, you are extremely welcome! We await your feedback at github.
The scratchpad offers simple, local storage functionality. Please go to CollaCoq if you want to share your developments with other users.
Alt+Enter or Alt+→ goes to the current point; Alt+N/P or Alt+↓/↑ will move through the proof; F8 or the power icon toggles the goal panel.
We don't provide a Coq tutorial (yet), but as a showcase, we display a proof of the infinitude of primes in Coq. The proof relies in the Mathematical Components library by the MSR/Inria team led by Georges Gonthier, so our first step will be to load it and set a few Coq options:
Once the basic environment has been set up, we can proceed to the proof:
The lemma states that given a number m, there is a primer 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` greater than `m`. What would be a suitable `p`? Choosing as `p` the first prime divisor of `m! + 1` works. As we will shortly see, properties of divisibility will imply that `p` is 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!`, but `p` prime cannot divide 1, a necessary condition for `p` to divide `m! + 1`.
jsCoq provides many other packages, including Coq's standard library and the mathematical components library. Feel free to experiment, and bear with the alpha status of this demo.
JsCoq's homepage is at github https://github.com/ejgallego/jscoq ¡Salut!