\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

Setting properties of a function's arguments¶

Command Arguments reference arg_specs* , implicits_alt** : args_modifier+,?¶

argument_spec::=!? name % scope_key?arg_specs::=argument_spec|/|&|( argument_spec+ ) % scope_key?|[ argument_spec+ ] % scope_key?|{ argument_spec+ } % scope_key?implicits_alt::=name|[ name+ ]|{ name+ }args_modifier::=simpl nomatch|simpl never|default implicits|clear implicits|clear scopes|clear bidirectionality hint|rename|assert|extra scopes|clear scopes and implicits|clear implicits and scopes

Specifies properties of the arguments of a function after the function has already been defined. It gives fine-grained control over the elaboration process (i.e. the translation of Gallina language extensions into the core language used by the kernel). The command's effects include:

Making arguments implicit. Afterward, implicit arguments must be omitted in any expression that applies reference.
Declaring that some arguments of a given function should be interpreted in a given scope.
Affecting when the simpl and cbn tactics unfold the function. See Effects of Arguments on unfolding.
Providing bidirectionality hints. See Bidirectionality hints.

This command supports the local and global attributes. Default behavior is to limit the effect to the current section but also to extend their effect outside the current module or library file. Applying local limits the effect of the command to the current module if it's not in a section. Applying global within a section extends the effect outside the current sections and current module in which the command appears.

/
the function will be unfolded only if it's applied to at least the arguments appearing before the /. See Effects of Arguments on unfolding.

Error The / modifier may only occur once.¶

&
tells the type checking algorithm to first type check the arguments before the & and then to propagate information from that typing context to type check the remaining arguments. See Bidirectionality hints.

Error The & modifier may only occur once.¶

( ... ) % scope?
(name₁ name₂ ...)%scope is shorthand for name₁%scope name₂%scope ...

[ ... ] % scope?
declares the enclosed names as implicit, non-maximally inserted. [name₁ name₂ ... ]%scope is equivalent to [name₁]%scope [name₂]%scope ...

{ ... } % scope?
declares the enclosed names as implicit, maximally inserted. {name₁ name₂ ... }%scope is equivalent to {name₁}%scope {name₂}%scope ...

!
the function will be unfolded only if all the arguments marked with ! evaulate to constructors. See Effects of Arguments on unfolding.

name % scope?
a formal parameter of the function reference (i.e. the parameter name used in the function definition). Unless rename is specified, the list of names must be a prefix of the formal parameters, including all implicit arguments. _ can be used to skip over a formal parameter. scope can be either a scope name or its delimiting key. See Binding arguments to a scope.

clear implicits
makes all implicit arguments into explicit arguments

default implicits
automatically determine the implicit arguments of the object. See Automatic declaration of implicit arguments.

rename
rename implicit arguments for the object. See the example here.

assert
assert that the object has the expected number of arguments with the expected names. See the example here: Renaming implicit arguments.

Warning This command is just asserting the names of arguments of qualid. If this is what you want, add ': assert' to silence the warning. If you want to clear implicit arguments, add ': clear implicits'. If you want to clear notation scopes, add ': clear scopes'¶

clear scopes
clears argument scopes of reference

extra scopes
defines extra argument scopes, to be used in case of coercion to Funclass (see Implicit Coercions) or with a computed type.

simpl nomatch
prevents performing a simplification step for reference that would expose a match construct in the head position. See Effects of Arguments on unfolding.

simpl never
prevents performing a simplification step for reference. See Effects of Arguments on unfolding.

clear bidirectionality hint
removes the bidirectionality hint, the &

implicits_alt
use to specify alternative implicit argument declarations for functions that can only be applied to a fixed number of arguments (excluding, for instance, functions whose type is polymorphic). For parsing, the longest list of implicit arguments matching the function application is used to select which implicit arguments are inserted. For printing, the alternative with the most implicit arguments is used; the implict arguments will be omitted if Printing Implicit is not set. See the example here.

Use About to view the current implicit arguments setting for a reference.

Or use the Print Implicit command to see the implicit arguments of an object (see Displaying implicit arguments).

Manual declaration of implicit arguments¶

Example

