Generalizing a hypothesis when possible

Question

Suppose I have a goal of the form

forall x, A x -> B x -> P

where x does not occur free in P (the bound x is not involved in the conclusion). By doing intros here, I will get three separate hypotheses in my proof:

x : nat
H0 : A x
H1 : B x
===============
P

But I need to strengthen my hypotheses and get the following.

H0 : forall x, A x -> B x
===============
P

so that I can instantiate x to whatever I need.

Since x does not occur in P, it is logically valid to have

(forall x, A x -> B x -> P) -> ((forall x, A x -> B x) -> P)

My question is, how can I do this in Coq?

Answer 1

As Anton pointed out, we need some more context to understand what you are trying to do. Nevertheless, here are some ideas that might help you.

You first asked how to get from a context like this

x  : nat
H1 : A x
H2 : B x

to a context like this

H : forall x' : nat, A x' -> B x'

There is no way of accomplishing that for every A and B, even if you know that A is valid for some number. For instance, suppose that A x means "x is even", and B x means "x is zero"; that is,

A x := exists y, x = 2 * y
B x := x = 0

The only information that the first set of hypotheses gives you is that x is zero. The second set of hypotheses, however, is contradictory, because it asserts that every even number is equal to zero. Since you cannot add contradictory hypotheses from consistent ones, you cannot go from the first context to the second.

There are, of course, other cases where going from one context to the other is possible: if you manage to prove forall x', A x' -> B x' assuming that A x and B x hold for some x. For this, you need the assert tactic. If you execute

assert (H : forall x', A x' -> B x').

Coq will generate two subgoals: one where you have to prove forall x', A x' -> B x' given your previous hypotheses, and another one where the context gets a new hypothesis H : forall x', A x' -> B x'.