Commands¶
Displaying¶
- Command Print Term? reference univ_name_list?¶
- univ_name_list
::=
@{ name* }Displays definitions of terms, including opaque terms, for the object
reference
.Term
- a syntactic marker to allow printing a term that is the same as one of the variousPrint
commands. For example,Print All
is a different command, whilePrint Term All
shows information on the object whose name is "All
".univ_name_list
- locally renames the polymorphic universes ofreference
. The name_
means the usual name is printed.
- Error This object does not support universe names.¶
- Command Print All¶
This command displays information about the current state of the environment, including sections and modules.
Query commands¶
Unlike other commands, query_command
s may be prefixed with
a goal selector (natural:
) to specify which goals it applies to.
If no selector is provided,
the command applies to the current goal. If no proof is open, then the command only applies
to accessible objects. (see Section Invocation of tactics).
Eval
and Compute
are also query_command
s, which are
described elsewhere
- Command About reference univ_name_list?¶
Displays information about the
reference
object, which, if a proof is open, may be a hypothesis of the selected goal, or an accessible theorem, axiom, etc.: its kind (module, constant, assumption, inductive, constructor, abbreviation, …), long name, type, implicit arguments and argument scopes (as set in the definition ofreference
or subsequently with theArguments
command). It does not print the body of definitions or proofs.
- Command Check term¶
Displays the type of
term
. When called in proof mode, the term is checked in the local context of the selected goal (possibly by using single numbered goal selectors). This command tries to resolve existential variables as much as possible.
- Command Type term¶
Displays the type of
term
, same asCheck
, but will fail if any existential variables are unable to be resolved.
- Command Search search_query+ insideinoutside qualid+?¶
This command can be used to filter the goal and the global context to retrieve objects whose name or type satisfies a number of conditions. Library files that were not loaded with
Require
are not considered. TheSearch Blacklist
table can also be used to exclude some things from all calls toSearch
.The output of the command is a list of qualified identifiers and their types. If the
search_querySearch Output Name Only
flag is on, the types are omitted.::=
search_item|
- search_query|
[ search_query++| ]Multiple
search_item
s can be combined into a complexsearch_query
:- search_query
Excludes the objects that would be filtered by
search_query
. See this example.[ search_query+ | ... | search_query+ ]
This is a disjunction of conjunctions of queries. A simple conjunction can be expressed by having a single disjunctive branch. For a conjunction at top-level, the surrounding brackets are not required.
::=
headhypconclheadhypheadconcl :? string % scope_key?|
headhypconclheadhypheadconcl :? one_pattern|
is : logical_kindSearched objects can be filtered by patterns, by the constants they contain (identified by their name or a notation) and by their names. The location of the pattern or constant within a term
one_pattern
Search for objects whose type contains a subterm matching the pattern
one_pattern
. Holes of the pattern are indicated by_
or?ident
. If the same?ident
occurs more than once in the pattern, all occurrences in the subterm must be identical. See this example.string % scope_key?
If
string
is a substring of a valid identifier and no% scope_key
is provided, search for objects whose name containsstring
. See this example.Otherwise, search for objects whose type contains the reference that this string, interpreted as a notation, is attached to (as described in
reference
). See this example.
Note
To refer to a string used in a notation that is a substring of a valid identifier, put it between single quotes or explicitly provide a scope. See this example.
hyp:
The provided pattern or reference is matched against any subterm of an hypothesis of the type of the objects. See this example.
headhyp:
The provided pattern or reference is matched against the subterms in head position (any partial applicative subterm) of the hypotheses of the type of the objects. See the previous example.
concl:
The provided pattern or reference is matched against any subterm of the conclusion of the type of the objects. See this example.
headconcl:
The provided pattern or reference is matched against the subterms in head position (any partial applicative subterm) of the conclusion of the type of the objects. See the previous example.
head:
This is simply the union between
headconcl:
andheadhyp:
.is: logical_kind
- logical_kind
::=
thm_tokenassumption_token|
DefinitionExampleContextPrimitiveSymbol|
CoercionInstanceSchemeCanonicalSubClass|
FixpointCoFixpointFieldMethodFilters objects by the keyword that was used to define them (
Theorem
,Lemma
,Axiom
,Variable
,Context
,Primitive
...) or its status (Coercion
,Instance
,Scheme
,Canonical
,SubClass
,Field
for record fields,Method
for class fields). Note thatCoercion
s,Canonical Structure
s,Instance
s andScheme
s can be defined without using those keywords. See this example.
Additional clauses:
insidein qualid+
- limit the search to the specified modulesoutside qualid+
- exclude the specified modules from the search
- Error Module/section qualid not found.¶
There is no constant in the environment named
qualid
, wherequalid
is in aninside
oroutside
clause.
Example: Searching for a pattern
- Require Import PeanoNat.
We can repeat meta-variables to narrow down the search. Here, we are looking for commutativity lemmas.
- Search (_ ?n ?m = _ ?m ?n).
- Nat.land_comm: forall a b : nat, Nat.land a b = Nat.land b a Nat.lor_comm: forall a b : nat, Nat.lor a b = Nat.lor b a Nat.lxor_comm: forall a b : nat, Nat.lxor a b = Nat.lxor b a Nat.lcm_comm: forall a b : nat, Nat.lcm a b = Nat.lcm b a Nat.min_comm: forall n m : nat, Nat.min n m = Nat.min m n Nat.gcd_comm: forall n m : nat, Nat.gcd n m = Nat.gcd m n Bool.xorb_comm: forall b b' : bool, xorb b b' = xorb b' b Nat.max_comm: forall n m : nat, Nat.max n m = Nat.max m n Nat.mul_comm: forall n m : nat, n * m = m * n Nat.add_comm: forall n m : nat, n + m = m + n Bool.orb_comm: forall b1 b2 : bool, (b1 || b2)%bool = (b2 || b1)%bool Bool.andb_comm: forall b1 b2 : bool, (b1 && b2)%bool = (b2 && b1)%bool Nat.eqb_sym: forall x y : nat, (x =? y) = (y =? x)
Example: Searching for part of an identifier
- Search "_assoc".
- or_assoc: forall A B C : Prop, (A \/ B) \/ C <-> A \/ B \/ C and_assoc: forall A B C : Prop, (A /\ B) /\ C <-> A /\ B /\ C eq_trans_assoc: forall [A : Type] [x y z t : A] (e : x = y) (e' : y = z) (e'' : z = t), eq_trans e (eq_trans e' e'') = eq_trans (eq_trans e e') e''
Example: Searching for a reference by notation
- Search "+".
- plus_O_n: forall n : nat, 0 + n = n plus_n_O: forall n : nat, n = n + 0 plus_n_Sm: forall n m : nat, S (n + m) = n + S m plus_Sn_m: forall n m : nat, S n + m = S (n + m) mult_n_Sm: forall n m : nat, n * m + n = n * S m f_equal2_plus: forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2 nat_rect_plus: forall (n m : nat) {A : Type} (f : A -> A) (x : A), nat_rect (fun _ : nat => A) x (fun _ : nat => f) (n + m) = nat_rect (fun _ : nat => A) (nat_rect (fun _ : nat => A) x (fun _ : nat => f) m) (fun _ : nat => f) n
Example: Disambiguating between part of identifier and notation
- Require Import PeanoNat.
In this example, we show two ways of searching for all the objects whose type contains
Nat.modulo
but which do not contain the substring "mod".- Search "'mod'" -"mod".
- Nat.bit0_eqb: forall a : nat, Nat.testbit a 0 = (a mod 2 =? 1) Nat.Div0.div_exact: forall a b : nat, a = b * (a / b) <-> a mod b = 0 Nat.land_ones: forall a n : nat, Nat.land a (Nat.ones n) = a mod 2 ^ n Nat.testbit_spec': forall a n : nat, Nat.b2n (Nat.testbit a n) = (a / 2 ^ n) mod 2 Nat.pow_div_l: forall a b c : nat, b <> 0 -> a mod b = 0 -> (a / b) ^ c = a ^ c / b ^ c Nat.testbit_eqb: forall a n : nat, Nat.testbit a n = ((a / 2 ^ n) mod 2 =? 1) Nat.testbit_false: forall a n : nat, Nat.testbit a n = false <-> (a / 2 ^ n) mod 2 = 0 Nat.testbit_true: forall a n : nat, Nat.testbit a n = true <-> (a / 2 ^ n) mod 2 = 1
- Search "mod"%nat -"mod".
- Nat.bit0_eqb: forall a : nat, Nat.testbit a 0 = (a mod 2 =? 1) Nat.Div0.div_exact: forall a b : nat, a = b * (a / b) <-> a mod b = 0 Nat.land_ones: forall a n : nat, Nat.land a (Nat.ones n) = a mod 2 ^ n Nat.testbit_spec': forall a n : nat, Nat.b2n (Nat.testbit a n) = (a / 2 ^ n) mod 2 Nat.pow_div_l: forall a b c : nat, b <> 0 -> a mod b = 0 -> (a / b) ^ c = a ^ c / b ^ c Nat.testbit_eqb: forall a n : nat, Nat.testbit a n = ((a / 2 ^ n) mod 2 =? 1) Nat.testbit_false: forall a n : nat, Nat.testbit a n = false <-> (a / 2 ^ n) mod 2 = 0 Nat.testbit_true: forall a n : nat, Nat.testbit a n = true <-> (a / 2 ^ n) mod 2 = 1
Example: Search in hypotheses
The following search shows the objects whose type contains
bool
in an hypothesis as a strict subterm only:- Add Search Blacklist "internal_".
- Search hyp:bool -headhyp:bool.
- Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat Byte.of_bits: bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) -> Byte.byte Byte.to_bits_of_bits: forall b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))), Byte.to_bits (Byte.of_bits b) = b
Example: Search in conclusion
The following search shows the objects whose type contains
bool
in the conclusion as a strict subterm only:- Search concl:bool -headconcl:bool.
- Byte.to_bits: Byte.byte -> bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true andb_true_intro: forall [b1 b2 : bool], b1 = true /\ b2 = true -> (b1 && b2)%bool = true Byte.to_bits_of_bits: forall b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))), Byte.to_bits (Byte.of_bits b) = b bool_choice: forall [S : Set] [R1 R2 : S -> Prop], (forall x : S, {R1 x} + {R2 x}) -> {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
Example: Search by keyword or status
The following search shows the definitions whose type is a
nat
or a function which returns anat
and the lemmas about+
:- Search [ is:Definition headconcl:nat | is:Lemma (_ + _) ].
- Nat.two: nat Nat.zero: nat Nat.one: nat Nat.succ: nat -> nat Nat.log2: nat -> nat Nat.sqrt: nat -> nat Nat.square: nat -> nat Nat.double: nat -> nat Nat.pred: nat -> nat Nat.ldiff: nat -> nat -> nat Nat.tail_mul: nat -> nat -> nat Nat.land: nat -> nat -> nat Nat.div: nat -> nat -> nat Nat.modulo: nat -> nat -> nat Nat.lor: nat -> nat -> nat Nat.lxor: nat -> nat -> nat Nat.of_hex_uint: Hexadecimal.uint -> nat Nat.of_uint: Decimal.uint -> nat Nat.of_num_uint: Number.uint -> nat length: forall [A : Type], list A -> nat plus_n_O: forall n : nat, n = n + 0 plus_O_n: forall n : nat, 0 + n = n plus_n_Sm: forall n m : nat, S (n + m) = n + S m plus_Sn_m: forall n m : nat, S n + m = S (n + m) mult_n_Sm: forall n m : nat, n * m + n = n * S m
The following search shows the instances whose type includes the classes
Reflexive
orSymmetric
:- Require Import Morphisms.
- Search is:Instance [ Reflexive | Symmetric ].
- iff_Symmetric: Symmetric iff iff_Reflexive: Reflexive iff impl_Reflexive: Reflexive Basics.impl eq_Symmetric: forall {A : Type}, Symmetric eq eq_Reflexive: forall {A : Type}, Reflexive eq Equivalence_Reflexive: forall {A : Type} {R : Relation_Definitions.relation A}, Equivalence R -> Reflexive R Equivalence_Symmetric: forall {A : Type} {R : Relation_Definitions.relation A}, Equivalence R -> Symmetric R PreOrder_Reflexive: forall {A : Type} {R : Relation_Definitions.relation A}, PreOrder R -> Reflexive R PER_Symmetric: forall {A : Type} {R : Relation_Definitions.relation A}, PER R -> Symmetric R neq_Symmetric: forall {A : Type}, Symmetric (fun x y : A => x <> y) reflexive_eq_dom_reflexive: forall {A B : Type} {R' : Relation_Definitions.relation B}, Reflexive R' -> Reflexive (eq ==> R')%signature
The following search outputs operations on
nat
defined in the prelude either with theDefinition
orFixpoint
keyword:- Search (nat -> nat -> nat) -bool [ is:Definition | is:Fixpoint ].
- Nat.lxor: nat -> nat -> nat Nat.ldiff: nat -> nat -> nat Nat.lor: nat -> nat -> nat Nat.land: nat -> nat -> nat Nat.gcd: nat -> nat -> nat Nat.modulo: nat -> nat -> nat Nat.div: nat -> nat -> nat Nat.min: nat -> nat -> nat Nat.pow: nat -> nat -> nat Nat.tail_mul: nat -> nat -> nat Nat.tail_add: nat -> nat -> nat Nat.sub: nat -> nat -> nat Nat.mul: nat -> nat -> nat Nat.add: nat -> nat -> nat Nat.max: nat -> nat -> nat Nat.tail_addmul: nat -> nat -> nat -> nat Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat Nat.log2_iter: nat -> nat -> nat -> nat -> nat
- Command SearchPattern one_pattern insideinoutside qualid+?¶
Displays the name and type of all hypotheses of the selected goal (if any) and theorems of the current context ending with
forall binder*,? P_{i} ->* C
that match the patternone_pattern
.See
Search
for an explanation of theinside
/in
/outside
clauses.Example:
SearchPattern
examples- Require Import Arith.
- [Loading ML file ring_plugin.cmxs (using legacy method) ... done]
- SearchPattern (_ + _ = _ + _).
- Nat.add_comm: forall n m : nat, n + m = m + n Nat.add_succ_comm: forall n m : nat, S n + m = n + S m Nat.add_shuffle0: forall n m p : nat, n + m + p = n + p + m Nat.add_shuffle3: forall n m p : nat, n + (m + p) = m + (n + p) Nat.add_assoc: forall n m p : nat, n + (m + p) = n + m + p f_equal2_plus: forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2 Nat.add_shuffle2: forall n m p q : nat, n + m + (p + q) = n + q + (m + p) Nat.add_shuffle1: forall n m p q : nat, n + m + (p + q) = n + p + (m + q)
- SearchPattern (nat -> bool).
- Nat.odd: nat -> bool Init.Nat.odd: nat -> bool Nat.even: nat -> bool Init.Nat.even: nat -> bool Init.Nat.testbit: nat -> nat -> bool Nat.leb: nat -> nat -> bool Nat.eqb: nat -> nat -> bool Init.Nat.eqb: nat -> nat -> bool Nat.ltb: nat -> nat -> bool Nat.testbit: nat -> nat -> bool Init.Nat.leb: nat -> nat -> bool Init.Nat.ltb: nat -> nat -> bool BinNat.N.testbit_nat: BinNums.N -> nat -> bool BinPosDef.Pos.testbit_nat: BinNums.positive -> nat -> bool BinPos.Pos.testbit_nat: BinNums.positive -> nat -> bool BinNatDef.N.testbit_nat: BinNums.N -> nat -> bool
- SearchPattern (forall l : list _, _ l l).
- List.incl_refl: forall [A : Type] (l : list A), List.incl l l List.lel_refl: forall [A : Type] (l : list A), List.lel l l
- SearchPattern (?X1 + _ = _ + ?X1).
- Nat.add_comm: forall n m : nat, n + m = m + n
- Command SearchRewrite one_pattern insideinoutside qualid+?¶
Displays the name and type of all hypotheses of the selected goal (if any) and theorems of the current context that have the form
forall binder*,? P_{i} ->* LHS = RHS
whereone_pattern
matches eitherLHS
orRHS
.See
Search
for an explanation of theinside
/in
/outside
clauses.Example:
SearchRewrite
examples- Require Import Arith.
- SearchRewrite (_ + _ + _).
- Nat.add_shuffle0: forall n m p : nat, n + m + p = n + p + m Nat.add_assoc: forall n m p : nat, n + (m + p) = n + m + p Nat.add_shuffle2: forall n m p q : nat, n + m + (p + q) = n + q + (m + p) Nat.add_shuffle1: forall n m p q : nat, n + m + (p + q) = n + p + (m + q) Nat.add_carry_div2: forall (a b : nat) (c0 : bool), (a + b + Nat.b2n c0) / 2 = a / 2 + b / 2 + Nat.b2n (Nat.testbit a 0 && Nat.testbit b 0 || c0 && (Nat.testbit a 0 || Nat.testbit b 0))
- Table Search Blacklist string¶
This table specifies a set of strings used to exclude lemmas from the results of
Search
,SearchPattern
andSearchRewrite
queries. A lemma whose fully qualified name contains any of the strings will be excluded from the search results. The default blacklisted substrings are_subterm
,_subproof
andPrivate_
.Use the
Add
andRemove
commands to update the set of blacklisted strings.
- Flag Search Output Name Only¶
This flag restricts the output of search commands to identifier names; turning it on causes invocations of
Search
,SearchPattern
,SearchRewrite
etc. to omit types from their output, printing only identifiers.
Requests to the environment¶
- Command Print Assumptions reference¶
Displays all the assumptions (axioms, parameters and variables) a theorem or definition depends on.
The message "Closed under the global context" indicates that the theorem or definition has no dependencies.
- Command Print Opaque Dependencies reference¶
Displays the assumptions and opaque constants that
reference
depends on.
- Command Print Transparent Dependencies reference¶
Displays the assumptions and transparent constants that
reference
depends on.
- Command Print All Dependencies reference¶
Displays all the assumptions and constants
reference
depends on.
- Command Locate reference¶
- reference
::=
qualid|
string % scope_key?Displays the full name of objects from Coq's various qualified namespaces such as terms, modules and Ltac, thereby showing the module they are defined in. It also displays notation definitions.
Note that objects are reported only when the module containing them has been loaded, such as through a
Require
command. Notation definitions are reported only when the containing module has been imported (e.g. withRequire Import
orImport
).Objects defined with commands such as
Definition
,Parameter
,Record
,Theorem
and their numerous variants are shown asConstant
in the output.qualid
refers to object names that end with
qualid
.string % scope_key?
refers to definitions of notations.
string
can be a single token in the notation such as "->
" or a pattern that matches the notation. See Locating notations.% scope_key
, if present, limits the reference to the scope bound to the delimiting keyscope_key
, such as, for example,%nat
. (see Section Local interpretation rules for notations)
- Command Locate Library qualid¶
Displays the full name, status and file system path of the module
qualid
, whether loaded or not.
- Command Locate File string¶
Displays the file system path of the file ending with
string
. Typically,string
has a suffix such as.cmo
or.vo
or.v
file, such asNat.v
.
Example: Locate examples
- Locate nat.
- Inductive Coq.Init.Datatypes.nat
- Locate Datatypes.O.
- Constructor Coq.Init.Datatypes.O (shorter name to refer to it in current context is O)
- Locate Init.Datatypes.O.
- Constructor Coq.Init.Datatypes.O (shorter name to refer to it in current context is O)
- Locate Coq.Init.Datatypes.O.
- Constructor Coq.Init.Datatypes.O (shorter name to refer to it in current context is O)
- Locate I.Dont.Exist.
- No object of suffix I.Dont.Exist
Printing flags¶
- Flag Fast Name Printing¶
When this flag is turned on, Coq uses an asymptotically faster algorithm for the generation of unambiguous names of bound variables while printing terms. While faster, it is also less clever and results in a typically less elegant display, e.g. it will generate more names rather than reusing certain names across subterms. This flag is not enabled by default, because as Ltac observes bound names, turning it on can break existing proof scripts.
Loading files¶
Coq offers the possibility of loading different parts of a whole development stored in separate files. Their contents will be loaded as if they were entered from the keyboard. This means that the loaded files are text files containing sequences of commands for Coq’s toplevel. This kind of file is called a script for Coq. The standard (and default) extension of Coq’s script files is .v.
- Command Load Verbose? stringident¶
Loads a file. If
ident
is specified, the command loads a file namedident.v
, searching successively in each of the directories specified in the load path. (see Section Logical paths and the load path)If
string
is specified, it must specify a complete filename.~
and .. abbreviations are allowed as well as shell variables. If no extension is specified, Coq will use the default extension.v
.Files loaded this way can't leave proofs open, nor can
Load
be used inside a proof.We discourage the use of
Load
; useRequire
instead.Require
loads.vo
files that were previously compiled from.v
files.Verbose
displays the Coq output for each command and tactic in the loaded file, as if the commands and tactics were entered interactively.- Error Load is not supported inside proofs.¶
- Error Files processed by Load cannot leave open proofs.¶
Compiled files¶
This section describes the commands used to load compiled files (see Chapter Coq commands for documentation on how to compile a file). A compiled file is a particular case of a module called a library file.
- Command From dirpath? Require ImportExport import_categories?? filtered_import+¶
- dirpath
::=
ident .* identLoads compiled files into the Coq environment. For the first
qualid
in eachfiltered_import
, the command looks in the load path for a compiled fileident.vo
whose logical name has the formdirpath.ident_{implicit}.*qualid
(ifFrom dirpath
is given) orident_{implicit}.*qualid
(if the optionalFrom
clause is absent).ident_{implicit}.*
represents the parts of the fully qualified name that are implicit. For example,From Coq Require Nat
loadsCoq.Init.Nat
andInit
is implicit.ident
is the final component of thequalid
.If a file is found, its logical name must be the same as the one used to compile the file. Then the file is loaded as well as all the files it depends on (recursively). All the files must have been compiled with the same version of Coq.
Import
- additionally does anImport
on the loaded module, making components defined in the module available by their short namesExport
- additionally does anExport
on the loaded module, making components defined in the module available by their short names and marking them to be exported by the current module
If the required file has already been loaded, it is not reloaded. If
Import
orExport
are present, the command also does the equivalent of theImport
orExport
commands.A single file can be loaded with several variations of the
Require
command. For example, the-Q path Lib
command line parameter associates the filepath/Foo/File.vo
with the logical nameLib.Foo.File
. It allows this file to be loaded throughRequire Lib.Foo.File
,From Lib Require Foo.File
,From Lib Require File
orFrom Lib.Foo Require File
. The-R path Lib
command line parameter allows loading the file with the additional alternativesRequire Foo.File
andRequire File
In particular,From
is useful to ensure that the file comes from a particular package or subpackage. Use of-Q
is better for avoiding ambiguous path names.Exact matches are preferred when looking for a file with the logical name
dirpath.ident_{implicit}.*qualid
orident_{implicit}.*qualid
(that is, matches where the implicit part is empty). If the name exactly matches in multiple-R
or-Q
options, the file corresponding to the last-R
or-Q
specified is used. (InPrint LoadPath
, that's the first match from the top.)If there is no exact match, the matches from the last
-R
or-Q
are selected. If this results in a unique match, the corresponding file is selected. If this results in several matches, it is an error. The difference between the-R
and the-Q
option is that non-exact matches are allowed for-Q
only ifFrom
is present. Matching is done when the script is compiled or processed rather than when its .vo file is loaded. .vo files use fully-qualified names.We recommend you use
-R
only to refer to files in the same package. Use-Q
(if necessary) to refer to files in a different package.- Error Cannot find library foo in loadpath.¶
The command did not find the file foo.vo. Either foo.v exists but is not compiled or foo.vo is in a directory which is not in your load path.
- Error Required library qualid matches several files in path (found file_{1}.vo, file_{2}.vo, ...).¶
The file to load must be required with a more discriminating suffix, or, at worst, with its full logical name.
- Error Compiled library ident.vo makes inconsistent assumptions over library qualid.¶
The command tried to load library file
ident
.vo that depends on some specific version of libraryqualid
which is not the one already loaded in the current Coq session. Probablyident.v
was not properly recompiled with the last version of the file containing modulequalid
.
- Error Bad magic number.¶
The file
ident.vo
was found but either it is not a Coq compiled module, or it was compiled with an incompatible version of Coq.
- Error The file ident.vo contains library qualid_{1} and not library qualid_{2}.¶
The library
qualid_{2}
is indirectly required by aRequire
. The load path mapsqualid_{2}
toident.vo
, which was compiled using a load path that bound it toqualid_{1}
. Usually the appropriate solution is to recompileident.v
using the correct load path.
- Warning Require inside a module is deprecated and strongly discouraged. You can Require a module at toplevel and optionally Import it inside another one.¶
Note that the
Import
andExport
commands can be used inside modules.See also
Chapter Coq commands
- Command Print Libraries¶
This command displays the list of library files loaded in the current Coq session.
- Command Declare ML Module string+¶
Loads an OCaml plugin and its dependencies dynamically. The
string
argument must be a valid findlib plugin name, for examplecoq-core.plugins.ltac
. As of Coq 8.16, the command also supports a legacy syntax compatible with the plugin loading system used in Coq 8.0-8.15, see below.The first component of the plugin name is a package name that has to be in scope of
findlib
's' search path. One can see the paths explored byfindlib
by runningocamlfind printconf
and get the list of available libraries by runningocamlfind list | grep coq
(Coq libraries are typically namedcoq-something
).This command is reserved for plugin developers, who should provide a
.v
file containing the command. Users of the plugin will usually require the resulting.vo
file which will then transitively load the required plugin.If you are writing a plugin, you thus need to generate the right metadata so
findlib
can locate your plugin. This usually involves generating some kind ofMETA
file and placing it in a place wherefindlib
can see it. Different build systems provide different helpers to do this: see here for coq_makefile, and here for Dune.Note that the plugin loading system for Coq changed in 8.16 to use findlib. Previous Coq versions loaded OCaml dynamic objects by first locating the object file from
-I
directives, then directly invokingDynlink.loadfile
. For compatibility purposes, 8.16 still supports this legacy method, with the syntax beingDeclare ML Module "my_package_plugin:pkg.plugin.my-package".
, wheremy_package_plugin
is the name of the OCaml object file.This is useful if you are still using a third party build system such as Dune or your own.
This command supports the
local
attribute. If present, the listed files are not exported, even if they're outside a section.- Error File not found on loadpath: string.¶
findlib
is not able to find the plugin name. Possible reasons are:The plugin does not exist or is misspelled. You can get the list of available libraries by running
ocamlfind list | grep coq
.The metadata for
findlib
has not been set properly (see above).
- Error Dynlink error: execution of module initializers in the¶
- Error plugin name anymore. Plugins should be loaded using their¶
- Error public name according to findlib, for example¶
- Error package-name.foo and not foo_plugin.¶
The plugin declaration in some
.mlg
file does not match thefindlib
plugin name. In the example ofcoq-core.plugins.ltac
, one has to writeDECLARE PLUGIN "coq-core.plugins.ltac"
.
- Command Print ML Modules¶
Print the name of all findlib libraries loaded with
Declare ML Module
.
Load paths¶
Changed in version 8.18: Commands to manage load paths within Coq have been removed. Load paths can be managed using Coq command line options or enviroment variables (see Logical paths and the load path).
- Command Print LoadPath dirpath?¶
Displays the current Coq load path. If
dirpath
is specified, displays only the paths that extend that prefix. In the output, the logical path<>
represents an empty logical path.
- Command Print ML Path¶
Displays the current OCaml loadpath, as provided by the command line option
-I string
(cf.Declare ML Module
).
Extra Dependencies¶
Dependencies on external files, i.e. non .v
files, can be declared as
follows:
- Command From dirpath Extra Dependency string as ident?¶
Adds an additional dependency of the current
.v
file on an external file. This information is included in thecoqdep
tool generated list of dependencies. The file namestring
must exist relative to one of the top directories associated withdirpath
.string
can include directory separators (/
) to select a file in a subdirectory. Path elements instring
must be valid Coq identifiers, e.g. they cannot contain characters such as-
or,
. See Lexical conventions.
When ident
is provided, that name can be used by OCaml code, typically
in a plugin, to access the full path of the external file via the API
ComExtraDeps.query_extra_dep
.
Backtracking¶
The backtracking commands described in this section can only be used
interactively, they cannot be part of a Coq file loaded via
Load
or compiled by coqc
.
- Command Reset ident¶
This command removes all the objects in the environment since
ident
was introduced, includingident
.ident
may be the name of a defined or declared object as well as the name of a section. One cannot reset over the name of a module or of an object inside a module.
- Command Reset Initial¶
Goes back to the initial state, just after the start of the interactive session.
- Command Back natural?¶
Undoes all the effects of the last
natural sentence
s. Ifnatural
is not specified, the command undoes one sentence. Sentences read from a.v
file via aLoad
are considered a single sentence. WhileBack
can undo tactics and commands executed within proof mode, once you exit proof mode, such as withQed
, all the statements executed within are thereafter considered a single sentence.Back
immediately followingQed
gets you back to the state just after the statement of the proof.- Error Invalid backtrack.¶
The user wants to undo more commands than available in the history.
- Command BackTo natural¶
This command brings back the system to the state labeled
natural
, forgetting the effect of all commands executed after this state. The state label is an integer which grows after each successful command. It is displayed in the prompt when in -emacs mode. Just asBack
(see above), theBackTo
command now handles proof states. For that, it may have to undo some extra commands and end on a statenatural′ ≤ natural
if necessary.
Quitting and debugging¶
- Command Quit¶
Causes Coq to exit. Valid only in coqtop.
- Command Drop¶
This command temporarily enters the OCaml toplevel. It is a debug facility used by Coq’s implementers. Valid only in the bytecode version of coqtop. The OCaml command:
#use "include";;
adds the right loadpaths and loads some toplevel printers for all abstract types of Coq- section_path, identifiers, terms, judgments, …. You can also use the file base_include instead, that loads only the pretty-printers for section_paths and identifiers. You can return back to Coq with the command:
go();;
Warning
It only works with the bytecode version of Coq (i.e.
coqtop.byte
, see Sectioninteractive-use
).You must have compiled Coq from the source package and set the environment variable COQTOP to the root of your copy of the sources (see Section
customization-by-environment-variables
).
- Command Instructions sentence¶
Executes
sentence
and displays the number of CPU instructions needed to execute it. This command is currently only supported on Linux systems, but does not fail on unsupported sustems, where it instead prints an error message in the place of the instruction count.
- Command Redirect string sentence¶
Executes
sentence
, redirecting its output to the file "string
.out".If
string
is a relative filename, it refers to the directory specified by the command line option-output-directory
, if set (see Command line options) and otherwise, the current directory. UsePwd
to display the current directory.
- Command Timeout natural sentence¶
Executes
sentence
. If the operation has not terminated afternatural
seconds, then it is interrupted and an error message is displayed.
- Command Fail sentence¶
For debugging scripts, sometimes it is desirable to know whether a command or a tactic fails. If
sentence
fails, thenFail sentence
succeeds (except for anomalies or for critical failures such as "stack overflow"), without changing the proof state. In interactive mode, the system prints a message confirming the failure.
- Command Succeed sentence¶
If
sentence
succeeds, thenSucceed sentence
succeeds without changing the proof state. Ifsentence
fails, thenSucceed sentence
fails showing the error message forsentence
. In interactive mode, the system prints the messageThe command has succeeded and its effects have been reverted.
confirming the success. This command can be useful for writing tests.
Note
Time
, Redirect
, Timeout
, Fail
and Succeed
are
control_command
s. For these commands, attributes and goal
selectors, when specified, are part of the sentence
argument, and thus come after
the control command prefix and before the inner command or tactic. For
example: Time #[ local ] Definition foo := 0.
or Fail Timeout 10 all: auto.
Controlling display¶
- Option Warnings "-+? ident+,"¶
This option configures the display of warnings. The
ident
s are warning or category names. Adding-
in front of a warning or category disables it, adding+
makes it an error.Warning name and categories are printed between brackets when the warning is displayed (the warning name appears first). Warnings can belong to multiple categories. The special category
all
contains all warnings, and the special categorydefault
contains the warnings enabled by default.Coq defines a set of core warning categories, which may be extended by plugins, so this list is not exhaustive. The core categories are:
automation
,bytecode-compiler
,coercions
,deprecated
,extraction
,filesystem
,fixpoints
,fragile
,funind
,implicits
,ltac
,ltac2
,native-compiler
,numbers
,parsing
,pedantic
,records
,ssr
,syntax
,tactics
,user-warn
,vernacular
.The flags are interpreted from left to right, so in case of an overlap, the flags on the right have higher priority, meaning that
A,-A
is equivalent to-A
.See also the
warnings
attribute, which can be used to configure the display of warnings for a single command.
- Option Debug "-? ident+,"¶
This option configures the display of debug messages. Each
ident
enables debug messages for that component, while-ident
disables messages for the component.all
activates or deactivates all other components.backtrace
controls printing of error backtraces.Test
Debug
displays the list of components and their enabled/disabled state.
- Option Printing Width natural¶
This option sets which left-aligned part of the width of the screen is used for display. At the time of writing this documentation, the default value is 78.
- Option Printing Depth natural¶
This option controls the nesting depth of the formatter used for pretty- printing. Beyond this depth, display of subterms is replaced by dots. At the time of writing this documentation, the default value is 50.
- Flag Printing Compact Contexts¶
This flag controls the compact display mode for goals contexts. When on, the printer tries to reduce the vertical size of goals contexts by putting several variables (even if of different types) on the same line provided it does not exceed the printing width (see
Printing Width
). At the time of writing this documentation, it is off by default.
- Flag Printing Unfocused¶
This flag controls whether unfocused goals are displayed. Such goals are created by focusing other goals with bullets or curly braces. It is off by default.
- Flag Printing Dependent Evars Line¶
This flag controls the printing of the “(dependent evars: …)” information after each tactic. The information is used by the Prooftree tool in Proof General. (https://askra.de/software/prooftree)
Printing constructions in full¶
- Flag Printing All¶
Coercions, implicit arguments, the type of pattern matching, but also notations (see Syntax extensions and notation scopes) can obfuscate the behavior of some tactics (typically the tactics applying to occurrences of subterms are sensitive to the implicit arguments). Turning this flag on deactivates all high-level printing features such as coercions, implicit arguments, returned type of pattern matching, notations and various syntactic sugar for pattern matching or record projections. Otherwise said,
Printing All
includes the effects of the flagsPrinting Implicit
,Printing Coercions
,Printing Synth
,Printing Projections
, andPrinting Notations
. To reactivate the high-level printing features, use the commandUnset Printing All
.Note
In some cases, setting
Printing All
may display terms that are so big they become very hard to read. One technique to work around this is useUndelimit Scope
and/orClose Scope
to turn off the printing of notations bound to particular scope(s). This can be useful when notations in a given scope are getting in the way of understanding a goal, but turning off all notations withPrinting All
would make the goal unreadable.
Controlling Typing Flags¶
- Flag Guard Checking¶
This flag can be used to enable/disable the guard checking of fixpoints. Warning: this can break the consistency of the system, use at your own risk. Decreasing argument can still be specified: the decrease is not checked anymore but it still affects the reduction of the term. Unchecked fixpoints are printed by
Print Assumptions
.
- Attribute bypass_check(guard= yesno?)¶
This boolean attribute is similar to the
Guard Checking
flag, but on a per-declaration basis. Disable guard checking locally withbypass_check(guard)
.
- Flag Positivity Checking¶
This flag can be used to enable/disable the positivity checking of inductive types and the productivity checking of coinductive types. Warning: this can break the consistency of the system, use at your own risk. Unchecked (co)inductive types are printed by
Print Assumptions
.
- Attribute bypass_check(positivity= yesno?)¶
This boolean attribute is similar to the
Positivity Checking
flag, but on a per-declaration basis. Disable positivity checking locally withbypass_check(positivity)
.
- Flag Universe Checking¶
This flag can be used to enable/disable the checking of universes, providing a form of "type in type". Warning: this breaks the consistency of the system, use at your own risk. Constants relying on "type in type" are printed by
Print Assumptions
. It has the same effect as-type-in-type
command line argument (see Command line options).
- Attribute bypass_check(universes= yesno?)¶
This boolean attribute is similar to the
Universe Checking
flag, but on a per-declaration basis. Disable universe checking locally withbypass_check(universes)
.
- Command Print Typing Flags¶
Print the status of the three typing flags: guard checking, positivity checking and universe checking.
Example
- Unset Guard Checking.
- Print Typing Flags.
- check_guarded: false check_positive: true check_universes: true definitional uip: false
- Fixpoint f (n : nat) : False := f n.
- f is defined f is recursively defined (guarded on 1st argument)
- Fixpoint ackermann (m n : nat) {struct m} : nat := match m with | 0 => S n | S m => match n with | 0 => ackermann m 1 | S n => ackermann m (ackermann (S m) n) end end.
- ackermann is defined ackermann is recursively defined (guarded on 1st argument)
- Print Assumptions ackermann.
- Axioms: ackermann is assumed to be guarded.
Note that the proper way to define the Ackermann function is to use an inner fixpoint:
- Fixpoint ack m := fix ackm n := match m with | 0 => S n | S m' => match n with | 0 => ack m' 1 | S n' => ack m' (ackm n') end end.
- ack is defined ack is recursively defined (guarded on 1st argument)
Typing flags may not be changed while inside sections.
Internal registration commands¶
Due to their internal nature, the commands that are presented in this section are not for general use. They are meant to appear only in standard libraries and in support libraries of plug-ins.
Exposing constants to OCaml libraries¶
- Command Register qualid_{1} as qualid_{2}¶
Makes the constant
qualid_{1}
accessible to OCaml libraries under the namequalid_{2}
. The constant can then be dynamically located in OCaml code by callingCoqlib.lib_ref "qualid_{2}"
. The OCaml code doesn't need to know where the constant is defined (what file, module, library, etc.).As a special case, when the first segment of
qualid_{2}
iskernel
, the constant is exposed to the kernel. For instance, thePrimInt63
module features the following declaration:Register bool as kernel.ind_bool.This makes the kernel aware of the
bool
type, which is used, for example, to define the return type of the#int63_eq
primitive.See also
- Command Print Registered¶
List the currently registered constants.
- Command Register Scheme qualid_{1} as qualid_{2} for qualid_{3}¶
Make the constant
qualid_{1}
accessible to the "scheme" mechanism for scheme kindqualid_{2}
and inductivequalid_{3}
.
- Command Print Registered Schemes¶
List the currently registered schemes.
This can be useful to find information about the (currently undocumented) scheme kinds.
Inlining hints for the fast reduction machines¶
Registering primitive operations¶
- Command Primitive ident_decl : term? := #ident¶
Makes the primitive type or primitive operator
#ident
defined in OCaml accessible in Coq commands and tactics. For internal use by implementors of Coq's standard library or standard library replacements. No space is allowed after the#
. Invalid values give a syntax error.For example, the standard library files
PrimInt63.v
andPrimFloat.v
usePrimitive
to support, respectively, the features described in Primitive Integers and Primitive Floats.The types associated with an operator must be declared to the kernel before declaring operations that use the type. Do this with
Primitive
for primitive types andRegister
with thekernel
prefix for other types. For example, inPrimInt63.v
,#int63_type
must be declared before the associated operations.