The Rocq Prover
9.0+alpha
  • Introduction and Contents

Specification language

  • Core language
    • Basic notions and conventions
      • Syntax and lexical conventions
        • Syntax conventions
        • Lexical conventions
      • Essential vocabulary
      • Settings
        • Attributes
        • Flags, Options and Tables
    • Sorts
    • Functions and assumptions
      • Binders
      • Functions (fun) and function types (forall)
      • Function application
      • Assumptions
    • Definitions
      • Let-in definitions
      • Type cast
      • Top-level definitions
      • Assertions and proofs
    • Conversion rules
      • α-conversion
      • β-reduction
      • δ-reduction
      • ι-reduction
      • ζ-reduction
      • η-expansion
      • Examples
      • Proof Irrelevance
      • Convertibility
    • Typing rules
      • The terms
      • Typing rules
      • Subtyping rules
      • The Calculus of Inductive Constructions with impredicative Set
    • Variants and the match construct
      • Variants
        • Private (matching) inductive types
      • Definition by cases: match
    • Record types
      • Defining record types
      • Constructing records
      • Accessing fields (projections)
      • Settings for printing records
      • Primitive Projections
        • Reduction
        • Compatibility Constants for Projections
    • Inductive types and recursive functions
      • Inductive types
        • Simple inductive types
        • Simple indexed inductive types
        • Parameterized inductive types
        • Mutually defined inductive types
      • Recursive functions: fix
      • Top-level recursive functions
      • Theory of inductive definitions
        • Types of inductive objects
        • Well-formed inductive definitions
        • Destructors
        • Fixpoint definitions
    • Coinductive types and corecursive functions
      • Coinductive types
        • Caveat
      • Co-recursive functions: cofix
      • Top-level definitions of corecursive functions
    • Sections
      • Using sections
      • Summary of locality attributes in a section
      • Typing rules used at the end of a section
    • The Module System
      • Modules and module types
      • Using modules
        • Examples
      • Qualified names
      • Controlling the scope of commands with locality attributes
      • Summary of locality attributes in a module
      • Typing Modules
    • Primitive objects
      • Primitive Integers
      • Primitive Floats
      • Primitive Arrays
      • Primitive (Byte-Based) Strings
    • Polymorphic Universes
      • General Presentation
      • Polymorphic, Monomorphic
      • Cumulative, NonCumulative
        • Specifying cumulativity
        • Cumulativity Weak Constraints
      • Global and local universes
      • Conversion and unification
      • Minimization
      • Explicit Universes
      • Printing universes
        • Polymorphic definitions
      • Sort polymorphism
      • Universe polymorphism and sections
    • SProp (proof irrelevant propositions)
      • Basic constructs
      • Encodings for strict propositions
      • Definitional UIP
        • Non Termination with UIP
      • Debugging \(\SProp\) issues
    • User-defined rewrite rules
      • Symbols
      • Rewrite rules
      • Pattern syntax
      • Higher-order pattern holes
      • Universe polymorphic rules
      • Rewrite rules, type preservation, confluence and termination
      • Compatibility with the eta laws
      • Level of support
  • Language extensions
    • Existential variables
      • Inferable subterms
      • e* tactics that can create existential variables
      • Automatic resolution of existential variables
      • Explicit display of existential instances for pretty-printing
      • Solving existential variables using tactics
    • Implicit arguments
      • The different kinds of implicit arguments
        • Implicit arguments inferable from the knowledge of other arguments of a function
        • Implicit arguments inferable by resolution
      • Maximal and non-maximal insertion of implicit arguments
        • Trailing Implicit Arguments
      • Casual use of implicit arguments
      • Declaration of implicit arguments
        • Implicit Argument Binders
        • Mode for automatic declaration of implicit arguments
        • Controlling strict implicit arguments
        • Controlling contextual implicit arguments
        • Controlling reversible-pattern implicit arguments
        • Controlling the insertion of implicit arguments not followed by explicit arguments
        • Combining manual declaration and automatic declaration
      • Explicit applications
      • Displaying implicit arguments
      • Displaying implicit arguments when pretty-printing
      • Interaction with subtyping
      • Deactivation of implicit arguments for parsing
      • Implicit types of variables
      • Implicit generalization
    • Extended pattern matching
      • Variants and extensions of match
        • Multiple and nested pattern matching
        • Pattern-matching on boolean values: the if expression
        • Irrefutable patterns: the destructuring let variants
        • Controlling pretty-printing of match expressions
        • Conventions about unused pattern-matching variables
      • Patterns
      • Multiple patterns
      • Aliasing subpatterns
      • Nested patterns
      • Disjunctive patterns
      • About patterns of parametric types
        • Parameters in patterns
      • Implicit arguments in patterns
      • Matching objects of dependent types
      • Understanding dependencies in patterns
      • When the elimination predicate must be provided
        • Dependent pattern matching
        • Multiple dependent pattern matching
        • Patterns in in
      • Using pattern matching to write proofs
      • Pattern-matching on inductive objects involving local definitions
      • Pattern-matching and coercions
      • When does the expansion strategy fail?
    • Syntax extensions and notation scopes
      • Notations
        • Basic notations
        • Precedences and associativity
        • Complex notations
        • Simple factorization rules
        • Use of notations for printing
        • The Infix command
        • Reserving notations
        • Simultaneous definition of terms and notations
        • Enabling and disabling notations
        • Displaying information about notations
        • Locating notations
        • Inheritance of the properties of arguments of constants bound to a notation
        • Notations and binders
        • Notations with recursive patterns
        • Notations with recursive patterns involving binders
        • Predefined entries
        • Custom entries
        • Syntax
      • Notation scopes
        • Global interpretation rules for notations
        • Local interpretation rules for notations
        • The type_scope notation scope
        • The function_scope notation scope
        • Notation scopes used in the standard library of Rocq
        • Displaying information about scopes
      • Abbreviations
      • Numbers and strings
        • Number notations
        • String notations
      • Tactic Notations
    • Setting properties of a function's arguments
      • Manual declaration of implicit arguments
      • Automatic declaration of implicit arguments
      • Renaming implicit arguments
      • Binding arguments to scopes
      • Effects of Arguments on unfolding
      • Bidirectionality hints
    • Implicit Coercions
      • General Presentation
      • Coercion Classes
      • Coercions
      • Reversible Coercions
      • Identity Coercions
      • Inheritance Graph
      • Coercion Classes
      • Displaying Available Coercions
      • Activating the Printing of Coercions
      • Classes as Records
      • Coercions and Sections
      • Coercions and Modules
      • Examples
    • Typeclasses
      • Typeclass and instance declarations
      • Binding typeclasses
      • Parameterized instances
      • Sections and contexts
      • Building hierarchies
        • Superclasses
        • Substructures
      • Command summary
        • Typeclasses Transparent, Typeclasses Opaque
        • Settings
        • Typeclasses eauto
    • Canonical Structures
      • Declaration of canonical structures
      • Notation overloading
        • Derived Canonical Structures
      • Hierarchy of structures
        • Compact declaration of Canonical Structures
    • Program
      • Elaborating programs
        • Syntactic control over equalities
        • Program Definition
        • Program Fixpoint
        • Program Lemma
      • Solving obligations
      • Frequently Asked Questions
    • Commands
      • Displaying
      • Query commands
      • Requests to the environment
      • Printing flags
      • Loading files
      • Compiled files
      • Load paths
      • Extra Dependencies
      • Backtracking
      • Quitting and debugging
      • Controlling display
      • Printing constructions in full
      • Controlling Typing Flags
      • Internal registration commands
        • Exposing constants to OCaml libraries
        • Inlining hints for the fast reduction machines
        • Registering primitive operations