Inductive list (A : Type) : Type := | nil : list A | cons : A -> list A -> list A.: list is defined list_rect is defined list_ind is defined list_rec is defined list_sind is defined
Check (cons nat 3 (nil nat)).: cons nat 3 (nil nat) : list nat
Arguments cons [A] _ _.
Arguments nil {A}.
Check (cons 3 nil).: cons 3 nil : list nat
Fixpoint map (A B : Type) (f : A -> B) (l : list A) : list B := match l with nil => nil | cons a t => cons (f a) (map A B f t) end.: map is defined map is recursively defined (guarded on 4th argument)
Fixpoint length (A : Type) (l : list A) : nat := match l with nil => 0 | cons _ m => S (length A m) end.: length is defined length is recursively defined (guarded on 2nd argument)
Arguments map [A B] f l.
Arguments length {A} l. Check (fun l:list (list nat) => map length l).: fun l : list (list nat) => map length l : list (list nat) -> list nat

Example: Multiple alternatives with implicits_alt

Arguments map [A B] f l, [A] B f l, A B f l.
Check (fun l => map length l = map (list nat) nat length l).: fun l : list (list nat) => map length l = map length l : list (list nat) -> Prop

Automatic declaration of implicit arguments¶

The "default implicits" args_modifier clause tells Coq to automatically determine the implicit arguments of the object.

Auto-detection is governed by flags specifying whether strict, contextual, or reversible-pattern implicit arguments must be considered or not (see Controlling strict implicit arguments, Controlling contextual implicit arguments, Controlling reversible-pattern implicit arguments and also Controlling the insertion of implicit arguments not followed by explicit arguments).

Example: Default implicits

Inductive list (A:Set) : Set := | nil : list A | cons : A -> list A -> list A.: list is defined list_rect is defined list_ind is defined list_rec is defined list_sind is defined
Arguments cons : default implicits.
Print Implicit cons.: cons : forall [A : Set], A -> list A -> list A Argument A is implicit
Arguments nil : default implicits.
Print Implicit nil.: nil : forall A : Set, list A
Set Contextual Implicit.
Arguments nil : default implicits.
Print Implicit nil.: nil : forall {A : Set}, list A Argument A is implicit and maximally inserted

The computation of implicit arguments takes account of the unfolding of constants. For instance, the variable p below has type (Transitivity R) which is reducible to forall x,y:U, R x y -> forall z:U, R y z -> R x z. As the variables x, y and z appear strictly in the body of the type, they are implicit.

Parameter X : Type.: X is declared
Definition Relation := X -> X -> Prop.: Relation is defined
Definition Transitivity (R:Relation) := forall x y:X, R x y -> forall z:X, R y z -> R x z.: Transitivity is defined
Parameters (R : Relation) (p : Transitivity R).: R is declared p is declared
Arguments p : default implicits.
Print p.: *** [ p : Transitivity R ] Expanded type for implicit arguments p : forall [x y : X], R x y -> forall z : X, R y z -> R x z Arguments p [x y] _ [z]
Print Implicit p.: p : forall [x y : X], R x y -> forall z : X, R y z -> R x z Arguments x, y, z are implicit
Parameters (a b c : X) (r1 : R a b) (r2 : R b c).: a is declared b is declared c is declared r1 is declared r2 is declared
Check (p r1 r2).: p r1 r2 : R a c

Renaming implicit arguments¶

Example: (continued) Renaming implicit arguments

Arguments p [s t] _ [u] _: rename.
Check (p r1 (u:=c)).: p r1 (u:=c) : R b c -> R a c
Check (p (s:=a) (t:=b) r1 (u:=c) r2).: p r1 r2 : R a c
Fail Arguments p [s t] _ [w] _ : assert.: The command has indeed failed with message: Flag "rename" expected to rename u into w.

Binding arguments to a scope¶

The following command declares that the first two arguments of plus_fct are in the scope delimited by the key F (Rfun_scope) and the third argument is in the scope delimited by the key R (R_scope).

Arguments plus_fct (f1 f2)%F x%R.

When interpreting a term, if some of the arguments of reference are built from a notation, then this notation is interpreted in the scope stack extended by the scope bound (if any) to this argument. The effect of the scope is limited to the argument itself. It does not propagate to subterms but the subterms that, after interpretation of the notation, turn to be themselves arguments of a reference are interpreted accordingly to the argument scopes bound to this reference.

