Use ALT-(up-arrow) and ALT-(down-arrow) to process this document inside your browser, line-by-line.
Use ALT-(right-arrow) to go to the cursor.
You can
save your edits
inside your browser and
load them back.
Finally, you can
download
your working copy of the file, e.g., for sending it to teachers.

- Some parts are copied/adapted from Quick-Reference-for-Beginners
- For a complete reference see the Coq Reference Manual

- Declarations
- Management of the goal:
- Introduction
- Generalization
- Clearing

- Trivial proofs:
- Computation
- Assumption
- Hints

- Proofs on inductive definitions:
- Case analysis
- Induction

- Logical connectives in Prop:
- Implication
- Universal quantification
- Conjunction
- Disjunction
- Negation
- Existential quantification
- Double implication
- Reflect

- Rewriting, congruence
- Queries and Inspection:
- Search
- About
- Check

The first lines of a `.v` file are usually naming the libraries
that will be used to write definitions, statements and prove them,
the syntax, assuming the library `〈lib〉` is installed, is as follow.

From 〈lib〉 Require Import 〈module(s)〉.

For most of the lectures we use simplified versions of the mathcomp library.

From mathcomp Require Import mini_ssreflect 〈other mini mathcomp libs〉.

However, in this cheat sheet, which is more complete, we use:

The keyword `Definition` declares a term, a type, a proposition, or a
non-recursive function. It looks like:

Definition 〈name〉 : 〈type〉 := 〈value〉.

It's possible to omit the `type` if Coq can infer it from the value,
which then looks like:

Definition 〈name〉 := 〈value〉.

But we strongly suggest that you enforce type annotations in definitions, for the sake of documentation and robustness.

For functions, the arguments can go before or after the colon. That is, saying:

Definition 〈name〉 : 〈type1〉 -> 〈type2〉 -> 〈type3〉 := fun 〈argname〉 〈argname〉 => 〈body〉.is equivalent to:

Definition 〈name〉 (〈argname〉 : 〈type1〉) : 〈type2〉 -> 〈type3〉 := fun 〈argname〉 => 〈body〉. Definition 〈name〉 (〈argname〉 : 〈type1〉) (〈argname〉 : 〈type2〉) : 〈type3〉 := 〈body〉.

`Fixpoint` defines a *recursive* function. Syntax is similar to `Definition`:

Fixpoint 〈name〉 : 〈type〉 := fun 〈arguments...〉 => 〈body〉. Fixpoint 〈name〉 (〈argname〉 : 〈type〉) (argname : 〈type〉) ... : 〈type〉 := 〈body〉.

Such a definition is accepted if termination is ensured by a recursive call on a strict subterm.

`Lemma` is the most common type of proof declaration. It allows to define a
term using a gradual, interactive construction, possibly using
instructions called tactics. This mode of interaction is called proof-mode

.

The syntax looks like:

Lemma 〈name〉 : 〈proof statement〉. Proof. 〈proof body〉 Qed.

`Theorem`, `Remark`, `Corollary` are synonyms.

You can omit writing `Proof` before your proof, but it's convention, and
visually helps separate the proof from the proof statement when the statement
is long and complicated.

The `〈proof statement〉` can in fact be any type, but it is usually a type
of type `Prop`.

If you don't finish your proof but want to exit your lemma, you can't use
`Qed`. Instead, you have two options: `Admitted`.

This will let other proofs see and use your unfinished
lemma, even though you haven't yet proven it. Naturally, this means it's
important to remember if you're depending on an admitted lemma, because it
means your top-level proof might not be correct. To see the admitted proofs
a lemma or theorem depends on, type `Print Assumptions `.

A proof in progress looks like this in the dedicated buffer:

〈name1〉 : 〈type1〉 〈name1〉 : 〈type1〉 ... 〈namek〉 : 〈typek〉 =================== 〈statement〉

What is above the `===` is the proof context, a list of named
assumptions, with their type. What is above the `====` is a type,
with possible prenex quantification and arrows. Part of the
formal proof, the boring one, deals with moving items around
the `====`. Only the top most assumption or quantified variable
can be named and used to the context: this is an introduction step.
Any item from the context can be pushed on top of the statement
(provided that this complies with possible dependencies): this
is a generalization step.

As much as possible, simple proofs = short scripts.
The `by []` tactic solves trivial goals, and fails if it did not work.
Trivial here means:

One of the most useful commands for discovering lemmas or functions
that have already been defined is `Search`.