### Using `example` Directive Correctly

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

Use the `example::` directive to introduce illustrative examples that follow a definition or explanation. Do not embed definitions directly within the `example::` directive.

```rst
.. code::

   .. example:: Using proof-irrelevance

      If you assume the axiom above, …
```

```rst
.. code::

   Here is a useful axiom:

   .. example::

      .. rocqdoc::

         Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y.
```

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

### Install Python Dependencies for HTML Documentation

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

Installs necessary Python packages for building the HTML reference manual. Ensure pip and setuptools are installed first.

```bash
pip3 install sphinx sphinx-rtd-theme beautifulsoup4 \
                 antlr4-python3-runtime==4.7.1 pexpect
```

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

### Create Rocq Opam Switch and Install Core

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

Sets up an opam switch with specific OCaml variants and installs the rocq-core package. This is a recommended environment for compiling the stdlib.

```bash
opam switch create rocq --packages="ocaml-variants.4.14.1+options,ocaml-option-flambda"
eval $(opam env)
opam install rocq-core
```

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

### Create an Example Admonition

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

The `example` directive creates a generic admonition. Text following the directive header can be used as the example's title.

```rst
.. example:: Adding a hint to a database

   The following adds ``plus_comm`` to the ``plu`` database:

   .. rocqdoc::

      Hint Resolve plus_comm : plu.
```

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

### Install Rocq Stdlib

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

Installs the compiled Rocq standard library to the appropriate location. This command typically follows a successful 'make' command.

```bash
make install
```

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

### Coq Notation DSL Example

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

Illustrates a Coq notation pattern using the custom DSL. This example shows a `Hint Extern` command with a natural number, an optional pattern, and a mandatory tactic.

```rst
Hint Extern @natural {? @pattern} => @tactic
```

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

### Rocqtop Interaction Example

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

Demonstrates how to document interactions with Rocqtop using the 'rocqtop' directive, including options and code to be sent.

```rst
.. rocqtop:: in reset

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

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

### Initial Clone and Remote Setup

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

Clone the official repository and set up 'upstream' and 'origin' remotes for your fork. Ensure the pre-commit hook is copied to the .git/hooks directory.

```shell
git clone https://github.com/coq-community/stdlib -o upstream
cd stdlib
git remote add origin git@github.com:$YOURNAME/stdlib
# Make sure you click the fork button on GitHub so that this repository exists
cp dev/tools/pre-commit .git/hooks/ # Setup the pre-commit hook
```

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

### Running Coq Test Suite Examples

Source: https://github.com/rocq-prover/stdlib/blob/master/test-suite/README.md

Demonstrates how to simulate a failing test, run the test suite, and observe the failure report. Also shows how to correct the test and rerun.

```bash
$ echo Fail. > success/fail.v # make some failing test

$ make
TEST      prerequisite/make_local.v
...
TEST      success/fail.v
...
BUILDING SUMMARY FILE
FAILURES
    success/fail.v...Error! (should be accepted)
Makefile:189: recipe for target 'all failed
make: *** [report] Error 1

$ make report PRINT_LOGS=1
BUILDING SUMMARY FILE
logs/success/fail.v.log
==========> TESTING success/fail.v <==========
Welcome to Rocq (version information)
Skipping rcfile loading.
File "/path/to/success/fail.v", line 1, characters 4-5:
Error:
Syntax error: [vernac:Vernac.vernac_control] expected after 'Fail' (in [vernac:Vernac.vernac_control]).

0m0.000000s 0m0.000000s
0m0.040000s 0m0.000000s
==========> FAILURE <==========
    success/fail.v...Error! (should be accepted)

FAILURES
    success/fail.v...Error! (should be accepted)
Makefile:189: recipe for target 'report' failed
make: *** [report] Error 1

$ echo 'Comments "foo".' > success/fail.v

$ make
TEST      success/fail.v
BUILDING SUMMARY FILE
NO FAILURES

