How do I read the definition of ex_intro?

Question

I'm reading Mike Nahas's introductory Coq tutorial, which says:

The arguments to "ex_intro" are:

• the predicate
• the witness
• a proof of the predicated called with the witness

I looked at the definition:

Inductive ex (A:Type) (P:A -> Prop) : Prop :=
  ex_intro : forall x:A, P x -> ex (A:=A) P.

and I'm having trouble parsing it. Which parts of the expression forall x:A, P x -> ex (A:=A) P correspond to those three arguments (predicate, witness, and proof)?

Answer 1

To understand what Mike meant, it's better to launch the Coq interpreter and query for the type of ex_intro:

Check ex_intro.

You should then see:

ex_intro
     : forall (A : Type) (P : A -> Prop) (x : A), P x -> exists x, P x

This says that ex_intro takes not only 3, but 4 arguments:

• the type of the thing you're quantifying over, A;
• the predicate P : A -> Prop;
• the witness x : A; and
• a proof of P x, asserting that x is a valid witness.

If you combine all of those things, you get a proof of exists x : A, P x. For example, @ex_intro nat (fun n => n = 3) 3 eq_refl is a proof of exists n, n = 3.

Thus, the difference between the actual type of ex_intro and the one you read on the definition is that the former includes all of the parameters that are given in the header -- in this case, A and P.