Prerequisites

Some knowledge of formal logic and proof theory (as well as general mathematical maturity and experience with proofs) will be helpful.

Note

Code snippets can be copied by hovering over the snippet and clicking the button which appears on the top right.

Some snippets are declared as files—those can be downloaded directly by clicking the button next to the filename.

Instructions

If you’re on the lab computers, everything is already installed—just open CoqIDE.

If you’re using your own computer, download and install the latest version of the Coq Platform. This should install, amongst other things, CoqIDE—we recommend using this if you’re new to Coq. The install size is fairly big so make sure you have enough disk space.

If you know what you’re doing, there’s also generally decent support for using Coq in your preferred text editor (as long as you’re not using Windows). As far as I know, VS Code and Emacs have the best experience as of this writing.

You must put everything into a single file for submission. The file should look like this:

CoqLab01.v
1
2
3
4
5
6
Section CoqLab01.
Context (A B C D : Prop).

(* your lab work goes here *)

End CoqLab01.

You can skip ahead to the lab questions if you’re confident enough, but I highly recommend reading through the next two sections to get an overview of the tactics required for the lab, and a worked example.

Basic Tactics

Tactics are commands you can run that transform the proof state in some way. You will need three tactics for this lab: intros, apply, and exact.

For a simple description of these tactics (and many others) I recommend you take a look at this simplified tactic index. It also has some examples of the tactics in use.

If you’re feeling particularly adventurous, I encourage you to brave the official Coq tactic index. For example, you can read some very detailed info about the apply tactic here.

Worked Example

Let’s prove that

\[\begin{aligned} A, \; A \to B, \; B \to C \; \vdash \; C \tag{∗} \end{aligned}\]

using Coq.

First, though, we should remind ourselves what this means. The mathematical expression \(\Gamma \vdash \phi\) means that, from the list of assumptions \(\Gamma\), we can prove the proposition \(\phi\). Therefore, \((∗)\) means this: given that we know

  1. \(A\)
  2. \(A \to B\)
  3. \(B \to C\)

we should be able to prove \(C\).

In Coq, we can represent the situation like this.

Example.v
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
Section WorkedExample.

Context (A B C : Prop).

Hypotheses
  (H1 : A)
  (H2 : A -> B)
  (H3 : B -> C).

Goal C.

End WorkedExample.

Step the proof state to the goal (Ctrl+↓ in CoqIDE). You should see this.

1
2
3
4
5
6
7
A, B, C : Prop
H1 :  A
H2 :  A -> B
H3 :  B -> C
—————————————————————————————
(1/1)
C

Our goal is C; that is what we want to prove. What we know is listed above the line. In order: we know that A, B, and C are propositions. We know that A is true. We know that A -> B is true. We know that B -> C is true. Each of these hypotheses has a label that we’ll use to refer to that proposition in the proof.

Our first attempt at a proof will use backward reasoning. Forward reasoning starts with hypotheses and tries to work towards the goal. Backward reasoning, by contrast, starts from the goal and tries to work backward to the hypotheses.

Here is the basic idea of backward reasoning. Notice that the goal is C and that our hypothesis H3 : B -> C has the conclusion C. If we were somehow able to prove B, we could then use the fact that we know B -> C to get C—which is our goal. Therefore, it suffices for us to prove B. (And we hope of course that we can prove B.)

This little bit of reasoning is encoded by the apply tactic. When we issue the command apply H3, what we’re instructing Coq to do is this: Check if the conclusion of H3 matches the goal. If it does, replace the goal with H3’s premises. Let’s do that now.

1
2
Goal C.
  apply H3.

Step the proof forward (Ctrl+↓). The proof state should look like this.

1
2
3
4
5
6
7
A, B, C : Prop
H1 :  A
H2 :  A -> B
H3 :  B -> C
—————————————————————————————
(1/1)
B

It’s exactly as before, but the goal is now B. Progress!

Notice that we can do exactly the same thing again, but this time with the hypothesis H2.

1
2
3
Goal C.
  apply H3.
  apply H2.

After stepping forward, the proof state should now look like this.

