### Install Coq Prover and Verify Installation

Source: https://github.com/rocq-prover/rocq/wiki/Getting-Started

Provides quick command-line instructions for installing the Coq Platform on macOS and Linux, and a command to verify the installation across systems. Windows users are directed to download an installer.

```Shell
brew install coq
```

```Shell
sudo snap install coq-prover
```

```Shell
coqc --version
```

--------------------------------

### Build and Install Rocq and RocqIDE from Source

Source: https://github.com/rocq-prover/rocq/blob/master/INSTALL.md

These commands perform a developer build setup, then compile and install the Rocq runtime, core components, and RocqIDE. The `dune install` command places the compiled binaries and libraries into the specified prefix.

```Shell
make dunestrap
dune build -p rocq-runtime,coq-core,rocq-core,coqide-server,rocqide
dune install --prefix=<install_prefix> rocq-runtime coq-core rocq-core coqide-server rocqide
```

--------------------------------

### Setup GitLab CI Runner for Coq Benchmarking

Source: https://github.com/rocq-prover/rocq/wiki/Benchmarking

This bash script automates the setup of a Linux machine to act as a GitLab CI runner specifically for Coq project benchmarking. It installs essential tools like `opam`, `time`, `linux-perf`, and various development libraries, configures kernel parameters for performance events, and registers the runner with GitLab using a provided token. This setup is crucial for accurate and consistent benchmark execution.

```bash
# opam, time and perf for the bench
# perl and gmp for zarith
# zlib1g-dev for timelog2html
# m4, autoconf and automake for hott and others
# jq for fiat-crypto and zulip posting
# python-is-python3 for test suite's timing table invocation
sudo apt-get install -y curl opam time linux-perf perl libgmp-dev zlib1g-dev m4 automake autoconf jq python-is-python3

sudo bash -c 'echo -1 > /proc/sys/kernel/perf_event_paranoid'
sudo bash -c "echo 'kernel.perf_event_paranoid = -1' > /etc/sysctl.d/00-coq-bench.conf"

curl -L "https://packages.gitlab.com/install/repositories/runner/gitlab-runner/script.deb.sh" | sudo bash

sudo env GITLAB_RUNNER_DISABLE_SKEL=true apt-get install -y gitlab-runner

sudo gitlab-runner register \
     --non-interactive \
     --url 'https://gitlab.com' \
     --registration-token TOKEN \
     --name "$(hostname -f)" \
     --tag-list timing \
     --executor shell

sudo gitlab-runner start
```

--------------------------------

### Install Coq using Homebrew

Source: https://github.com/rocq-prover/rocq/wiki/Installation-of-Coq-on-Mac

Install the Coq proof assistant on macOS systems using the Homebrew package manager. This provides a straightforward way to get Coq up and running.

```Shell
brew install coq
```

--------------------------------

### Install Coq using Nix

Source: https://github.com/rocq-prover/rocq/wiki/Installation-of-Coq-on-Mac

Install the Coq proof assistant using the Nix package manager. This method is suitable for systems leveraging Nix for declarative package management.

```Shell
nix-env -iA nixpkgs.coq
```

--------------------------------

### Launch CoqIDE User Interface

Source: https://github.com/rocq-prover/rocq/wiki/Installation-of-Coq-on-Linux

This command launches the CoqIDE graphical user interface in the background. CoqIDE is a dedicated editor for Coq, providing an interactive environment for writing, checking, and managing Coq proofs. Ensure CoqIDE is part of your Coq Platform installation or installed separately.

```Shell
coqide &
```

--------------------------------

### Coq Tutorial Setup and Module Definition for Extraction Examples

Source: https://github.com/rocq-prover/rocq/wiki/AUGER_ExtractionTuto

This snippet includes the introductory comments for the Coq extraction tutorial, setting the context and scope. It also contains essential setup commands like `Require Import Utf8_core` and `Set Implicit Arguments`, and defines the `Examples1` module to encapsulate the subsequent extraction demonstrations.

```Coq
(** * A small tutorial on extraction to OCaml code from Coq 8.3*)
(**
 This tutorial only contains some hints and examples and is not
 intended to replace the documentation page about
 #<A HREF="Reference-Manual027.html">extraction</A>#.
 This is not very OCaml specific;
 it can also be run with the Haskell extraction for example,
 but comments may be inapropriate.
 Notations are used a lot, to make the code readable,
 so do some #<A HREF="Reference-Manual015.html">trip</A>#
 on notations if you are not very familiar to it.
 This tutorial doesn't use the [Section] mechanism,
 since it is not supported for extraction.
 As I am not used to [Program], I have not used it,
 but I develop here some tools to replace it partially
 (I do not care here of well-foundation for programs).
 The monad system was already used in the Compcert project.
 About the coq version, it is just a hint to tell how old this
 tutorial is, all of this should work on all the 8.x line.
 As making a good tutorial is time consuming, I didn't wrote
 a true tutorial, rather a commented benchmark that the user
 may freely modify for its own tests of the different features.
*)
Require Import Utf8_core.
Set Implicit Arguments.
Module Examples1.
```

```Coq
End Examples1.
```

--------------------------------

### Rocq Build and Setup Commands

Source: https://github.com/rocq-prover/rocq/wiki/DevelopmentTutorial

Essential commands for setting up and building the Rocq project, including bootstrapping Dune for OCaml compilation and executing full project compilation targets.

```Shell
dune build
make dunestrap
make check
make world
```

--------------------------------

### Initialize Rocq Development Shell for Third-Party Project

Source: https://github.com/rocq-prover/rocq/blob/master/dev/ci/nix/README.md

