I’m starting to get more of the pieces of the theorem proving puzzle. Going through “Software Foundations” and having “Type Theory and Formal Proof” as a reference has been very helpful with putting the pieces together. I’m starting to understand why folks like type theory. The encoding of logic and computation with types is surprisingly elegant. Most of the pieces fall out of abstraction and application/beta-reduction which is kinda amazing.

But enough of that. While going through “Software Foundations” I had to do an exercise about reversing lists. More specifically, reversing lists is an involution and involutions more generally are bijections so I wanted to prove this in the more general setting without having to worry about reversing lists.

This isn’t hard to do and in fact requires only very few tactics. Of course, the human proofs are much simpler because we don’t have to be as pedantic when dealing with equality. When working in Coq we have to spell out all the details about rewriting both sides of an equality. Anyway, that’s the high level overview so let’s spell out the details.

First we need a section with a few axioms that describe involutions

Section Involution. (* Domain and co-domain for the involution *) Variable A : Type. (* The involution *) Variable I : A -> A. (* The specification for I to be involutive *) Hypothesis involution : forall x : A, I (I x) = x.

In plain english the above just says we have some function `f : A -> A`

that satisfies `f(f(x)) = x`

. So if you know anything about functions then the proof that `f`

is a bijection is trivial because `f`

is its own two sides inverse, qed. The formalization in Coq is somewhat more involved but not by much.

There are two things we need to show: `I`

is injective, `I`

is surjective. For some reason I thought that showing it is injective would be simpler but it’s not so I’ll present surjectivity first

Theorem surjective : forall x : A, exists y : A, I y = x. Proof. intro. refine (ex_intro _ (I x) _). exact (involution x). Qed.

I learned about `refine`

and `ex_intro`

from reading the Coq tutorial. I still don’t understand how it all works but I know when I’m stuck I can try to refine the goal and it usually gets me closer to what I want to prove. I’ve made a note to better understand what the tactics actually do as I progress through various tutorials instead of just winging it. For the time being I’m going to leave it as an intuitive mystery.

Next up is injectivity. This one is simple if you’re doing an informal proof because you just apply `I`

to both sides of the equation and then use the involutive property to conclude that `x = y`

. I couldn’t figure out a simple way to apply a function to both sides of an equation so I had to make do with `elim`

and `rewrite`

. Here’s what that looks like

Theorem injective : forall (x y : A), I x = I y -> x = y. Proof. intros x y H. (* H : I x = I y |- x = y*) elim involution with y. (* ... |- x = I (I y) *) elim H. (* ... |- x = I (I x) *) rewrite -> involution. (* ... |- x = x *) trivial. Qed.

Hopefully the comments make it somewhat more clear what is in the context and what we’re trying to prove. We get what we want by rewriting with the involutive property and the hypothesis a few times but it still feels more complicated than necessary to me because it’s not a direct proof. Instead of applying `I`

to both sides of the equality and calling it a day we have to work backwards to our hypothesis which feels less intuitive if you’re familiar with the informal forward proof.

But anyway, that proves that all involutions are bijections

End Involution.