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.

VU Master Course Cheat Sheet.


Outline of the document


Declarations

Require and Import

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:


Definition

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

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

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 .


Management of the goal

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.


Trivial Proofs

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


Proofs on inductive definitions


Logical connectives in Prop


Rewriting, congruence


Queries and Inspection

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