This command executes a shell script to set up a development environment for a specified third-party project (e.g., 'example'). It builds Rocq and other project dependencies, then opens a shell with all required tools, such as `coqtop`, available in the PATH.

```Shell
./dev/ci/nix/shell example
```

--------------------------------

### Configure Rocq Environment Variables via File

Source: https://github.com/rocq-prover/rocq/blob/master/INSTALL.md

This example shows the format for `coq_environment.txt`, a file used to seed environment variables like `ROCQLIB` for Rocq binaries. The values follow OCaml's escaping conventions.

```Text
ROCQLIB="some path"
```

--------------------------------

### Install Python Package Managers on Debian/Ubuntu

Source: https://github.com/rocq-prover/rocq/blob/master/doc/README.md

This `apt` command installs `pip` and `setuptools` on Debian or Ubuntu systems. These tools are essential for managing and installing Python packages, which are dependencies for building the Coq documentation.

```Shell
apt install python3-pip python3-setuptools
```

--------------------------------

### Verify Coq installation

Source: https://github.com/rocq-prover/rocq/wiki/Installation-of-Coq-on-Mac

Run this command in your terminal to check if Coq was successfully installed and to display its version, confirming the installation's integrity.

```Shell
coqc -v
```

--------------------------------

### Install RocqIDE System Dependencies on Debian/Ubuntu

Source: https://github.com/rocq-prover/rocq/blob/master/INSTALL.md

This command installs the necessary GTK and GtkSourceView development libraries required for building RocqIDE on Debian or Ubuntu systems.

```Shell
sudo apt-get install libgtksourceview-3.0-dev
```

--------------------------------

### Set Up OCaml Environment for Rocq with Opam

Source: https://github.com/rocq-prover/rocq/blob/master/INSTALL.md

These commands create a new Opam switch with specific OCaml versions and options, then install the required OCaml packages (dune, ocamlfind, zarith, lablgtk3-sourceview3) for compiling Rocq.

```Shell
opam switch create rocq --packages="ocaml-variants.4.14.1+options,ocaml-option-flambda"
eval $(opam env)
opam install dune ocamlfind zarith lablgtk3-sourceview3
```

--------------------------------

### Manage Rocq Packages with Opam

Source: https://github.com/rocq-prover/rocq/blob/master/doc/sphinx/practical-tools/utilities.rst

Provides common opam commands for listing, installing, and updating Rocq-related packages, including how to add development repositories. Includes an example of listing installed Coq packages and their versions.

```APIDOC
opam list "coq-*"
  - Description: Lists all available and installed Coq packages.
opam list "coq-*" --installed
  - Description: Lists only the installed Coq packages.
opam install <package name>
  - Description: Installs a specified package on your system.
  - Parameters:
    - <package name>: The name of the package to install.
opam update
  - Description: Updates the list of available packages from opam repositories.
opam repo add coq-extra-dev https://rocq-prover.org/opam/extra-dev
  - Description: Adds the 'coq-extra-dev' opam repository to access development packages.
```

```Shell
opam list "coq-*" --installed
```

```Output
coq-bignums               8.15.0          Bignums, the Coq library of arbitrary large numbers
```

--------------------------------

### Install Full LaTeX Dependencies for Coq PDF/PS Documentation on Debian/Ubuntu

Source: https://github.com/rocq-prover/rocq/blob/master/doc/README.md

This command installs the complete TeX Live distribution on Debian/Ubuntu. It provides all LaTeX tools, including `pdflatex`, `dvips`, and `latexmk`, necessary for compiling Coq documentation into PDF and PostScript formats.

```Shell
apt install texlive-full
```

--------------------------------

### Install Minimal LaTeX Dependencies for Coq PDF/PS Documentation on Debian/Ubuntu

Source: https://github.com/rocq-prover/rocq/blob/master/doc/README.md

This command installs a reduced set of TeX Live packages on Debian/Ubuntu, sufficient for building Coq documentation in PDF and PostScript formats. This option saves disk space compared to the full TeX Live installation.

```Shell
apt install texlive-latex-extra texlive-fonts-recommended texlive-xetex \
                latexmk fonts-freefont-otf
```

--------------------------------

### Coq `intros` Proof Tactic

Source: https://github.com/rocq-prover/rocq/wiki/Quick-Reference-for-Beginners

Documentation for the `intros` tactic, which moves `forall` arguments and preconditions into the "known" section of the proof state. It explains its behavior, caveats (e.g., with `induction`), and provides detailed examples demonstrating its effect on proof goals.

```APIDOC
Coq `intros` Proof Tactic:\n\nPurpose:\n  The `intros` tactic separates the proof state into hypotheses (above the ===== line) and the goal (below the ==== line).\n  It works on `forall` arguments and the first arguments to `implies`.\n\nBehavior:\n  If the goal is `forall x y, x < y -> x <= y`, `intros` will move `x`, `y`, and `x < y` into the hypotheses.\n\nCaveats:\n  - When using the `induction` tactic, it's often important to leave `forall`s intact; avoid running `intros` automatically in such cases.\n\nExamples:\n\nModule IntrosExamples.\n  (* [intros] pulls [forall] arguments into the "known" section *)\n  Lemma simple_intros : forall a : nat, 0 <= a.\n  Proof.\n    (*\n       ============================\n       forall a : nat, 0 <= a *)\n    intros.\n    (* a : nat\n       ============================\n       0 <= a *)\n  Abort.\n\n  (* if you put the argument before the colon, it's already "introduced" *)\n  Lemma intros_unneeded (a : nat) : 0 <= a.\n  Proof.\n    (* a : nat\n       ============================\n       0 <= a *)\n    intros. (* no-op *)\n  Abort.\n\n  (* [intros] also pulls preconditions into the "known" section *)\n  Lemma intros_precondition : forall a : nat, a <> 0 -> 0 < a.\n  Proof.\n    (*\n       ============================\n       forall a : nat, a <> 0 -> 0 <= a *)\n    intros.\n    (* a : nat\n       H : a <> 0\n       ============================\n       0 <= a *)\n  Abort.\nEnd IntrosExamples.
```