```

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

### Serve Local Documentation with Python HTTP Server

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

Starts a local HTTP server in the specified directory to serve the generated HTML documentation. This avoids potential issues when opening local files directly in a browser.

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

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

### Rocq Attribute Example

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

Shows an example of an attribute in Rocq, specifically the 'local' attribute.

```rst
.. attr:: local
```

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

### List Operations

Source: https://context7.com/rocq-prover/stdlib/llms.txt

Examples of computing list length and concatenation.

```Coq
Compute length [1; 2; 3].   (* = 3 *)
Compute [1; 2] ++ [3; 4].   (* = [1; 2; 3; 4] *)
```

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

### Rocq Grammar Production Example

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

Demonstrates the syntax for defining grammar productions using the 'prodn' directive, including referencing existing definitions and continuing productions.

```rst
.. prodn:: occ_switch ::= { {? {| + | - } } {* @natural } }
term += let: @pattern := @term in @term
| second_production
```

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

### Rocq Tactic Example (Assert)

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

Demonstrates the 'assert' tactic, which applies another tactic to solve subgoals.

```rst
.. tacv:: assert @form by @tactic
```

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

### Rocq Exception Example

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

Provides an example of an error raised by a Rocq command or tactic, nested within a tactic definition.

```rst
.. exn:: Proof is not complete
```

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

### Rocq Theorem Example

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

Documents a mathematical theorem related to the ceiling function in Rocq.

```rst
.. thm:: Bound on the ceiling function
```

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

### Build Sphinx Documentation with Warning Logging

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

Builds the Sphinx documentation, configuring `SPHINXWARNOPT` to log all warnings to a specified file instead of stopping compilation. This example logs warnings to `/tmp/warn.log`.

```bash
SPHINXWARNOPT="-w/tmp/warn.log" make refman-html
```

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

### Rocq Flag Example

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

Demonstrates a Rocq flag, which is a boolean setting, and its effect on type declarations.

```rst
.. flag:: Nonrecursive Elimination Schemes
```

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

### Rocq Command Definition Example

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

Shows the definition of a Rocq command using the 'cmd' directive, including its signature and a brief explanation.

```rst
.. cmd:: Infix @string := @one_term {? ( {+, @syntax_modifier } ) } {? : @ident }
```

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

### Check Integer Arithmetic Expression

Source: https://github.com/rocq-prover/stdlib/blob/master/doc/sphinx/language/coq-library.rst

This example demonstrates how to check a simple integer addition expression using the ZArith module and its associated scope.

```coq
From Stdlib Require Import ZArith.
Check (2 + 3)%Z.
Open Scope Z_scope.
Check 2 + 3.
```

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

### Rocq Table Example

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

Illustrates a Rocq table, which is a setting comprising a set of values, used here for a search blacklist.

```rst
.. table:: Search Blacklist @string
   :name: Search Blacklist
```

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

### Rocq Warning Example

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

Illustrates a warning message from Rocq concerning ambiguous coercion paths.

```rst
.. warn:: Ambiguous path
```

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

### Rocq Option Example

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

Shows a Rocq option with a non-boolean value, controlling the display of hypotheses in goals.

```rst
.. opt:: Hyps Limit @natural
   :name: Hyps Limit
```

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

### Notation Syntax Example

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

The `:n:` role is used for text employing notation syntax like `@id` or `{+, …}`. It's helpful for explaining tactic equivalences.

```rst
:n:`generalize @term as @ident` is just like :n:`generalize @term`, but
   it names the introduced hypothesis :token:`ident`.
