Say I have the following:
Lemma my_lemma :
forall a b c,
a -> (b -> c) -> d.
Proof.
intros.
Then, above the line, I get:
X : a
X0 : b -> c
Let's say that in my proof, I know I'm going to need c
somewhere. And I know how to prove b
from a
, but it's not very easy. One possibility is:
assert b.
+ (* proof of b here *)
+ (* proof using c here *)
In this simple case, that's quite painless. However, I want to achieve the same effect without specifying b
, because I often have hypotheses with more complicated premises that I don't want to type out explicitly in assert
.
pose
doesn't do what I want because it requires me to prove a
first, so automation tactics don't work as well because they don't know that I'm trying to prove a
. apply
doesn't do what I want either because it requires me to turn my goal into the same form as the implication first, which also doesn't play nice with automation tactics.
In summary, I want to be able to take a hypothesis H
that's an implication, and get two subgoals:
H
.H
as a new hypothesis.
And I want to do this without explicitly typing out the premise of H
.I think lapply
gets closest to the desired behaviour:
Variant
lapply <term>
This tactic applies to any goal, say
G
. The argument term has to be well-formed in the current context, its type being reducible to a non-dependent productA -> B
withB
possibly containing products. Then it generates two subgoalsB->G
andA
. Applyinglapply H
(whereH
has typeA->B
andB
does not start with a product) does the same as giving the sequencecut B. 2:apply H.
wherecut
is described below.
In your example, we get:
Lemma my_lemma :
forall a b c d,
a -> (b -> c) -> d.
Proof.
intros.
lapply X0.
+ intro.
(* prove d using c *)
admit.
+ (* prove b *)
admit.
Admitted.