--------------------------------

### Extending Rocq Makefile Rules Example

Source: https://github.com/rocq-prover/rocq/blob/master/doc/sphinx/practical-tools/utilities.rst

Illustrates how to extend standard Makefile targets like `pre-all` and `install-extra` to inject custom commands. This allows users to execute specific actions before the main build target or after the installation process, such as printing messages or copying additional files.

```Makefile
pre-all::
        echo "This line is print before making the all target"
install-extra::
        cp ThisExtraFile /there-it-goes
```

--------------------------------

### Serve Coq HTML Documentation Locally with Python

Source: https://github.com/rocq-prover/rocq/blob/master/doc/README.md

This command navigates into the generated HTML documentation directory and starts a simple HTTP server using Python's `http.server` module. This allows users to view the documentation locally in a web browser, avoiding potential issues with direct file opening.

```Shell
cd _build/default/doc/refman-html/ && python3 -m http.server
```

--------------------------------

### Enter Nix Shell for Rocq Dependencies

Source: https://github.com/rocq-prover/rocq/blob/master/INSTALL.md

This command uses Nix to enter a shell environment where all required build dependencies for Rocq are automatically provided, simplifying dependency management.

```Shell
nix-shell
```

--------------------------------

### Install additional Coq packages with opam

Source: https://github.com/rocq-prover/rocq/wiki/Installation-of-Coq-on-Mac

After setting up the Coq platform, use this command to install extra Coq packages via opam, extending the functionality of your Coq environment.

```Shell
opam install coq-packagename
```

--------------------------------

### Install Additional Coq Packages with Opam

Source: https://github.com/rocq-prover/rocq/wiki/Installation-of-Coq-on-Linux

This command allows users to install additional Coq packages using the opam package manager. It is typically used after the Coq Platform has been set up and an opam switch is active. Replace 'coq-packagename' with the specific name of the Coq library or tool you wish to install.

```Shell
opam install coq-packagename
```

--------------------------------

### Rocq Prover Setup and Basic Rewrite Example

Source: https://github.com/rocq-prover/rocq/blob/master/doc/sphinx/proof-engine/ssreflect-proof-language.rst

This snippet demonstrates the initial setup for a Rocq/SSR proof script, including importing the ssreflect library and configuring implicit arguments. It then defines simple functions and a lemma, showcasing the 'rewrite' tactic with explicit redex selection to simplify a term.

```Coq
From Corelib Require Import ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
```

```Coq
Definition double x := x + x.
Definition ddouble x := double (double x).
Lemma test x : ddouble x = 4 * x.
rewrite [ddouble _]/double.
```

--------------------------------

### Install Python Dependencies for Coq HTML Documentation

Source: https://github.com/rocq-prover/rocq/blob/master/doc/README.md

This command installs the necessary Python packages, including Sphinx and its extensions, required to build the Coq reference manual in HTML format. These packages are crucial for processing reStructuredText sources.

```Shell
pip3 install sphinx sphinx_rtd_theme beautifulsoup4 \
                 antlr4-python3-runtime==4.7.1 pexpect sphinxcontrib-bibtex
```

--------------------------------

### Install OCaml Language Server Protocol Server

Source: https://github.com/rocq-prover/rocq/wiki/DevelSetup

Installs the `ocaml-lsp-server` using the OPAM package manager. This server provides essential language features like autocompletion, diagnostics, and go-to-definition for OCaml development environments, significantly enhancing the experience in editors like VSCode.

```shell
opam install ocaml-lsp-server
```

--------------------------------

### Coq: Basic `intros` Tactic Usage

Source: https://github.com/rocq-prover/rocq/wiki/Quick-Reference-for-Beginners

Demonstrates the `intros` tactic to introduce hypotheses from the goal into the context. This example shows `intros` working with a simple implication where no universal quantifiers are present.

```Coq
Lemma intros_precondition' : 1 <> 0 -> 0 < 1.
Proof.
    intros.
Abort.
```

--------------------------------

### Coq: Recursive `seq` Function Definition

Source: https://github.com/rocq-prover/rocq/wiki/Quick-Reference-for-Beginners

Defines a recursive `seq` function that generates a list of sequential natural numbers, starting from `start` with a given `length`. This function serves as a concrete example to demonstrate a common pitfall in inductive proofs related to accidentally making the inductive hypothesis too weak.

```Coq
Fixpoint seq (start len : nat) : list nat :=
  match len with
  | O => nil
  | S len' =>
    cons start (seq (S start) len')
  end.
```

--------------------------------

### Rocq Commands: Show Intro and Show Intros

Source: https://github.com/rocq-prover/rocq/blob/master/doc/sphinx/proofs/writing-proofs/proof-mode.rst

These commands assist in understanding how `intro` and `intros` tactics would name variables. `Show Intro` provides the name for the first product if the current goal begins with one, while `Show Intros` simulates the naming process for multiple introductions, aiding in robust script writing.

```APIDOC
Show Intro
  - If the current goal begins by at least one product, prints the name of the first product as it would be generated by an anonymous 'intro'.
  - The aim is to ease the writing of more robust scripts.
  - Prints nothing in the case of a non-product goal.

Show Intros
  - Similar to 'Show Intro', simulates the naming process of the 'intros' tactic.
```

--------------------------------

### Coq Induction Proof: Correctly Generalizing Inductive Hypothesis

