在 Coq 中，有没有一种方法可以方便地证明假设的前提？答案

【问题标题】：In Coq, is there a way to prove a premise of a hypothesis conveniently?在 Coq 中，有没有一种方法可以方便地证明假设的前提？
【发布时间】：2022-04-27 03:12:28
【问题描述】：

我的证明上下文中有H : P -> Q，我需要Q 来完成我的证明，但我没有任何P 的证据：

有没有什么战术或者其他可以将前提 P 设为新目标，然后将 P -> Q 替换为 Q 在目标P 被证明之后。那我就可以直接用Q来证明原来的目的了。

不过，我也可以使用assert (HP : P) 然后用(H HP)得到一个Q，但是我必须手动复制P，不方便（特别是当P很长，而H : P -> Q还在的时候）。

我读了this，但没有任何用处，也许我错过了。

【问题讨论】：

标签： coq

【解决方案1】：

我认为您正在寻找的是策略apply。

【讨论】：

【解决方案2】：

我同意 Pierre Jouvelot 的观点，即您正在寻找 apply 策略（我邀请您接受他的回答）。为了补充这个答案，我将提出一些更接近前向推理的东西，正如你的问题所暗示的那样。

您不需要了解以下内容，但它定义了一个 forward 策略，可以满足您的需求：

Ltac forward_gen H tac :=
  match type of H with
  | ?X → _ => let H' := fresh in assert (H':X) ; [tac|specialize (H H'); clear H']
  end.

Tactic Notation "forward" constr(H) := forward_gen H ltac:(idtac).
Tactic Notation "forward" constr(H) "by" tactic(tac) := forward_gen H tac.

然后您可以应用forward H 为P 生成目标。在原始目标中，H : P -> Q 被 H : Q 替换。

【讨论】：