\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \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}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \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{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#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}\]

# 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 various `Print` commands. For example, `Print All` is a different command, while `Print Term All` shows information on the object whose name is "`All`".

  - `univ_name_list` - locally renames the polymorphic universes of `reference`. The name `_` means the usual name is printed.

  Error qualid not a defined object.
  Error Universe instance length is natural but should be natural.
  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.

Command Inspect natural

  This command displays the `natural` last objects of the current environment, including sections and modules.

Command Print Section qualid

  Displays the objects defined since the beginning of the section named `qualid`.

## 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 may be the name of any accessible defined symbol, such as a theorem, constructor, fixpoint or module. If a proof is open, `reference` may refer to a hypothesis of the selected goal. The information includes: the kind of the object (module, constant, assumption, inductive, constructor, abbreviation, projection, coercion, …), long name, type, opacity/transparency, implicit arguments, argument names and argument scopes (as set in the definition of `reference` or subsequently with the `Arguments` command). It does not print the body of definitions or proofs.

  See `Strategy` for details on opacity.

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 as `Check`, but will fail if any existential variables are unable to be resolved.

Command Search search_query+ inside​in​outside 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. Searched objects can be filtered by patterns, by the constants they contain (identified by their name or a notation), by their names and by their location (e.g. `head`). Library files that were not loaded with `Require` are not considered. The `Search Blacklist` table can also be used to exclude some things from all calls to `Search`.

  The output of the command is a list of qualified identifiers and their types. If the `Search Output Name Only` flag is on, the types are omitted.

  search_query`::=`search_item`````|`- search_query`````|`[ search_query++| ]``

  Multiple `search_item`s can be combined into a complex `search_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.

  search_item`::=`head​hyp​concl​headhyp​headconcl :? string % scope_key?`````|`head​hyp​concl​headhyp​headconcl :? one_pattern`````|`is : logical_kind``
  `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 contains `string`. 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:` and `headhyp:`.

  `is: logical_kind`
    logical_kind`::=`thm_token​assumption_token`````|`Definition​Example​Context​Primitive​Symbol`````|`Coercion​Instance​Scheme​Canonical​SubClass`````|`Fixpoint​CoFixpoint​Field​Method``

    Filters 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 that `Coercion`s, `Canonical Structure`s, `Instance`s and `Scheme`s can be defined without using those keywords. See this example.

  Additional clauses:

  - `inside​in qualid+` - limit the search to the specified modules

  - `outside qualid+` - exclude the specified modules from the search

  The specified modules can be the current file or a currently opened module. For instance, when using Rocq interactively in a file `Foo.v`, the command `Search _ in Foo.` displays every (non-blacklisted) constants previously defined in the file `Foo`. Inside a `Module` `A`, `Search _ in A` similarly displays every constant defined up to this point in the `Module` `A`. See this example.

  Error Module/section qualid not found.

    There is no constant in the environment named `qualid`, where `qualid` is in an `inside` or `outside` clause.

  Example: Searching for a pattern

  From Stdlib Require Import PeanoNat.
    Toplevel input, characters 27-35: > From Stdlib Require Import PeanoNat. > ^^^^^^^^ Error: Cannot find a physical path bound to logical path PeanoNat with prefix Stdlib.

  We can repeat meta-variables to narrow down the search. Here, we are looking for commutativity lemmas. The following example requires the Stdlib library.

  Search (_ ?n ?m = _ ?m ?n).

  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

  The following example requires the Stdlib library.

  From Stdlib Require Import PeanoNat.
    Toplevel input, characters 27-35: > From Stdlib Require Import PeanoNat. > ^^^^^^^^ Error: Cannot find a physical path bound to logical path PeanoNat with prefix Stdlib.

  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".
    Toplevel input, characters 0-22: > Search "'mod'" -"mod". > ^^^^^^^^^^^^^^^^^^^^^^ Error: Unable to interpret "'mod'" as a reference.
  Search "mod"%nat -"mod".
    Toplevel input, characters 0-24: > Search "mod"%nat -"mod". > ^^^^^^^^^^^^^^^^^^^^^^^^ Error: Unable to interpret "mod" as a reference.

  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.
    bool_of_sumbool: forall [A B : Prop], {A} + {B} -> {b : bool | if b then A else B} sumbool_of_bool: forall b : bool, {b = true} + {b = false} 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 a `nat` 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` or `Symmetric`:

  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 the `Definition` or `Fixpoint` 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

  Example: Search in current file or `Module`

  The following example shows how to filter `Search` output in an interactive session. Note that with `rocq top`, the current pseudo-file is named `Top`, it can be replaced with the name of the current file (without the trailing `.v`) when using an IDE.

  Definition b := 42.
    b is defined
  Search _ in Top.
    b: nat
  Module A.
    Interactive Module A started
  Definition a := 12.
    a is defined
  Search _ in A.
    a: nat
  End A.
    Module A is defined
  Search _ in Top.
    b: nat A.a: nat

Command SearchPattern one_pattern inside​in​outside 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*,? Pi ->* C` that match the pattern `one_pattern`.

  See `Search` for an explanation of the `inside`/`in`/`outside` clauses.

  Example: `SearchPattern` examples

  The following example requires the Stdlib library.

  From Stdlib Require Import Arith.
    Toplevel input, characters 27-32: > From Stdlib Require Import Arith. > ^^^^^ Error: Cannot find a physical path bound to logical path Arith with prefix Stdlib.
  SearchPattern (_ + _ = _ + _).
    f_equal2_plus: forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
  SearchPattern (nat -> bool).
    Nat.odd: nat -> bool Nat.even: nat -> bool Nat.ltb: nat -> nat -> bool Nat.testbit: nat -> nat -> bool Nat.leb: nat -> nat -> bool Nat.eqb: nat -> nat -> bool
  SearchPattern (forall l : list _, _ l l).
  SearchPattern (?X1 + _ = _ + ?X1).

Command SearchRewrite one_pattern inside​in​outside 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*,? Pi ->* LHS = RHS` where `one_pattern` matches either `LHS` or `RHS`.

  See `Search` for an explanation of the `inside`/`in`/`outside` clauses.

  Example: `SearchRewrite` examples

  The following example requires the Stdlib library.

  From Stdlib Require Import Arith.
    Toplevel input, characters 27-32: > From Stdlib Require Import Arith. > ^^^^^ Error: Cannot find a physical path bound to logical path Arith with prefix Stdlib.
  SearchRewrite (_ + _ + _).

Flag Search Blacklist Locals

  By default `Search` excludes lemmas declared with `local` from its results (except for those from the current module or its parents). Unsetting this flag will include such lemmas in the results.

Table Search Blacklist string

  This table specifies a set of strings used to exclude lemmas from the results of `Search`, `SearchPattern` and `SearchRewrite` 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` and `Private_`.

  Use the `Add` and `Remove` 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) one or more theorems or definitions depends on.

  The message "Closed under the global context" indicates that all the theorems and definitions have 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 Rocq'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. with `Require Import` or `Import`).

  Objects defined with commands such as `Definition`, `Parameter`, `Record`, `Theorem` and their numerous variants are shown as `Constant` 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 key `scope_key`, such as, for example, `%nat`. (see Section Local interpretation rules for notations)

Command Locate Term reference

  Like `Locate`, but limits the search to terms

Command Locate Module qualid

  Like `Locate`, but limits the search to modules

Command Locate Ltac qualid

  Like `Locate`, but limits the search to Ltac tactics

Command Locate Ltac2 qualid

  Like `Locate`, but limits the search to Ltac2 tactics.

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 as `Nat.v`.

Example: Locate examples

Locate nat.
  Inductive Corelib.Init.Datatypes.nat
Locate Datatypes.O.
  Constructor Corelib.Init.Datatypes.O (shorter name to refer to it in current context is O)
Locate Init.Datatypes.O.
  Constructor Corelib.Init.Datatypes.O (shorter name to refer to it in current context is O)
Locate Stdlib.Init.Datatypes.O.
  No object of suffix Stdlib.Init.Datatypes.O
Locate I.Dont.Exist.
  No object of suffix I.Dont.Exist

## Printing flags

Flag Fast Name Printing

  When this flag is turned on, Rocq 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

Rocq 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 Rocq's toplevel. This kind of file is called a script for Rocq. The standard (and default) extension of Rocq's script files is .v.

Command Load Verbose? string​ident

  Loads a file. If `ident` is specified, the command loads a file named `ident.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, Rocq 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`; use `Require` instead. `Require` loads `.vo` files that were previously compiled from `.v` files.

  `Verbose` displays the Rocq output for each command and tactic in the loaded file, as if the commands and tactics were entered interactively.

  Error Can’t find file ident on loadpath.
  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 The Rocq Prover 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 Import​Export import_categories?? filtered_import+
  dirpath`::=`ident .* ident``

  Loads compiled files into the Rocq environment. For the first `qualid` in each `filtered_import`, the command looks in the load path for a compiled file `ident.vo` whose logical name has the form `dirpath.identimplicit.*qualid` (if `From dirpath` is given) or `identimplicit.*qualid` (if the optional `From` clause is absent). `identimplicit.*` represents the parts of the fully qualified name that are implicit. For example, `From Stdlib Require Nat` loads `Stdlib.Init.Nat` and `Init` is implicit. `ident` is the final component of the `qualid`.

  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 Rocq.

  - `Import` - additionally does an `Import` on the loaded module, making components defined in the module available by their short names

  - `Export` - additionally does an `Export` 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` or `Export` are present, the command also does the equivalent of the `Import` or `Export` 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 file `path/Foo/File.vo` with the logical name `Lib.Foo.File`. It allows this file to be loaded through `Require Lib.Foo.File`, `From Lib Require Foo.File`, `From Lib Require File` or `From Lib.Foo Require File`. The `-R path Lib` command line parameter allows loading the file with the additional alternatives `Require Foo.File` and `Require 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.identimplicit.*qualid` or `identimplicit.*qualid` (that is, matches where the implicit part is empty). For both exact and other matches, local loadpaths are considered first, then installed ones. Paths considered as installed are typically the `user-contrib` directory and paths provided via the `ROCQPATH` environment variable, see `Print LoadPath`. In each attempt (exact local, exact installed, local and installed), several matching files are signaled by an error.

  The difference between the `-R` and the `-Q` option is that non-exact matches are allowed for `-Q` only if `From` 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 load qualid: no physical path bound to dirpath.
  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 file1.vo, file2.vo, ...).

    Either the file to load must be required with a more discriminating suffix (at worst, with its full logical name) or there is an error in the configuration (command line arguments or environment variables).

  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 library `qualid` which is not the one already loaded in the current Rocq session. Probably `ident.v` was not properly recompiled with the last version of the file containing module `qualid`.

  Error Bad magic number.

    The file `ident.vo` was found but either it is not a Rocq compiled module, or it was compiled with an incompatible version of Rocq.

  Error The file ident.vo contains library qualid1 and not library qualid2.

    The library `qualid2` is indirectly required by a `Require`. The load path maps `qualid2` to `ident.vo`, which was compiled using a load path that bound it to `qualid1`. Usually the appropriate solution is to recompile `ident.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` and `Export` commands can be used inside modules.

    See also

    Chapter The Rocq Prover commands