Source: https://github.com/rocq-prover/rocq/wiki/Quick-Reference-for-Beginners

This Coq example demonstrates how to correctly structure an inductive proof to ensure the inductive hypothesis remains general. By reordering the arguments in the lemma statement (`forall len start`), the `induction` tactic preserves the universal quantification over `start`, allowing the hypothesis to be applied effectively.

```Coq
  Lemma good_inductive_hypothesis :
    forall len start,
      length (seq start len) = len.
  Proof.
    (*
      ============================
      forall len start : nat, length (seq start len) = len *)
    induction len.
    { (* subgoal 1 (len = 0) *)

      (*
         ============================
         forall start, length (seq start 0) = 0 *)
      intros.
      cbn [seq length].

      (*
         ============================
         0 = 0 *)
      reflexivity. }
    { (* subgoal 2 (len = S len') *)

      (* len : nat
         IHlen : forall start, length (seq start len) = len
         ============================
         forall start, length (seq start (S len)) = S len *)

      (* Our inductive hypothesis has a [forall] now! *)

      intros.
      cbn [seq length].

      (*  len : nat
          IHlen : forall start : nat, length (seq start len) = len
          start : nat
          ============================
          S (length (seq (S start) len)) = S len *)
      rewrite IHlen. (* ...and we can use it to prove the goal *)

      (*  len : nat
          IHlen : forall start : nat, length (seq start len) = len
          start : nat
          ============================
         S len = S len *)
      reflexivity. }
  Qed.
End InductionExamples.
```

--------------------------------

### Execute a Basic Coq Proof in Browser

Source: https://github.com/rocq-prover/rocq/wiki/Getting-Started

Demonstrates a simple arithmetic theorem and its proof steps in Coq. This snippet can be run directly in the jsCoq scratchpad to observe Coq's proof-stepping mechanism.

```Coq
Theorem HelloCoq : 4 * 10 + 2 = 42.
Proof. simpl. reflexivity. Qed.
```

--------------------------------

### Example CoqProject File Configuration

Source: https://github.com/rocq-prover/rocq/blob/master/doc/sphinx/practical-tools/utilities.rst

Presents a comprehensive example of a `_CoqProject` file, illustrating the use of various entries such as `-R` for logical paths, `-arg` for passing options to `rocq compile`, directory inclusions, and comments. It also shows options specific to `rocq makefile` like `-generate-meta-for-package`.

```Coq
-R theories/ MyCode
-arg "-w all"
# include everything under "theories", e.g. foo.v and bar.v
theories
-I src/
# include everything under "src", e.g. baz.mlg bazaux.ml and qux_plugin.mlpack
src
-generate-meta-for-package my-package
```

--------------------------------

### Setup and Build Rocq Plugin Tutorial Project

Source: https://github.com/rocq-prover/rocq/blob/master/doc/plugin_tutorial/README.md

Commands to navigate into a tutorial directory, generate Merlin configuration, and build the plugin project.

```shell
cd plugin_tutorials/tuto0
make .merlin                # run before opening .ml files in your editor
make                        # build
```

--------------------------------

### Install Coq Project using CoqMakefile

Source: https://github.com/rocq-prover/rocq/blob/master/doc/sphinx/practical-tools/utilities.rst

Provides the shell command to install a Coq project from its directory using the `CoqMakefile` generated by the Rocq build system.

```Shell
make -f CoqMakefile install
```

--------------------------------

### Verify Coq Compiler Installation

Source: https://github.com/rocq-prover/rocq/wiki/Installation-of-Coq-on-Linux

This command checks the installed version of the Coq compiler (coqc). Running this command successfully indicates that Coq has been correctly installed and is accessible in your system's PATH, allowing you to compile Coq files.

```Shell
coqc -v
```

--------------------------------

### Launching Rocq Developer Shell with Dune Utop

Source: https://github.com/rocq-prover/rocq/blob/master/dev/doc/build-system.dune.md

These commands demonstrate how to launch a developer shell using `dune utop`. This allows loading specific project libraries (e.g., `engine` or `plugins/ltac`) into the `utop` environment for interactive development.

```bash
dune utop $library
```

```bash
dune utop engine
```

```bash
dune utop plugins/ltac
```

--------------------------------

### Install Coq using MacPorts

Source: https://github.com/rocq-prover/rocq/wiki/Installation-of-Coq-on-Mac

Install the Coq proof assistant on macOS systems using the MacPorts package manager. This method offers an alternative to Homebrew for package management.

```Shell
sudo port install coq
```

--------------------------------

### Rocq Command Parameter and Startup Script Configuration

Source: https://github.com/rocq-prover/rocq/blob/master/doc/sphinx/practical-tools/coq-commands.rst

Explains the hierarchy of parameter passing mechanisms in Rocq and details the behavior and search paths for the `coqrc` startup script, including command-line options to control its use.

```APIDOC
Rocq Command Parameter Mechanisms:
Parameters are passed in the following order of importance:
1. Command line options
2. Environment variables
3. The `coqrc` start up script

`coqrc` Startup Script:
  - Purpose: Implicitly prepends a startup script to any document Rocq reads (interactive session or file to compile).
  - Search Order (first file found is used):
    1. `$XDG_CONFIG_HOME/coqrc.<VERSION>`
    2. `$XDG_CONFIG_HOME/coqrc`
    3. `$HOME/.coqrc.<VERSION>`
    4. `$HOME/.coqrc`
  - Variables:
    - `<VERSION>`: The version of Rocq (e.g., as shown by `rocq --version`).
    - `$XDG_CONFIG_HOME`: An environment variable.
    - `$HOME`: The user's home directory.
  - Command Line Options:
    - `-init-file file`: Uses the specified file instead of a startup script from a configuration directory.
    - `-q`: Prevents the use of any startup script.
```

