Gravatar rfw.name

Experiments with Coq

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:

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:

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.

comments powered by Disqus