Applying apply tactic to premises instead of the goal

Question

If the goal state is like this:

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

Then I can convert it to the following state using apply H2 tactic:

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

Now, I want to do the same but for hypothesis:

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

I want to introduce a new hypothesis(or simplify the existing hypothesis) such that I have a new H3 : b in premises. Is that possible ?

I tried various variations of apply but everything is leading to some kind of error. Code for bringing up to the above state:

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

Arthur Azevedo De Amorim Arthur Azevedo De Amorim · Accepted Answer · 2017-04-14T01:34:37

This is not possible, because your test lemma does not hold. For instance, take a to be True and b to be False. Both premises (a and b -> a) hold, yet b does not hold.

This would work, however, if you changed the statement of your result a little:

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

1 Answers