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 对 bug/wrong 进行了某种简化，因为 simple inversion 也给出了一个可以证明目标的假设。

Coq 中与依赖类型的关系

Relations with dependent types in Coq

coq

dependent-type