Functions and assumptions¶
Binders¶
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)¶
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 : type, term
denotes the
product of the variable ident
of type type
, over the term term
.
As for abstractions, forall
is followed by a binder list, and products
over several variables are equivalent to an iteration of one-variable
products. Note that term
is intended to be a type.
If the variable ident
occurs in term
, the product is called
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
. The non dependent product is used both to denote
the propositional implication and function types.
Function application¶
termfun term
denotes applying the function termfun
to term
.
termfun termi+
denotes applying
termfun
to the arguments termi
. It is
equivalent to ( … ( termfun term1 ) … ) termn
:
associativity is to the left.
The notation (ident := term)
for arguments is used for making
explicit the value of implicit arguments (see
Section Explicit applications).
Assumptions¶
Assumptions extend the environment with axioms, parameters, hypotheses
or variables. An assumption binds an ident
to a type
. It is accepted
by Coq if and only if this type
is a correct type in the environment
preexisting 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 ( num )?? ( assumpt )+assumpt
¶ - |ConjectureConjectures|ParameterParameters|HypothesisHypotheses|VariableVariables
These commands bind one or more
ident
(s) to specifiedtype
(s) as their specifications in the global context. 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).