--------------------------------

### Rocq Build System Integration Examples

Source: https://github.com/rocq-prover/rocq/blob/master/doc/sphinx/practical-tools/coq-commands.rst

This section provides examples of how to integrate Rocq's compiled interfaces into a build system like `make`. It demonstrates commands for compiling statements (.vos) and proofs (.vok) across multiple files, highlighting how to leverage parallelism for faster overall compilation.

```Shell
make foo.required_vos
# Compiles f1.v and f2.v using -vos option (skips proofs), producing f1.vos and f2.vos.
# Assumes foo.v depends on f1.v and f2.v.
# Prepares for interactive work on foo.v.

make vos
# Compiles statements (excluding proofs) in all files (f1.v ... fn.v) with linear dependencies.

make -j vok
# Compiles all proofs in parallel for files f1.v ... fn.v.
# Assumes 'make vos' has been run.
```

--------------------------------

### Coq Setup and Definitions for Tactic Examples

Source: https://github.com/rocq-prover/rocq/blob/master/doc/sphinx/proof-engine/ssreflect-proof-language.rst

Provides common Coq setup commands and definitions (axioms, notations, inductive types, definitions) used across various tactic examples in the Rocq prover documentation. This includes imports for ssreflect, ssrfun, and ssrbool, along with custom definitions for natural numbers and lists.

```Coq
From Corelib Require Import ssreflect ssrfun ssrbool.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Set Warnings "-notation-overridden".

Axiom leq : nat -> nat -> bool.
Notation "m <= n" := (leq m n) : nat_scope.
Notation "m < n" := (S m <= n) : nat_scope.
Inductive Ord n := Sub x of x < n.
Notation "'I_ n" := (Ord n) (at level 8, n at level 2, format "''I_' n").
Arguments Sub {_} _ _.
Definition val n (i : 'I_n) := let: Sub a _ := i in a.
Definition insub n x :=
  if @idP (x < n) is ReflectT _ Px then Some (Sub x Px) else None.
Axiom insubT : forall n x Px, insub n x = Some (Sub x Px).

Axiom subnn : forall n : nat, n - n = 0.
Parameter map : (nat -> nat) -> list nat -> list nat.
Parameter sumlist : list nat -> nat.
Axiom eq_map :
  forall F1 F2 : nat -> nat,
  (forall n : nat, F1 n = F2 n) ->
  forall l : list nat, map F1 l = map F2 l.
```

--------------------------------

### Build and Test Rocq Project

Source: https://github.com/rocq-prover/rocq/blob/master/dev/doc/README.md

A sequence of shell commands to clone the Rocq repository, navigate into the project directory, and use `make` targets or `dune exec` to build and test the Rocq prover. This includes commands for checking available targets, building OCaml files, building the complete Coq standard library, and compiling a specific `.v` file.

```Shell
$ git clone https://github.com/rocq-prover/rocq.git
$ cd coq
$ make
$ make check
$ make world
$ dune exec -- rocq test.v
```

--------------------------------

### Install Additional Coq Packages with opam

Source: https://github.com/rocq-prover/rocq/wiki/Installation-of-Coq-on-Windows

Demonstrates how to install additional Coq packages using the opam package manager after the Coq Platform has been successfully set up. This command is executed in a shell environment, typically within a Linux or Cygwin setup.

```Shell
opam install coq-packagename
```

--------------------------------

### Set up Coq Environment for Notations

Source: https://github.com/rocq-prover/rocq/blob/master/doc/sphinx/user-extensions/syntax-extensions.rst

Initializes the Coq environment by importing the `ListDef` library and enabling the printing of notations, which is crucial for observing the effects of defined abbreviations and notations.

```Coq
Require Import ListDef.
Set Printing Notations.
```

--------------------------------

### Shell: Launching RocqIDE from Command Line

Source: https://github.com/rocq-prover/rocq/blob/master/doc/sphinx/practical-tools/coqide.rst

Instructions for launching the RocqIDE application from the command line. Users can open specific Coq script files by providing their names as arguments, or start with a single unnamed scratch buffer. The command also accepts many options compatible with `rocq top`.

```Shell
rocqide
rocqide <script_file_names.v>
rocqide --help
```

--------------------------------

### Coq `set` Tactic: Basic Abbreviation Example

Source: https://github.com/rocq-prover/rocq/blob/master/doc/sphinx/proof-engine/ssreflect-proof-language.rst

An example demonstrating the `set` tactic to abstract the subterm `f x` as `t` within a lemma. Includes necessary Coq setup commands.

```Coq
From Corelib Require Import ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Axiom f : nat -> nat.

Lemma test x :  f x + f x = f x.
set t := f _.
```

--------------------------------

### Coq ssreflect Environment Setup

Source: https://github.com/rocq-prover/rocq/blob/master/doc/sphinx/proof-engine/ssreflect-proof-language.rst

Initializes the Coq environment by importing necessary ssreflect and ssrbool libraries and setting implicit argument behavior for subsequent examples. This setup is common for ssreflect proofs.

```Coq
From Corelib Require Import ssreflect ssrbool.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
```

--------------------------------

### Build Coq Documentation Targets with Make

Source: https://github.com/rocq-prover/rocq/blob/master/doc/README.md

These `make` commands compile various components of the Coq documentation. They allow building the reference manual in HTML or PDF, the core library documentation, and the ML API documentation into specified output directories.

```Shell
make refman-html
```

```Shell
make refman-pdf
```

```Shell
make corelib-html
```

```Shell
make apidoc
```

--------------------------------

### Coq Example: `under` Tactic with `bigop` Theory