Command Print Libraries

  This command displays the list of library files loaded in the current Rocq session.

Command Declare ML Module string+

  Loads OCaml plugins and their dependencies dynamically. The `string` arguments must be valid findlib plugin names, for example `rocq-runtime.plugins.ltac`.

  Effects (such as adding new commands) from the explicitly requested plugin are activated, but effects from implicitly loaded dependencies are not activated.

  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 by `findlib` by running `ocamlfind printconf` and get the list of available libraries by running `ocamlfind list | grep coq` (Coq libraries are typically named `coq-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 of `META` file and placing it in a place where `findlib` can see it. Different build systems provide different helpers to do this: see here for rocq makefile, and here for Dune.

  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 shared library failed: Coq Error: string is not a valid
  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 the `findlib` plugin name. In the example of `rocq-runtime.plugins.ltac`, one has to write `DECLARE PLUGIN "rocq-runtime.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 Rocq have been removed. Load paths can be managed using Rocq command line options or enviroment variables (see Logical paths and the load path).

Command Print LoadPath dirpath?

  Displays the current Rocq 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. Also prints whether a loadpath is considered installed (`i`) or not, see `Require`.

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 the `rocq dep` tool generated list of dependencies. The file name `string` must exist relative to one of the top directories associated with `dirpath`. `string` can include directory separators (`/`) to select a file in a subdirectory. Path elements in `string` must be valid Rocq 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`.

> Warning File ... found twice in ...

>   The file is found in more than once in the top directories associated with the given `dirpath`. In this case the first occurrence is selected.

## Backtracking

The backtracking commands described in this section can only be used interactively, they cannot be part of a Rocq file loaded via `Load` or compiled by `rocq compile`.

Command Reset ident

  This command removes all the objects in the environment since `ident` was introduced, including `ident`. `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. If `natural` is not specified, the command undoes one sentence. Sentences read from a `.v` file via a `Load` are considered a single sentence. While `Back` can undo tactics and commands executed within proof mode, once you exit proof mode, such as with `Qed`, all the statements executed within are thereafter considered a single sentence. `Back` immediately following `Qed` 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 as `Back` (see above), the `BackTo` command now handles proof states. For that, it may have to undo some extra commands and end on a state `natural′ ≤ natural` if necessary.

## Quitting and debugging

Command Quit

  Causes Rocq to exit. Valid only in `rocq repl-with-drop`.

Command Drop

  This command temporarily enters the OCaml toplevel. It is a debug facility used by Rocq's implementers. Valid only in `rocq repl-with-drop`. The OCaml command:

      #use "include";;

  adds the right loadpaths and loads some toplevel printers for all abstract types of Rocq- 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 Rocq with the command:

      go();;

Command Time sentence

  Executes `sentence` and displays the time needed to execute it.

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 systems, where it instead prints an error message in the place of the instruction count.

Command Profile string? sentence

  Executes `sentence` and displays profiling information. If `string` is given, a full trace is written to "`string`.json".

  If `string` is a relative filename, it refers to the directory specified by the command line option `-output-directory`, if set and otherwise, the current directory. Use `Pwd` to display the current directory.

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. Use `Pwd` to display the current directory.

Command Timeout natural sentence

  Executes `sentence`. If the operation has not terminated after `natural` seconds, then it is interrupted and an error message is displayed.

  Option Default Timeout natural

    When this option is set, each `sentence` is treated as if it was prefixed with `Timeout` `natural`, except for `Timeout` commands themselves. If unset, no timeout is applied.

Command Fail sentence

  For debugging scripts, sometimes it is desirable to know whether a command or a tactic fails. If `sentence` fails, then `Fail 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.

  Error The command has not failed!

    If the given `command` succeeds, then `Fail sentence` fails with this error message.

Command Succeed sentence

  If `sentence` succeeds, then `Succeed sentence` succeeds without changing the proof state. If `sentence` fails, then `Succeed sentence` fails showing the error message for `sentence`. In interactive mode, the system prints the message `The 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

Flag Silent

  This flag controls the normal displaying.

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 category `default` contains the warnings enabled by default.

  Rocq 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`, `rewrite-rules`, `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 flags `Printing Implicit`, `Printing Coercions`, `Printing Synth`, `Printing Projections`, and `Printing Notations`. To reactivate the high-level printing features, use the command `Unset 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 use `Undelimit Scope` and/or `Close 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 with `Printing All` would make the goal unreadable.

Flag Printing Fully Qualified

  When this flag is turned on, all names (global references such as constants, inductives, constructors, and section variables, as well as modules, module types, universes, etc) are printed using their fully qualified paths. This is useful when there are multiple objects with the same short name in different modules, and you want to clearly distinguish them.

  For example, if you have both `Foo.ax` and `Bar.ax` defined, turning on this flag will ensure they are printed as `Module.Foo.ax` and `Module.Bar.ax` respectively (where `Module` is the top-level module name), rather than potentially ambiguous short names.

  This flag is off by default.

## 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= yes​no?)

  This boolean attribute is similar to the `Guard Checking` flag, but on a per-declaration basis. Disable guard checking locally with `bypass_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= yes​no?)

  This boolean attribute is similar to the `Positivity Checking` flag, but on a per-declaration basis. Disable positivity checking locally with `bypass_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= yes​no?)

  This boolean attribute is similar to the `Universe Checking` flag, but on a per-declaration basis. Disable universe checking locally with `bypass_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 qualid1 as qualid2

  Makes the constant `qualid1` accessible to OCaml libraries under the name `qualid2`. The constant can then be dynamically located in OCaml code by calling `Rocqlib.lib_ref "qualid2"`. 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 `qualid2` is `kernel`, the constant is exposed to the kernel. For instance, the `PrimInt63` 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.

  This command supports attributes `local`, `export` and `global`. The default is `global`, even inside sections.

  See also

  Primitive Integers

Command Print Registered

  List the currently registered constants.

Command Register Scheme qualid1 as qualid2 for qualid3

  Make the constant `qualid1` accessible to the "scheme" mechanism for scheme kind `qualid2` and inductive `qualid3`.

  This command supports attributes `local`, `export` and `global`. The default is `global`, even inside sections.

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

Command Register Inline qualid

  Gives a hint to the reduction machines (VM and native) that the body of the constant `qualid` should be inlined in the generated code.

### Registering primitive operations

Command Primitive ident_decl : term? := #ident

  Makes the primitive type or primitive operator `#ident` defined in OCaml accessible in Rocq commands and tactics. For internal use by implementors of Rocq'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` and `PrimFloat.v` use `Primitive` 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 and `Register` with the `kernel` prefix for other types. For example, in `PrimInt63.v`, `#int63_type` must be declared before the associated operations.

  Error The type ident must be registered before this construction can be typechecked.

    The type must be defined with `Primitive` command before this `Primitive` command (declaring an operation using the type) will succeed.

Other versions v: 9.2

Versions
  dev
  stable
  9.2
  9.1
  9.0
  8.20
  8.19
  8.18
  8.17
  8.16
  8.15
  8.14
  8.13
  8.12
  8.11
  8.10
  8.9
  8.8
  8.7
  8.6
  8.5
  8.4
  8.3
  8.2
  8.1
  8.0

Downloads
  PDF