Small Inversions for Proof Irrelevance

This blog post is about an apparently not-too-well-known Rocq trick. The reason this trick is well-known is that it is only needed in niche situations. Specifically, when one wants to prove that some P : Prop has unique proofs. Formally, we say that P has unique proofs when ∀ (a b : P), a = b.

Why Do You Need This?

Proof uniqueness is occasionally important. The reason I’m writing this blog post is because I talked to Clément Pit-Claudel at the Rocq’n’Share 2026, about how he faced this problem and did not know the solution I am presenting here. Clément needed proof uniqueness because he was working with a “map” data structure built from sorted lists; in other words this data structure carries a list along with a proof that this is sorted. We want this data structure to enjoy Leibniz equality, which means that the built-in equality in our type theory should be meaningful. Here concretely, this means that two maps should be equal when they have the same entries (i.e. lookups behave the same). This is why Clément required the list to be sorted in the first place. But besides reasoning about sorted lists, the proof of Leibniz equality also requires showing that if the two lists are equal, then the two proofs that the lists are sorted are also equal. This statement might seem weird to the classical mathematician, but it makes perfect sense in type theory. It connects to the notion of proof relevance.

Relevant Proofs

Rocq’s type theory is independent of the principle that all proofs are irrelevant. This means that it is sound to assume proof irrelevance as an axiom:

Axiom proof_irrel : forall (P : Prop) (p1 p2 : P), p1 = p2.

This axiom says that all proofs of a proposition P are equal. In other word, it says that proofs have no computational structure; and all proofs of a proposition can be exchanged for different ones without breaking anything.

Of course, it would be very reasonable to assume this axiom and go on with our lives. Similarly, we could also use SProp which has this axiom built-in. But doing so would be boring, so we are not going to do that. Instead, we force ourselves to live in a world without any axioms in Rocq; a world where a proposition can have two different proofs. And this even makes sense: After all, a proposition P ∨ Q, where both P and Q are true, can be proven in two different ways.

Note that Rocq’s type theory bends over backwards to prevent us from proving that these two proofs would be different, just like it prevents us from proving they are the same. Some users of Rocq care about meta-theoretic properties like canonicity, which is broken by assuming axioms like proof irrelevance. This is why we do not always want to assume the axiom, and why Rocq ensures the axiom remains independent so that both kinds of users are satisfied.

Which Propositions Have Unique Proofs?

So, the above axiom is independent, and it might make sense to consider disjunctions to have two different proofs (depending on which side is chosen). But there are some propositions for which the proofs are already unique in Rocq’s core type theory without any additional axioms. We collect them in the following table:

To see why the entires are what they are, let us look at some in more detail. The proposition True is defined as the following inductive type:

Inductive True := I : True.

This type has exactly one constructor, so by case analysis on any proof p : True, we can learn that it is precisely I and thus they’re all the same. For False, proof uniqueness follows from the fact that a proof of false is contradictory and thus implies everything (the explosion principle). A proof of P ∧ Q is just a pair, and two pairs are equal if their components are. Note that implication does not have unique proofs because implications are proven by writing a function, and Rocq does not have function extensionality.

The case for equality x = y is more interesting: Equality proofs are unique if the type of x (and y) has decidable equality! This is precisely Hedberg’s theorem.

Hedberg’s theorem and the broader structure of equality in Martin-Löf type theory is very deep and we only have limited time to get into it here. For more information, I recommend you read chapter 30 of this textbook by Gert Smolka. This in chapter 30.4 of this textbook, you will also find an introduction to Small Inversions, the real subject of this article. It is this chapter (30.4) that is the source of much of the material for this blog post.

Proof Uniqueness for Inductively Defined Propositions

The main question we want to tackle in this article is how we can prove that our own (index) inductive proposition has unique proofs. For the impatient, here is the summarized recipe:

1. State (and prove) a Small Inversion lemma for the inductive type.
2. The proof that p1 = p2 is by induction on p1 (with p2 quantified). This might need a “dependent induction” scheme, see below.
3. In each case, you can now invert p2 using the small inversion lemma.
4. The rest of the proof should be straightforward.

Small Inversion

