Search code examples
coq

Introducing a new assumption/hypothesis by adding it as subgoal

Let's suppose that I have the following proof state:

1 subgoal
P, Q : Prop
H : P -> Q
-------------------(1/1)
Q

and I know a way to prove P, how may I add an "inline proof" of it so that I can have it in my list of assumptions?

Solution

  • The tactic assert does exactly that.

    Using assert (<proposition>) breaks your objective into two subgoals, in the first you have to prove "<proposition>" with your current assumptions, and the second has your original goal as the objective, but with "<proposition>" added to the list of assumptions.

    You may also specify its name with assert (<proposition>) as <name> or assert (<name>: <proposition>).

    Another option is to use cut (<proposition>).

    It also creates two objectives, one of the form <proposition> -> <your objective> (then you can get your hypothesis by using intros, or intros <name> if you want to specify its name), and another one in which you have to prove "<prososition>" with your current assumptions.