Search code examples
coq

Disjunction and the error `No product after head reduction'

In CoqIde I entered the following code:

Theorem or_left : P -> P \/ Q.

Proof.
intros S V S_holds.

This produces the error No product even after head-reduction. What is the problem and what does this mean?

Solution

  • It means that you are trying to introduce too many things with intros. Your goal is P -> (P \/ Q) (I added the parentheses for clarity). Thus, there is only one assumption to introduce, not three.

    Possibly what happened is that you expect to introduce a name for P, a name for Q, and a name for the assumption that P holds, but in your theorem statement you are using previously defined P and Q, so there is no need to introduce names for them. In fact, if you paste your example to a fresh file you will get a different error:

    Error: The reference P was not found in the current environment.

    You need something like

    Variables P Q : Prop.

    somewhere in your context for your code to compile.

    Alternatively, you can write

    Theorem or_left : forall (P Q : Prop), P -> P \/ Q.

    or

    Theorem or_left (P Q : Prop) : P -> P \/ Q.

    The former will let you introduce P and Q with different names, while the latter has them already introduced for you.