Proofs

  • Basic proof writing
    • Proof mode
      • Proof State
      • Entering and exiting proof mode
        • Proof using options
        • Name a set of section hypotheses for Proof using
      • Proof modes
      • Managing goals
        • Focusing goals
        • Shelving goals
        • Reordering goals
      • Proving a subgoal as a separate lemma: abstract
      • Requesting information
      • Showing differences between proof steps
        • How to enable diffs
        • How diffs are calculated
        • "Show Proof" differences
      • Delaying solving unification constraints
      • Proof maintenance
      • Controlling proof mode
      • Controlling memory usage
    • Tactics
      • Common elements of tactics
        • Reserved keywords
        • Invocation of tactics
        • Bindings
        • Intro patterns
        • Occurrence clauses
      • Applying theorems
      • Managing the local context
      • Controlling the proof flow
      • Classical tactics
      • Performance-oriented tactic variants
    • Reasoning with equalities
      • Tactics for simple equalities
      • Rewriting with Leibniz and setoid equality
      • Rewriting with definitional equality
      • Applying conversion rules
        • Fast reduction tactics: vm_compute and native_compute
        • Computing in a term: eval and Eval
      • Controlling reduction strategies and the conversion algorithm
    • Reasoning with inductive types
      • Applying constructors
      • Case analysis
      • Induction
      • Equality of inductive types
        • Helper tactics
      • Generation of induction principles with Scheme
        • Automatic declaration of schemes
        • Combined Scheme
      • Generation of inversion principles with Derive Inversion
      • Examples of dependent destruction / dependent induction
        • A larger example
    • The SSReflect proof language
      • Introduction
        • Acknowledgments
      • Usage
        • Getting started
        • Compatibility issues
      • Gallina extensions
        • Pattern assignment
        • Pattern conditional
        • Parametric polymorphism
        • Anonymous arguments
        • Wildcards
        • Definitions
        • Abbreviations
        • Basic localization
      • Basic tactics
        • Bookkeeping
        • The defective tactics
        • Discharge
        • Introduction in the context
        • Generation of equations
        • Type families
      • Control flow
        • Indentation and bullets
        • Terminators
        • Selectors
        • Iteration
        • Localization
        • Structure
      • Rewriting
        • An extended rewrite tactic
        • Remarks and examples
        • Rewriting under binders
        • Locking, unlocking
        • Congruence
      • Contextual patterns
        • Syntax
        • Matching contextual patterns
        • Examples
        • Patterns for recurrent contexts
      • Views and reflection
        • Interpreting eliminations
        • Interpreting assumptions
        • Interpreting goals
        • Boolean reflection
        • The reflect predicate
        • General mechanism for interpreting goals and assumptions
        • Interpreting equivalences
        • Declaring new Hint Views
        • Multiple views
        • Additional view shortcuts
      • Synopsis and Index
        • Parameters
        • Items and switches
        • Tactics
        • Tacticals
        • Commands
        • Settings
  • Automatic solvers and programmable tactics
    • Solvers for logic and equality
    • Micromega: solvers for arithmetic goals over ordered rings
      • Short description of the tactics
      • Positivstellensatz refutations
      • lra: a decision procedure for linear real and rational arithmetic
      • lia: a tactic for linear integer arithmetic
        • High level view of lia
        • Cutting plane proofs
        • Case split
      • nra: a proof procedure for non-linear arithmetic
      • nia: a proof procedure for non-linear integer arithmetic
      • psatz: a proof procedure for non-linear arithmetic
      • zify: pre-processing of arithmetic goals
    • ring and field: solvers for polynomial and rational equations
      • What does this tactic do?
      • The variables map
      • Is it automatic?
      • Concrete usage
      • Adding a ring structure
      • How does it work?
      • Dealing with fields
      • Adding a new field structure
      • History of ring
      • Discussion
    • Nsatz: a solver for equalities in integral domains
      • More about nsatz
    • Programmable proof search
      • Tactics
      • Hint databases
        • Creating hint databases
        • Hint databases defined in the Rocq standard library
      • Creating Hints
        • Hint locality
      • Setting implicit automation tactics
    • Generalized rewriting
      • Introduction to generalized rewriting
        • Relations and morphisms
        • Adding new relations and morphisms
        • Rewriting and nonreflexive relations
        • Rewriting and nonsymmetric relations
        • Rewriting in ambiguous setoid contexts
        • Rewriting with Type valued relations
      • Declaring rewrite relations
      • Commands and tactics
        • First class setoids and morphisms
        • Tactics enabled on user provided relations
        • Printing relations and morphisms
        • Deprecated syntax and backward incompatibilities
      • Extensions
        • Rewriting under binders
        • Subrelations
        • Constant unfolding during rewriting
        • Constant unfolding during Proper-instance search
      • Strategies for rewriting
        • Usage
        • Definitions
  • Creating new tactics
    • Ltac
      • Defects
      • Syntax
      • Values
        • Syntactic values
        • Substitution
        • Local definitions: let
        • Function construction and application
        • Tactics in terms
      • Goal selectors
      • Processing multiple goals
      • Branching and backtracking
      • Control flow
        • Sequence: ;
        • Do loop
        • Repeat loop
        • Catching errors: try
        • Conditional branching: tryif
      • Alternatives
        • Branching with backtracking: +
        • Local application of tactics: [> ... ]
        • First tactic to succeed
        • Solving
        • First tactic to make progress: ||
        • Detecting progress
      • Success and failure
        • Checking for success: assert_succeeds
        • Checking for failure: assert_fails
        • Failing
        • Soft cut: once
        • Checking for a single success: exactly_once
      • Manipulating values
        • Pattern matching on terms: match
        • Pattern matching on goals and hypotheses: match goal
        • Filling a term context
        • Generating fresh hypothesis names
        • Computing in a term: eval
        • Getting the type of a term
        • Manipulating untyped terms: type_term
        • Counting goals: numgoals
        • Testing boolean expressions: guard
        • Checking properties of terms
      • Timing
        • Timeout
        • Timing a tactic
        • Timing a tactic that evaluates to a term: time_constr
      • Print/identity tactic: idtac
      • Tactic toplevel definitions
        • Defining Ltac symbols
        • Printing Ltac tactics
      • Examples of using Ltac
        • Proof that the natural numbers have at least two elements
        • Proving that a list is a permutation of a second list
        • Deciding intuitionistic propositional logic
        • Deciding type isomorphisms
      • Debugging Ltac tactics
        • Backtraces
        • Tracing execution
        • Interactive debugger
        • Profiling Ltac tactics
        • Run-time optimization tactic
    • Ltac2
      • General design
      • ML component
        • Overview
        • Type Syntax
        • Type declarations
        • APIs
        • Term Syntax
        • Ltac2 Definitions
        • Printing Ltac2 tactics
        • Reduction
        • Typing
        • Effects
      • Meta-programming
        • Overview
        • Quotations
        • Term Antiquotations
        • Match over terms
        • Match over goals
        • Match on values
      • Notations
        • Abbreviations
        • Defining tactics
        • Syntactic classes
      • Evaluation
      • Debug
      • Profiling
      • Compatibility layer with Ltac1
        • Ltac1 from Ltac2
        • Ltac2 from Ltac1
        • Switching between Ltac languages
      • Transition from Ltac1
        • Syntax changes
        • Tactic delay
        • Variable binding
        • Exception catching

