Welcome to this basic Coq tutorial! Before we start, be sure to have Coq installed and a IDE configured for Coq ready to go. Please check the installation page for instructions on how to install Coq and an IDE for Coq.

A presentation of the tutorial was given live over Zoom. A recording of that Zoom meeting is available here.

We will first have a look at Coq as a programming language.

First, we will see how to define datatypes. In Coq, we can define algebraic datatypes using the Inductive construct. For instance, to define booleans, one simply needs to write:

 Inductive bool : Type :=
  | true
  | false.
 

The name of the type defined here is bool, and the type as two constructors: true and false.

Note the point at the end of the definition. Each command in Coq is ended by a single point.

Important note: If you are following along in your IDE (which we highly suggest you do), be sure to interpret commands as we go along. Your IDE should have a button / command to interpret forward by one command, or to interpret to the current cursor.

To check the type of an expression, you may find useful to use the Check command. Simply type and interpret the following command to see the type of true:

 Check true.
 

The result (which is true : bool) should appear in a panel of your IDE.

We can also define inductive data types in Coq. For instance, here is a definition of generic lists in Coq:

 Inductive list (A : Type): Type :=
  | nil : list A
  | cons : A -> list A -> list A.
 

Notice that list takes a type parameter A. We write list A for a list of elements of type A. If you check the type of nil and of cons, you will see that they have as a first argument the type A.

 Check nil.
Check cons.
 

Therefore, if we were, for instance, to build a list containing the bools true and false, we would have to explicitly pass the type parameter bools to all constructors.

 Check (cons bool true (cons bool false (nil bool))).
 

Coq however support implicit parameters. To declare the type parameter A of the two constructors as implicit, we can use the following commands:

 Arguments nil {A}.
Arguments cons {A}.
 

Once this is done, we can build lists without explicitly passing the type argument.

 Check (cons true (cons false nil)).
 

If you wish to be able to explicitly pass arguments to implicit parameters, simply add an @ before the name of the definition:

 Check (@nil bool).
 

There are a few datatypes that are defined by default in Coq. Natural numbers and pairs are two such datatypes.

Natural numbers are of type nat. The type is also defined inductively. The constructor is O for 0 and the second S for the successor. Coq also has built-in syntax for natural numbers, so that you can write 0 for O, 1 for S O, 2 for S (S O) and so on.

The type of pairs of values of types T1 and T2 is written as T1 * T2. Pairs have a single constructor. We write the pair of x and y as (x, y).

 Check (0, 1).
 

One final noteworthy construct of Coq is the option type constructor, which is used to represent optional values.

You can check the definition of option and of its two constructors Some and None by issuing the command:

 Print option.
 

We have seen how to define inductive types and their constructors. In this section, we will see how to define functions on those datatypes.

As a first example, consider the following definition for boolean negation:

 Definition negb (b: bool): bool :=
  match b with
  | true => false
  | false => true
  end.
 

The name of the function is negb and it takes a single parameter b of type bool. The return type of the function is bool.

The body of the function is a single match expression. The first case indicates that, when b is true, then the result is false. The second case specifies that, when b is false, then the result is true.

When performing pattern matching, Coq makes sure that the patterns cover all cases. The wildcard pattern _ is used to match against all remaining cases. Such a pattern is useful for instance in the following definition of boolean conjunction:

 Definition andb (b1 b2: bool): bool :=
  match (b1, b2) with
  | (true, true) => true
  | _ => false
  end.
 

The Definition command that we have used so far is quite restrictive in the sense that it does not allow for recursion. To build a recursive function, one must use a different command than Definition, namely Fixpoint. Here is how one could define the length of a list as a recursive function:

 Fixpoint length {A : Type} (xs: list A): nat :=
  match xs with
  | nil => 0
  | cons x xs' => S (length xs')
  end.
 

Note that the type parameter A is enclosed in curly brackets, which indicates that the parameter is implicit.

Similarly, here is how we can define concatenation of lists:

 Fixpoint app {A : Type} (xs ys: list A): list A :=
  match xs with
  | nil => ys
  | cons x xs' => cons x (app xs' ys)
  end.
 

And here is how one could write list reversal using an helper recursive function with an accumulator:

 Fixpoint rev_acc {A: Type} (xs acc: list A): list A :=
  match xs with
  | nil => acc
  | cons x xs' => rev_acc xs' (cons x acc) 
  end.

Definition rev {A: Type} (xs: list A): list A := rev_acc xs nil.
 

Finally, before we move on to theorems and proofs, it is worth mentioning that Coq also supports let expressions and if expressions.

 Compute (let x := 3 in x + x).
Compute (if andb true false then 1 else 0).
 

Also, note the command Compute to compute the result of expressions!

It may seem strange that the built-in if construct of Coq works on our own definition of boolean. If fact if expressions are simply syntactic sugar for pattern matching when the condition type has exactly two constructors. The then branch corresponds to the first constructor, while the else branch to the second. This means that you can also have natural numbers as conditions of if expressions:

 Compute (if 0 then true else false).
