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 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
ButtonKey bindingAction
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!