Newer
Older
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<title>jsCoq – Use Coq in Your Browser</title>
<meta http-equiv="content-type" content="text/html;charset=utf-8" />
<meta name="description" content="An Online IDE for the Coq Theorem Prover" />
<link rel="stylesheet" type="text/css" href="node_modules/bootstrap/dist/css/bootstrap.min.css">
<script src="node_modules/bootstrap/dist/js/bootstrap.min.js"></script>
<link rel="stylesheet" type="text/css" href="ui-css/landing-page.css">
<body class="jscoq-main">
<div id="ide-wrapper" class="toggled">
<div id="code-wrapper">
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
<div id="document-wrapper">
<!------------------------------->
<!-- N A V B A R -->
<!------------------------------->
<nav class="navbar sticky-top navbar-expand-lg navbar-light bg-light">
<div class="container-fluid">
<a class="navbar-brand"><img src="ui-images/favicon.png"></a>
<button class="navbar-toggler" type="button" data-bs-toggle="collapse" data-bs-target="#navbarSupportedContent" aria-controls="navbarSupportedContent" aria-expanded="false" aria-label="Toggle navigation">
<span class="navbar-toggler-icon"></span>
</button>
<div class="collapse navbar-collapse" id="navbarSupportedContent">
<ul class="navbar-nav me-auto mb-2 mb-lg-0">
<li class="nav-item dropdown">
<a class="nav-link dropdown-toggle" href="#" id="navbarAbout" role="button" data-bs-toggle="dropdown" aria-expanded="false">
About
</a>
<ul class="dropdown-menu" aria-labelledby="navbarDropdown">
<li><a class="dropdown-item" href="#">jsCoq Dev Team</a></li>
<li><hr class="dropdown-divider"></li>
<li><a class="dropdown-item" href="#">Coq Proof Assistant</a></li>
<li><a class="dropdown-item" href="#">company-coq</a></li>
</ul>
</li>
<li class="nav-item dropdown">
<a class="nav-link dropdown-toggle" href="#" id="navbarExamples" role="button" data-bs-toggle="dropdown" aria-expanded="false">
Examples
</a>
<ul class="dropdown-menu" aria-labelledby="navbarDropdown">
<li><a class="dropdown-item" href="#">Infinitude of Primes</a></li>
<li><a class="dropdown-item" href="#">Irrationality of <img class="symbol-sqrt" src="ui-images/sqrt.svg">2</a></li>
<li><hr class="dropdown-divider"></li>
<li><a class="dropdown-item" href="/ext/sf"><img class="symbol-book" src="ui-images/book.svg">Software Foundations</a></li>
</ul>
</li>
</ul>
</div>
</div>
<a id="scratchpad" href="examples/scratchpad.html" title="Open scratchpad"></a>
</nav>
<!------------------------------->
<h3>Welcome to the <span class="jscoq-name">jsCoq</span> Interactive Online System!</h3>
Welcome to the <span class="jscoq-name">jsCoq</span> technology demo!
<span class="jscoq-name">jsCoq</span> is an interactive,
web-based environment for the Coq Theorem prover, and is a collaborative
development effort. See the <a href="#team">list of contributors</a>
below.
<span class="jscoq-name">jsCoq</span> is open source. If you find any problem or want to make
any contribution, you are extremely welcome! We await your
feedback at <a href="https://github.com/jscoq/jscoq">GitHub</a>
and <a href="https://coq.zulipchat.com/#narrow/stream/256336-jsCoq">Zulip</a>.
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
<h4>Instructions:</h4>
<p>
The following document contains embedded Coq code.
All the code is editable and can be run directly on the page.
Once <span class="jscoq-name">jsCoq</span> finishes loading, you are
free to experiment by stepping through the proof and viewing intermediate
proof states on the right panel.
</p>
<h5>Actions:</h5>
<table class="doc-actions">
<tr><th>Button</th><th>Key binding</th><th>Action</th></tr>
<tr>
<td><img src="ui-images/down.png" height="15px"><img src="ui-images/up.png" height="15px"></td>
<td>
<kbd>Alt</kbd>+<kbd>↓</kbd>/<kbd>↑</kbd> or<br/>
<kbd>Alt</kbd>+<kbd>N</kbd>/<kbd>P</kbd>
</td>
<td>Move through the proof.</td>
</tr>
<tr>
<td><img src="ui-images/to-cursor.png" height="20px"></td>
<td>
<kbd>Alt</kbd>+<kbd>Enter</kbd> or<br/> <kbd>Alt</kbd>+<kbd>→</kbd>
</td>
<td>Run (or go back) to the current point.</td>
</tr>
<tr>
<td><img src="ui-images/power-button-512-black.png" height="20px"></td>
<td><kbd>F8</kbd></td>
<td>Toggles the goal panel.</td>
</tr>
</table>
<h5>Creating your own proof scripts:</h5>
The <a href="examples/scratchpad.html">scratchpad</a> offers simple, local
storage functionality. It also allows you to share your development with
other users in a manner that is similar to Pastebin.
<h4>A First Example: The Infinitude of Primes</h4>
If you are new to Coq, check out this
<a href="examples/nahas_tutorial.html">introductory tutorial</a> by
<a href="https://mdnahas.github.io">Mike Nahas</a>.
As a more advanced showcase, we display a proof of the infinitude of primes in Coq.
The proof relies on the <a href="https://math-comp.github.io">Mathematical Components</a>
library from the
<a href="http://ssr.msr-inria.inria.fr/">MSR/Inria</a> team led
by Georges Gonthier, so our first step will be to load it:
</p>
</div>
<div>
<textarea id="addnC" >
From Coq Require Import ssreflect ssrfun ssrbool.
From mathcomp Require Import eqtype ssrnat div prime. </textarea>
<h5>Ready to do Proofs!</h5>
Once the basic environment has been set up, we can proceed to
the proof:
</p>
</div> <!-- panel-heading -->
<div>
<textarea id="prime_above1" >
(* A nice proof of the infinitude of primes, by Georges Gonthier *)
Lemma prime_above m : {p | m < p & prime p}.
Proof. </textarea>
<p>
The lemma states that for any number <code>m</code>,
there is a prime number larger than <code>m</code>.
Coq is a <em>constructive system</em>, 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 <code>p</code>
What would be a suitable <code>p</code>?
Choosing <code>p</code> to be the first prime divisor of <code>m! + 1</code>
works.
As we will shortly see, properties of divisibility will imply that
<code>p</code> must be greater than <code>m</code>.
</p>
<textarea id="prime_above2" >
have /pdivP[p pr_p p_dv_m1]: 1 < m`! + 1
by rewrite addn1 ltnS fact_gt0.</textarea>
<p>
Our first step is thus to use the library-provided lemma
<code>pdivP</code>, which states that every number is divided by a
prime. Thus, we obtain a number <code>p</code> and the corresponding
hypotheses <code>pr_p : prime p</code> and <code>p_dv_m1</code>,
"p divides m! + 1".
The ssreflect tactic <code>have</code> provides a convenient way to
instantiate this lemma and discard the side proof obligation
<code>1 < m! + 1</code>.
</p>
<textarea id="prime_above3" >
exists p => //; rewrite ltnNge; apply: contraL p_dv_m1 => p_le_m.</textarea>
<p>
It remains to prove that <code>p</code> is greater than <code>m</code>.
contraposition with the divisibility hypothesis, which gives us
the goal "if <code>p ≤ m</code> then <code>p</code> is not a prime divisor of
</p>
<textarea id="prime_above4" >
by rewrite dvdn_addr ?dvdn_fact ?prime_gt0 // gtnNdvd ?prime_gt1.
<p>
The goal follows from basic properties of divisibility, plus
from the fact that if <code>p ≤ m</code>, then <code>p</code> divides
<code>m!</code>, so that for <code>p</code> to divide
<code>m! + 1</code> it must also divide 1,
in contradiction to <code>p</code> being prime.
</p>
<hr/>
<span class="jscoq-name">jsCoq</span> provides many other packages,
including Coq's standard library and the
<a href="https://math-comp.github.io"></a>mathematical components</a>
library.
Feel free to experiment, and bear with the beta status of this demo.
</p>
</div> <!-- /#panel body -->
<div id="team">
<a name="team"></a>
<p><i>The dev team</i></p>
<ul>
<li>
<a href="https://www.irif.fr/~gallego/">Emilio Jesús Gallego Arias</a>
(<a href="https://www.inria.fr">Inria</a>,
<a href="https://u-paris.fr">Université de Paris</a>,
<a href="https://www.irif.fr">IRIF</a>)
</li>
<li>
<a href="https://www.cs.technion.ac.il/~shachari/">Shachar Itzhaky</a>
(<a href="https://cs.technion.ac.il">Technion</a>)
</li>
</ul>
<p><i>Contributors</i></p>
<ul>
<li>
Benoît Pin
(<a href="https://www.cri.ensmp.fr/">CRI</a>,
<a href="http://www.mines-paristech.eu">MINES ParisTech</a>)
</li>
</ul>
</div>
</div> <!-- /#code-wrapper -->
<script src="ui-js/jscoq-loader.js" type="text/javascript"></script>
var jscoq_ids = ['addnC', 'prime_above1', 'prime_above2', 'prime_above3', 'prime_above4' ];
implicit_libs: false,
editor: { mode: { 'company-coq': true } },
all_pkgs: ['coq', 'mathcomp', 'equations', 'elpi', 'quickchick', 'lf', 'plf']
};
/* Global reference */
JsCoq.start(jscoq_ids, jscoq_opts).then(res => coq = res);