Understanding Curry-Howard through Rocq

Before I ever started my PhD, I could have recited to you the Curry-Howard Isomorphism: proofs are programs, and programs are proofs. But it was only when I started working on proof compilation in the interactive theorem prover Rocq (formerly known as Coq) that I feel that I truly understood it – along with why it works, why theorem provers work, and all sorts of cool tricks and connections you can use.

This blog post will hopefully share this understanding with you, all without writing too much Rocq code. So if you too are wondering how it is that proofs are programs, and programs are proofs, and why you should care, read onward!

Proofs are Programs

This direction made the most sense to me in undergrad: proofs are algorithms that show you how to arrive at the conclusion of the lemma being proved, and since programs are representations of algorithms, a proof is actually a kind of program.

I could leave it at that, and many people might be satisfied with that explanation. But, we can also ask: what happens when you write down a proof in an interactive theorem prover (ITP) like Rocq? Usually, to prove any statement, you’ll write down a proof script, and end it with Qed, as you might in mathematics. However, you can also end a proof with Defined. As an example, take this proof that addition is commutative over the natural numbers – the actual content of the proof script (everything between Proof. and Defined.) does not matter so much.

Lemma addition_is_commutative :
  forall (n m: nat),
    n + m = m + n.
Proof.
  induction n; simpl; intros.
  - rewrite <- plus_n_O. eauto.
  - rewrite IHn. rewrite plus_n_Sm. eauto.
Defined.

Now, I can actually print my lemma.

Print addition_is_commutative.

The result is this (admittedly hard to read) output of what is called the proof term, which is a lot more text than we had to write in the proof script:

addition_is_commutative =
fun n : nat =>
nat_ind (fun n0 : nat => forall m : nat, n0 + m = m + n0)
  ((fun m : nat =>
    eq_ind m (fun n0 : nat => m = n0) eq_refl (m + 0)
           (plus_n_O m))
   :
   forall m : nat, 0 + m = m + 0)
  (fun (n0 : nat) (IHn : forall m : nat, n0 + m = m + n0) =>
   (fun m : nat =>
    eq_ind_r (fun n1 : nat => S n1 = m + S n0)
      (eq_ind_r (fun n1 : nat => n1 = m + S n0) eq_refl
                (plus_n_Sm m n0))
      (IHn m))
   :
   forall m : nat, S n0 + m = m + S n0) n
     : forall n m : nat, n + m = m + n

If I elide over most of the innards of the proof term, leaving just the outermost function applications, and add some parentheses for clarity, we get something that is perhaps a bit more digestable:

addition_is_commutative =
(fun (n: nat) => nat_ind (...) (...) (...) n)
  : forall (n m: nat), n + m = m + n

What this is saying is that the content of the addition_is_commutative proof is a function, where the type of that function ends up being…the statement of the lemma! It turns out that while we were writing that proof script, behind the scenes, it was actually constructing this function, the proof term. In other words, writing the proof script was actually programming.

Programs are Proofs

Now, to try to understand the other direction, we might want to try to invert the reasoning from the last section. So, programs are algorithms, so they’re proofs…?

…I never felt like this was a very satisfying conclusion however. A mobile phone app, for instance, didn’t seem to have an immediate “proof” as a goal. So where was the proof statement hiding?

Well, let’s take a look at any function:

Definition my_definition : input1 -> input2 -> output :=
  (* … *)

We don’t even need the content of my_definition, so for now, let’s just focus on its type. One way to read this type is: “Given something of type input1 and something of type input2, I can produce something of type output.” Now let’s consider a lemma statement:

Lemma my_lemma : premise1 -> premise2 -> conclusion.

We can read this lemma as stating “If premise1, then if premise2, then conclusion can be reached.”

What escaped me when I first learned how to use Rocq was that there is a reason why both of these statements use : and ->: the : is giving the type of the object being defined, and -> is a way to combine those types! In my head, I had two different interpretations of :: one for Definitions, meaning “type of”, and one for lemmas, meaning “states that”. Similarly, I had two different interpretations of ->: function arrow and logical implication.

But it’s actually just the same thing!

So, a program is a proof of its type: that we can come up with an algorithm that meets the type specification. Returning to the mobile app example, its code is a proof that the design and specification can be met, giving a whole new meaning to the phrase “proof of concept”.

Types as Logical Propositions

Before I move on, I just wanted to reiterate a fact that I only brushed on in the past two sections: types are logical propositions. We have already seen that we can encode implication as ->, and it turns out that the fact that Rocq is dependently typed allows it to express universal and existential quantification too! There’s a lot more to get into on this topic (it could be its own blog post), so for now, let’s see how we can leverage the Curry-Howard Isomorphism.

Construction as Truth; Proof Checking as Type Checking

I was both a math and computer science major in undergrad, and one of my undergraduate mathematics professors once mentioned to me that there existed a whole community of mathematicians that did not use proof by contradiction: constructive mathematics.

