Welcome to the HoTT-Coq JsCoq Instance!

jsCoq is an interactive, web-based environment for the Coq Theorem prover, that runs Coq directly in your browser

Instructions:

The following document contains embedded Coq code. All the code is editable and can be run directly on the page. Once jsCoq finishes loading, you are free to experiment by stepping through the proof and viewing intermediate proof states on the right panel.

Actions:

Button	Key binding	Action
	Alt+↓/↑ or Alt+N/P	Move through the proof.
	Alt+Enter or Alt+→	Run (or go back) to the current point.
	F8	Toggles the goal panel.

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.

A HoTT example

This instance of jsCoq provides support only for the HoTT library. Our first step will be to load its prelude:

From HoTT Require Import Overture. From HoTT Require Import Spaces.Nat. Import Decidable. Open Scope nat_scope.

Ready to do Proofs!

Once the basic environment has been set up, we can proceed to do a simple proof:

(* A proof that natural numbers have decidable equality. *) Lemma decidable_nat_eq (x y : nat) : Decidable (x = y). Proof. Print Decidable.

The lemma states that for any two natural numbers x and y, we can decide their equality. Coq is a constructive system, which among other things implies that to show the existence of an object, we need to actually provide an algorithm that will construct it. In this case, we need to find a proof of either x = y or ~ (x = y), for any x and y.

induction x in y |- *.

We proceed by induction on x, but we must generalize the induction hypothesis over any y.

- destruct y; [left; reflexivity|right; intros eq; discriminate]. - destruct y; [right; intros eq; discriminate|]. destruct (IHx y) as [|Hxy]. * left; apply ap. assumption. * right.

The proof then proceeds by case analysis over y in both subgoals. We find ourselves in a state where we must show that if x, y are two different numbers, then their successors must also be different. This is a common consequence of the injectivity of constructors of inductive types. Let's look for a lemma to apply:

Search (_ <> _). now apply not_eq_S. Qed.

That's it for the shortest introduction to Coq ever!

---