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.
We can use Coq’s interactive mode,
coqtop. It gives us a prompt:
Naturally, we want to prove something. We can use the
Goal 1 + 1 = 2.
We then get something that looks like this:
1 subgoal ============================ 1 + 1 = 2
Let’s prove this!
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
Abort (discard) our proof, so let’s just
A Vaguely More Exciting Proof
Why don’t we prove something slightly less trivial than \(1 + 1 = 2\)? What about some simple logic:
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
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,
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
Ha! As \(A\) is equivalent to \(B\), our goal of \(B\) is exactly our hypothesis,
get there, we can apply our hypothesis
H to the goal:
1 subgoal A : Prop B : Prop H : A <-> B HA : A ============================ A
Then tell Coq to match \(A\) with
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
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:
Again, we want to use the
intro tactic or the sneaky shortcut,
1 subgoal x : nat H : even x ============================ even (S (S x))
intros automatically derives all hypotheses possible. Let’s push on! Looking at
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
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:
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
since it’s not inductive:
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
1 subgoal x : nat H : even x ============================ odd (S x)
odd (S x) is implied by
even n, so we just apply
1 subgoal x : nat H : even x ============================ even x
And again, we use
Hooray, we proved something else!
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