Coq: Prove Your Code is Correct (No, Really)

What Even Is Coq?

Imagine if your compiler didn't just check types — it checked logic. What if you could write 2 + 2 = 4 and have the computer verify it's true, not just run it and hope? That's Coq.

Coq is a proof assistant — a tool where you write mathematical proofs, and the computer checks every single step. No handwaving. No "trust me, it works." The compiler either accepts your proof or tells you exactly where you're wrong.

It's used to verify:

• The Paris Métro line 14's autopilot software
• The CompCert C compiler (used in aviation)
• Fundamental theorems in mathematics (the Four Color Theorem took 6 years to formalize)

And today, you're going to learn it in 15 minutes.

Installation

# macOS
brew install coq coqide

# Ubuntu
apt install coq coqide

# Or just use the browser: https://coq.vercel.app

The browser version is the easiest — open it and follow along.

Your First Proof

Open Coq and type this:

Theorem my_first_proof : 1 + 1 = 2.
Proof.
  reflexivity.
Qed.

Hit the "advance" button (or Ctrl+Down). You should see:

No more goals.

Congratulations. You just proved that 1 + 1 = 2. To a computer. Formally. With a certificate.

Let's unpack what happened:

• Theorem — "I'm about to make a claim"
• my_first_proof — the name of the theorem (call it whatever you want)
• : 1 + 1 = 2 — the actual claim
• Proof. — "here comes the proof"
• reflexivity. — "both sides are literally the same thing, QED"
• Qed. — "I'm done, lock it in"

reflexivity is a tactic — a proof step. It works when both sides of = reduce to the same value. Since 1 + 1 computes to 2, and 2 = 2 is obvious, we're done.

What Is a Tactic?

A proof in Coq is interactive. At any point, Coq shows you the current goal — what you still need to prove. You apply tactics to make progress until there are no goals left.

Think of it like a video game:

• Goal = the boss you need to defeat
• Tactics = your moves
• Qed = you win

Let's try a slightly harder example:

Theorem add_comm_simple : 2 + 3 = 3 + 2.
Proof.
  reflexivity.
Qed.

Still works! Coq just computes both sides and sees they're both 5.

Introducing Variables

What if we don't know the specific numbers? What if we want to say "addition is commutative for all natural numbers"?

Theorem add_comm : forall n m : nat, n + m = m + n.

forall means "for all". nat is the type of natural numbers. This is saying: "no matter what n and m you pick, n + m = m + n."

Can we just use reflexivity? Try it:

Proof.
  reflexivity.  (* This will FAIL *)
Qed.

Nope. n and m are unknown — Coq can't just compute. We need to do real work.

Proof.
  intros n m.
  induction n.
  - simpl. rewrite add_0_r. reflexivity.
  - simpl. rewrite IHn. rewrite add_succ_r. reflexivity.
Qed.

Okay, that got more complex. Let's slow down and understand the tactics:

The Core Tactics Cheat Sheet

intros

Moves variables from the goal into your context (like function arguments).

(* Goal: forall n : nat, n + 0 = n *)
intros n.
(* Now you have n in context, goal is: n + 0 = n *)

simpl

Simplifies/computes things.

(* Goal: 0 + n = n *)
simpl.
(* Goal: n = n  -- because 0 + n reduces to n by definition *)

reflexivity

Closes the goal when both sides are identical.

rewrite

Substitutes one thing for another using an equation.

(* You have: H : a = b *)
(* Goal: a + 1 = 3 *)
rewrite H.
(* Goal: b + 1 = 3 *)

induction

The big one. Proof by induction.

induction n.
(* Creates two goals:
   1. Base case: prove for n = 0
   2. Inductive case: assuming IHn (the hypothesis), prove for S n *)

apply

Use a theorem or hypothesis to close a goal.

apply IHn.

destruct

Case analysis — split on possible values.

destruct b.  (* if b is bool, creates two goals: one for true, one for false *)

Let's Prove Something Real

Let's define our own function and prove something about it.

