删除 Coq 中的琐碎匹配子句

问题描述

考虑以下示例：

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".

有没有办法去掉这个匹配子句？

解决方法

如果不假设额外的公理，通常是 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_not 中为 prf 插入 castLemma0 意味着 not x = x，这肯定是错误的。

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

顺便提一下，最近添加了一个（仍然是实验性的）功能 SProp (documentation)，如果您还 Set Definitional UIP 可以证明这一点。

因为 prf 是一个标识符，dependent destruction 策略（来自 Coq.Program.Equality）可以处理由 convoy 模式引入的对 prf0 的依赖。例如：

Require Import Coq.Program.Equality.

Lemma castLemma0 {A : Set} : forall (x : A) prf,cast prf x = x.
Proof.
  intros.
  compute.
  dependent destruction prf.
  reflexivity.
Qed.

（不过，我不知道 dependent destruction 是否依赖于任何新的公理，但也许其他人可以帮助澄清。）更新： OP 发现它使用eq_rect_eq（≣ 依赖等式的注入性 ≣ 身份证明的唯一性 ≣ 自反身份证明的唯一性 ≣ 公理 K，根据 Coq.Logic.EqdepFacts）。不幸的是，这使得这个特殊的证明相当循环。不过，我会留下这个答案，以防其他人觉得它有用。

还值得注意的是，如果您想从属地销毁一个表达式，而不仅仅是一个标识符，那么这种策略及其相关性就不再适用了。我实际上不知道这个问题的解决方案，或者即使有一个一般的解决方案。（要与比我知识渊博的人进行更深入的讨论，请参阅 https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/.60dependent.20destruction.60.20of.20expressions/near/209916250。）

coq pattern-matching