At the time, I thought that those mathematicians were crazy. I asked the professor, “Why would you want to give up such a powerful tool? Some proofs are more easily proved using contradiction, and there are some lemmas that can’t be proved without it.” He replied something to the effect of, “Well, in some ways of thinking, how do you know that it was valid unless you provided an actual construction of it?”

It was probably a few years into my PhD when I realized that I had stumbled into just that very sphere of thinking! Rocq is built on constructive logic. And there is a good reason for it.

One of the goals of interactive theorem provers like Rocq and Lean is to create reliable, machine checkable proofs. How do we ensure that a proof is valid?

Well, we know that our proofs are actually programs in this instance, and not only that, they are programs that need to have a particular type: a type that is the logical statement that is being proved. Therefore, we can get proof checking out of type checking!

Type Constructors Construct Truths

We’re not limited to mere implication. Rocq allows you to write types that can be constructed from smaller instances of themselves. These are inductive datatypes. Common examples include the natural numbers and lists:

Inductive nat :=
| O : nat
| S : nat -> nat.

Inductive list (T: Type) :=
| nil : list T
| cons : T -> list T -> list T.

These types tell us that there exist an initial, “smallest” inhabitant of the type, called O (zero) and nil respectively, and that in order to construct larger inhabitants, you can apply S to any natural number, and cons to a new head element and an existing list.

You can also use inductive datatypes to create new mathematical statements, predicates that can only exist if constructed properly:

Inductive is_even : nat -> Prop :=
| is_even_zero :
  is_even 0
| is_even_ss :
  forall (n: nat),
    is_even n ->
    is_even (S (S n)).

The is_even inductive datatype has two constructors: is_even_zero constructs the even-ness of zero, and is_even_ss constructs the even-ness of the successor of the successor of n (i.e., n + 1 + 1 = n + 2), given evidence that n is already even. If we can construct an instance of is_even n, for some n, that instance can be a proof of n’s-evenness.

If I want to prove that 4 is even, then I can prove that it is by applying the appropriate constructors:

Lemma is_even_4_lemma : is_even 4.
Proof.
  eapply is_even_ss. eapply is_even_ss. eapply is_even_zero.
Defined.

…but I can also write down this definition, which applies the constructors manually:

Definition is_even_4_definition : is_even 4 :=
  is_even_ss 2 (is_even_ss 0 is_even_zero).

I don’t even have to do it so directly, however. Since programs are proofs, and proof scripts create programs, I can also use a proof script to write the program is_even_4_definition, and use further automation to apply the correct constructor at each step:

Definition is_even_4_lemma' : is_even 4.
Proof.
  repeat econstructor.
Defined.

Print is_even_4_lemma'.
(*
is_even_4_lemma' =
is_even_ss 2 (is_even_ss 0 is_even_zero)
     : is_even 4
*)

Metaproving

Perhaps we wanted an automated way of proving that any natural number is even, and not just 4.

Well, we can write a function for that!

Fixpoint construct_is_even (n: nat) : option (is_even n) :=
  match n with
  | 0 => Some (is_even_zero)
  | 1 => None
  | S (S m) =>
      match construct_is_even m with
      | Some pf => Some (is_even_ss m pf)
      | None => None
      end
  end.

Note that not all numbers are even, so we have to tell Rocq that this function only sometimes returns evidence of n being even: option (is_even n). An option T is a type that can be instantiated by either Some t (where t has type T) or by None.

Let’s break this down by cases: given n, we have some options:

• If n is 0, then we can construct that 0 is even with is_even_zero
• If n is 1, then that’s definitely not true, so we return None
• Otherwise, we have n = m + 2. Then we try to construct proof that m is even.
  • If it is, and we get some proof pf of m’s even-ness, then we can construct the proof that m + 2 is even: is_even_ss m pf
  • If we can’t construct the proof of m being even, then we return None.

While this example is a bit silly, it hints at ways that you could build automation for Rocq: automatically building proofs using metaprogramming, or metaproving.

How far can we go: Conclusions and Takeaways

We’ve seen that the Curry-Howard Isomorphism is embodied very neatly in theorem provers like Rocq, and how understanding the Curry-Howard Isomorphism opens up a whole range of possibilities, such as machine checkable proofs, new logical predicates through inductive types (where the construction of the object of such a type is a proof of a predicate), and functions that can automate the proving of these predicates.

To answer the question of this section, on how far we can go: well, so much further!

• You can write proofs about your proof-producing functions
  • For instance, we might want to know that the function construct_is_even is complete: i.e., for any even number, its result is not None.
  • We gain its soundness (i.e., every number for which a proof of evenness is generated is actually even) from the fact the function type-checks
• You can write inductive datatypes that prove properties about other proofs
• You can prove properties about your inductive datatypes that are proofs of properties about other proofs…

the list goes on! It’s just turtles programs all the way down.