```

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

### Coq Floating-Point Evaluation Examples

Source: https://github.com/rocq-prover/stdlib/blob/master/doc/sphinx/language/coq-library.rst

Demonstrates various floating-point computations and comparisons in Coq, including division by zero and NaN handling. Use this to test Coq's float evaluation behavior.

```coq
Open Scope float_scope.
Eval compute in 1 + 0.5.
Eval compute in 1 / 0.
Eval compute in 1 / -0.
Eval compute in 0 / 0.
Eval compute in 0 ?= -0.
Eval compute in nan ?= nan.
Eval compute in next_down (-1).
```

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

### Rocq Command Variant Example

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

Illustrates a variant of a Rocq command using the 'cmdv' directive, which is equivalent to another command.

```rst
.. cmdv:: Parameter @ident : @term.
```

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

### Rocq Tactic Example (Fail)

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

Documents the 'fail' tactic in Rocq, which always fails and is useful for defining other tacticals.

```rst
.. tacn:: fail
```

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

### Rocq Code Snippet

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

Use the `:g:` role for Gallina and Ltac snippets. This role is suitable for inline code examples.

```rst
:g:`apply plus_comm; reflexivity`
```

```rst
:g:`Set Printing All.`
```

```rst
:g:`forall (x: t), P(x)`
```

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

### ZArith: Parity and Divisibility Checks

Source: https://context7.com/rocq-prover/stdlib/llms.txt

Defines and provides examples for checking even/odd properties and divisibility for Z integers. Uses `Z.Even` and `Z.Odd` for parity, and the `|` operator for divisibility.

```coq
Definition is_even (z : Z) : Prop := Z.Even z.
Definition is_odd  (z : Z) : Prop := Z.Odd z.
```

```coq
Example six_is_even : Z.Even 6.
Proof. exists 3. reflexivity. Qed.
```

```coq
Example div_example : (4 | 12)%Z.
Proof. exists 3. reflexivity. Qed.
```

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

### Define Coq Tactic Variant and Exception

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

Example of defining a custom tactic variant (`tacv`) and an associated exception (`exn`) using Coq's Sphinx domain. Use this to document specific Coq tactics and their potential errors.

```rst
.. tacv:: simpl @pattern at {+ @natural}
   :name: simpl_at

   This applies ``simpl`` only to the :n:`{+ @natural}` occurrences of the subterms
   matching :n:`@pattern` in the current goal.

   .. exn:: Too few occurrences
      :undocumented:
```

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

### Build Reference Manual in HTML

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

Builds the reference manual in HTML format. The output is placed in `_build/default/doc/refman-html`.

```bash
make refman-html
```

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

### Build Standard Library Documentation in HTML

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

Builds the standard library documentation in HTML format. The output is placed in `_build/default/doc/stdlib/html`.

```bash
make stdlib-html
```

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

### Rocq Tactic Example

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

Defines a Rocq tactic using the 'tacn' directive, specifying its arguments and behavior.

```rst
.. tacn:: do @natural @expr
```

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

### Rocq Tactic Variant Example

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

Shows a variant of a Rocq tactic, 'fail', with an optional failure level.

```rst
.. tacv:: fail @natural
```

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

### Initialize Theme Settings with Alpine.js

Source: https://github.com/rocq-prover/stdlib/blob/master/doc/common/styles/html/coqremote/footer.html

Initializes theme settings using Alpine.js, storing preferences in localStorage. It checks for existing storage access and applies the system's default dark mode preference if available.

```javascript
document.addEventListener('alpine:init', () => {
Alpine.store('themeSettings', {
init() {
this.storageAccess = localStorage.getItem('storageAccess')
this.preference = localStorage.getItem('theme') || "system"
this.isSystemDefaultDark = window.matchMedia && window.matchMedia('(prefers-color-scheme: dark)').matches
},
selected: '',
alertOpen: false,
storageAccess: false,
preference: undefined,
isSystemDefaultDark: false,
setPreference(preference) {
if (!this.storageAccess) {
if (!window.confirm("We will remember your choice in your browser's LocalStorage. Allow this?")) {
return;
}
localStorage.setItem('storageAccess', true)
storageAccess = true;
}
this.selected = preference;
this.preference = preference
localStorage.setItem('theme', preference)
if (preference === 'dark') {
document.body.classList.add("dark");
}
if (preference === 'light') {
document.body.classList.remove("dark");
}
if (preference === 'system') {
if (this.isSystemDefaultDark) {
document.body.classList.add("dark");
} else {
document.body.classList.remove("dark");
}
localStorage.removeItem('theme')
return
}
},
})
})
```

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

### Lists: Basic List Operations and Notations

Source: https://context7.com/rocq-prover/stdlib/llms.txt

Introduces basic list construction and operations in Coq's `Lists.List` module. Includes defining a list, accessing head/tail, and handling empty lists. Requires `ListNotations`.

```coq
Definition ex_list : list nat := [1; 2; 3; 4; 5].
```

```coq
Compute hd 0 ex_list.
(* = 1 *)
```

```coq
Compute hd_error ex_list.
(* = Some 1 *)
```

```coq
Compute hd_error ([] : list nat).
(* = None *)
```

```coq
Compute tl ex_list.
(* = [2; 3; 4; 5] *)
```

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

### Using `rocqdoc` for Axioms

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

Use the `rocqdoc::` directive to present axioms and other definitions. This ensures they are displayed correctly and can be referenced.

```rst
.. code::

   Here is a useful axiom:

   .. rocqdoc::

      Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y.
