## Inversion

When I first learned about the inversion tactic, I was constantly getting it mixed up with destruct. When plugging in a USB drive, one always finds themselves trying the wrong side first. Similarly, I would always try the wrong tactic first before realizing my mistake.

In fact, the two are quite similar in their goal. destruct is the classic means of case analysis. When one invokes destruct x, the proof branches into $n$ proof goals, for the $n$ constructors of the inductive type x.

Let’s take a look at what a proof using destruct looks like under the hood.

destruct structures our proof term as an if statement. More generally, it generates a match statement on the inductive term’s constructors.

It is important to note here that the match statement does not take into account any parameters to the inductive term which should in theory contradict certain cases. Because destruct just generates a simple match, this information is not taken into account, and is actually erased!

Let’s construct an example.

We would like to perform case analysis on the even 1 term to show both options are impossible.

But we lose the information that the term was parameterized over 1!

Even if we use the eqn variant, destruct will erase our parameter.

What we need here is inversion. inversion also considers the possible constructors of the term. However, it actually looks at the values of the inductive term’s parameters to determine which cases are impossible.

Conceptually, it is as if we are looking at the constructors, and reasoning about them in reverse. What constructors could have produced this term? The name “inversion” is intentionally suggestive of this backward reasoning over constructors.

In this case, inversion solves our goal instantly, since there are no possible cases.

How would we go about replicating this behavior? Well, we know destruct erases the value of our parameters, but what if we replaced our values with variables, and specified the value of the variable in a separate hypothesis?

The parameter is still being erased! The reason why is that the value of x is overwritten by the case analysis. What we need to do is remember the value of x in a separate hypothesis as an equality.

While not strictly neccessary, clearing the definition of x makes the context more readable.

There we go! We see the x_eq hypothesis was preserved, which we can discriminate in both cases.

For fun, why don’t we automate this with a tactic? The general process is:

1. Replace values with variables
2. Remember the equality between the new variable and its value.
3. Clear the definition of the variable.
4. Destruct the inductive term

We can add more steps for convenience, such as substituting the equalities back after the destruct step, and checking if any case is discriminable.

These automatically generated names are ugly, but they should be largely erased after substitution.

Success!

Let’s try our hand at a more complicated example, where inversion doesn’t trivially solve our goal.

Clearly, we can see our little inv tactic is really helpful for reasoning about these dependent terms!

To close things out, I should point out that our inv tactic actually diverges from the inversion tactic in a couple important ways. First, the inversion tactic will actually preserve the original term. For instance, consider again the andb_true proof.

Using inversion here on b won’t actually destruct it, although it will fork our proof goal into two identical goals.

This is because inversion actually makes a copy of the term, and destructs the copy. The idea is that we only want inversion to perform case analysis on the facts which produced the constructor, not on the constructor itself. We can replicate that behavior easily enough.

The other thing inversion can do that inv can’t is extract sub-equalities:

However, this behavior is not in line with the goal of the rest of the tactic, so I’d argue is out of place being included in inversion.

The more specialized injectivity accomplishes the same fundamental task: