大佬教程收集整理的这篇文章主要介绍了删除 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）。不幸的是，这使得这个特殊的证明相当循环。不过，我会留下这个答案，以防其他人觉得它有用。
还值得注意的是，如果您想从属地销毁一个表达式@H_674_86@，而不仅仅是一个标识符，那么这种策略及其相关性就不再适用了。我实际上不知道这个问题的解决方案，或者即使有一个一般的解决方案。 （要与比我知识渊博的人进行更深入的讨论，请参阅 https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/.60dependent.20destruction.60.20of.20expressions/near/209916250。）
以上是大佬教程为你收集整理的删除 Coq 中的琐碎匹配子句全部内容，希望文章能够帮你解决删除 Coq 中的琐碎匹配子句所遇到的程序开发问题。
如果觉得大佬教程网站内容还不错，欢迎将大佬教程推荐给程序员好友。
本图文内容来源于网友网络收集整理提供，作为学习参考使用，版权属于原作者。
如您有任何意见或建议可联系处理。小编QQ：384754419，请注明来意。