```

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

### ZArith: Using `lia` Tactic for Linear Arithmetic

Source: https://context7.com/rocq-prover/stdlib/llms.txt

Illustrates the use of the `lia` tactic to automatically prove goals involving linear arithmetic on Z integers. This tactic is effective for discharging simple arithmetic equalities and inequalities.

```coq
Lemma z_lia_example (n m : Z) : n + m = m + n.
Proof. lia. Qed.
```

```coq
Lemma z_bound (n : Z) : 0 <= n -> n < 10 -> 0 <= n * n < 100.
Proof. lia. Qed.
```

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

### Build Rocq Stdlib

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

Compiles the Rocq standard library after setting up the environment. This command should be run from the root of the stdlib source directory.

```bash
make
```

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

### ZArith: Basic Binary Integer Arithmetic

Source: https://context7.com/rocq-prover/stdlib/llms.txt

Demonstrates basic arithmetic operations for signed binary integers (Z). Includes addition, absolute value, division, modulo, and GCD. Requires opening the Z_scope.

```coq
Compute (3 + (-5))%Z.
(* = -2 *)
```

```coq
Compute Z.abs (-7).
(* = 7 *)
```

```coq
Compute Z.div 10 3.
(* = 3 (truncated toward zero) *)
```

```coq
Compute Z.modulo 10 3.
(* = 1 *)
```

```coq
Compute Z.gcd 12 8.
(* = 4 *)
```

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

### Well-Founded Recursion in Coq

Source: https://context7.com/rocq-prover/stdlib/llms.txt

Illustrates well-founded recursion using the Wellfounded module. Demonstrates checking well-foundedness and applying well-founded induction.

```Coq
From Stdlib Require Import Wellfounded.Wellfounded.

(* lt is well-founded on nat *)
Check Nat.lt_wf_0 : well_founded Nat.lt.

(* Well-founded induction *)
Lemma wf_induction_example : forall n : nat, n = n.
Proof.
  apply (well_founded_induction Nat.lt_wf_0 (fun n => n = n)).
  intros. reflexivity.
Qed.

(* Defining a function by well-founded recursion on a custom measure *)
Definition ack_measure (p : nat * nat) : nat :=
  let (m, n) := p in m + n.

(* Using Fix from Stdlib.Init.Wf for well-founded fixpoints *)
Require Import Stdlib.Init.Wf.
Check Fix : forall (A : Type) (R : A -> A -> Prop), 
  well_founded R -> 
  forall P : A -> Type, 
  (forall x : A, (forall y : A, R y x -> P y) -> P x) -> 
  forall x : A, P x.