Note

In notations, the subterms matching the identifiers of the notations are interpreted in the scope in which the identifiers occurred at the time of the declaration of the notation. Here is an example:

Parameter g : bool -> bool.: g is declared
Declare Scope mybool_scope.
Notation "@@" := true (only parsing) : bool_scope.: Setting notation at level 0.
Notation "@@" := false (only parsing): mybool_scope.
Bind Scope bool_scope with bool.
Notation "# x #" := (g x) (at level 40).
Check # @@ #.: # true # : bool
Arguments g _%mybool_scope.
Check # @@ #.: # true # : bool
Delimit Scope mybool_scope with mybool.
Check # @@%mybool #.: # false # : bool

Effects of `Arguments` on unfolding¶

simpl never indicates that a constant should never be unfolded by cbn, simpl or hnf:

Example

Arguments minus n m : simpl never.

After that command an expression like (minus (S x) y) is left untouched by the tactics cbn and simpl.
A constant can be marked to be unfolded only if it's applied to at least the arguments appearing before the / in a Arguments command.

Example

Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x).
fcomp is defined

Arguments fcomp {A B C} f g x /.

Notation "f \o g" := (fcomp f g) (at level 50).

After that command the expression (f \o g) is left untouched by simpl while ((f \o g) t) is reduced to (f (g t)). The same mechanism can be used to make a constant volatile, i.e. always unfolded.

Example

Definition volatile := fun x : nat => x.
volatile is defined

Arguments volatile / x.
A constant can be marked to be unfolded only if an entire set of arguments evaluates to a constructor. The ! symbol can be used to mark such arguments.

Example

Arguments minus !n !m.

After that command, the expression (minus (S x) y) is left untouched by simpl, while (minus (S x) (S y)) is reduced to (minus x y).
simpl nomatch indicates that a constant should not be unfolded if it would expose a match construct in the head position. This affects the cbn, simpl and hnf tactics.

Example

Arguments minus n m : simpl nomatch.

In this case, (minus (S (S x)) (S y)) is simplified to (minus (S x) y) even if an extra simplification is possible.

In detail: the tactic simpl first applies $\beta$$\iota$-reduction. Then, it expands transparent constants and tries to reduce further using $\beta$$\iota$-reduction. But, when no $\iota$ rule is applied after unfolding then $\delta$-reductions are not applied. For instance trying to use simpl on (plus n O) = n changes nothing.

Bidirectionality hints¶

When type-checking an application, Coq normally does not use information from the context to infer the types of the arguments. It only checks after the fact that the type inferred for the application is coherent with the expected type. Bidirectionality hints make it possible to specify that after type-checking the first arguments of an application, typing information should be propagated from the context to help inferring the types of the remaining arguments.

An Arguments command containing arg_specs₁ & arg_specs₂ provides bidirectionality hints. It tells the typechecking algorithm, when type checking applications of qualid, to first type check the arguments in arg_specs₁ and then propagate information from the typing context to type check the remaining arguments (in arg_specs₂).

Example: Bidirectionality hints

In a context where a coercion was declared from bool to nat:

Definition b2n (b : bool) := if b then 1 else 0.: b2n is defined
Coercion b2n : bool >-> nat.: b2n is now a coercion

Coq cannot automatically coerce existential statements over bool to statements over nat, because the need for inserting a coercion is known only from the expected type of a subterm:

Fail Check (ex_intro _ true _ : exists n : nat, n > 0).: The command has indeed failed with message: The term "ex_intro ?P true ?y" has type "exists y, ?P y" while it is expected to have type "exists n : nat, n > 0" (cannot unify "bool" and "nat").

However, a suitable bidirectionality hint makes the example work:

Arguments ex_intro _ _ & _ _.
Check (ex_intro _ true _ : exists n : nat, n > 0).: ex_intro (fun n : nat => n > 0) true ?g : exists n : nat, n > 0 : exists n : nat, n > 0 where ?g : [ |- (fun n : nat => n > 0) true]

Coq will attempt to produce a term which uses the arguments you provided, but in some cases involving Program mode the arguments after the bidirectionality starts may be replaced by convertible but syntactically different terms.