pattern-matching - 删除 Coq 中的琐碎匹配子句

Question

考虑以下示例:

Definition cast {A : Set} (B : Set) (prf : A = B) (x : A)   : B.
  rewrite prf in x.
  refine x.
Defined.

Lemma castLemma0 {A : Set} : forall (x : A) prf, cast A prf x = x.
Proof.
  intros.
  compute.
???

在计算步骤之后，我们留下以下上下文和子目标

A : Set
x : A
prf : A = A
______________________________________(1/1)
match prf in (_ = y) return y with
| eq_refl => x
end = x

显然左手边和右手边是相等的。但我不确定如何摆脱左侧烦人的“匹配”子句。特别是，尝试破坏 prf 会产生以下错误

Abstracting over the terms "A" and "prf"
leads to a term
fun (A0 : Set) (prf0 : A0 = A0) =>
match prf0 in (_ = y) return y with
| eq_refl => x
end = x which is ill-typed.
Reason is: In pattern-matching on term 
"prf0" the branch for constructor 
"eq_refl" has type "A" which should be 
"A0".

有没有办法摆脱这个匹配子句？

Answer 1

如果不假设额外的公理，这在 Coq 中是无法证明的，通常是 eq_rect_eq 或等效的东西(身份证明的唯一性 (UIP) 或公理 K)。

如果你将 castLemma0 限制为 eq_refl 的情况，即 forall (x : A)，cast A eq_refl x = x，这可通过反身性证明。

理解为什么这是不可证明的一种方法是接受假设公理 bool_eq_not : bool = bool 使得 cast bool bool_eq_not x = not x。在 castLemma0 中为 prf 插入 bool_eq_not 会暗示 not x = x，这肯定是错误的。

证明这是可能的，需要演示一个类型理论模型，其中 bool_eq_nat 是可构造的。这首先在 Martin Hofmann 和 Thomas Streicher 的论文“类型理论的群解释”中完成。此后出现了其他几个模型，包括 Voevodsky 的单纯集合模型，以及立方集合中的几个构造模型。这些研究是同伦类型理论(HoTT)领域的一个方面。

---

附带说明一下，最近添加了一个(仍处于试验阶段)功能SProp (documentation)如果您还 Set Definitional UIP 可以证明这一点。