在COQ中，有没有办法方便地证明假设的前提？

Question

我有h：p - ＆gt; q在我的证明上下文中，我需要q完成我的证明，但是我没有任何p：

是否有策略或其他任何可以 使前提p一个新目标，然后替换p - ＆gt; Q带有q 在证明目标p之后。 然后，我可以直接使用Q来证明原始目标。

但是，我也可以使用断言（HP：P） 然后使用（HP）获取Q，但是我必须手动复制p，这是不便的（尤其是当> 时p是长的，h：p - ＆gt; q仍然存在）。

我阅读 this 那。

Answer 1

我认为您正在寻找的是Tactic 应用。

Answer 2

我同意Pierre Jouvelot的观点，您正在寻找应用 tactic（我邀请您接受他的答案）。为了补充这个答案，我将在您的问题所暗示的那样提出一些更接近前进的推理。

您不需要了解以下内容，但它定义了执行您想要的 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 - ＆gt; Q被h：q取代。