coq - 没有公理的棘手依赖模式匹配

Question

假设我有以下类型:

Inductive foo : Type -> Type :=
  | A : forall X, Empty_set -> foo X
  | B : foo unit.

我可以证明以下内容:

Lemma obv : forall x : foo unit, x = B.

没有公理？ 依赖破坏策略很容易解决这个问题，但这引入了公理JMeq_eq。我发现this文章，但它似乎不适用于本例，因为 Type 没有 UIP。

Answer 1

不，如果没有单价性或 UIP 之类的东西，这是无法证明的。类型 foo unit 与类型 unit = unit 同构，因此证明 foo unit 的所有居民都等于 B 与证明 unit = unit 的所有居民都等于 eq_refl 相同，在 Coq 中，如果没有公理就无法证明这一点。