\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} \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}[4]{\kw{Ind}[#2](#3:=#4)} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} \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{\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

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

Coq terms can include existential variables which represents unknown subterms to eventually be replaced by actual subterms.

Existential variables are generated in place of unsolvable 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 unsolvable 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 of its context of definition, its instance, written under the form { ident := term*; } is appending to its name, indicating how the variables of its defining context are instantiated. The variables of the context of the existential variables which are instantiated by themselves are not written, unless the Printing Existential Instances flag is on (see Section Explicit displaying of existential instances for pretty-printing), and this is why an existential variable used in the same context as its context of definition is written with no instance.

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]

Set Printing Existential Instances.

Check (fun x y => _) 0 1.

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

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.

Explicit displaying of existential instances for pretty-printing

Flag Printing Existential Instances

This flag (off by default) activates the full display of how the context of an existential variable is instantiated at each of the occurrences of the existential variable.

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.