The whole proof hinges on having “nice” small inversion lemmas. Such a lemma characterizes which constructor was used for your constructing a proof, based on the indices. Following the source material by Gert Smolka, we will use the following inductive definition:

Inductive lt (n : nat) : nat -> Prop :=
| ltS1 : lt n (S n)
| ltS2 m : lt n m -> lt n (S m).

This definition encodes that n < m. In fact, it is equivalent to the Stdlib’s version of n < m. Let’s prove that:

Lemma lt_is_lt n m :
  lt n m <-> n < m.
Proof.
  split.
  - induction 1; lia.
  - intros (p&->&_)%Nat.le_exists_sub.
    induction p.
    + simpl. econstructor.
    + simpl. econstructor 2. easy.
Qed.

The forwards direction is a simple induction on the inductive type above. The other way uses a lemma about < from the standard library.

Please Just Finally Show Me the Small Inversion Lemma

Lemma lt_sinv {n m} (H : lt n m) : match m as m'
  return lt n m' -> Prop with
  | 0 => fun _ => False
  | S m' => fun H =>
       (exists (Heq : m' = n), (eq_rect _ (fun x => lt n (S x)) H _ Heq) = ltS1 n)
    \/  exists Hrec, H = ltS2 _ _ Hrec
  end H.
Proof.
  destruct H.
  - left. exists eq_refl. simpl. reflexivity.
  - right. eexists. reflexivity.
Qed.

There it is. Looks scary, right?

Let’s discuss it step-by-step. First, we have the lemma statement. The lemma says that H : lt n m has a particular shape depending on the shape of m. If m is 0 then we have a contradiction, i.e. it is never the case that m = 0. If, however, m = S m', then there are two cases:

In the first case, our proof Hrec is constructed from ltS1 and thus n = m'. This is the hardest case to state, since we need the equality n = m' and then rewrite with it. Here, H has type lt n (S m') but ltS1 n has type lt n (S n), and while we know that n = m', we need to tell Rocq that this means that these types are in fact the same. We thus need to cast the value ltS1 n to the other type, using the fact that these types are equal.

The second case is easier: Here we just know that there is a “sub-proof” Hrec : lt n m', and our proof H is just precisely ltS2 n m' Hrec.

The proof of this lemma is easy: We destruct H and depending on which constructor was used to construct the proof, we prove the one or the other side.

Proving Uniqueness

We can now prove uniqueness. First, we need the dependently typed induction scheme for lt, which Rocq can auto-generate for us:

Scheme Induction for lt Sort Prop.

This declares lt_ind_dep which is like lt_ind but it tells us which constructurs we are made of in each case.

We can now follow the recipe above and prove the following:

Lemma lt_uniq n m (H1 H2 : lt n m) : H1 = H2.
Proof.
  revert H2. induction H1 as [|?? IH] using lt_ind_dep; intros H2.
  all: destruct (lt_sinv H2) as [(Heqm&Heq1)|(Hrec&Heq2)].
  - rewrite <-eq_rect_eq_dec in Heq1. 2: decide equality. easy.
  - exfalso. enough (n < n) by lia. now apply lt_is_lt.
  - subst n. exfalso. eapply Nat.lt_irrefl, lt_is_lt. eassumption.
  - rewrite Heq2. f_equal. apply IH.
Qed.

We do induction on H1 with H2 quantified, and then in each case apply out lt_sinv lemma to H2. This leaves us with four cases:

The first case is where H1 and H2 are constructed using ltS1. This case is almost immediate, since we need to prove that ltS1 n = H2 while knowing that ltS1 n = eq_rect n _ H2 _ Heq where Heqm : n = n. This opens the can of worms that is working with equalities and casts. We would need that Heqm = eq_refl to eliminate this cast. But since nat has decidable equality, we know (thanks to Hedberg’s theorem) that all proofs of n = n are equal. Thus can eliminiate the cast, and then are done. In Rocq, this is done using the Eqdep_dec.eq_rect_eq_dec theorem; and we show that nat indeed has decidable equality using decide equality.

The second case is symmetric to the third case: Here we know that one side is ltS1 and the other side is ltS2. Since we can not prove that these are equal, we need to derive a contradiction. In this case, the contradiction is that we know that both n = S m' and that lt n (S m'). From the latter, it follows that n < S m' and then we can derive a contradiction using the usual arithmetic reasoning.

The last case has both sides constructed using ltS2, and so both sides have a “recursive sub-proof.” We only need to prove that these sub-proofs are equal to each other, and this follows from the induction hypothesis.

And with this, we are done.

The High-Level Point

This proof shows all the intricacies one can encounter when proving that one’s index-inductives have unique proofs.

One difficult aspect was that our type had a constructor (ltS1) which identified different indices with each other. When this is the case, we will likely need an equality cast in our inversion principle. This also means that we can only hope for proof uniqueness when that equality itself has unique proofs, since will later on have to eliminate a cast using this equality.

The second difficult aspect was deriving a contradiction when one proof used ltS1 and the other uses ltS2. Here, we had to argue using the arithmetic properties of <. For this, we relied on the Stdlib, but we could have also started developing our theory about lt from scratch to eventually prove that lt n n is contradictory.

Bonus: Proof Uniqueness of Sorted

As a bonus, I want to show you the proof I gave to Clément. This is for showing that Sorted from the Rocq standard library has unique proofs, given that the sorting relation itself has unique proofs. This proof is actually much simpler than the one above, since it does not need ot reason about equality casts.

From Stdlib Require Import List Sorted RelationClasses Arith Permutation.

(* The definition of proof irrelevance. *)
Definition PI (P : Prop) := forall (a b : P), a = b.

(* The "small inversion" principle for [HdRel]. *)
Lemma HdRel_sinv A (R : A -> A -> Prop) a ls hr :
  match ls as lsx return HdRel R a lsx -> Prop
  with nil  => fun x => x = HdRel_nil R a
  | b :: bs => fun x => exists p, x = HdRel_cons R a b bs p end hr.
Proof.
  destruct hr.
  - easy.
  - eexists. reflexivity.
Qed.

(* The small inversion principle for [Sorted]. *)
Lemma Sorted_sinv A (R : A -> A -> Prop) ls s :
  match ls as lsx return Sorted R lsx -> Prop
  with nil  => fun x => x = Sorted_nil R
  | b :: bs => fun x => exists p1 p2, x = @Sorted_cons A R b bs p1 p2 end s.
Proof.
  destruct s.
  - easy.
  - eexists _, _. reflexivity.
Qed.

Scheme Induction for Sorted Sort Prop.
Section SortedPI.

  Context (A : Type).
  Context (R : A -> A -> Prop).
  Context (Hpi : forall a1 a2, PI (R a1 a2)).

  Lemma HdRel_PI (a : A) ls : PI (HdRel R a ls).
  Proof.
    (* Proof is simple enough: destruct one, invert the other. *)
    intros p1 p2. destruct p2.
    - apply (HdRel_sinv A R a nil p1).
    - edestruct (HdRel_sinv A R a _ p1) as [q1 H].
      rewrite H. f_equal. apply Hpi.
  Qed.

  Lemma Sorted_PI (ls : list A) : PI (Sorted R ls).
  Proof.
    intros p1 p2.
    (* Induction with p1 quantified. We can not use the [in p1|-*] because
       that is incompatible with [using] for no good reason. *)
    revert p1. induction p2 as [|??? IH] using Sorted_ind_dep; intros p1.
    - apply (Sorted_sinv A R nil p1).
    - destruct (Sorted_sinv A R _ p1) as (q1&q2&H).
      rewrite H. f_equal.
      + eapply IH.
      + apply HdRel_PI.
  Qed.

End SortedPI.

Conclusion

It turns out that Small Inversions are a quite powerful principle. This is perhaps not surprising to the working dependent type theorists, but many people use Rocq without really engaging with this aspect of it.

I learned most of what I know about dependent types from Gert Smolka’s book Modeling and Proving in Computational Type Theory, which I already mentioned above. It is also where the proof about lt comes from. (The one for Sorted I was then able to write myself.)

Another great book on dependently typed programming is Adam Chlipala’s Certified Programming with Dependent Types. Small Inversions were originally discovered by Monin in 2010.

Thanks to Clément for motivating me to write this post.