Compendium

Coq (Rocq) — Reference

10 min read

Coq (Rocq) — Reference

Source: https://rocq-prover.org/

Coq (Rocq) — Reference

2025 rename: The project formerly known as Coq (1989-2025) was renamed to The Rocq Prover. Timeline: rename announced 2023-10-11 by the dev team; officially completed with the Rocq 9.0.0 release on 2025-03-12 (https://rocq-prover.org/releases/9.0.0). Subsequent releases (9.1, 9.2) carry the Rocq name natively. The kernel, language, and tactic system are unchanged — this is a rebranding, not a fork. The new name honors Inria Rocquencourt, the original development site. The canonical slug for this note remains coq for backward compatibility; the current project URL is https://rocq-prover.org/ (legacy https://coq.inria.fr/ now redirects there).

  • Created: 1984 (initial development by Thierry Coquand and Gérard Huet at INRIA); first public release as “Coq” 1989. Renamed Rocq 2025.
  • Latest stable: Rocq 9.2.0 (per https://rocq-prover.org/, 2025); the Rocq Platform 2025.08 bundles the prover with curated libraries.
  • Owner / steward: Inria (national lead) plus a distributed core team across academic institutions; community governance via the Rocq Team and an enhancement-process (CEP) model. https://rocq-prover.org/about
  • Paradigms: Dependently-typed functional language plus interactive tactic-based proof assistant; dual-purpose like Lean and Agda but with much heavier emphasis on the proof side.
  • Typing: pCuIC — Polymorphic Cumulative Calculus of Inductive Constructions (impredicative Prop, predicative cumulative Type hierarchy).
  • Memory: Implemented in OCaml; proofs and terms live on the OCaml heap with OCaml’s GC. Extracted code uses the target language’s runtime.
  • Compilation: The kernel checks proofs; user proofs are normally interpreted, but vm_compute and native_compute (via OCaml’s native compiler) provide fast reduction. Code is extracted to OCaml/Haskell/Scheme for execution.
  • Primary domains: Formal verification (CompCert, certified compilers, cryptographic protocols), formalized mathematics (Four-Color, Feit-Thompson), program logic research, type-theory research itself.
  • Official docs: https://rocq-prover.org/ • https://rocq-prover.org/docs/ • Reference manual: https://rocq-prover.org/refman/

At a glance

Rocq (née Coq) is the oldest of the four dependently-typed assistants and the source of much of the type theory the others reuse. Its strengths are a tiny trusted kernel, a very mature Ltac/Ltac2 tactic ecosystem, and decades of accumulated formalizations. Its weaknesses (compared to Lean 4) are a slower elaborator, awkward dependent pattern matching without the Equations plugin, and a more arcane module system. Source: https://rocq-prover.org/about, https://rocq-prover.org/docs/.

Getting started

  • Install: Use opam (the OCaml package manager):

    opam install rocq-prover         # or: opam install coq (legacy alias)

    Or install the Rocq Platform for a curated bundle (https://github.com/rocq-prover/platform). Windows users: the Platform installer is the easy path.

  • Editor: VsRocq (VS Code, https://github.com/rocq-prover/vsrocq), Proof General (Emacs, https://proofgeneral.github.io/), CoqIDE (ships with the prover; will be renamed RocqIDE).

  • Hello world:

    Definition hello : string := "Hello, Rocq!".

    Or a smallest proof:

    Theorem identity : forall (A : Type) (a : A), a = a.
Proof. intros. reflexivity. Qed.

  • Project layout: A _CoqProject file lists source files and module roots:

    -Q theories MyProj
theories/Foo.v
theories/Bar.v

    Build with coq_makefile -f _CoqProject -o Makefile && make, or use dune (https://github.com/rocq-prover/rocq/wiki/Dune).

  • REPL / proof env: rocq top (or coqtop) is the interactive toplevel; in practice everyone uses Proof General or VsRocq, which keep the proof state visible and stepped.

Basics

  • Types & literals: nat, Z (BinInt.Z — binary integers), bool, string, list A, option A, prod A B. Numeric literals are notation; Open Scope nat_scope. etc.

  • Variables / scoping: let x := e in body. Section / End for shared parameters; Variable, Hypothesis, Context.

  • Control flow: Pure functional. if cond then a else b works on any 2-constructor inductive (most commonly bool). match e with ... end.

  • Functions:

    Fixpoint length {A} (xs : list A) : nat :=
  match xs with
  | nil => 0
  | _ :: rest => S (length rest)
  end.

    All Fixpoints must be syntactically structurally recursive; otherwise use Function, Program Fixpoint, or Equations.

  • Strings: String (cons-cell strings of bytes — surprisingly inefficient; use bytestring libs for real work).

  • Collections: list, option, Vector.t n A (length-indexed), Ensemble, FSet/FMap (functorial sets/maps from the stdlib’s module system). Coq.MSets and Coq.FSets are the practical interfaces.

Intermediate

  • Type system depth: pCuIC. Prop is impredicative (you can quantify over all of Prop in Prop); Type is predicative with cumulative universes (Type@{i} ⊆ Type@{i+1}). SProp (definitionally proof-irrelevant Prop) added in 8.10. Inductive types include indexed families, mutual blocks, and (with extensions) coinductive types via CoFixpoint.
  • Modules: Module system is a separate language layer with functors (parameterized modules), Module Type signatures, refinement, and inclusion. Powerful but syntactically heavy. (https://rocq-prover.org/refman/language/core/modules.html)
  • Error handling: Pure programs use option/sum. Tactics that fail are caught with try, ;, ||, first [...]. Extracted code maps to the target language’s exceptions.
  • Concurrency primitives: None at the language level — Rocq is a checker, not a runtime. Extracted programs inherit the target language’s concurrency.
  • I/O: None in the kernel. Extracted code does I/O via the target language. The coq-extraction toolchain emits OCaml/Haskell/Scheme.
  • Stdlib highlights: Coq.Init, Coq.Arith, Coq.ZArith, Coq.Reals (classical reals), Coq.Lists, Coq.MSets, Coq.Strings, Coq.Logic. Most “real” math users prefer mathcomp (https://math-comp.github.io/) — Gonthier’s small-scale-reflection library powering the Feit-Thompson formalization.

Advanced

  • Memory / GC: OCaml-runtime; not user-controlled.
  • Concurrency: N/A (see above).
  • FFI: No direct FFI in the language. Plugins extend the toplevel via the OCaml plugin API (https://rocq-prover.org/refman/using/tools/plugin.html). For verified-and-runnable code, write the program in Rocq, prove it, then Extraction to OCaml/Haskell.
  • Reflection:
    • Ltac reflection — pattern-match on terms inside tactics.
    • MetaCoq (https://metacoq.github.io/) — Coq formalized in Coq. Lets you reify terms, manipulate them as data, then unquote. Used to build verified plugins and certifying type-checkers.
  • Performance tools:
    • vm_compute — bytecode VM reduction (fast).
    • native_compute — compiles the term via OCaml’s native compiler then runs it (fastest).
    • Time, Time Eval, Profile commands.
    • coqchk — re-checks a compiled .vo from scratch using only the kernel.
  • Tactics & proof automation:
    • auto, eauto, intuition, tauto, congruence, lia (linear integer arithmetic), nia, lra, nra, ring, field, omega (deprecated, replaced by lia).
    • Hint databases (Hint Resolve, Hint Rewrite, Hint Constructors).
    • SearchPattern, Search, SearchAbout — lemma discovery.
    • firstorder — first-order proof search.
    • Equations plugin (https://mattam82.github.io/Coq-Equations/) — dependent pattern matching with with clauses, eliminator generation, well-founded recursion. Almost mandatory for serious dependently-typed programming in Rocq.

God mode

  • Ltac vs Ltac2: Ltac is the legacy untyped tactic language — flexible, infamous for surprising failure modes (it backtracks unpredictably and has no static checking). Ltac2 (https://rocq-prover.org/refman/proof-engine/ltac2.html, shipped 8.11) is a typed, OCaml-flavored replacement with first-class tactics, match! for syntactic patterns, and proper exceptions. Use Ltac2 for new tactic libraries.
  • Definitional vs propositional equality: = (eq) is propositional — you prove it. Definitional equality is what the kernel decides automatically (beta/iota/delta/zeta + UIP for SProp). The gap is a constant source of subtle bugs and the reason rewrite exists.
  • Prop vs Set vs Type: Prop (impredicative, eliminates only into Prop modulo singleton elimination), Set (predicative Type@{0}, basically deprecated as a separate concept — most code uses Type), Type@{i} (predicative hierarchy). Universe polymorphism (Polymorphic Definition foo ...) is opt-in but increasingly common.
  • Program mode + obligations: Program Definition / Program Fixpoint lets you write a definition with _ holes that get turned into proof obligations. Useful for sigma-type-laden code.
  • MetaCoq: A Coq plugin that defines Coq’s term language as a Coq inductive type, providing quote and unquote plus a verified type-checker (SafeChecker) and a verified erasure pipeline. The basis for trusted reflection. https://metacoq.github.io/
  • Module system + functors: Parametrize a Module by a Module Type. Used heavily by MSets/FMaps. Notation: Module Foo (X : ORDERED) <: SET. ... End Foo.
  • Notation system: Notation and Reserved Notation define mixfix operators with precedence and associativity, scoped via Open Scope/Bind Scope. Powerful (mathcomp leans on it) and infamous for parsing-conflict errors.
  • Equations plugin: Industrial-strength dependent pattern matching with with/rec/by, eliminator generation (funelim), and graph reasoning. https://mattam82.github.io/Coq-Equations/
  • native_compute vs vm_compute: vm_compute reduces via Coq’s bytecode interpreter (always available, ~100× faster than simpl). native_compute compiles to native via OCaml — another 10-50× on heavy proofs but pulls OCaml at proof time.
  • 2025 Rocq rename + governance: The “Coq” name had grown awkward in international and modern contexts (multiple languages, multiple connotations). After a community poll the Core team chose Rocq (homophone of “rock”, honoring Rocquencourt, the original Inria site). Renaming touched binary names (coqtop → rocq top, coqc → rocq compile) and the file extensions remain .v. Backward-compat aliases retained for one major release. (https://rocq-prover.org/news/2025-05-14-rename-rocq.html, https://rocq-prover.org/about)
  • Famous formalizations:
    • CompCert (Leroy et al., 2006-) — verified optimizing C compiler. https://compcert.org/
    • Four-Color Theorem (Gonthier, 2005) — first major proof done in Coq with reflection.
    • Feit-Thompson Odd Order Theorem (Gonthier et al., 2012) — 170,000 lines of Coq across mathcomp.
    • VST (Verified Software Toolchain) — Hoare-logic verification for C. https://vst.cs.princeton.edu/
    • Iris (https://iris-project.org/) — concurrent separation logic framework.

Idioms & style

  • Naming: lowerCamelCase for definitions in core (addn, subn in mathcomp); some libraries use snake_case. Theorems read like sentences: Nat.add_comm. Tactics named with terse mnemonics by convention.
  • Formatter / linter: No standard formatter. The Rocq Platform CI enforces compile-clean across versions; mathcomp imposes its own style (“small-scale reflection”) with a strong preference for Boolean propositions over Prop propositions (so they’re decidable and apply-able with case/elim).
  • Idiomatic patterns: Use Prop for specifications; reflect to bool for computation (mathcomp’s ==, <= returning bool is canonical). Prefer simpl in *; auto with arith style chains; tag lemmas into hint dbs early; structure proofs with ; (sequential), ;[ t1 | t2 ] (per-goal).
  • What experts look for: Short reflective proofs; absence of Admitted/Axiom; correct use of Polymorphic/Universe Polymorphic; careful kernel-checked extraction; mathcomp-style modules/sections.

Ecosystem

Gotchas

  • Qed. vs Defined.: Qed. makes the proof opaque (kernel checks but body becomes inaccessible). Defined. keeps it transparent (necessary for proofs you’ll compute on later, e.g., dependent definitions).
  • Admitted.: Records the goal as an axiom — the proof is incomplete. Easy to miss in a large project; CI should grep for it.
  • Universe inconsistencies: Cryptic errors when two stacks of Type collide. Add Set Universe Polymorphism. or use explicit universe annotations.
  • Dependent pattern matching is painful without Equations. The built-in match has the “convoy pattern” trap and limited support for indexed types.
  • Ltac is dynamically typed. A typo in a tactic name only fails at proof time. Ltac2 fixes this — migrate when possible.
  • simpl is inscrutable: Its reduction strategy is heuristic and version-dependent. Use cbn (more predictable) or vm_compute/native_compute for closed terms.
  • Notation conflicts: Two libraries that both Open Scope something can produce parse errors that look unrelated. Fix with explicit scope keys ((x + y)%nat).
  • Module-system performance cliff: Heavy use of functors slows everything. Mathcomp uses canonical structures + HB instead.
  • The 2025 rename does not change .v files, but tooling (coq_makefile, coqdep, IDE configs) may need updating to the rocq binaries. Old documentation under coq.inria.fr redirects to rocq-prover.org.

Citations

Graph View