```

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

### String Operations in Coq

Source: https://context7.com/rocq-prover/stdlib/llms.txt

Demonstrates basic string manipulation and comparison using the Stdlib.Strings module. Requires opening the string_scope.

```Coq
From Stdlib Require Import Strings.String Strings.Ascii.

Open Scope string_scope.

(* String literals via double-quote notation *)
Definition hello : string := "hello".
Definition world : string := "world".

(* Append *)
Compute hello ++ " " ++ world.  (* = "hello world" *)

(* Length *)
Compute String.length hello.    (* = 5 *)

(* Boolean equality *)
Compute ("hello" =? "hello")%string.  (* = true *)
Compute ("hello" =? "world")%string.  (* = false *)

(* eqb_spec: reflection lemma *)
Lemma str_eq : ("hello" =? "hello")%string = true.
Proof. reflexivity. Qed.

Lemma str_neq : ("hello" =? "world")%string = false.
Proof. reflexivity. Qed.

(* Decidable equality *)
Lemma string_eq_dec : forall s1 s2 : string, {s1 = s2} + {s1 <> s2}.
Proof. apply string_dec. Qed.

(* Substring *)
Compute substring 0 5 "hello world".  (* = "hello" *)
Compute substring 6 5 "hello world".  (* = "world" *)
```

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

### Format Inference Rules

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

Use the `inference` directive to format inference rules, including premises and conclusions. It can also serve as an example for creating custom Sphinx directives.

```rst
.. inference:: Prod-Pro

   \WTEG{T}{s}
   s \in \Sort
   \WTE{\Gamma::(x:T)}{U}{\Prop}
   -----------------------------
   \WTEG{\forall~x:T,U}{\Prop}
```

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

### Preparing a Fix with Git

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

Commands to prepare a fix: checkout master, pull updates, create a new topic branch, add modified files, commit with a detailed message, and push to your origin branch.

```shell
# Make sure we start from an up-to-date master
git checkout master
git pull --ff-only # If this fails, then your master branch is messy
git checkout -b my-topic-branch
# Modify some files
git add .
# Every untracked or modified file will be included in the next commit
# You can also replace the dot with an explicit list of files
git commit -m "My commit summary.

You can add more information on multiple lines,
but you need to skip a line first."
git push -u origin my-topic-branch
# Next time, you push to this branch, you can just do git push
```

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

### Correct Nested Directive Usage

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

Demonstrates the correct way to nest `cmd` and `cmdv` directives, ensuring proper indentation for nested content.

```rst
.. code::

   .. cmd:: Foo @bar

      Foo the first instance of :token:`bar`\ s.

      .. cmdv:: Foo All

         Foo all the :token:`bar`\ s in
         the current context
```

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

### Lists: Length and Append (`++`)

Source: https://context7.com/rocq-prover/stdlib/llms.txt

Demonstrates calculating the length of a list and appending two lists using the `++` operator. Includes a lemma `app_len` proving that the length of a concatenated list is the sum of the individual lengths.

```coq
Compute length ex_list.
(* = 5 *)
```

```coq
Compute [1;2] ++ [3;4].
(* = [1;2;3;4] *)
```

```coq
Lemma app_len (A:Type) (l1 l2 : list A) : length (l1 ++ l2) = length l1 + length l2.
Proof. apply length_app. Qed.
```

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

### PeanoNat Module for Natural Numbers in Coq

Source: https://context7.com/rocq-prover/stdlib/llms.txt

Introduces recursion and induction principles for natural numbers using the Arith.PeanoNat module. Standard induction and helper lemmas are demonstrated.

```Coq
From Stdlib Require Import Arith.PeanoNat.

(* Recursion combinator *)
Definition factorial : nat -> nat :=
  Nat.recursion 1 (fun n acc => (n + 1) * acc).

