将策略应用于前提而不是目标

Question

如果目标状态是这样的：

  a : Prop
  b : Prop
  H1 : a
  H2 : b -> c
  ============================
   c

然后我可以使用apply H2策略将其转换为以下状态：

  a : Prop
  b : Prop
  H1 : a
  H2 : b -> c
  ============================
   b

现在，我想做同样的事情，但是对于假设：

  a : Prop
  b : Prop
  H1 : a
  H2 : b -> a
  ============================
   b

我想引入一个新假设（或简化现有假设），这样我就有了一个新的 H3 : b 前提。这可能吗？

我尝试了 apply 的各种变体，但一切都会导致某种错误。进入上述状态的代码：

Lemma test : forall {a b : Prop},
    a /\ (b -> a) -> b.
Proof.
  intros a b.
  intros [H1 H2].
Abort.

Answer 1

这是不可能的，因为你的 test 引理不成立。例如，将 a 设为 True，将 b 设为 False。两个前提（a 和 b -> a）都成立，但 b 不成立。

但是，如果您对结果的陈述稍作更改，这会奏效：

Lemma test : forall a b : Prop, a /\ (a -> b) -> b.
Proof. intros [H1 H2]. apply H2 in H1. exact H1. Qed.

Applying apply tactic to premises instead of the goal