\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#3})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

Existential variables

Existential variables represent as yet unknown values.

term_evar::=_|?[ ident ]|?[ ?ident ]|?ident @{ ident := term+; }?

Coq terms can include existential variables that represent unknown subterms that are eventually replaced with actual subterms.

Existential variables are generated in place of unsolved implicit arguments or “_” placeholders when using commands such as Check (see Section Requests to the environment) or when using tactics such as refine, as well as in place of unsolved instances when using tactics such that eapply. An existential variable is defined in a context, which is the context of variables of the placeholder which generated the existential variable, and a type, which is the expected type of the placeholder.

As a consequence of typing constraints, existential variables can be duplicated in such a way that they possibly appear in different contexts than their defining context. Thus, any occurrence of a given existential variable comes with an instance of its original context. In the simple case, when an existential variable denotes the placeholder which generated it, or is used in the same context as the one in which it was generated, the context is not displayed and the existential variable is represented by “?” followed by an identifier.

Parameter identity : forall (X:Set), X -> X.
identity is declared
Check identity _ _.
identity ?X ?y : ?X where ?X : [ |- Set] ?y : [ |- ?X]
Check identity _ (fun x => _).
identity (forall x : ?S, ?S0) (fun x : ?S => ?y) : forall x : ?S, ?S0 where ?S : [ |- Set] ?S0 : [x : ?S |- Set] ?y : [x : ?S |- ?S0]

In the general case, when an existential variable ?ident appears outside its context of definition, its instance, written in the form { ident := term*; }, is appended to its name, indicating how the variables of its defining context are instantiated. Only the variables that are defined in another context are displayed: this is why an existential variable used in the same context as its context of definition is written with no instance. This behavior may be changed: see Explicit display of existential instances for pretty-printing.

Check (fun x y => _) 0 1.
(fun x y : nat => ?y) 0 1 : ?T@{x:=0; y:=1} where ?T : [x : nat y : nat |- Type] ?y : [x : nat y : nat |- ?T]

Existential variables can be named by the user upon creation using the syntax ?[ident]. This is useful when the existential variable needs to be explicitly handled later in the script (e.g. with a named-goal selector, see Goal selectors).

Inferable subterms

Expressions often contain redundant pieces of information. Subterms that can be automatically inferred by Coq can be replaced by the symbol _ and Coq will guess the missing piece of information.

e* tactics that can create existential variables

A number of tactics have companion tactics that create existential variables when the base tactic would fail because of uninstantiated variables. The companion tactic names begin with an e followed by the name of the base tactic. For example, eapply works the same way as apply, except that it will create new existential variable(s) when apply would fail.

Example: apply vs eapply

Both tactics unify the goal with n < p in the theorem. m is unspecified. This makes apply fail, while eapply creates a new existential variable ?m.

Require Import Arith.
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Goal forall i j, i < j.
1 goal ============================ forall i j : nat, i < j
intros.
1 goal i, j : nat ============================ i < j
(* Theorem lt_trans : forall n m p, n < m -> m < p -> n < p. *)
Fail apply Nat.lt_trans.
The command has indeed failed with message: Unable to find an instance for the variable m.
eapply Nat.lt_trans.
2 focused goals (shelved: 1) i, j : nat ============================ i < ?m goal 2 is: ?m < j

The e* tactics include:

Note that eassumption and eauto behave differently from the others.

Automatic resolution of existential variables

Existential variables that are used in other goals are generally resolved automatically as a side effect of other tactics.

Example: Automatic resolution of existential variables

?x and ?m are used in other goals. The exact shown below determines the values of these variables by unification, which resolves them.

Require Import Arith.
Set Printing Goal Names.
Goal forall n m, n <= m -> ~ m < n.
1 goal (?Goal) ============================ forall n m : nat, n <= m -> ~ m < n
intros x y H1 H2.
1 goal (?Goal) x, y : nat H1 : x <= y H2 : y < x ============================ False
eapply Nat.lt_irrefl. (* creates ?x : nat as a shelved goal *)
1 focused goal (shelved: 1) (?Goal) x, y : nat H1 : x <= y H2 : y < x ============================ ?x < ?x
eapply Nat.le_lt_trans. (* creates ?m : nat as a shelved goal *)
2 focused goals (shelved: 2), goal 1 (?Goal) x, y : nat H1 : x <= y H2 : y < x ============================ ?x <= ?m goal 2 (?Goal0) is: ?m < ?x
Unshelve. (* moves the shelved goals into focus--not needed and usually not done *)
4 goals, goal 1 (?Goal) x, y : nat H1 : x <= y H2 : y < x ============================ ?x <= ?m goal 2 (?Goal0) is: ?m < ?x goal 3 (?x) is: nat goal 4 (?m) is: nat
exact H1. (* resolves the first goal and by side effect ?x and ?m *)
1 goal (?Goal) x, y : nat H1 : x <= y H2 : y < x ============================ y < x