Source: https://github.com/rocq-prover/rocq/blob/master/doc/sphinx/proof-engine/ssreflect-proof-language.rst

A Coq code example demonstrating the setup for using the `under` tactic, including imports, implicit arguments, and the definition of a `bigop` structure from the Mathematical Components library.

```Coq
From Corelib Require Import ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Coercion is_true : bool >-> Sortclass.

Reserved Notation "\big [ op / idx ]_ ( m <= i < n | P ) F"
  (at level 36, F at level 36, op, idx at level 10, m, i, n at level 50,
           format "'[' \big [ op / idx ]_ ( m  <=  i  <  n  |  P )  F ']'").
Variant bigbody (R I : Type) : Type :=
  BigBody : forall (_ : I) (_ : forall (_ : R) (_ : R), R) (_ : bool) (_ : R), bigbody R I.

Parameter bigop :
  forall (R I : Type) (_ : R) (_ : list I) (_ : forall _ : I, bigbody R I), R.

Axiom eq_bigr_ :
  forall (R : Type) (idx : R) (op : forall (_ : R) (_ : R), R) (I : Type)
```

--------------------------------

### Rocq Inductive Type Definition Example

Source: https://github.com/rocq-prover/rocq/blob/master/doc/sphinx/proofs/writing-proofs/reasoning-inductives.rst

An example demonstrating the definition of an inductive type `contains0` in Rocq, which is a (co)inductively defined proposition. This snippet shows the basic syntax for starting an inductive definition.

```Rocq
reset all.

Inductive contains0 : list nat -> Prop :=
```

--------------------------------

### CoqProject -R Option for Package Installation Structure

Source: https://github.com/rocq-prover/rocq/blob/master/doc/sphinx/practical-tools/utilities.rst

Demonstrates the effect of the `-R` option in `_CoqProject` on the installed package directory structure. It shows how source paths are mapped to the logical package name and subsequently to the `user-contrib` directory upon installation.

```Coq
-R theories MyPackage
theories/File1.v
theories/SubDir/File2.v
```

--------------------------------

### Running Rocq Project Test Suite

Source: https://github.com/rocq-prover/rocq/blob/master/dev/doc/build-system.dune.md

These commands show how to execute the Rocq project's test suite. Options include running tests incrementally with `make -C test-suite` or `make test-suite`, and performing full hygienic runs using `dune runtest`, with support for parallel execution via `NJOBS`.

```bash
make -C test-suite
```

```bash
make test-suite
```

```bash
dune runtest
```

```bash
NJOBS=8 dune runtest
```

--------------------------------

### Basic Coq Proof Structure with `lia`

Source: https://github.com/rocq-prover/rocq/wiki/Quick-Reference-for-Beginners

Demonstrates a simple Coq proof using `intro` to set up the goal and the `lia` (linear integer arithmetic) tactic to resolve a contradiction, concluding the proof with `Qed`.

```Coq
intro. (* now our goal says [False]! We have to prove that the hypotheses\n              contradict. *)\nlia. (* luckily, [lia] is pretty smart. *)\nQed.\nEnd NotExamples.
```

--------------------------------

### Rocq Print Namespace Command and Example

Source: https://github.com/rocq-prover/rocq/blob/master/doc/sphinx/language/core/modules.rst

Explains the `Print Namespace` command, which lists names and types of loaded constants whose fully qualified names start with a given `dirpath`. Provides examples demonstrating its use with different path granularities.

```APIDOC
Print Namespace @dirpath
  - Prints the names and types of all loaded constants whose fully qualified names start with the specified dirpath.
  - dirpath: Can include module names.
```

```Rocq
Module A.
Definition foo := 0.
Module B.
Definition bar := 1.
End B.
End A.
```

```Rocq
Print Namespace Top.
Print Namespace Top.A.
Print Namespace Top.A.B.
```

--------------------------------

### _CoqProject File Listing Specific Rocq Files

Source: https://github.com/rocq-prover/rocq/blob/master/doc/sphinx/practical-tools/utilities.rst

This `_CoqProject` example demonstrates how to explicitly list individual `.v` files to be included in the project, rather than entire directories. It declares `theories` as the top directory for `MyPackage` and then specifies `File1.v` and `SubDir/File2.v` for compilation.

```CoqProject
-R theories MyPackage
theories/File1.v
theories/SubDir/File2.v
```

--------------------------------

### Defining Inductive Relation and Parameter for Inversion Example

Source: https://github.com/rocq-prover/rocq/blob/master/doc/sphinx/proofs/writing-proofs/reasoning-inductives.rst

Defines the `Le` (less than or equal) inductive relation over natural numbers and declares a parameter `P` for use in subsequent inversion examples. This setup provides the context for demonstrating inversion lemma generation.

```Rocq
Inductive Le : nat -> nat -> Set :=
| LeO : forall n:nat, Le 0 n
| LeS : forall n m:nat, Le n m -> Le (S n) (S m).

Parameter P : nat -> nat -> Prop.
```

--------------------------------

### Coq: `intros` Tactic with Explicit Argument Naming

Source: https://github.com/rocq-prover/rocq/wiki/Quick-Reference-for-Beginners

Illustrates how to use the `intros` tactic to introduce universally quantified variables and hypotheses, explicitly assigning custom names to them. This provides more readable proof contexts.

```Coq
Lemma intros_names : forall a : nat, a <> 0 -> 0 < a.
Proof.
    intros x y.
Abort.
```

--------------------------------

### Ltac Example: Selector Reordering Goals

Source: https://github.com/rocq-prover/rocq/blob/master/doc/sphinx/proof-engine/ltac.rst