(* Define a doubling function *)
Fixpoint double (n : nat) : nat :=
  match n with
  | 0    => 0
  | S n' => S (S (double n'))
  end.

Fixpoint is for recursive functions. match is pattern matching. S n' means "successor of n'" — Coq represents natural numbers as 0, S 0, S (S 0), ... (Peano arithmetic).

Now let's prove that double n = n + n:

Theorem double_is_add : forall n : nat, double n = n + n.
Proof.
  intros n.
  induction n as [| n' IHn'].
  - (* Base case: n = 0 *)
    simpl.
    reflexivity.
  - (* Inductive case: n = S n' *)
    simpl.
    rewrite IHn'.
    rewrite <- plus_n_Sm.
    reflexivity.
Qed.

Step by step:

1. intros n — bring n into scope
2. induction n as [| n' IHn'] — induct on n, naming the predecessor n' and inductive hypothesis IHn'
3. First - bullet handles the base case
4. Second - bullet handles the inductive step
5. rewrite IHn' — substitute double n' = n' + n' into the goal
6. rewrite <- plus_n_Sm — apply a lemma backwards (the <- flips direction)

Types Are Propositions (Mind = Blown)

Here's the coolest thing about Coq: types and propositions are the same thing.

This is the Curry-Howard correspondence:

So when you write a function in Coq, you're also writing a proof. A function of type A -> B is literally a proof that "if A is true, then B is true."

(* This function IS a proof of "if P then P" *)
Definition identity : forall P : Prop, P -> P :=
  fun P proof => proof.

(* Equivalently, as a theorem: *)
Theorem p_implies_p : forall P : Prop, P -> P.
Proof.
  intros P proof.
  exact proof.
Qed.

exact is a tactic that says "this term is the proof you're looking for."

A Worked Example: Lists

Let's do something practical. We'll prove that reversing a list twice gives back the original list.

Require Import List.
Import ListNotations.

(* reverse (reverse l) = l *)
Theorem rev_involutive : forall A (l : list A),
    rev (rev l) = l.
Proof.
  intros A l.
  induction l as [| x xs IHxs].
  - (* Base case: empty list *)
    simpl.
    reflexivity.
  - (* Inductive case *)
    simpl.
    rewrite rev_app_distr.
    simpl.
    rewrite IHxs.
    reflexivity.
Qed.

This is a real theorem about real data structures. Coq verified that reversing a list twice always gives back the original — for all possible lists, not just the ones you tested.

The Magic of SearchAbout

Lost? Don't know which lemma to use? Coq has a search:

Search (_ + 0 = _).     (* find lemmas about adding 0 *)
Search (rev (_ ++ _)).  (* find lemmas about rev and append *)

This is incredibly useful. Most Coq work is knowing which existing lemmas to apply.

Common Beginner Mistakes

"reflexivity didn't work" → Try simpl first, then reflexivity. Or the sides aren't actually equal.

"I'm stuck with a weird goal" → Use simpl to reduce it. Use unfold myDef to expand definitions.

"induction isn't working" → Make sure you haven't already intros'd the variable you want to induct on. Induct first, then intros.

"I don't know what lemma to use" → Search. Always Search.

Where to Go Next

You've learned:

• ✅ What Coq is and why it matters
• ✅ Basic tactics: intros, simpl, reflexivity, rewrite, induction, apply
• ✅ How to define functions with Fixpoint
• ✅ The Curry-Howard correspondence
• ✅ How to prove things about lists

Next steps:

Software Foundations — the best free textbook on Coq, written by Benjamin Pierce. Volume 1 (Logical Foundations) is where everyone starts.

Certified Programming with Dependent Types — more advanced, by Adam Chlipala. Opinionated and brilliant.

Coq'Art — the original Coq textbook.

The Big Picture

Most programming is testing. You run your code on some inputs and hope it works on the rest.

Coq is proving. You write a mathematical argument that your code is correct for all possible inputs, and the computer checks every step of that argument.

It's slower. It's harder. And for critical systems — compilers, operating systems, cryptographic protocols — it's the only way to be truly sure.

Now go break some proofs. 🐓