Using the Rocq Prover

  • Libraries and plugins
    • The Coq libraries
      • The prelude
        • Notations
        • Logic
        • Datatypes
        • Specification
        • Basic Arithmetic
        • Well-founded recursion
        • Tactics
      • Users’ contributions
    • Program extraction
      • Generating ML Code
      • Extraction Options
        • Setting the target language
        • Inlining and optimizations
        • Extra elimination of useless arguments
        • Realizing axioms
        • Realizing inductive types
        • Generating FFI Code
        • Avoiding conflicts with existing filenames
        • Additional settings
      • Differences between Rocq and ML type systems
      • Some examples
        • A detailed example: Euclidean division
        • Extraction's horror museum
        • Users' Contributions
    • Program derivation
    • Functional induction
      • Advanced recursive functions
      • Tactics
      • Generation of induction principles with Functional Scheme
    • Writing Rocq libraries and plugins
      • Deprecating library objects, tactics or library files
      • Triggering warning for library objects or library files
  • Command-line and graphical tools
    • Building Rocq Projects
      • Rocq configuration basics
        • Installing the Rocq Prover and Rocq packages with opam
        • Setup for working on your own projects
        • Building a project with _CoqProject (overview)
        • Logical paths and the load path
        • Modifying multiple interdependent projects at the same time
        • Installed and uninstalled packages
        • Upgrading to a new version of Rocq
      • Building a Rocq project with rocq makefile (details)
        • Comments
      • Building a Rocq project with Dune
      • rocq dep: Computing Module dependencies
      • Split compilation of native computation files
      • Using Rocq as a library
      • Embedded Rocq phrases inside LaTeX documents
      • Man pages
    • The Rocq Prover commands
      • Interactive use (rocq repl)
      • Batch compilation (rocq compile)
      • Customization at launch time
      • Command parameters
        • coqrc start up script
        • Environment variables
        • Command line options
      • Profiling
      • Compiled interfaces (produced using -vos)
      • Compiled libraries checker (rocqchk)
    • Documenting Rocq files with rocq doc
      • Principles
        • Rocq material inside documentation.
        • Pretty-printing.
        • Sections
        • Lists.
        • Rules.
        • Emphasis.
        • Escaping to LaTeX and HTML.
        • Verbatim
        • Hyperlinks
        • Hiding / Showing parts of the source
      • Usage
        • Command line options
      • The rocq doc LaTeX style file
    • CoqIDE
      • Managing files and buffers, basic editing
      • Running Coq scripts
      • Asynchronous mode
      • Commands and templates
      • Queries
      • Compilation
      • Customizations
        • Preferences
        • Key bindings
      • Using Unicode symbols
        • Displaying Unicode symbols
        • Bindings for input of Unicode symbols
        • Adding custom bindings
        • Character encoding for saved files
      • Debugger
        • Breakpoints
        • Call Stack and Variables
        • Supported use cases
    • Asynchronous and Parallel Proof Processing
      • Proof annotations
        • Automatic suggestion of proof annotations
      • Proof blocks and error resilience
        • Caveats
      • Interactive mode
      • Limiting the number of parallel workers
        • Caveats