This example demonstrates how goal selectors can be used to reorder and apply tactics to specific goals within a multi-goal context in Rocq. It shows the initial goal setup and the application of `idtac` to goals 1 and 3 after splitting.

```Ltac
Goal 1=0 /\ 2=0 /\ 3=0.
```

```Ltac
repeat split.
1,3: idtac.
```

--------------------------------

### `makecoq` Command Line Usage Examples

Source: https://github.com/rocq-prover/rocq/wiki/CoqDevelopment/RaccourcisPourDevelopperSousEmacs

Examples demonstrating how to invoke the `makecoq` script with various arguments to compile specific Coq components. These commands show how to compile `coqtop.byte`, entire `theories`, or only the initial files of the library using `BEST=byte`.

```Shell
makecoq bin/coqtop.byte
makecoq theories
makecoq BEST=byte theories
```

--------------------------------

### Set up a Goal for Ltac2 Examples

Source: https://github.com/rocq-prover/rocq/blob/master/doc/sphinx/proof-engine/ltac2.rst

Sets up a simple `True` goal, which is a common starting point for demonstrating Ltac2 tactics.

```Ltac2
Goal True.
```

--------------------------------

### Coq Example: Initializing Standard I/O Streams

Source: https://github.com/rocq-prover/rocq/wiki/AUGER_Monad

This Coq example defines `some_std_streams`, an initial I/O state record. It sets `stdin` to a stream containing the string 'Hello, World!', while `stdout` and `stderr` are initialized as `EmptyStream`. This setup is useful for testing I/O functions with predefined input.

```Coq
Example some_std_streams :=
{| stdin := ltS ("H"::"e"::"l"::"l"::"o"::","::" "::"W"::"o"::"r"::"l"::"d"::
                 "!"::nil);
   stdout := EmptyStream;
   stderr := EmptyStream
|}.
```

--------------------------------

### Common Dune Build Targets for Rocq Project

Source: https://github.com/rocq-prover/rocq/blob/master/dev/doc/build-system.dune.md

These `dune build` commands illustrate various ways to compile the Rocq project. They cover building the entire project, specific targets (like `.cmxa` or binaries), individual packages, and a quick check mode for ML files.

```bash
dune build
```

```bash
dune build @install
```

```bash
dune build $TARGET
```

```bash
dune build $PACKAGE.install
```

```bash
dune build @check
```

--------------------------------

### Generating and Compiling Rocq Projects with _CoqProject

Source: https://github.com/rocq-prover/rocq/blob/master/doc/sphinx/practical-tools/utilities.rst

These commands illustrate the workflow for building a Rocq project using a `_CoqProject` file. The first command generates a makefile (`CoqMakefile`) from the `_CoqProject` definition, and the second command compiles the project using the generated makefile.

```Shell
rocq makefile -f _CoqProject -o CoqMakefile
```

```Shell
make -f CoqMakefile
```

--------------------------------

### Coq Induction Proof: Demonstrating a Failed Inductive Hypothesis

Source: https://github.com/rocq-prover/rocq/wiki/Quick-Reference-for-Beginners

This Coq code snippet illustrates a common error in inductive proofs where the inductive hypothesis becomes too specific. The `induction` tactic, when applied to `len` after `start` has been introduced, prevents the hypothesis from being universally quantified over `start`, leading to a proof failure.

```Coq
      forall start len : nat, length (seq start len) = len *)
    induction len.
    { (* subgoal 1 (len = 0) *)

      (* start : nat
         ============================
         length (seq start 0) = 0 *)
      cbn [seq length].

      (* start : nat
         ============================
         0 = 0 *)
      reflexivity. }
    { (* subgoal 2 (len = S len') *)

      (* start, len : nat
         IHlen : length (seq start len) = len
         ============================
         length (seq start (S len)) = S len *)

      (* Take a close look at the inductive hypothesis, and notice that it
         doesn't apply to just any [start]; it requires the specific argument
         we had to begin with, and that's going to be a problem. *)

      cbn [seq length].

      (* start, len : nat
         IHlen : length (seq start len) = len
         ============================
         S (length (seq (S start) len)) = S len *)

      (* Now our goal talks about starting with [S start], and our inductive
         hypothesis doesn't apply at all. We need the hypothesis to say
         [forall start]. *)
  Abort.
```

--------------------------------

### Rocqtop Interactive Proof Commands with Diffs

Source: https://github.com/rocq-prover/rocq/blob/master/doc/sphinx/proofs/writing-proofs/proof-mode.rst

Demonstrates a sequence of interactive commands for `rocqtop`, including setting diffs and applying tactics like `split` and `intros`, to illustrate how proof states change and diffs are displayed.

```Rocqtop
Set Diffs "on".
Parameter P : nat -> Prop.
Goal P 1 /\ P 2 /\ P 3.
split.
2: split.
Goal forall n m : nat, n + m = m + n.
intros n.
intros m.
```

--------------------------------

### Introducing Hypotheses with `intro` and `intros` in Rocq

Source: https://github.com/rocq-prover/rocq/blob/master/doc/sphinx/proof-engine/tactics.rst

Illustrates the use of `intro` and `intros` tactics to introduce variables and hypotheses into the local context. `intro` introduces one item at a time, while `intros` can introduce multiple items in a single command, providing a more concise way to manage context.

```Rocq
Goal forall m n, m < n -> (let x := 0 in True).
intro m.
intro n.
intro H.
intro x.
```

```Rocq
Goal forall m n, m < n -> (let x := 0 in True).
intros m n H x.
```

--------------------------------

### Rocq/Coq Example: Demonstrating Proof Diffs with `intros`

Source: https://github.com/rocq-prover/rocq/blob/master/doc/sphinx/proofs/writing-proofs/proof-mode.rst

