1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
|
.. extracted from Gallina extensions chapter
.. _existential-variables:
Existential variables
---------------------
:gdef:`Existential variables <existential variable>` represent as yet unknown
values.
.. insertprodn term_evar term_evar
.. prodn::
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 :ref:`requests-to-the-environment`) or when using tactics such as
:tacn:`refine`, as well as in place of unsolved instances when using
tactics such that :tacn:`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.
.. coqtop:: all
Parameter identity : forall (X:Set), X -> X.
Check identity _ _.
Check identity _ (fun x => _).
In the general case, when an existential variable :n:`?@ident` appears
outside its context of definition, its instance, written in the
form :n:`{ {*; @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 :ref:`explicit-display-existentials`.
.. coqtop:: all
Check (fun x y => _) 0 1.
Existential variables can be named by the user upon creation using
the syntax :n:`?[@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 :ref:`goal-selectors`).
.. extracted from Gallina chapter
.. index:: _
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.
.. extracted from Gallina extensions chapter
.. _explicit-display-existentials:
Explicit displaying of existential instances for pretty-printing
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
.. flag:: Printing Existential Instances
This :term:`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.
.. coqtop:: all
Check (fun x y => _) 0 1.
Set Printing Existential Instances.
Check (fun x y => _) 0 1.
.. _tactics-in-terms:
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 :ref:`ltac`.
.. coqtop:: all
Definition foo (x : nat) : nat := ltac:(exact x).
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.
|
