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 current version requires Chrome >= 48 or Firefox >= 45. Below, we provide an example of jsCoq, go to CollaCoq if you want a page with Save/Load capabilities.
Alt-Enter (Cmd should work in Macs too) goes to the current point; Alt-N/P or Alt-Down/Up will move through the proof; F8 or the power icon toogles 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 enviroment has been setup, we can proceed to do the proof:
The lemma states that given a number m, there is a primer number larger than m.
Which is this prime number? A suitable candidate is provided by the first prime divisor of !m + 1. The lemma `pdivP` states that every number is divided by a prime, so we use it go the number we want.
Now we need to prove that such prime divisor p is indeed greater than m. Using contraposition, we can instead prove that p <= m implies that p is not a primer divisor of !m + 1.
This follows from the fact that p, with p < m, divides !m, but a prime number cannot divide 1.
jsCoq provides many other packages, including most of Coq's standard library and the full 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!