2.7 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.7.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.
Set Implicit Arguments.
This command switches the automatic implicit arguments
mode on. To switch it off, use Unset Implicit Arguments..
The mode is off by default.
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 < Set Implicit Arguments.
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.7.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.
2.7.3 Canonical structures
A canonical structure is an instance of a record/structure type that
can be used to solve equations involving implicit arguments. Assume
that qualid denotes an object (Build_struc c1 ... cn) in the
structure struct of which the fields are x1, ...,
xn. Assume that qualid is declared as a canonical structure
using the command
Canonical Structure qualid.
Then, each time an equation of the form (xi
?)=bdizci has to be solved during the
type-checking process, qualid is used as a solution. Otherwise
said, qualid is canonically used to equip the field ci into a
complete structure built on ci.
Canonical structures are particularly useful when mixed with
coercions and implicit arguments. Here is an example.
Coq < Require Relations.
Coq < Require EqNat.
Coq < Set Implicit Arguments.
Coq < Structure Setoid : Type :=
Coq < {Carrier :> Set;
Coq < Equal : (relation Carrier);
Coq < Prf_equiv : (equivalence Carrier Equal)}.
Coq < Definition is_law := [A,B:Setoid][f:A->B]
Coq < (x,y:A) (Equal x y) -> (Equal (f x) (f y)).
Coq < Axiom eq_nat_equiv : (equivalence nat eq_nat).
Coq < Definition nat_setoid : Setoid := (Build_Setoid eq_nat_equiv).
Coq < Canonical Structure nat_setoid.
Thanks to nat_setoid declared as canonical, the implicit
arguments A and B can be synthesized in the next statement.
Coq < Lemma is_law_S : (is_law S).
1 subgoal
============================
(is_law S)
Remark: If a same field occurs in several canonical structure, then
only the structure declared first as canonical is considered.
Variants:
-
Canonical Structure ident := term : type.
Canonical Structure ident := term.
Canonical Structure ident : type := term.
These are equivalent to a regular definition of ident followed by
the declaration
Canonical Structure ident.
See also: more examples in user contribution category
(Rocq/ALGEBRA).