Stream: Coq users

Topic: Wrong inversion simplification


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Paolo Giarrusso (Jan 13 2022 at 18:22):

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

view this post on Zulip Meven Lennon-Bertrand (Jan 13 2022 at 18:37):

Surprisingly enough, casealso does the job(!)


Last updated: Jan 29 2023 at 01:02 UTC