1
2
3
4
5
6
7
A, B, C : Prop
H1 :  A
H2 :  A -> B
H3 :  B -> C
—————————————————————————————
(1/1)
A

Now the goal is A. But we already know that A is true, since it is one of our hypotheses. Therefore, the proof is complete—we just need to instruct Coq to match the goal with the right hypothesis. For that, we can use the tactic exact.

1
2
3
4
Goal C.
  apply H3.
  apply H2.
  exact H1.

The proof should be complete, and the proof state should look like this.

1
No more subgoals.

We can close the proof with the vernacular command Qed.

1
2
3
4
5
Goal C.
  apply H3.
  apply H2.
  exact H1.
Qed.

Now the proof is fully complete and saved.

This way of expressing the term to be proved can be a little verbose. We could, alternatively, have set the proof up like this.

1
2
3
4
Context (A B C : Prop).

(*   ↓H1     ↓H2         ↓H3      *)
Goal A -> (A -> B) -> (B -> C) -> C.

This is equivalent to what we had before, but the proof begins in a different state.

1
2
3
4
A, B, C : Prop
—————————————————————————————
(1/1)
A -> (A -> B) -> (B -> C) -> C

Recall that if we want to prove a proposition of the form \(P \to Q\), we take \(P\) as a hypothesis, then try to prove \(Q\). This is the introduction rule for implication and is encoded in Coq by the tactic intros.

The tactic intros can be used in one of two ways. First is on its own, with no arguments. When used like this, it will apply the introduction rule for implication as many times as it can and automatically give unique names to all the generated hypotheses. The second way is with arguments. When used like this, it will apply the introduction rule \(n\) times (where \(n\) is the number of provided arguments) and name the hypotheses according to the parameter names.

For example, we can do this:

1
2
Goal A -> (A -> B) -> (B -> C) -> C.
  intros.

… to get the proof state:

1
2
3
4
5
6
7
A, B, C : Prop
H0 :  A
H1 :  A -> B
H2 :  B -> C
—————————————————————————————
(1/1)
C

(Note how Coq automatically names the hypotheses.) Or, we can do this:

1
2
Goal A -> (A -> B) -> (B -> C) -> C.
  intros a a_impl_b b_impl_c.

… and get the proof state:

1
2
3
4
5
6
7
A, B, C : Prop
a :  A
a_impl_b :  A -> B
b_impl_c :  B -> C
—————————————————————————————
(1/1)
C

It’s up to you which method you prefer.

Questions

Prove the following lemmas in Coq. When you have completed a proof, replace Admitted with Qed. You can download the file by clicking the button next to the filename.

CoqLab01.v
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
Section CoqLab01.
Context (A B C D : Prop).

(* Implication is transitive. *)
Lemma q1 : (A -> B) -> (B -> C) -> (A -> C).
Proof.
  (* todo *)
Admitted.

(* Anything implies itself. *)
Lemma q2 : A -> A.
Proof.
  (* todo *)
Admitted.

(* Extra hypotheses can be introduced without affecting
 * provability. *)
Lemma q3 : A -> (B -> A).
Proof.
  (* todo *)
Admitted.

(* The order of the hypotheses is irrelevant. *)
Lemma q4 : (A -> B -> C) -> B -> A -> C.
Proof.
  (* todo *)
Admitted.

(* Duplicate hypotheses can be merged. *)
Lemma q5 : (A -> A -> B) -> A -> B.
Proof.
  (* todo *)
Admitted.

(* Duplicate hypotheses can be introduced. *)
Lemma q6 : (A -> B) -> A -> A -> B.
Proof.
  (* todo *)
Admitted.

(* Diamond lemma:
 *        A
 *      ↙   ↘           A
 *     B     C    ~>    ↓
 *      ↘   ↙           D
 *        D
 *)
Lemma q7 : (A -> B) -> (A -> C) -> (B -> C -> D) -> A -> D.
Proof.
  (* todo *)
Admitted.

(* Weak version of Peirce’s law. The strong version implies
 * LEM and therefore can’t be proved in constructive logic. *)
Lemma q8 : ((((A -> B) -> A) -> A) -> B) -> B.
Proof.
  (* todo *)
Admitted.

End CoqLab01.