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

问题描述 投票:2回答:1

让我们有一个归纳类型为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.

如果无法证明,为什么?

coq
1个回答
0
投票

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

foo true = foo false -> true = false

鉴于truefalse不同,如果该定理是可证明的,则应该有可能证明foo truefoo false不同。问题在于这两种类型是isomorphic

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将不一致。

© www.soinside.com 2019 - 2024. All rights reserved.