如何破坏 coq 目标中的存在答案

【问题标题】：How to destruct a exist in goal for coq如何破坏 coq 目标中的存在
【发布时间】：2017-01-09 16:58:59
【问题描述】：

这有点笼统，所以请随时询问详细信息，我简化了以使问题更易于沟通。

说我的目标是

let (r,_) := f x in Q r

其中f x 的类型为{u | P u}。

我想“破坏”它，以便拥有Q r 以P r 为假设的目标。实现这一目标的最佳方法是什么？过去，我已经实现了我想要的

pose (f x).

然后简化。

这里有一些简化的代码。

Parameter T:Type.
Parameter P:T -> Prop.

Axiom A : {t:T|P t}.

Definition myvar:T.
  destruct A.
  exact x.
Defined.
Theorem B : P myvar.

【问题讨论】：

看来我完全没有得到你的问题。如果我的回答不是针对真正的问题，您能否更详细地解释您的问题？

标签： coq

【解决方案1】：

unfold myvar; destruct A.

将在这种特殊情况下解决您的目标。

一般来说，destruct 策略可以与任何术语一起使用，它会尝试将术语抽象出来并破坏它。但是请注意，这有时可能会失败，尤其是在使用依赖类型时。

原因是destruct在下面使用了galina match，而在Coq中，如果不仔细，模式匹配可能会丢失一些打字信息，更多信息请搜索“Convoy Pattern”。

【讨论】：

这条评论看起来很傻，但我可以让 coq 推断 A 吗？在我的用例中，A 不是公理而是相当复杂，但类型仍然像我的示例。
当然你可以使用 ltac 的match _ ；或者，您可以使用 set t := pat 为复杂模式使用匹配别名。

【解决方案2】：

如果需要，您可以命名 destruct 策略的“输出”：

(* Stupid definitions to create a minimal example *)
Parameter A: Set.
Parameter P Q: A -> Prop.
Definition f (x: A) : {r | P r }.
Admitted.

Goal (forall x, let (r, _) := f x in Q r).
intro x.
destruct f as [r hr]. (* you goal has now r: A and hr : P r as premises *)
Abort.

编辑：评论后的更多信息。如果您不命名它们，Coq 将使用基于 xi 变量 (x0, x1, ...) 的方案自动为您命名。如果您不关心第二部分的名称，则只能强制命名第一个变量使用destruct f as [r].

【讨论】：

这有什么帮助？如果你没有明确命名它们，Coq 会自动命名它们。
OP 询问他如何在目标中使用Q r，在上下文中使用P r。如果你不命名它们，Coq 确实会命名它们，但使用x0（取决于上下文...）而不是r。我只是在这里回答问题。如果你真的需要，你只能命名第一个，但我通常会命名 destruct 的所有输出或不命名。
我不认为OP的问题是“如何命名destruct生成的前提？”
那我没看懂问题