Coq中与依赖类型的关系

Question

我想在Coq中定义两个类型族上的关系，并提出了以下定义dep_rel和身份关系dep_rel_id:

Require Import Coq.Logic.JMeq.
Require Import Coq.Program.Equality.
Require Import Classical_Prop.
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. subst.
Abort.

inversion H似乎忽略了dep_rel_id i x i x中的两个x是相同的这一事实。我最终得到了证明状态：

E : Type -> Type
j : Type
x, y, x0 : E j
H2 : existT (fun x : Type => E x) j x0 = existT (fun x : Type => E x) j x
H : dep_rel_id j x j y
x1 : E j
H5 : existT (fun x : Type => E x) j x1 = existT (fun x : Type => E x) j y
x2 : E j
H4 : j = j
============================
existT E j x = existT E j x1

我不认为这个进球可以用这种方式来证明。对于这种情况，有什么我不知道的战术吗？

顺便说一句，我能够用一个经过调整的定义来证明这个引理，如下所示：

Inductive dep_rel_id' {X} : dep_rel X X :=
| dep_rel_id_intro' i x j y:
i = j -> x ~= y -> dep_rel_id' i x j y.
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. subst.
apply inj_pair2 in H0.
apply inj_pair2 in H1. subst.
reflexivity.
Qed.

但我仍然很好奇这是否可以用一种更简单的方式完成(可能不使用JMeq？(。感谢你的建议。

Answer 1

不确定inversion的问题是什么，事实上，它似乎已经失去了对一个重要等式的跟踪。然而，使用case H而不是inversion H似乎效果不错：

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.
case H.
reflexivity.
Qed.

但让case或destruct做inversion做不到的工作让我很惊讶。我怀疑inversion的某种错误简化，因为simple inversion也给出了一个可以证明目标的假设。