The ?x and ?m goals ask for proof that nat has an inhabitant, i.e. it is not an empty type. This can be proved directly by applying a constructor of nat, which assigns values for ?x and ?m. However if you choose poorly, you can end up with unprovable goals (in this case 0 < 0). Like this:

Require Import Arith.
Set Printing Goal Names.
Goal forall n m, n <= m -> ~ m < n.
1 goal (?Goal) ============================ forall n m : nat, n <= m -> ~ m < n
intros x y H1 H2.
1 goal (?Goal) x, y : nat H1 : x <= y H2 : y < x ============================ False
eapply Nat.lt_irrefl. (* creates ?x : nat as a shelved goal *)
1 focused goal (shelved: 1) (?Goal) x, y : nat H1 : x <= y H2 : y < x ============================ ?x < ?x
eapply Nat.le_lt_trans. (* creates ?m : nat as a shelved goal *)
2 focused goals (shelved: 2), goal 1 (?Goal) x, y : nat H1 : x <= y H2 : y < x ============================ ?x <= ?m goal 2 (?Goal0) is: ?m < ?x
Unshelve. (* moves the shelved goals into focus--not needed and usually not done *)
4 goals, goal 1 (?Goal) x, y : nat H1 : x <= y H2 : y < x ============================ ?x <= ?m goal 2 (?Goal0) is: ?m < ?x goal 3 (?x) is: nat goal 4 (?m) is: nat
3-4: apply 0. (* assigns values to ?x and ?m *)
2 goals, goal 1 (?Goal) x, y : nat H1 : x <= y H2 : y < x ============================ 0 <= 0 goal 2 (?Goal0) is: 0 < 0

Explicit display of existential instances for pretty-printing

Flag Printing Existential Instances

Activates the full display of how the context of an existential variable is instantiated at each of the occurrences of the existential variable. Off by default.

Check (fun x y => _) 0 1.
(fun x0 y0 : nat => ?y@{x0:=x; y0:=y; x:=x0; y:=y0}) 0 1 : ?T@{x0:=x; y0:=y; x:=0; y:=1} where ?T : [x0 : nat y0 : nat H1 : x0 <= y0 H2 : y0 < x0 x : nat y : nat |- Type] ?y : [x0 : nat y0 : nat H1 : x0 <= y0 H2 : y0 < x0 x : nat y : nat |- ?T]
Set Printing Existential Instances.
Check (fun x y => _) 0 1.
(fun x0 y0 : nat => ?y@{x0:=x; y0:=y; H1:=H1; H2:=H2; x:=x0; y:=y0}) 0 1 : ?T@{x0:=x; y0:=y; H1:=H1; H2:=H2; x:=0; y:=1} where ?T : [x0 : nat y0 : nat H1 : x0 <= y0 H2 : y0 < x0 x : nat y : nat |- Type] ?y : [x0 : nat y0 : nat H1 : x0 <= y0 H2 : y0 < x0 x : nat y : nat |- ?T@{x0:=x0; y0:=y0; H1:=H1; H2:=H2; x:=x; y:=y}]

Solving existential variables using tactics

Instead of letting the unification engine try to solve an existential variable by itself, one can also provide an explicit hole together with a tactic to solve it. Using the syntax ltac:(tacexpr), the user can put a tactic anywhere a term is expected. The order of resolution is not specified and is implementation-dependent. The inner tactic may use any variable defined in its scope, including repeated alternations between variables introduced by term binding as well as those introduced by tactic binding. The expression tacexpr can be any tactic expression as described in Ltac.

Definition foo (x : nat) : nat := ltac:(exact x).
foo is defined

This construction is useful when one wants to define complicated terms using highly automated tactics without resorting to writing the proof-term by means of the interactive proof engine.