删除 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

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

如果限制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。插入bool_eq_notfor prfincastLemma0就意味着not x = x，这肯定是错误的。

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

作为旁注，有一个最近添加的（并且仍然是实验性的）功能SProp（文档），如果您也Set Definitional UIP让您证明这一点。