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

```
Lemma andb_true: forall b: bool, andb b true = b.
Proof using.
intros *.
destruct b; exact eq_refl.
Defined.
Print andb_true.
(* andb_true =
fun b : bool =>
if b as b0 return ((b0 && true)%bool = b0) then eq_refl else eq_refl
: forall b : bool, (b && true)%bool = b
*)
```

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

```
Inductive even: nat -> Prop :=
| is_even_0 : even 0
| is_even_SS : forall n, even n -> even (S (S n)).
Lemma not_even_1 : ~ even 1.
Proof using.
intro contra.
```

We would like to perform case analysis on the `even 1`

term to show both options
are impossible.

```
destruct contra.
```

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

!

```
Undo.
```

Even if we use the `eqn`

variant, `destruct`

will erase our parameter.

```
destruct contra eqn:case.
Undo.
```

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.

```
inversion contra.
```

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?

```
Undo.
set (x := 1) in contra.
destruct contra.
```

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.

```
Undo.
assert (x_eq: x = 1) by exact (eq_refl _).
```

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

```
clearbody x.
destruct contra.
```

There we go! We see the `x_eq`

hypothesis was preserved, which we can discriminate
in both cases.

```
Undo.
destruct contra; discriminate x_eq.
Qed.
```

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.

```
Ltac gen_eq H x :=
let i := fresh in
set (i := x) in H;
let eq := fresh in
assert (eq: i = x) by exact eq_refl;
clearbody i.
Goal ~ even 1.
intro contra.
gen_eq contra 1.
```

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

```
Abort.
Ltac gen_eq_non_vars H :=
repeat match type of H with
| context[_ ?x] =>
assert_fails (is_var x);
gen_eq H x
end.
Goal ~ even 1.
intro contra.
gen_eq_non_vars contra.
Abort.
Ltac inv H :=
gen_eq_non_vars H;
destruct H;
subst;
try discriminate.
Goal ~ even 1.
intro contra.
inv contra.
```

Success!

```
Qed.
```

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

```
Require Import Coq.Lists.List.
Import ListNotations.
Inductive in_list {A} (a: A): list A -> Prop :=
| in_head : forall t,
in_list a (a :: t)
| in_tail : forall x t,
in_list a t ->
in_list a (x :: t).
Goal forall x, in_list x [1;2] -> x = 1 \/ x = 2.
intros * H.
inv H.
- injection H1; repeat intros ->.
auto.
- injection H1; repeat intros ->.
clear H1.
inv H.
+ injection H1; repeat intros ->.
auto.
+ injection H1; repeat intros ->.
clear H1.
inv H.
Qed.
```

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.

```
Lemma andb_true': forall b: bool, andb b true = b.
Proof using.
intros *.
```

Using `inversion`

here on `b`

won’t actually destruct it, although it will fork
our proof goal into two identical goals.

```
inversion b.
Undo.
```

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.

```
Ltac inv H ::=
let H' := fresh H in
pose proof H as H';
gen_eq_non_vars H';
destruct H';
subst;
try discriminate.
inv b.
Abort.
```

The other thing `inversion`

can do that `inv`

can’t is extract sub-equalities:

```
Goal forall a b, S a = S b -> a = b.
intros * H.
inversion H.
```

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:

```
Undo.
injection H.
auto.
Qed.
```