forked from jscoq/jscoq
/
index.html
274 lines (258 loc) · 11.1 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
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
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
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
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
<!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="icon" href="ui-images/favicon.png">
<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>
</head>
<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><hr class="dropdown-divider"></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>
<!-- these are only available from the full website -->
<li><a class="dropdown-item" href="/fun/coqoban.html">🎡 Çoqoban</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>
<!------------------------------->
<div id="document">
<div>
<h3>Welcome to the <span class="jscoq-name">jsCoq</span> Interactive Online System!</h3>
<p>
<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.
</p>
<p>
<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>.
</p>
<h4>A First Example: <code>rev</code> <code>∘</code> <code>rev = id</code></h4>
<p>
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.
</p>
<p>
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 Coq Require Import List.
Import ListNotations.</textarea>
<p class="interim">
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>.
</p>
<textarea class="snippet">Lemma rev_snoc_cons A :
forall (x : A) (l : list A), rev (l ++ [x]) = x :: rev l.</textarea>
<p class="interim">
This proposition is proven by way of the standard induction on
the structure of the list <code>l</code>.
</p>
<textarea class="snippet">Proof.
induction l.
- reflexivity.
- simpl. rewrite IHl. simpl. reflexivity.
Qed.</textarea>
<p class="interim">
Now we prove the central equality with a similar induction.
</p>
<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>
<p class="interim">
Finally, we apply functional extensionality to produce the equality
as it was written in the title.
</p>
<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.
Qed.</textarea>
<hr/> <!-- end of proof -->
<h4>Quick start</h4>
<p>
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>.
</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/power-button-512-black.png" height="20px"></td>
<td class="has-kbd"><kbd>F8</kbd></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>
<td class="has-kbd">
<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 class="has-kbd">
<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>
<td></td>
<td class="has-kbd">
<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>
</tr>
</table>
<h5>Creating your own proof scripts</h5>
<p>
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.
</p>
<h5>There's more</h5>
<p>
See the <a href="https://github.com/jscoq/jscoq/tree/v8.16/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>
<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>
<p>
<i>¡Salut!</i>
</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> <!-- /#document -->
</div> <!-- /#document-wrapper -->
</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'];
var jscoq_opts = {
implicit_libs: false,
focus: 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 */
var coq;
JsCoq.start(jscoq_ids, jscoq_opts).then(res => {
coq = res;
coq.loadSymbolsFrom('./examples/examples.symb.json');
});
</script>
</body>
</html>