A Coq/Rocq example defining an inductive type `ev` and a fixpoint `double`, then setting up a goal and applying the `intros` tactic. This setup is used to illustrate how Rocq's `Diffs` option can highlight changes in the proof state, such as new hypotheses and modified conclusions.

```Rocq
Inductive ev : nat -> Prop :=
| ev_0 : ev 0
| ev_SS : forall n : nat, ev n -> ev (S (S n)).

Fixpoint double (n:nat) :=
  match n with
  | O => O
  | S n' => S (S (double n'))
  end.

Goal forall n, ev n -> exists k, n = double k.
intros n E.
```

--------------------------------

### Coq: List Induction Example

Source: https://github.com/rocq-prover/rocq/wiki/Quick-Reference-for-Beginners

Illustrates induction on a list type (`list nat`) to prove a fundamental property about list concatenation: `length (ls1 ++ ls2) = length ls1 + length ls2`. This example showcases the application of the inductive hypothesis (`IHls1`) and common list manipulation tactics like `rewrite` and `cbn`.

```Coq
Lemma list_induction :
  forall (A : Type) (ls1 ls2 : list nat),
    length (ls1 ++ ls2) = length ls1 + length ls2.
Proof.
  induction ls1; intros.
  { rewrite app_nil_l.
    cbn [length].
    lia. }
  { rewrite <-app_comm_cons.
    cbn [length].
    rewrite IHls1.
    lia. }
Qed.
```

--------------------------------

### Rocqtop Interactive Session Example

Source: https://github.com/rocq-prover/rocq/blob/master/doc/sphinx/README.rst

Demonstrates how to use the `rocqtop` directive to embed and execute Rocq code within documentation, showing how to print a type and define a variable in an interactive session.

```Rocq
Print nat.
Definition a := 1.
```

--------------------------------

### Coq Forall for Implications (Transitivity Example)

Source: https://github.com/rocq-prover/rocq/wiki/Quick-Reference-for-Beginners

This example illustrates how the `forall` quantifier can be used to express logical implications in Coq, specifically demonstrating the transitivity property of the less-than relation. It compares two ways of writing the same implication: one using explicit hypothesis declarations and another using the more readable arrow (`->`) notation for chained implications.

```Coq
  Definition lt_transitive : Prop :=
    forall a b c (Hab : a < b) (Hbc : b < c),
      a < c.
  Definition lt_transitive' : Prop :=
    forall a b c,
      a < b ->
      b < c ->
      a < c.
```

--------------------------------

### Coq Foundational Syntax and Proof Tactics Reference

Source: https://github.com/rocq-prover/rocq/wiki/Quick-Reference-for-Beginners

A quick reference for foundational Coq syntax and proof tactics. This section outlines common declarations, inspection commands, basic types, propositional logic constructs, and frequently used proof tactics. It serves as an informal, incomplete overview for new users.

```APIDOC
Declarations:
  Definition
  Fixpoint
  Lemma
  Theorem
  Inductive

Inspection:
  Search
  Check
  Print

Miscellaneous:
  nat
  match

Propositions:
  Prop
  forall
  exists
  and (/\)
  or (\/)
  implies (->)
  not (~)
  eq (=)
  not-eq (<>)

Proofs:
  intros
  apply
  rewrite
  reflexivity
  cbv
  cbn
  induction
  lia
  nia
  replace
```

--------------------------------

### Coq Not-Equality Notation (`<>`)

Source: https://github.com/rocq-prover/rocq/wiki/Quick-Reference-for-Beginners

Documentation for Coq's `not-eq` notation (`<>`), which is syntactic sugar for `~ (x = y)`. It provides examples of its usage in defining propositions and preconditions within a module.

```APIDOC
Coq Not-Equality Notation (<>):\n\nDefinition:\n  The notation `x <> y` is syntactic sugar for `~ (x = y)`.\n  It means "not equal".\n\nExamples:\n\nModule NotEqExamples.\n\n  (* using <> to state a simple [Prop] *)\n  Definition one_neq_2 : Prop := 1 <> 2.\n\n  (* using <> to state a precondition *)\n  Definition nonzero_pos : Prop :=\n    forall n : nat,\n      n <> 0 ->\n      0 < n.\nEnd NotEqExamples.
```

--------------------------------

### Example RocqIDE Custom Key Binding Configuration

Source: https://github.com/rocq-prover/rocq/blob/master/doc/sphinx/practical-tools/coqide.rst

This example demonstrates the format for `coqide.bindings` files, used to define custom key bindings for Unicode symbol input in RocqIDE. Each line specifies a key, its corresponding Unicode value, and an optional priority. Higher priority values ensure that shorter prefixes resolve to the intended binding.

```Configuration
\par ||
\pi π 1
\le ≤ 1
\lambda λ 2
\lambdas λs
```

--------------------------------

### Coq Lemma Proof for Trivial Proposition

Source: https://github.com/rocq-prover/rocq/wiki/Quick-Reference-for-Beginners

A basic example of a Coq lemma proving the `True` proposition. This snippet demonstrates the use of the `trivial` tactic for straightforward proofs.

```Coq
Lemma simple : True.
Proof.
  trivial. (* in this case, we just tell Coq "this proof is easy" *)
Qed.
```

--------------------------------

### Run Rocq Plugin Tutorial and Load Module

Source: https://github.com/rocq-prover/rocq/blob/master/doc/plugin_tutorial/README.md

Instructions for running the Rocq prover with the compiled tutorial plugin and loading the necessary module within a Rocq session.

```bash
cd tuto0; make
rocq top -I src -R theories Tuto0
```

```coq
Require Import Tuto0.Loader. HelloWorld.
```