Tutorial by Examples

Testing without installing For new users who wish to start testing Coq without installing it on their machine, there is an online IDE called JsCoq (presentation here). The package sub-window allows testing various well-known additional packages. Installation The download page contains installers ...

Theorem my_first_theorem : 1 + 1 = 2. Proof. reflexivity. Qed. Try it in your browser.

You can install the whole bundle by downloading the dmg package from here. The bundle contains a CoqIDE that can be used for writing your proofs or you can use coqtop command to run the interpreter on your terminal Installation of Coq on MacOS is easy using homebrew as well brew install coq or i...

Warning: this is not the standard way of installing Coq. For users of Linux (and MacOS) who wish to gain access to up-to-date versions of Coq or to be able to use several versions of Coq on the same machine, without the hassle of using opam, and without having to compile from source, this is an alt...

Here is a simple proof by induction. Require Import Coq.Setoids.Setoid. Require Import Coq.Arith.Lt. (* A number is less than or equal to itself *) Theorem aLTEa : forall a, a <= a. auto with arith. (* This follows by simple arithmetic *) Qed. Theorem simplALTE : forall a ...