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" />
<style>body { visibility: hidden; } /* FOUC avoidance */</style>
<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="node_modules/katex/dist/katex.min.css">
<link rel="stylesheet" type="text/css" href="ui-css/landing-page.css">
<link rel="stylesheet" type="text/css" href="ui-css/kbd.css">
<script src="ui-js/jscoq-loader.js" type="text/javascript"></script>
<body class="jscoq-main">
<div id="ide-wrapper" class="toggled">
<div id="code-wrapper">
<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" 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="#team">jsCoq Dev Team</a></li>
<li><a class="dropdown-item" href="https://coq.inria.fr">Coq Proof Assistant</a></li>
<li><a class="dropdown-item" href="https://github.com/cpitclaudel/company-coq">company-coq</a></li>
</ul>
</li>
<li class="nav-item dropdown">
<a class="nav-link dropdown-toggle" 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="examples/inf-primes.html">Infinitude of Primes</a></li>
<li><a class="dropdown-item" href="examples/sqrt_2.html">Irrationality of <span class="math"><img class="symbol-sqrt" src="ui-images/sqrt.svg">2</span></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">
<span class="newcomer scratchpad-tip">open the scratchpad<br/>to start editing</span>
</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>.
<h4>A First Example:
<span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1.1017em;vertical-align:-0.1944em;"></span><span class="mord sqrt"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.9072em;"><span class="svg-align" style="top:-3em;"><span class="pstrut" style="height:3em;"></span><span class="mord" style="padding-left:0.833em;"><span class="mord">2</span></span></span><span style="top:-2.8672em;"><span class="pstrut" style="height:3em;"></span><span class="hide-tail" style="min-width:0.853em;height:1.08em;"><svg xmlns="http://www.w3.org/2000/svg" width='400em' height='1.08em' viewBox='0 0 400000 1080' preserveAspectRatio='xMinYMin slice'><path d='M95,702
c-2.7,0,-7.17,-2.7,-13.5,-8c-5.8,-5.3,-9.5,-10,-9.5,-14 c0,-2,0.3,-3.3,1,-4c1.3,-2.7,23.83,-20.7,67.5,-54 c44.2,-33.3,65.8,-50.3,66.5,-51c1.3,-1.3,3,-2,5,-2c4.7,0,8.7,3.3,12,10 s173,378,173,378c0.7,0,35.3,-71,104,-213c68.7,-142,137.5,-285,206.5,-429 c69,-144,104.5,-217.7,106.5,-221 l0 -0 c5.3,-9.3,12,-14,20,-14 H400000v40H845.2724 s-225.272,467,-225.272,467s-235,486,-235,486c-2.7,4.7,-9,7,-19,7 c-6,0,-10,-1,-12,-3s-194,-422,-194,-422s-65,47,-65,47z M834 80h400000v40h-400000z'/></svg>
</span></span></span><span class="vlist-s"></span></span><span class="vlist-r"><span class="vlist" style="height:0.1328em;"><span></span></span></span></span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mrel"><span class="mord vbox"><span class="thinbox"><span class="rlap"><span class="strut" style="height:0.8889em;vertical-align:-0.1944em;"></span><span class="inner"><span class="mord"><span class="mrel"></span></span></span><span class="fix"></span></span></span></span></span></span><span class="base"><span class="strut" style="height:0.5782em;vertical-align:-0.0391em;"></span><span class="mrel">∈</span><span class="mspace" style="margin-right:0.2778em;"></span></span><span class="base"><span class="strut" style="height:0.8556em;vertical-align:-0.1667em;"></span><span class="mord mathbb">Q</span></span></span></span>
</h4>
The following is a simple proof that <span class="math"><img class="symbol-sqrt" src="ui-images/sqrt.svg">2</span>
cannot be expressed as the ratio of two integers; that is, for every two integers
<span class="math"><i>p</i></span> and <span class="math"><i>q</i></span>,
<span class="math">(<i>p/q</i>)<sup>2</sup> ≠ 2</span>.
This is a simplified version of a similar
<a href="https://github.com/coq-community/qarith-stern-brocot/blob/master/theories/sqrt2.v">proof by Milad Niqui</a>.
Use <span class="has-kbd"><kbd>Alt</kbd>+<kbd>↓</kbd>/<kbd>↑</kbd></span> to step through the proof,
and observe the proof state on the right panel.
</p>
<textarea class="snippet">
From Examples Require Import sqrt_2.
Theorem sqrt2_not_rational :
forall p q : nat, q <> 0 -> p^2 <> 2 * q^2.</textarea>
<p class="interim">
First, we simplify the goal a bit by inlining the
definition of <span class="math"><span class="symbol-square">⃞</span><sup>2</sup></span>.
</p>
<textarea class="snippet">
Proof.
assert (forall x, x ^ 2 = x * x) as sq by (simpl; lia).
intros p q; rewrite! sq; clear sq.</textarea>
<p class="interim">
The proof proceeds by <a href="https://en.wikipedia.org/wiki/Mathematical_induction#Complete_(strong)_induction"></https:>complete induction</a>
on <span class="math"><i>q</i></span>, generalizing over
<span class="math"><i>p</i></code>.
</p>
<textarea class="snippet">
revert p.
induction q as [q IH] using (well_founded_ind lt_wf).
intros p Hneq.</textarea>
<p class="interim">
The gist of the proof is realizing that it can be obtained by
instantiating the induction hypothesis with values
<span class="math">3<i>q</i><span class="symbol-minus">–</span>2<i>p</i></span> and
<span class="math">3<i>p</i><span class="symbol-minus">–</span>4<i>q</i></span>.
</p>
<textarea class="snippet">
specialize IH with (y := 3 * q - 2 * p) (p := 3 * p - 4 * q).</textarea>
<p class="interim">
The rest follows from simpler inequalities,
<span class="math">2<i>p</i> < 3<i>q</i>
< 2<i>p</i><span class="symbol-plus">+</span><i>q</i></span>
<span class="math">4<i>q</i> < 3<i>p</i></span>.
These are not included in the example; for details, see
<a href="examples/sqrt_2.html">the full proof</a>.
</p>
<textarea class="snippet">
intro Heq; apply IH.
- apply comparison_3q2p. all: auto.
- apply Nat.sub_gt. apply comparison_2p3q. all: auto.
- rewrite! sub_square_identity.
+ clear IH; lia.
+ auto using comparison_2p3q, Nat.lt_le_incl.
+ auto using comparison_4q3p, Nat.lt_le_incl.
<hr/> <!-- end of proof -->
<h4>Quick start</h4>
Use the <a href="examples/scratchpad.html">scratchpad <span class="scratchpad-small"></span></a>
for a fresh page to write your proofs on.
<span class="jscoq-name">jsCoq</span> provides basic UI for running
and inspecting proofs, similar to IDEs such as <a href="https://coq.inria.fr/refman/practical-tools/coqide.html">CoqIDE</a>,
<a href="https://proofgeneral.github.io/">Proof General</a>,
and <a href="https://github.com/coq-community/vscoq">VSCoq</a>.
<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/power-button-512-black.png" height="20px"></td>
<td>Toggles the goal panel.</td>
</tr>
<tr>
<td><img src="ui-images/down.png" height="15px"><img src="ui-images/up.png" height="15px"></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>
<kbd>Alt</kbd>+<kbd>Enter</kbd> or<br/> <kbd>Ctrl</kbd>+<kbd>Enter</kbd><br/>
(⌘ on Mac)
</td>
<td>Run (or go back) to the current point.</td>
</tr>
<tr>
<kbd>Ctrl</kbd>+<img class="symbol-mouse" src="ui-images/pointer.svg">
</td>
<td>Hover executed statements to peek at the proof state after each step.</td>
<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.
<h5>There's more</h5>
<p>
See the <a href="https://github.com/jscoq/jscoq/tree/v8.15/docs">official docs</a>
on GitHub for more details on using, building, embedding, and integrating
<span class="jscoq-name">jsCoq</span> in your developments.
</p>
<span class="jscoq-name">jsCoq</span> comes with a variety of addon packages,
including Coq's standard library and the
<a href="https://math-comp.github.io">mathematical components</a>
library.
Feel free to experiment, and let us know if you have any suggestions
and/or when you have done something cool with <span class="jscoq-name">jsCoq</span>.
😎
</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 -->
</div> <!-- /#ide-wrapper -->
<script type="text/javascript">
if (!localStorage['scratchpad.last_filename'])
setTimeout(() => document.body.classList.add('welcome'), 1500);
var jscoq_ids = ['.snippet'];
implicit_libs: false,
editor: { mode: { 'company-coq': true } },
all_pkgs: {'+': ['coq', 'mathcomp', 'equations', 'elpi',
'quickchick', 'software-foundations',
'hahn', 'paco', 'snu-sflib',
'fcsl-pcm', 'htt', 'pnp', 'stdpp', 'iris'],
'./examples': ['examples']}
};
/* Global reference */
JsCoq.start(jscoq_ids, jscoq_opts).then(res => {
coq = res;
coq.loadSymbolsFrom('./examples/examples.symb.json');
});