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.
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. See below.
2.6.1 Implicit arguments: ``?''
When a subterm of a term can be automatically deduced by Coq it can be replaced by ?. This typically occurs when this subterm is the type of another subterm.Error message:
-
unconstrained isevar
Coq was not able to deduce an instantiation of a ``?''.
See also: Section 2.6.3.
2.6.2 Auto-detection of implicit arguments
There is an automatic mode to declare implicit 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.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.X is assumed
Coq < Definition Relation := X -> X -> Prop.Relation is defined
Coq < Definition Transitivity := [R:Relation]Coq < (x,y:X)(R x y) -> (z:X)(R y z) -> (R x z).Transitivity is defined
Coq < Variables R:Relation; p:(Transitivity R).R is assumed
p is assumed
Coq < Print p.*** [ p : (Transitivity R) ]
Positions [1;2;4] are implicit
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.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
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.Coq < Variables a,b,c:X; r1:(R a b); r2:(R b c).a is assumed
b is assumed
c is assumed
r1 is assumed
r2 is assumed
Coq < Check (p r1 r2).(p r1 r2)
: (R a c)
Coq < Check (p r1 4!c).(p r1 4!c)
: (R b c)->(R a c)
2.6.3 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.