## Stream: Coq users

### Topic: Wrong inversion simplification

#### Meven Lennon-Bertrand (Jan 13 2022 at 09:47):

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?

#### Meven Lennon-Bertrand (Jan 13 2022 at 09:48):

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

#### Pierre-Marie Pédrot (Jan 13 2022 at 10:41):

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

#### Pierre-Marie Pédrot (Jan 13 2022 at 10:41):

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

#### Pierre-Marie Pédrot (Jan 13 2022 at 10:42):

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

#### Paolo Giarrusso (Jan 13 2022 at 18:22):

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

#### Meven Lennon-Bertrand (Jan 13 2022 at 18:37):

Surprisingly enough, `case`also does the job(!)

Last updated: Jan 29 2023 at 01:02 UTC