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" />
<!-- Move to copy with the bundle -->
<link rel="icon" href="frontend/classic/images/favicon.png">
<style>body { visibility: hidden; } /* FOUC avoidance */</style>
<link rel="stylesheet" type="text/css" href="./dist/frontend/index.css">
<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="frontend/classic/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="frontend/classic/images/sqrt.svg">2</span></a></li>
<!-- these are only available from the full website -->
<li><a class="dropdown-item" href="/fun/coqoban.html">🎡 Çoqoban</a></li>
<li><a class="dropdown-item" href="/ext/sf"><img class="symbol-book" src="frontend/classic/images/book.svg">Software Foundations</a></li>
<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>
<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
that you wish to report or want to add your own 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: <code>rev</code> <code>∘</code> <code>rev = id</code></h4>
The following is a simple proof that <code>rev</code>, the standard list
reversal function as commonly defined in ML and other languages of the
family, is an involution.
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.
<textarea class="snippet">
From Coq Require Import List.
Import ListNotations.</textarea>
We are going to need a simpler auxiliary lemma, one that connects
<code>rev</code>, <code>::</code> (the list constructor, also known
as <code>cons</code>), and <code>snoc</code> (the dual of
<code>cons</code>, a function that appends an element at the end of
a list).
This is because the latter two participate in the definition of
the former, <code>rev</code>.
<textarea class="snippet">Lemma rev_snoc_cons A :
forall (x : A) (l : list A), rev (l ++ [x]) = x :: rev l.</textarea>
This proposition is proven by way of the standard induction on
the structure of the list <code>l</code>.
<textarea class="snippet">Proof.
induction l.
- reflexivity.
- simpl. rewrite IHl. simpl. reflexivity.
Qed.</textarea>
Now we prove the central equality with a similar induction.
<textarea class="snippet">Theorem rev_rev A : forall (l : list A), rev (rev l) = l.
Proof.
induction l.
- reflexivity.
- simpl. rewrite rev_snoc_cons. rewrite IHl.
reflexivity.
Qed.</textarea>
Finally, we apply functional extensionality to produce the equality
as it was written in the title.
<p class="interim">
There is only one syntactic difference, which is that, in Coq, we
need to pass an explicit value to the implicit (generic) type
parameter <code>A</code> of <code>rev</code>.
</p>
<textarea class="snippet">From Coq.Program Require Import Basics.
From Coq Require Import FunctionalExtensionality.
Open Scope program_scope.
Theorem rev_invol A : rev (A:=A) ∘ rev (A:=A) = id.
Proof.
apply functional_extensionality.
intro x.
unfold compose, id. rewrite rev_rev.
reflexivity.
<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>
<td><img src="frontend/classic/images/power-button-512-black.png" height="20px"></td>
<td>Toggles the goal panel.</td>
</tr>
<td><img src="frontend/classic/images/down.png" height="15px"><img src="frontend/classic/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="frontend/classic/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="frontend/classic/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>
See the <a href="https://github.com/jscoq/jscoq/tree/v8.17/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 -->
<script type="module">
var sp = new URLSearchParams(location.search);
setTimeout(() => document.body.classList.add('welcome'), 1500);
var jscoq_ids = ['.snippet'];
backend: sp.get('backend'),
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']
JsCoq.start(jscoq_ids, jscoq_opts).then(res => {
/* Global reference */
window.coq = res;