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.
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.