Compute factorial 0.   (* = 1 *)
Compute factorial 5.   (* = 120 *)

(* Standard induction on nat *)
Lemma sum_n (n : nat) : 2 * fold_left Nat.add (List.seq 1 n) 0 = n * (n + 1).
Proof.
  induction n as [|n IH]; [reflexivity|].
  rewrite List.seq_S, List.fold_left_app; simpl fold_left.
  rewrite <- IH. ring.
Qed.

(* pred_succ / pred_0 *)
Example pred_ex1 : Nat.pred 5 = 4. Proof. reflexivity. Qed.
Example pred_ex2 : Nat.pred 0 = 0. Proof. reflexivity. Qed.

(* lt_succ_r: bridge between < and <= *)
Lemma lt_le_bridge (n m : nat) : n < S m <-> n <= m.
Proof. apply Nat.lt_succ_r. Qed.
```

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

### Classical Logic Axioms in Coq

Source: https://context7.com/rocq-prover/stdlib/llms.txt

Introduces classical logic axioms in Coq, including the law of excluded middle (`classic`) and double-negation elimination (`NNPP`). It also demonstrates classical proof by contradiction and De Morgan's laws for negation.

```coq
From Stdlib Require Import Logic.Classical.

(* Law of excluded middle *)
Lemma lem_example (P : Prop) : P \/ ~ P.
Proof. apply classic. Qed.

(* Double negation elimination *)
Lemma dne_example (P : Prop) : ~ ~ P -> P.
Proof. apply NNPP. Qed.

(* Classical proof by contradiction *)
Lemma classic_absurd (P Q : Prop) : (~ P -> Q) -> ~ Q -> P.
Proof.
  intros H HQ.
  apply NNPP. intro HP.
  apply HQ. apply H. exact HP.
Qed.

(* imply_to_or: implication as disjunction *)
Lemma imp_or (P Q : Prop) : (P -> Q) -> ~ P \/ Q.
Proof. apply imply_to_or. Qed.

(* not_and_or: De Morgan for conjunction *)
Lemma not_and (P Q : Prop) : ~ (P /\ Q) -> ~ P \/ ~ Q.
Proof. apply not_and_or. Qed.
```

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

### Group Multiple Coq Commands as Synonyms

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

Demonstrates grouping multiple Coq commands (vernacs) that are synonyms using the `cmdv` directive. This is useful for documenting commands that share the same functionality but have different names.

```rst
.. cmdv:: Lemma @ident {* @binder } : @type
          Remark @ident {* @binder } : @type
          Fact @ident {* @binder } : @type
          Corollary @ident {* @binder } : @type
          Proposition @ident {* @binder } : @type
   :name: Lemma; Remark; Fact; Corollary; Proposition

   These commands are all synonyms of :n:`Theorem @ident {* @binder } : type`.
```

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

### Using `rocqdoc` for Syntax Highlighting

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

Employ the `rocqdoc::` directive for syntax highlighting of code blocks within documentation. This directive correctly renders code structures.

```rst
.. code::

   A tactic of the form:

   .. rocqdoc::

      do [ t1 | … | tn ].

   is equivalent to the standard Ltac expression:

   .. rocqdoc::

      first [ t1 | … | tn ].