Compute (if 42 then true else false).
 

We are now at the point where we can start with the most interesting part of Coq: proving theorems. A theorem is a proposition that has been proven.

In Coq, propositions are of type Prop. Just like types, propositions can be defined inductively using the Inductive command. There are a few already defined propositions:

You can check the definitions of proposition True and False by issuing the following commands:

 Print True.
Print False.
 

Note that the propositions True and False are different from the booleans true and false. true and false are constructors of the type bool, while True is a proposition with a single constructor I, and False is a proposition with no constructors at all. It is therefore impossible to build a proof of False.

Equality between two values of the same type also yields a proposition:

 Check (1 = 1).
Check (1 = 2).
 

To express that two values are not equal, we use the infix binary operator <>.

Implication is denoted by ->. For instance, here is the proposition that False implies True:

 Check (False -> True).
 

Negation is Coq is denoted not, or by the prefix operator ~. Negation is defined as implies False, which you can see by printing the definition of not.

 Print not.
 

Disjunction and conjunctions are respectively or and and. Often, we will use the infix binary operators \/ and /\ to refer to or and and. We encourage you to print the definitions of or and and.

Equivalence (“if and only if”) between propositions is named iff in Coq, and can written using the infix binary operator ↔. The proposition iff A B is defined to be (A → B) /\ (B → A).

Finally, coq supports quantifiers in propositions. The keyword for universal quantification forall and for existential quantification is exists. The following propositions showcase how to use such quantifiers:

 Check (forall (n : nat), n = 0).
Check (exists (n : nat), forall (m : nat), n = 0 \/ n = m).
 

Now that we know how to express propositions, it is finally time to prove some theorems! To state a theorem, use the command Theorem.

 Theorem app_nil_l : forall (T : Type) (xs : list T), app nil xs = xs.
 

The theorem is given a name, in this case app_nil_l. The proposition to be proven appears after the colon. In this example, the proposition states that, for any type T and list xs of type list T, if we concatenate nil to the left of xs then we get xs.

The command Lemma also exists and is equivalent to Theorem. Lemma however indicates to the reader the relative importance of the proven proposition.

Once the theorem is stated, we must actually prove it! To do so, we use the Proof command.

 Proof.
 

If you interpret the file up until that point, you should see that your IDE displays in some panel the proposition to be proven. To introduce all universally quantified parameters, as well as all hypotheses, we can use the tactic intros.

   intros T xs.
 

After interpreting that command, you should see in your IDE that the goal as now changed and that two arguments T and xs have been added to the context. It is also possible to omit the names and simply call intros, in which case Coq will choose names for you.

The next step in this proof is to apply some simplification. Since the definition of app does pattern matching on the left argument, it is possible to reduce the left side of the equality. To do so, simply invoke the tactic simpl.

   simpl.
 

Now, the goal should take the form of an equality between two equal terms. To solve this goal, simply use the reflexivity tactic.

   reflexivity.
 

After interpreting that tactic, the IDE should inform you that the proof is complete. Finally, to conclude the proof, simply add the command Qed.

 Qed.
 

In the rest of this tutorial, we will look at different tactics and see example proofs in which they are used.

The unfold tactic is used to replace a name by its definition. Below is an example of a use of that tactic:

 Lemma rev_rev_acc : forall A (xs : list A),
  rev xs = rev_acc xs nil.
Proof.
  intros.
  unfold rev.
  reflexivity.
Qed.
 

Many tactics will unfold definitions freely. In fact, reflexivity is such a tactic, and the above proof can simply be reduced to a single call to reflexivity.

The rewrite tactic is used to rewrite a subterm into the goal given an equality between the subterm and some other term. Here is an example of its use:

 Lemma negb_false_negb_negb_true : forall b,
  negb b = false -> negb (negb b) = true.
Proof.
  intros b H.
  rewrite -> H.
  simpl.
  reflexivity.
Qed.
 

After intros the context will contain the boolean b and the hypothesis H that negb b = false. Thanks to H, we can rewrite the subterm negb b into false. We can then proceed by calling simpl and reflexivity.

Some proofs will require you to do some case analysis. To do so, you may use the tactic destruct, as shown in the following example theorem:

 Theorem double_negb : forall (b : bool), negb (negb b) = b.
Proof.
  intros b.
  destruct b eqn:Eqb.
  + simpl. reflexivity.
  + simpl. reflexivity.
Qed.
 

The call to destruct b performs a case analysis on the boolean b. Since b is of type bool, it must be of the form of a constructor of bool (either true or false). After the call to destruct, the goal will be split into multiple subgoals, in this case two. In each subgoal, the value b be will replaced by true, respectively false, which allows us to eventually prove each subgoal. The proposition Eqb, with will contain either b = true or b = false depending on the subgoal, will also be added to the context. Note that the name Eqb is arbitrary and can be changed.

We use the bullet + to indicate that we handle the next subgoal. Subgoals can be nested. Indeed, it is entirely possible to perform case analysis within a subgoal. At each level of nesting a different bullet symbol should be used amongst +, - or *.

