With Pierre Boutillier, we have been working on a new Coq tactic lately, called invert. From my point of view, it started as a quest to build a replacement to the inversion tactic. inversion is a pain to use, as it generates sub-goals with many (dependent) equalities that must be substituted, which force the use of subst, which in turns also has its quirks, making the mantra inversion H; clear H; subst quite fragile. Furthermore, inversion has efficiency problems, being quite slow and generating big proof terms. From Pierre’s point of view, this work was a good way to implement a better destruct tactic, based on what he did during an internship (report in French (PDF)).

In a nutshell, the idea behind a destruction and an inversion is quite similar: it boils down to a case analysis over a given hypothesis. And there are quite a few tactics that follow this scheme: elim, case, destruct, inversion, dependent destruction, injection and discriminate (it is true that the last two tactics are quite specialized, but fit the bill nevertheless). Why on Earth would we need to add a new element to this list?

Well, it turns out that building on ideas by Jean-Francois Monin to make so called “small inversions”, one can unify the inner-working of most of the aforementioned list: it suffices to build the right return clause for the case analysis.

Let’s take an example.

1, equivalent to Streicher’s axiom K. (Just to keep tabs, note that running the Show Proof command in Coq outputs a partial proof term that is already 73 lines long at this point.)

If we use dependent destruction H instead of inversion, we get the expected hypothesis H: P n v (which is far better from an usability point of view). Yet, there is no magic here: dependent destruction simply used a dependent equality axiom internally to get rid of the dependent equality, and generates a 64 lines long proof term that is not very pretty.

At this point, one may wonder: what should the proof term look like? and, is it necessary to use the K axiom here?

A black belt Coq user versed in dependent types could write the following one.

this chapter.)

Then, what is diag? Well, it is a function that follows the structure of the arguments of P to single out impossible cases, and to refine the context in the other ones using dependent pattern matching, in order to reduce to the right type (the type of the initial conclusion of the goal). The idea behind such “small-scale inversions” was described by Monin in 2010 and is out of the scope of this blog post. What is new here is that we have mechanized the construction of the diag functions as a Coq tactic, making this whole approach practical.

All in all, using our new tactic, we can just use the following proof script:


We are still working on our prototype, but we are quite confident that we got the main thing right: mechanizing the construction of the return clause. We will come back to this blog when we need beta-testers!


  1. See the following FAQ question (Can I prove that the second components of equal dependent pairs are equal?). You may also be interested in this other question (What is Streicher’s axiom K?). The EqdepFacts standard library module, that has the equivalence proofs between all those subtle notions. Finally, if you want to finish this proof using these axioms, you can use Require Import Eqdep. then the inj_pair2 lemma. Once you’re done, Print Assumptions test. will let you check that you relied on an additional axiom – or Print Assumptions inj_pair2.↩︎

  2. Moreover, since our proof terms are less cluttered, it seems less likely than recursive definitions made in “proof mode” with invert will fail to pass the termination check once Coq’s guard condition deals properly with such commutative cuts, another part of Pierre’s thesis work.↩︎