The following problem was just posted on SO, but the behaviour seemed strange to me so I’d like to understand it better. The original problem was

```
Definition dep_rel (X Y: Type -> Type) :=
forall i, X i -> forall j, Y j -> Prop.
Inductive dep_rel_id {X} : dep_rel X X :=
| dep_rel_id_intro i x: dep_rel_id i x i x.
Lemma dep_rel_id_inv {E} i x j y:
@dep_rel_id E i x j y -> existT _ i x = existT _ j y.
Proof.
intros H.
inversion H.
Abort.
```

here `inversion H`

somehow lost the link between the two indices `x`

and `y`

, ensuing in an unprovable goal. However, using `simple inversion H`

instead of `inversion H`

seems to give a much better context – indeed, one which allows to prove the goal. So it seems like the simplification `inversion`

performs are somehow wrong here.

Does anyone have an idea of what happens, and whether this is a bug or a feature?

For the record, the hypotheses generated by `inversion`

are

```
i0 : Type
x0 : E i
H0 : i0 = i
H2 : existT (fun x : Type => E x) i x0 = existT (fun x : Type => E x) i x
H1 : i = j
x1 : E i
H4 : i = j
x2 : E i
H5 : existT (fun x : Type => E x) i x1 = existT (fun x : Type => E x) j y
```

while the ones generated by `simple inversion`

are

```
i0 : Type
x0 : E i0
H0 : i0 = i
H1 : existT (fun i : Type => E i) i0 x0 = existT (fun i : Type => E i) i x
H2 : i0 = j
H3 : existT (fun j : Type => E j) i0 x0 = existT (fun j : Type => E j) j y
```

IIRC `inversion`

tends to eagerly rewrite trivial equalities and is robust to failure, which would explain the difference in presence of heterogeneous equalities like here

it was never designed with clever equality manipulation in mind, so it's not surprising that it fails badly with this kind of examples

(this is now a *when the hell do we get small inversion in Coq* thread)

alternatively, Coq-Equations tactics should help here, e.g. `dependent elimination`

...

Surprisingly enough, `case`

also does the job(!)

Last updated: Sep 23 2023 at 14:01 UTC