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
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
|
Functions and assumptions
=========================
.. _binders:
Binders
-------
.. insertprodn open_binders binder
.. prodn::
open_binders ::= {+ @name } : @type
| {+ @binder }
name ::= _
| @ident
binder ::= @name
| ( {+ @name } : @type )
| ( @name {? : @type } := @term )
| @implicit_binders
| @generalizing_binder
| ( @name : @type %| @term )
| ' @pattern0
Various constructions such as :g:`fun`, :g:`forall`, :g:`fix` and :g:`cofix`
*bind* variables. A binding is represented by an identifier. If the binding
variable is not used in the expression, the identifier can be replaced by the
symbol :g:`_`. When the type of a bound variable cannot be synthesized by the
system, it can be specified with the notation :n:`(@ident : @type)`. There is also
a notation for a sequence of binding variables sharing the same type:
:n:`({+ @ident} : @type)`. A
binder can also be any pattern prefixed by a quote, e.g. :g:`'(x,y)`.
Some constructions allow the binding of a variable to value. This is
called a “let-binder”. The entry :n:`@binder` of the grammar accepts
either an assumption binder as defined above or a let-binder. The notation in
the latter case is :n:`(@ident := @term)`. In a let-binder, only one
variable can be introduced at the same time. It is also possible to give
the type of the variable as follows:
:n:`(@ident : @type := @term)`.
Lists of :n:`@binder`\s are allowed. In the case of :g:`fun` and :g:`forall`,
it is intended that at least one binder of the list is an assumption otherwise
fun and forall gets identical. Moreover, parentheses can be omitted in
the case of a single sequence of bindings sharing the same type (e.g.:
:g:`fun (x y z : A) => t` can be shortened in :g:`fun x y z : A => t`).
.. index:: fun
.. index:: forall
Functions (fun) and function types (forall)
-------------------------------------------
.. insertprodn term_forall_or_fun term_forall_or_fun
.. prodn::
term_forall_or_fun ::= forall @open_binders , @term
| fun @open_binders => @term
The expression :n:`fun @ident : @type => @term` defines the
*abstraction* of the variable :n:`@ident`, of type :n:`@type`, over the term
:n:`@term`. It denotes a function of the variable :n:`@ident` that evaluates to
the expression :n:`@term` (e.g. :g:`fun x : A => x` denotes the identity
function on type :g:`A`). The keyword :g:`fun` can be followed by several
binders as given in Section :ref:`binders`. Functions over
several variables are equivalent to an iteration of one-variable
functions. For instance the expression
:n:`fun {+ @ident__i } : @type => @term`
denotes the same function as :n:`{+ fun @ident__i : @type => } @term`. If
a let-binder occurs in
the list of binders, it is expanded to a let-in definition (see
Section :ref:`let-in`).
The expression :n:`forall @ident : @type, @term` denotes the
*product* of the variable :n:`@ident` of type :n:`@type`, over the term :n:`@term`.
As for abstractions, :g:`forall` is followed by a binder list, and products
over several variables are equivalent to an iteration of one-variable
products. Note that :n:`@term` is intended to be a type.
If the variable :n:`@ident` occurs in :n:`@term`, the product is called
*dependent product*. The intention behind a dependent product
:g:`forall x : A, B` is twofold. It denotes either
the universal quantification of the variable :g:`x` of type :g:`A`
in the proposition :g:`B` or the functional dependent product from
:g:`A` to :g:`B` (a construction usually written
:math:`\Pi_{x:A}.B` in set theory).
Non dependent product types have a special notation: :g:`A -> B` stands for
:g:`forall _ : A, B`. The *non dependent product* is used both to denote
the propositional implication and function types.
Function application
--------------------
.. insertprodn term_application arg
.. prodn::
term_application ::= @term1 {+ @arg }
| @ @qualid_annotated {+ @term1 }
arg ::= ( @ident := @term )
| @term1
:n:`@term__fun @term` denotes applying the function :n:`@term__fun` to :token:`term`.
:n:`@term__fun {+ @term__i }` denotes applying
:n:`@term__fun` to the arguments :n:`@term__i`. It is
equivalent to :n:`( … ( @term__fun @term__1 ) … ) @term__n`:
associativity is to the left.
The notation :n:`(@ident := @term)` for arguments is used for making
explicit the value of implicit arguments (see
Section :ref:`explicit-applications`).
.. _gallina-assumptions:
Assumptions
-----------
Assumptions extend the global environment with axioms, parameters, hypotheses
or variables. An assumption binds an :n:`@ident` to a :n:`@type`. It is accepted
by Coq only if :n:`@type` is a correct type in the global environment
before the declaration and if :n:`@ident` was not previously defined in
the same module. This :n:`@type` is considered to be the type (or
specification, or statement) assumed by :n:`@ident` and we say that :n:`@ident`
has type :n:`@type`.
.. _Axiom:
.. cmd:: @assumption_token {? Inline {? ( @natural ) } } {| {+ ( @assumpt ) } | @assumpt }
:name: Axiom; Axioms; Conjecture; Conjectures; Hypothesis; Hypotheses; Parameter; Parameters; Variable; Variables
.. insertprodn assumption_token of_type
.. prodn::
assumption_token ::= {| Axiom | Axioms }
| {| Conjecture | Conjectures }
| {| Parameter | Parameters }
| {| Hypothesis | Hypotheses }
| {| Variable | Variables }
assumpt ::= {+ @ident_decl } @of_type
ident_decl ::= @ident {? @univ_decl }
of_type ::= {| : | :> } @type
These commands bind one or more :n:`@ident`\(s) to specified :n:`@type`\(s) as their specifications in
the global environment. The fact asserted by :n:`@type` (or, equivalently, the existence
of an object of this type) is accepted as a postulate. They accept the :attr:`program` attribute.
:cmd:`Axiom`, :cmd:`Conjecture`, :cmd:`Parameter` and their plural forms
are equivalent. They can take the :attr:`local` :term:`attribute`,
which makes the defined :n:`@ident`\s accessible by :cmd:`Import` and its variants
only through their fully qualified names.
Similarly, :cmd:`Hypothesis`, :cmd:`Variable` and their plural forms are equivalent. Outside
of a section, these are equivalent to :n:`Local Parameter`. Inside a section, the
:n:`@ident`\s defined are only accessible within the section. When the current section
is closed, the :n:`@ident`\(s) become undefined and every object depending on them will be explicitly
parameterized (i.e., the variables are *discharged*). See Section :ref:`section-mechanism`.
:n:`:>`
If specified, :token:`ident_decl` is automatically
declared as a coercion to the class of its type. See :ref:`coercions`.
The :n:`Inline` clause is only relevant inside functors. See :cmd:`Module`.
.. example:: Simple assumptions
.. coqtop:: reset in
Parameter X Y : Set.
Parameter (R : X -> Y -> Prop) (S : Y -> X -> Prop).
Axiom R_S_inv : forall x y, R x y <-> S y x.
.. exn:: @ident already exists.
:name: ‘ident’ already exists. (Axiom)
:undocumented:
.. warn:: @ident is declared as a local axiom
Warning generated when using :cmd:`Variable` or its equivalent
instead of :n:`Local Parameter` or its equivalent.
.. note::
We advise using the commands :cmd:`Axiom`, :cmd:`Conjecture` and
:cmd:`Hypothesis` (and their plural forms) for logical postulates (i.e. when
the assertion :n:`@type` is of sort :g:`Prop`), and to use the commands
:cmd:`Parameter` and :cmd:`Variable` (and their plural forms) in other cases
(corresponding to the declaration of an abstract object of the given type).
|
