How to break up an implication into two subgoals in Coq?

Question

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:

• One to prove the premise of H.
• One to prove the same goal I already had, given the conclusion of H as a new hypothesis. And I want to do this without explicitly typing out the premise of H.

Answer 1

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 product A -> B with B possibly containing products. Then it generates two subgoals B->G and A. Applying lapply H (where H has type A->B and B does not start with a product) does the same as giving the sequence cut B. 2:apply H. where cut 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.