Note that it is possible to destruct compound expressions as well. In this case, it is often important to keep a trace of what the destructed expression was by not removing the eqn:E part.

When all subgoals start with the same prefix of tactics, it is possible to factor them out by using the ; operator, as exemplified by:

 Theorem double_negb' : forall (b : bool), negb (negb b) = b.
Proof.
  intros b.
  destruct b eqn:Eqb; simpl; reflexivity.
Qed.
 

When preceded by a ; a tactic applies to all current subgoal.

Sometimes, case analysis is not enough and inductive reasoning must be employed. For this purpose, Coq has the induction tactic.

 Theorem app_nil_r : forall A (xs : list A),
  app xs nil = xs.
Proof.
  intros.
  induction xs.
  + simpl. reflexivity.
  + simpl. rewrite -> IHxs.
    reflexivity.
Qed.
 

In that proof, the first case corresponds to the base case nil, while the second case corresponds to the inductive case cons. In the subgoal for the cons case, we are also provided with an induction hypothesis IHxs which states that app xs nil = xs. Using the rewrite tactic, we can rewrite occurences of app xs nil in the goal into xs.

Using the ; operator, this proof could also be written as:

 Theorem app_nil_r' : forall A (xs : list A),
  app xs nil = xs.
Proof.
  intros.
  induction xs; simpl.
  + reflexivity.
  + rewrite -> IHxs.
    reflexivity.
Qed.
 

The tactic inversion is used to do case analysis on the various ways a hypothesis may be true.

This tactic is also useful when an hypothesis contains an equality between two expressions of the same structure, such as in:

 Theorem cons_head_eq : forall T (x1 x2 : T) xs,
  cons x1 xs = cons x2 xs ->
  x1 = x2.
Proof.
  intros T x1 x2 xs H.
  inversion H.
  reflexivity.
Qed.
 

In that case, the call to inversion H generates the hypothesis that x1 = x2, and also rewrites it in the goal. The call to reflexivity completes the proof.

Also, inversion is very useful to handle contradictions in the hypotheses. When used on a contradictory hypothesis, inversion will immediately solve the current goal.

 Theorem negb_neq : forall b, negb b <> b.
Proof.
  intros b A.
  destruct b.
  + inversion A.
  + inversion A.
Qed.
 

The about proof makes use of the fact that negb b <> b is definitional equal to negb b = b → False. Therefore the hypothesis A initial contains the proposition negb b = b. In the two subgoals after destruct, the hypothesis turns into false = true respectively true = false, which inversion knows to be impossible.

The apply tactic is used to apply a hypothesis or an existing lemma to the current goal. The conclusion of the hypothesis must match the current goal.

 Lemma modus_ponens : forall (P Q : Prop),
  (P -> Q) -> P -> Q.
Proof.
  intros P Q H p.
  apply H.
  apply p.
Qed.
 

It is also possible to use apply in a hypothesis in the context. In this case, the hypothesis in the context acts as an argument to the hypothesis applied.

 Lemma modus_ponens' : forall (P Q : Prop),
  (P -> Q) -> P -> Q.
Proof.
  intros P Q H p.
  apply H in p.
  apply p.
Qed.
 

We the current goal is a conjunction, we can split each side into its own subgoal using the split tactic.

 Lemma app_eq_nil: forall A (xs ys : list A),
  app xs ys = nil ->
  xs = nil /\ ys = nil.
Proof.
  intros A xs.
  destruct xs.
  - intros. simpl in H.
    split.
    + reflexivity.
    + apply H.
  - intros. inversion H.
Qed.
 

When the goal is a disjunction, we can choose which side to prove by either using left or using right.

 Lemma length_non_zero_or_nil : forall T (xs : list T),
  xs = nil \/ length xs <> 0.
Proof.
  intros T xs.
  destruct xs.
  - left.
    reflexivity.
  - right.
    simpl.
    intros A.
    inversion A.
Qed.
 

When the goal is of the form exists x, …, you can apply the tactic exists to fix the existential quantified x to a term.

 Theorem larger_lists: forall T (x : T) (xs : list T), 
  exists (xs' : list T),
  length xs' = S (length xs).
Proof.
  intros T x xs.
  exists (cons x xs).
  simpl.
  reflexivity.
Qed.
 

Note that when you have an existentially quantified proposition as hypothesis, you may destruct it to get an actual witness. The above theorem could be rewritten as the following to exemplify this:

 Theorem larger_lists': forall T (xs : list T), 
  (exists x : T, True) ->
  exists (xs' : list T),
  length xs' = S (length xs).
Proof.
  intros T xs E.
  destruct E.
  exists (cons x xs).
  simpl.
  reflexivity.
Qed.
 

As a final tip, Coq also offers searching facilities to help you find useful lemmas in the standard library. The Search commands accepts a pattern and will look for theorems and definitions where the pattern matches (some part of) the signature.

 Search plus.
Search (S _ = S _ -> _ = _).