```

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

### Lists: Reverse and Map Operations

Source: https://context7.com/rocq-prover/stdlib/llms.txt

Demonstrates reversing a list using `rev` and applying a function to each element using `map`. Includes a lemma `rev_inv` proving that reversing a list twice returns the original list, and `map_len` proving length preservation.

```coq
Compute rev ex_list.
(* = [5;4;3;2;1] *)
```

```coq
Lemma rev_inv (A:Type)(l:list A): rev (rev l) = l.
Proof. apply rev_involutive. Qed.
```

```coq
Compute map (fun x => x * 2) ex_list.
(* = [2;4;6;8;10] *)
```

```coq
Lemma map_len (A B:Type)(f:A->B)(l:list A): length (map f l) = length l.
Proof. apply length_map. Qed.
```

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

### Correct Token Role Usage

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

Shows the correct usage of the `:n:` role for tactic equivalences, avoiding overuse of the `:token:` role for general notation.

```rst
This is equivalent to :n:`Axiom @ident : @term`.
```

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

### Avoiding `rocqtop` for Syntax Highlighting

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

Do not use the `rocqtop::` directive for general syntax highlighting of code. Use `rocqdoc::` instead for better compatibility and clarity.

```rst
.. code::

   A tactic of the form:

   .. rocqtop:: in

      do [ t1 | … | tn ].

   is equivalent to the standard Ltac expression:

   .. rocqtop:: in

      first [ t1 | … | tn ].
```

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

### Correct Tactic Notation Usage

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

Demonstrates the correct way to use the `:n:` role for tactic parameters like `@term` and `@ltac`, ensuring clarity in tactic descriptions.

```rst
:n:`power_tac @term [@ltac]`
  allows :tacn:`ring` and :tacn:`ring_simplify` to recognize …
```

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

### NArith: Basic Binary Natural Number Arithmetic

Source: https://context7.com/rocq-prover/stdlib/llms.txt

Demonstrates fundamental arithmetic operations for binary natural numbers (N). Includes addition, multiplication, exponentiation, division, and GCD. Requires opening the N_scope.

```coq
Compute N.add 100 200.
(* = 300 *)
```

```coq
Compute N.mul 1000 1000.
(* = 1000000 *)
```

```coq
Compute N.pow 2 32.
(* = 4294967296 *)
```

```coq
Compute N.div 1000 7.
(* = 142 *)
```

```coq
Compute N.gcd 48 18.
(* = 6 *)
```

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

### Lists: Membership and Decidable Equality

Source: https://context7.com/rocq-prover/stdlib/llms.txt

Demonstrates checking for element membership in a list using `In`. The `in_dec` lemma shows how to use decidable equality to prove membership or non-membership.

```coq
Lemma in_ex : In 3 ex_list.
Proof. simpl. tauto. Qed.
```

```coq
Lemma in_dec_example : {In 3 ex_list} + {~ In 3 ex_list}.
Proof. apply in_dec. apply Nat.eq_dec. Qed.
```

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

### Key Algebraic Lemmas for Natural Numbers

Source: https://context7.com/rocq-prover/stdlib/llms.txt

Illustrates proving commutativity of addition and distributivity of multiplication over addition.

```Coq
(* Key algebraic lemmas *)
Lemma add_comm_example (n m : nat) : n + m = m + n.
Proof. apply Nat.add_comm. Qed.

Lemma mul_dist_example (n m k : nat) : n * (m + k) = n * m + n * k.
Proof. apply Nat.mul_add_distr_l. Qed.
```

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

### Coq Real Number DiscrR Tactic

Source: https://github.com/rocq-prover/stdlib/blob/master/doc/sphinx/language/coq-library.rst

Uses the `discrR` tactic to prove that two real integer constants are different. Requires importing `DiscrR`.

```Coq
From Stdlib Require Import DiscrR.
Open Scope R_scope.
Goal 5 <> 0.
Proof.
discrR.
```

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

### Correct Notation Syntax

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

Use the `n:` role for names and attributes within notations. Avoid using plain quotes for these elements.

```rst
.. code::

   :n:`name={*; attr}`
```

```rst
.. code::

   ``name=``:n:`{*; attr}`
