coq - 相等索引的归纳类型意味着相等的索引

Question

让我们有一个由foo索引的归纳类型x : X。

Parameter X : Type.

Inductive foo : X -> Type :=
| constr : forall (x : X), foo x.

我很好奇，如果 foo x = foo y暗示 x = y。我不知道如何证明这一点。

Lemma type_equality_implies_index_equality : forall (x y : X), foo x = foo y -> x = y.

如果无法证明这一点，为什么呢？

Answer 1

无法证明。设置X := bool时，请考虑以下定理的特殊情况:

foo true = foo false -> true = false

给定 true和 false不同，如果该定理是可证明的，则应该有可能表明 foo true和 foo false不同。问题在于这两种类型是同构的:

Inductive foo : bool -> Type :=
| constr : forall (x : bool), foo x.

(* An isomorphism between foo true and foo false *)
Definition foo_t_f (x : foo true) : foo false := constr false.
Definition foo_f_t (x : foo false) : foo true := constr true.

(* Proofs that the functions are inverses of each other *)
Lemma foo_t_fK x : foo_f_t (foo_t_f x) = x.
Proof. unfold foo_f_t, foo_t_f. now destruct x. Qed.

Lemma foo_f_tK x : foo_t_f (foo_f_t x) = x.
Proof. unfold foo_f_t, foo_t_f. now destruct x. Qed.

在Coq的理论中，如果不假设额外的公理，就不可能证明两种同构类型是不同的。这就是对Coq理论(例如 homotopy type theory)进行扩展的原因。在HoTT中，同构类型可以证明是相等的，并且如果可以证明您的定理，HoTT将会是不一致的。