2.6 Implicit arguments
The Coq system allows to skip during a function application certain
arguments that can be automatically inferred from the other
arguments. Such arguments are called implicit. Typical implicit
arguments are the type arguments in polymorphic functions.
The user can force a subterm to be guessed by replacing it by
?. If possible, the correct subterm will be automatically generated.
Error message:
-
There is an unknown subterm I cannot solve
Coq was not able to deduce an instantiation of a ``?''.
In addition, there are two ways to systematically avoid to write
``?'' where a term can be automatically inferred.
The first mode is automatic. Switching to this mode forces some
easy-to-infer subterms to always be implicit.
The command to use the second mode is Syntactic
Definition.
2.6.1 Auto-detection of implicit arguments
There is an automatic mode to declare as implicit some arguments of
constants and variables which have a functional type. In this mode,
to every declared object (even inductive types and theirs constructors) is
associated the list of the positions of its implicit arguments. These
implicit arguments correspond to the arguments which can be deduced
from the following ones. Thus when one applies these functions to
arguments, one can omit the implicit ones. They are then automatically
replaced by symbols ``?'', to be inferred by the mechanism of
synthesis of implicit arguments.
Implicit Arguments switch.
If switch is On then the command switches on the automatic
mode. If switch is Off then the command switches off the
automatic mode. The mode Off is the default mode.
The computation of implicit arguments takes account of the
unfolding of constants. For instance, the variable p below has
a type (Transitivity R) which is reducible to (x,y:U)(R x
y) -> (z:U)(R y z) -> (R x z). As the variables x, y and
z appear in the body of the type, they are said implicit; they
correspond respectively to the positions 1, 2 and 4.
Coq < Implicit Arguments On.
Coq < Variable X : Type.
Coq < Definition Relation := X -> X -> Prop.
Coq < Definition Transitivity := [R:Relation]
Coq < (x,y:X)(R x y) -> (z:X)(R y z) -> (R x z).
Coq < Variables R:Relation; p:(Transitivity R).
Coq < Print p.
*** [ p : (Transitivity R) ]
Positions [1;2;4] are implicit
Coq < Variables a,b,c:X; r1:(R a b); r2:(R b c).
Coq < Check (p r1 r2).
(p r1 r2)
: (R a c)
Explicit Applications
The mechanism of synthesis of implicit arguments is not complete, so
we have sometimes to give explicitly certain implicit arguments of an
application. The syntax is i!term where i is the position
of an implicit argument and term is its corresponding explicit
term. The number i is called explicitation number. We can
also give all the arguments of an application, we have then to write
(!ident term1..termn).
Error message:
-
Bad explicitation number
Example:
Coq < Check (p r1 4!c).
(p r1 4!c)
: (R b c)->(R a c)
Coq < Check (!p a b r1 c r2).
(p r1 r2)
: (R a c)
Implicit Arguments and Pretty-Printing
The basic pretty-printing rules hide the implicit arguments of an
application. However an implicit argument term of an application
which is not followed by any explicit argument is printed as follows
i!term where i is its position.
2.6.2 User-defined implicit arguments: Syntactic definition
The syntactic definitions define syntactic constants, i.e. give a name
to a term possibly untyped but syntactically correct. Their syntax
is:
Syntactic Definition
name :=
term .
Syntactic definitions behave like macros: every occurrence of a
syntactic constant in an expression is immediately replaced by its
body.
Let us extend our functional language with the definition of the
identity function:
Coq < Definition explicit_id := [A:Set][a:A]a.
explicit_id is defined
We declare also a syntactic definition id:
Coq < Syntactic Definition id := (explicit_id ?).
id is now a syntax macro
The term (explicit_id ?) is untyped since the implicit
arguments cannot be synthesized. There is no type check during this
definition. Let us see what happens when we use a syntactic constant
in an expression like in the following example.
Coq < Check (id O).
(explicit_id nat O)
: nat
First the syntactic constant id is replaced by its
body (explicit_id ?) in the expression. Then the resulting
expression is evaluated by the typechecker, which fills in
``?
'' place-holders.
The standard usage of syntactic definitions is to give names to terms
applied to implicit arguments ``?
''. In this case, a special
command is provided:
Syntactic Definition
name :=
term |
n .
The body of the syntactic constant is term applied to n
place-holders ``?
''.
We can define a new syntactic definition id1 for explicit_id using this command. We changed the name of the
syntactic constant in order to avoid a name conflict with id.
Coq < Syntactic Definition id1 := explicit_id | 1.
id1 is now a syntax macro
The new syntactic constant id1 has the same behavior as id:
Coq < Check (id1 O).
(explicit_id nat O)
: nat
Warnings:
-
Syntactic constants defined inside a section are no longer
available after closing the section.
- You cannot see the body of a syntactic constant with a Print command.