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
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
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
But we lose the information that the term was parameterized over
Even if we use the
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
How would we go about replicating this behavior? Well, we know
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
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:
- Replace values with variables
- Remember the equality between the new variable and its value.
- Clear the definition of the variable.
- 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.
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
inversion tactic in a couple important ways. First, the
will actually preserve the original term. For instance, consider again the
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
The more specialized
injectivity accomplishes the same fundamental task: