# Coq Equality IV

## 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:

- 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.

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: