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 inversionare

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, casealso does the job(!)

Last updated: Sep 23 2023 at 14:01 UTC