### Welcome to the jsCoq Interactive Online System!

Welcome to the jsCoq technology demo! jsCoq is an interactive, web-based environment for the Coq Theorem prover, and is a collaborative development effort. See the list of contributors below.

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 and Gitter.

#### Instructions:

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.

##### Actions:

Button | Key binding | Action
--- | --- | ---
↓↑ | `Alt`+`↓`/`↑` or `Alt`+`N`/`P` | Move through the proof.
→ | `Alt`+`Enter` or `Alt`+`→` | Run (or go back) to the current point.
⏻ | `F8` | Toggles the goal panel.

##### Saving your own proof scripts:

The scratchpad offers simple, local storage functionality. Please go to CollaCoq if you want to share your developments with other users.

#### A First Example: The Infinitude of Primes

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:

From Coq Require Import ssreflect ssrfun ssrbool. From mathcomp Require Import eqtype ssrnat div prime.

##### Ready to do Proofs!

Once the basic environment has been set up, we can proceed to the proof:

(* A nice proof of the infinitude of primes, by Georges Gonthier *) Lemma prime_above m : {p | m < p & prime p}. 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`.

have /pdivP[p pr_p p_dv_m1]: 1 < m`! + 1 by rewrite addn1 ltnS fact_gt0.

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`.

exists p => //; rewrite ltnNge; apply: contraL p_dv_m1 => p_le_m.

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`".

by rewrite dvdn_addr ?dvdn_fact ?prime_gt0 // gtnNdvd ?prime_gt1. Qed.

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.

jsCoq provides many other packages, including Coq's standard library and the mathematical components library. Feel free to experiment, and bear with the beta status of this demo.

¡Salut!

The dev team

- Emilio Jesús Gallego Arias (Inria, Université de Paris, IRIF)
- Shachar Itzhaky (Technion)

Contributors

- Benoît Pin (CRI, MINES ParisTech)