**Note:** These are my personal experiences with Coq and should not be in any way considered authoritative — I’m not responsible if you try out what I did and Coq eats your laundry.

I decided to have some fun with Coq (yes, yes; it does sound like what you think it does).

## What is Coq?

Coq is a proof assistant — it assists with constructing formal proofs, as well as checking proofs for validity. It’s not just for mathematicians, though: The CompCert C compiler is an example of how using Coq can assist with writing formally correct software. However, it’s kind of tedious if you aren’t a mathematician, and I’m not nearly capable enough to write anything that interesting.

## Getting Started

We can use Coq’s interactive mode, `coqtop`

. It gives us a prompt:

`Coq <`

Naturally, we want to prove something. We can use the `Goal`

command:

```
Goal 1 + 1 = 2.
```

We then get something that looks like this:

```
1 subgoal
============================
1 + 1 = 2
```

Let’s prove this!

```
trivial.
```

How anticlimactic. We’ve just used Coq’s built-in definition of natural numbers to prove this. Coq should tell us *No more subgoals*, which means that we’ve completely proved our theorem. We can either `Save`

or `Abort`

(discard) our proof, so let’s just `Abort`

this.

## A Vaguely More Exciting Proof

Why don’t we prove something slightly less trivial than \(1 + 1 = 2\)? What about some simple logic:

$$(A \leftrightarrow B) \rightarrow A \rightarrow B$$

Or, in English, if A is equivalent to B, this implies that A implies B.

Let’s get proving!

```
Goal forall A B : Prop, (A <-> B) -> A -> B.
```

```
1 subgoal
============================
forall A B : Prop, (A <-> B) -> A -> B
```

We use the `forall`

quantifier to say that *for all values of A and B, the following proposition is true.*

We can start off by applying a tactic known as `intro`

— we can use it on any goal that is an implication, and it works by introducing hypotheses that are the left-hand side of an implication, for instance:

```
intro A.
intro B.
intro H.
intro HA.
```

```
1 subgoal
A : Prop
B : Prop
H : A <-> B
HA : A
============================
B
```

We’ve removed the for-all quantification from \(A\) and \(B\) and we’ve also derived two hypotheses: `H`

and `HA`

.

Ha! As \(A\) is equivalent to \(B\), our goal of \(B\) is exactly our hypothesis, `HA`

! To get there, we can apply our hypothesis `H`

to the goal:

```
apply H.
```

```
1 subgoal
A : Prop
B : Prop
H : A <-> B
HA : A
============================
A
```

Then tell Coq to match \(A\) with `HA`

:

```
exact HA.
```

We did it! We proved that \((A \leftrightarrow B) \rightarrow A \rightarrow B\) is, in fact, true! If you want to, you can save your proof with `Save`

.

## Slightly Less Trivial

Why don’t we prove something like an even number plus two is even? We’re going to need `Coq.Arith.Even`

here. Let’s formulate our goal:

```
Require Import Coq.Arith.Even.
Goal forall x : nat, even x -> even (S (S x)).
```

```
1 subgoal
============================
forall x : nat, even x -> even (S (S x))
```

Or, *the successor of the successor of an even number is even.* In math:

$$\forall x: x \in \mathbb{N} \rightarrow \text{even}(x) \rightarrow \text{even}(\text{S}(\text{S}(x)))$$

Again, we want to use the `intro`

tactic or the sneaky shortcut, `intros`

:

```
intros.
```

```
1 subgoal
x : nat
H : even x
============================
even (S (S x))
```

`intros`

automatically derives all hypotheses possible. Let’s push on! Looking at `Coq.Arith.Even`

, `odd`

and `even`

are defined with inductive cases. We can use this induction to work backwards — we can tell Coq that `even (S (S x))`

is just `odd (S x)`

, with the `case`

tactic:

```
case even_S.
```

```
2 subgoals
x : nat
H : even x
============================
forall n : nat, odd n -> even (S n)
subgoal 2 is:
odd (S x)
```

Again, we want to derive some hypotheses:

```
intros.
```

```
2 subgoals
x : nat
H : even x
n : nat
H0 : odd n
============================
even (S n)
subgoal 2 is:
odd (S x)
```

Now we can tell Coq that `even (S n)`

is implied by `odd n`

, this time with the `apply`

tactic since it’s not inductive:

```
apply even_S.
```

```
2 subgoals
x : nat
H : even x
n : nat
H0 : odd n
============================
odd n
subgoal 2 is:
odd (S x)
```

`odd n`

is one of our hypotheses, so we use `exact`

:

```
exact H0.
```

```
1 subgoal
x : nat
H : even x
============================
odd (S x)
```

`odd (S x)`

is implied by `even n`

, so we just apply `odd_S`

.

```
apply odd_S.
```

```
1 subgoal
x : nat
H : even x
============================
even x
```

And again, we use `exact`

.

```
exact H.
```

Hooray, we proved something else!

## Ending Remarks

If, for some reason, you’re masochistic and enjoy Coq (teehee), check out the Coq tutorial for more horrible adventures in theorem proving!

Also, you can have Coq prove the two theorems above as best as it can with `auto with *`

, so the whole going through it and proving everything manually is mostly redundant for such simple theorems.