```

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

### Coq Floats Library Import

Source: https://github.com/rocq-prover/stdlib/blob/master/doc/sphinx/language/coq-library.rst

Imports the `Floats` module from the standard library to access primitive floating-point operations.

```Coq
From Stdlib Require Import Floats.
```

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

### Check Core Datatype Constructors

Source: https://context7.com/rocq-prover/stdlib/llms.txt

Verify the types of fundamental constructors for boolean and natural number types.

```Coq
Check true : bool.
Check false : bool.
```

```Coq
Check O : nat.          (* zero *)
Check S O : nat.          (* one *)
Check 3 : nat.          (* notation for S (S (S O)) *)
```

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

### Natural Number Order Relations

Source: https://context7.com/rocq-prover/stdlib/llms.txt

Demonstrates using the less than or equal to operator and proving transitivity of the less than operator.

```Coq
(* Order *)
Example le_example : 3 <= 5.
Proof. repeat constructor. Qed.

Lemma lt_trans_example : 1 < 2 -> 2 < 3 -> 1 < 3.
Proof. intros. apply (Nat.lt_trans _ 2); assumption. Qed.
```

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

### Include TeX File for MathJax

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

The `preamble` directive is used to include a TeX file, primarily to inform MathJax about definitions and commands. The file content is wrapped in a math environment.

```rst
.. preamble:: preamble.tex
```

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

### Lists: Filter, Fold, and Boolean Checks

Source: https://context7.com/rocq-prover/stdlib/llms.txt

Illustrates filtering list elements based on a predicate (`filter`), accumulating a value from a list (`fold_left`, `fold_right`), and checking universal (`forallb`) or existential (`existsb`) properties.

```coq
Compute filter (fun x => Nat.leb 3 x) ex_list.
(* = [3;4;5] *)
```

```coq
Compute fold_left  Nat.add ex_list 0.
(* = 15 *)
```

```coq
Compute fold_right Nat.add 0 ex_list.
(* = 15 *)
```

```coq
Compute forallb (fun x => Nat.ltb 0 x) ex_list.
(* = true  (all > 0) *)
```

```coq
Compute existsb (fun x => Nat.eqb x 3) ex_list.
(* = true  (3 is in list) *)
```

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

### Correct Use of Sphinx Roles

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

Utilize Sphinx roles like `:tacn:` for tactics and `:exn:` for exceptions, and `:g:` for terms. This ensures proper cross-referencing and highlighting. Avoid using plain quotes for these.

```rst
.. code::

   The :tacn:`refine` tactic can raise the :exn:`Invalid argument` exception.
   The term :g:`let a = 1 in a a` is ill-typed.
```

```rst
.. code::

   The ``refine`` tactic can raise the ``Invalid argument`` exception.
   The term ``let a = 1 in a a`` is ill-typed.
```

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

### Display Rocqtop-Formatted Source Code

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

Use `rocqdoc` to display Rocq code. This directive is useful for highlighting code snippets within documentation.

```rst
.. rocqdoc::

   Rocq code to highlight
```

```rst
.. rocqdoc::

   Definition test := 1.
```

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

### NArith: Bitwise Operations

Source: https://context7.com/rocq-prover/stdlib/llms.txt

Demonstrates bitwise logical operations on N integers: bitwise AND (`N.land`), bitwise OR (`N.lor`), and left shift (`N.shiftl`).

```coq
Compute N.land 12 10.
(* = 8  (1100 & 1010 = 1000) *)
```

```coq
Compute N.lor  12 10.
(* = 14 (1100 | 1010 = 1110) *)
```

```coq
Compute N.shiftl 1 8.
(* = 256 *)
```

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

### Changelog Entry Format

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

This is the standard format for changelog entries, indicating the affected file and a description of the changes, including PR and issue references.

```rst
- in `SomeFile.v`

  + lemmas `lem1`, `lem2` and `lem3`
  (`#PRNUM <https://github.com/coq/stdlib/pull/PRNUM>`_,
  [fixes `#ISSUE1 <https://github.com/coq/stdlib/issues/ISSUE1>`_
  [ and `#ISSUE2 <https://github.com/coq/stdlib/issues/ISSUE2>`_],
  by Full Name[, with help / review of Full Name]).
```