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.

From Coq Require Import List. Import ListNotations.

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.

Lemma rev_snoc_cons A : forall (x : A) (l : list A), rev (l ++ [x]) = x :: rev l.

This proposition is proven by way of the standard induction on the structure of the list l.

Proof. induction l. - reflexivity. - simpl. rewrite IHl. simpl. reflexivity. Qed.

Now we prove the central equality with a similar induction.

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.

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.

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.

---

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!

The dev team

• Emilio Jesús Gallego Arias (Inria, Université de Paris, IRIF)
• Shachar Itzhaky (Technion)

Contributors

• Benoît Pin (CRI, MINES ParisTech)