Coq eapply generates a goal with a question mark while proving existence of a function

Question

I would like to prove that for every group there exists a minus function that takes an element of the group and returns its negative.

My Coq code is as follows:

Record Group:Type := {
G:Set;
plus: G->G->G;
O:G;
assoc: forall x y z:G, plus x (plus y z)=plus (plus x y) z;
neut: forall x:G, plus x O=x /\ plus O x=x;
neg: forall x:G, exists y:G, plus x y=O
}.

Lemma minus_exists(H:Group):exists minus_func:G H->G H, (forall x:G H, plus H x (minus_func(x))=O H).
eapply ex_intro.

The last tactic generates the following output:

  H : Group
  ============================
   forall x : G H, plus H x (?12 x) = O H

My first issue is the ?12 which I figure is probably a badly displayed character. What is the meaning of this and is there a way to make it readable.

My second question is how to complete the proof, which might become clearer after the first question is answered.

Answer 1

In my Coq version, I get instead:

forall x : G H, plus H x (?minus_func x) = O H

which is slightly better. In Coq, a term displayed of the form ?T is what we call a "meta" or an "existential variable" (evar).

The terminology comes from the field of logic programming and automated theorem proving, and it could be roughly interpreted as representing "an unknown term". Usually, evars play the role of variables in the unification process. The whole Coq proof engine is built around this notion of unknown or evar.

In your case, eapply ex_intro (or eexists) is missing the witness. Coq will create a new "evar" to stand for the missing function, and allows you to continue your proof. Note however that in order to complete the proof, you will need to provide a witness later on.

How are evars made into actual terms? The act of replacing an evar by an actual term is known as "instantiation". In many cases, instantiation will be performed by the unification algorithm. For instance, if we had a lemma:

Lemma f_plus x : plus H x (f x) = O H

we could do apply f_plus and ?minus_func would be replaced by f. Another way is to use the instantiate tactic, but it is obsolete these days. In our previous case, you could then write instantiate (1 := f) and that would replace ?minus_func by f. Due to technical reasons this approach is not well supported anymore, thus in practice you are bound to either instantiating evars by unification or providing the actual witness to tactics.

I suggest you read a bit more about unification and logic programming.

Answer 2

?12 is not a badly displayed character, it is a hole. The eapply tactics is a kind of "apply this lemma/hypothesis, but I don't have all the input at hand yet, so please insert holes instead, that I will fill later".

By entering eapply ex_intro (or eexists) you are just saying "There exists a function which I don't know yet, so please replace it by a hole, I will provide it later". However since the whole purpose of your lemma is to build this function, I'm not sure you are on the right path. Try proving your lemmas without any efoo tactics, you don't need them.