Appendix

  • History and recent changes
    • Early history of Coq
      • Historical roots
      • Versions 1 to 5
        • Version 1
        • Version 2
        • Version 3
        • Version 4
        • Version 5
      • Versions 6
        • Version 6.1
        • Version 6.2
        • Version 6.3
      • Versions 7
        • Summary of changes
        • Details of changes in 7.0 and 7.1
        • Details of changes in 7.2
        • Details of changes in 7.3
        • Details of changes in 7.4
    • Recent changes
      • Version 8.20
        • Summary of changes
        • Changes in 8.20.0
      • Version 8.19
        • Summary of changes
        • Changes in 8.19.0
        • Changes in 8.19.1
        • Changes in 8.19.2
      • Version 8.18
        • Summary of changes
        • Changes in 8.18.0
      • Version 8.17
        • Summary of changes
        • Changes in 8.17.0
        • Changes in 8.17.1
      • Version 8.16
        • Summary of changes
        • Changes in 8.16.0
        • Changes in 8.16.1
      • Version 8.15
        • Summary of changes
        • Changes in 8.15.0
        • Changes in 8.15.1
        • Changes in 8.15.2
      • Version 8.14
        • Summary of changes
        • Changes in 8.14.0
        • Changes in 8.14.1
      • Version 8.13
        • Summary of changes
        • Changes in 8.13+beta1
        • Changes in 8.13.0
        • Changes in 8.13.1
        • Changes in 8.13.2
      • Version 8.12
        • Summary of changes
        • Changes in 8.12+beta1
        • Changes in 8.12.0
        • Changes in 8.12.1
        • Changes in 8.12.2
      • Version 8.11
        • Summary of changes
        • Changes in 8.11+beta1
        • Changes in 8.11.0
        • Changes in 8.11.1
        • Changes in 8.11.2
      • Version 8.10
        • Summary of changes
        • Other changes in 8.10+beta1
        • Changes in 8.10+beta2
        • Changes in 8.10+beta3
        • Changes in 8.10.0
        • Changes in 8.10.1
        • Changes in 8.10.2
      • Version 8.9
        • Summary of changes
        • Details of changes in 8.9+beta1
        • Changes in 8.8.0
        • Changes in 8.8.1
      • Version 8.8
        • Summary of changes
        • Details of changes in 8.8+beta1
        • Details of changes in 8.8.0
        • Details of changes in 8.8.1
        • Details of changes in 8.8.2
      • Version 8.7
        • Summary of changes
        • Potential compatibility issues
        • Details of changes in 8.7+beta1
        • Details of changes in 8.7+beta2
        • Details of changes in 8.7.0
        • Details of changes in 8.7.1
        • Details of changes in 8.7.2
      • Version 8.6
        • Summary of changes
        • Potential sources of incompatibilities
        • Details of changes in 8.6beta1
        • Details of changes in 8.6
        • Details of changes in 8.6.1
      • Version 8.5
        • Summary of changes
        • Potential sources of incompatibilities
        • Details of changes in 8.5beta1
        • Details of changes in 8.5beta2
        • Details of changes in 8.5beta3
        • Details of changes in 8.5
        • Details of changes in 8.5pl1
        • Details of changes in 8.5pl2
        • Details of changes in 8.5pl3
      • Version 8.4
        • Summary of changes
        • Potential sources of incompatibilities
        • Details of changes in 8.4beta
        • Details of changes in 8.4beta2
        • Details of changes in 8.4
      • Version 8.3
        • Summary of changes
        • Details of changes
      • Version 8.2
        • Summary of changes
        • Details of changes
      • Version 8.1
        • Summary of changes
        • Details of changes in 8.1beta
        • Details of changes in 8.1gamma
        • Details of changes in 8.1
      • Version 8.0
        • Summary of changes
        • Details of changes in 8.0beta old syntax
        • Details of changes in 8.0beta new syntax
        • Details of changes in 8.0
  • Indexes
    • Glossary index
    • Command index
    • Tactic index
    • Attribute index
    • Flags, options and tables index
    • Errors and warnings index
    • Index
  • Bibliography
The Rocq Prover
  • »
  • Search

© Copyright 1999-2024, Inria, CNRS and contributors.

Built with Sphinx using a theme provided by Read the Docs.
Other versions v: 9.0+alpha
Versions
dev
stable
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