Welcome to the jsCoq Interactive Online System!
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 that you wish to report or want to add your own contribution, you are extremely welcome! We await your feedback at GitHub and Zulip.
A First Example: rev ∘ rev = id
The following is a simple proof that rev, the standard list
reversal function as commonly Definition x := 3. defined in ML and other languages of the
family, is an involution.
Use Alt+↓/↑ to step through the proof, and observe the proof state on the right panel.
We are going to need a simpler auxiliary lemma, one that connects
rev, :: (the list constructor, also known
as cons), and snoc (the dual of
cons, 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, rev.
This proposition is proven by way of the standard induction on
the structure of the list l.
Now we prove the central equality with a similar induction.
Finally, we apply functional extensionality to produce the equality as it was written in the title.
There is only one syntactic difference, which is that, in Coq, we
need to pass an explicit value to the implicit (generic) type
parameter A of rev.
Quick start
Use the scratchpad for a fresh page to write your proofs on. jsCoq provides basic UI for running and inspecting proofs, similar to IDEs such as CoqIDE, Proof General, and VSCoq.
Actions
| Button | Key binding | Action |
|---|---|---|
 |
F8 | Toggles the goal panel. |
  |
Alt+↓/↑ or Alt+N/P |
Move through the proof. |
 |
Alt+Enter or Ctrl+Enter (⌘ on Mac) |
Run (or go back) to the current point. |
Ctrl+
|
Hover executed statements to peek at the proof state after each step. |
Creating your own proof scripts
The scratchpad offers simple, local storage functionality. It also allows you to share your development with other users in a manner that is similar to Pastebin.
There's more
See the official docs on GitHub for more details on using, building, embedding, and integrating jsCoq in your developments.
jsCoq comes with a variety of addon packages, including Coq's standard library and the mathematical components library. Feel free to experiment, and let us know if you have any suggestions and/or when you have done something cool with jsCoq. 😎
¡Salut!