Functions and assumptions¶
Binders¶
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 fun
, forall
, fix
and 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 _
. When the type of a bound variable cannot be synthesized by the
system, it can be specified with the notation (ident : type)
. There is also
a notation for a sequence of binding variables sharing the same type:
(ident+ : type)
. A
binder can also be any pattern prefixed by a quote, e.g. '(x,y)
.
Some constructions allow the binding of a variable to value. This is
called a “let-binder”. The entry binder
of the grammar accepts
either an assumption binder as defined above or a let-binder. The notation in
the latter case is (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:
(ident : type := term)
.
Lists of binder
s are allowed. In the case of fun
and 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.:
fun (x y z : A) => t
can be shortened in fun x y z : A => t
).
Functions (fun) and function types (forall)¶
term_forall_or_fun::=
forall open_binders , type
|
fun open_binders => term
The expression fun ident : type => term
defines the
abstraction of the variable ident
, of type type
, over the term
term
. It denotes a function of the variable ident
that evaluates to
the expression term
(e.g. fun x : A => x
denotes the identity
function on type A
). The keyword fun
can be followed by several
binders as given in Section Binders. Functions over
several variables are equivalent to an iteration of one-variable
functions. For instance the expression
fun identi+ : type => term
denotes the same function as fun identi : type =>+ term
. If
a let-binder occurs in
the list of binders, it is expanded to a let-in definition (see
Section Let-in definitions).
The expression forall ident : type1, type2
denotes the
product type (or product) of the variable ident
of
type type1
over the type type2
. If ident
is used in
type2
, then we say the expression is a dependent product.
The intention behind a dependent product
forall x : A, B
is twofold. It denotes either
the universal quantification of the variable x
of type A
in the proposition B
or the functional dependent product from
A
to B
(a construction usually written
\(\Pi_{x:A}.B\) in set theory).
Non-dependent product types have a special notation: A -> B
stands for
forall _ : A, B
. Non-dependent product is used to denote both
propositional implication and function types.
These terms are also useful:
n : nat
is a dependent premise offorall n:nat, n + 0 = n
becausen
appears both in the binder of theforall
and in the quantified statementn + 0 = n
.A
andB
are non-dependent premises (or, often, just "premises") ofA -> B -> C
because they don't appear in aforall
binder.C
is the conclusion of the type, which is a second meaning for the term conclusion. (As noted,A -> B
is notation for the termforall _ : A, B
; the wildcard_
can't be referred to in the quantified statement.)
As for abstractions, forall
is followed by a binder list, and products
over several variables are equivalent to an iteration of one-variable
products.
Function application¶
term_application::=
term1 arg+
|
@ qualid_annotated term1+
arg::=
( ident := term )
|
( natural := term )
|
term1
term1fun term1
denotes applying the function term1fun
to term1
.
term1fun term1i+
denotes applying
term1fun
to the arguments term1i
. It is
equivalent to ( … ( term1fun term11 ) … ) term1n
:
associativity is to the left.
The @ qualid_annotated term1+
form requires specifying all arguments,
including implicit ones. Otherwise, implicit arguments need
not be given. See Implicit arguments.
The notations (ident := term)
and (natural := term)
for arguments are used for making explicit the value of implicit arguments.
See Explicit applications.
Assumptions¶
Assumptions extend the global environment with axioms, parameters, hypotheses
or variables. An assumption binds an ident
to a type
. It is accepted
by Coq only if type
is a correct type in the global environment
before the declaration and if ident
was not previously defined in
the same module. This type
is considered to be the type (or
specification, or statement) assumed by ident
and we say that ident
has type type
.
-
Command
assumption_token Inline ( natural )?? ( assumpt )+assumpt
¶ - assumption_token
::=
AxiomAxioms|
ConjectureConjectures|
ParameterParameters|
HypothesisHypotheses|
VariableVariablesassumpt
::=
ident_decl+ of_typeident_decl
::=
ident univ_decl?of_type
::=
::> typeThese commands bind one or more
ident
(s) to specifiedtype
(s) as their specifications in the global environment. The fact asserted bytype
(or, equivalently, the existence of an object of this type) is accepted as a postulate. They accept theprogram
attribute.Axiom
,Conjecture
,Parameter
and their plural forms are equivalent. They can take thelocal
attribute, which makes the definedident
s accessible byImport
and its variants only through their fully qualified names.Similarly,
Hypothesis
,Variable
and their plural forms are equivalent. Outside of a section, these are equivalent toLocal Parameter
. Inside a section, theident
s defined are only accessible within the section. When the current section is closed, theident
(s) become undefined and every object depending on them will be explicitly parameterized (i.e., the variables are discharged). See Section Section mechanism.:>
If specified,
ident_decl
is automatically declared as a coercion to the class of its type. See Implicit Coercions.
The
Inline
clause is only relevant inside functors. SeeModule
.
Example: Simple assumptions
- Parameter X Y : Set.
- X is declared Y is declared
- Parameter (R : X -> Y -> Prop) (S : Y -> X -> Prop).
- R is declared S is declared
- Axiom R_S_inv : forall x y, R x y <-> S y x.
- R_S_inv is declared
-
Warning
ident is declared as a local axiom
¶ Warning generated when using
Variable
or its equivalent instead ofLocal Parameter
or its equivalent.
Note
We advise using the commands Axiom
, Conjecture
and
Hypothesis
(and their plural forms) for logical postulates (i.e. when
the assertion type
is of sort Prop
), and to use the commands
Parameter
and Variable
(and their plural forms) in other cases
(corresponding to the declaration of an abstract object of the given type).