coqcoq-tacticimplication

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


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:


Solution

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