Rocq Prover

https://rocq-prover.org/doc/V9.1.0/refman/
Admin
Rocq Prover is an interactive theorem prover and proof assistant based on the Calculus of Inductive...
Tokens:323,373
Snippets:4,925
Trust Score:9.1
Update:2 months ago
Show doc for...
Tokens:
Raw
### Mathematical Components bigop setup

Source: https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/ssreflect-proof-language.html

Setup and definitions for the bigop theory used in the proof example.

```Coq
From Corelib Require Import ssreflect. 


Set Implicit Arguments. 


Unset Strict Implicit. 


Unset Printing Implicit Defensive. 


Coercion is_true : bool >-> Sortclass. 
    is_true is now a coercion  

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. 
    bigbody is defined  

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

Axiom eq_bigr_ : forall (R : Type) (idx : R) (op : forall (_ : R) (_ : R), R) (I : Type) (r : list I) (P : I -> bool) (F1 F2 : I -> R), (forall x : I, is_true (P x) -> F1 x = F2 x) -> bigop idx r (fun i : I => BigBody i op (P i) (F1 i)) = bigop idx r (fun i : I => BigBody i op (P i) (F2 i)). 
    eq_bigr_ is declared  

Axiom eq_big_ : forall (R : Type) (idx : R) (op : R -> R -> R) (I : Type) (r : list I) (P1 P2 : I -> bool) (F1 F2 : I -> R), (forall x : I, P1 x = P2 x) -> (forall i : I, is_true (P1 i) -> F1 i = F2 i) -> bigop idx r (fun i : I => BigBody i op (P1 i) (F1 i)) = bigop idx r (fun i : I => BigBody i op (P2 i) (F2 i)). 
    eq_big_ is declared  

Reserved Notation "\sum_ ( m <= i < n | P ) F" (at level 41, F at level 41, i, m, n at level 50, format "'[' \sum_ ( m <= i < n | P ) '/ ' F ']'"). 


Parameter index_iota : nat -> nat -> list nat. 
    index_iota is declared  

Notation "\big [ op / idx ]_ ( m <= i < n | P ) F" := (bigop idx (index_iota m n) (fun i : nat => BigBody i op P%bool F)). 


Notation "\sum_ ( m <= i < n | P ) F" := (\big[plus/O]_(m <= i < n | P%bool) F%nat). 


Notation eq_bigr := (fun n m => eq_bigr_ 0 plus (index_iota n m)). 


Notation eq_big := (fun n m => eq_big_ 0 plus (index_iota n m)). 


Parameter odd : nat -> bool. 
    odd is declared  

Parameter prime : nat -> bool. 
    prime is declared  

Parameter addnC : forall m n : nat, m + n = n + m. 
    addnC is declared  

Parameter muln1 : forall n : nat, n * 1 = n. 
    muln1 is declared  

Check eq_bigr. 
    eq_bigr : forall (n m : nat) (P : nat -> bool) (F1 F2 : nat -> nat), (forall x : nat, P x -> F1 x = F2 x) -> \sum_(n <= i < m | P i) F1 i = \sum_(n <= i < m | P i) F2 i  

Check eq_big. 
    eq_big : forall (n m : nat) (P1 P2 : nat -> bool) (F1 F2 : nat -> nat), (forall x : nat, P1 x = P2 x) -> (forall i : nat, P1 i -> F1 i = F2 i) -> \sum_(n <= i < m | P1 i) F1 i = \sum_(n <= i < m | P2 i) F2 i
```

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

### Setup for rewriting under binders example

Source: https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/ssreflect-proof-language.html

Initial definitions and axioms required to demonstrate the rewriting problem.

```coq
From Corelib Require Import ssreflect. 


Set Implicit Arguments. 


Unset Strict Implicit. 


Unset Printing Implicit Defensive. 


Axiom subnn : forall n : nat, n - n = 0. 
    subnn is declared  

Parameter map : (nat -> nat) -> list nat -> list nat. 
    map is declared  

Parameter sumlist : list nat -> nat. 
    sumlist is declared  

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. 
    eq_map is declared
```

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

### Require command example

Source: https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/vernacular-commands.html

An example showing how to load a module while specifying the directory path.

```text
From Stdlib Require Nat
```

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

### Setup for Generalized Rewriting Example

Source: https://rocq-prover.org/doc/V9.1.0/refman/addendum/generalized-rewriting.html

Initial imports and definitions required to demonstrate a setoid_rewrite failure.

```coq
Require Import Relation_Definitions RelationClasses Morphisms. 


Parameter A : Type. 
    A is declared  

Fixpoint In (a : A) (s : list A) {struct s} : Prop := match s with | nil => False | cons b s' => a = b \/ In a s' end. 
    In is defined In is recursively defined (guarded on 2nd argument)  

Definition same (s t : list A) : Prop := forall a : A, In a s <-> In a t. 
    same is defined  

Parameter same_equiv : Equivalence same. 
    same_equiv is declared  

#[local] Existing Instance same_equiv.
```

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

### Dependent Inversion Example

Source: https://rocq-prover.org/doc/V9.1.0/refman/proofs/writing-proofs/reasoning-inductives.html

Demonstrates the setup for dependent inversion where the hypothesis occurs in the goal.

```coq
Goal forall n m (H:Le (S n) m), Q (S n) m H.
intros.
```

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

### Setup Setoid Theory

Source: https://rocq-prover.org/doc/V9.1.0/refman/addendum/generalized-rewriting.html

Initial setup for a theory of homogeneous sets, including imports and parameter declarations.

```Coq
Require Export Setoid. 


Require Export Relation_Definitions. 


Set Implicit Arguments. 


Parameter set : Type -> Type. 
    set is declared  

Parameter empty : forall A, set A. 
    empty is declared  

Parameter eq_set : forall A, set A -> set A -> Prop. 
    eq_set is declared  

Parameter union : forall A, set A -> set A -> set A. 
    union is declared  

Axiom eq_set_refl : forall A, reflexive _ (eq_set (A:=A)). 
    eq_set_refl is declared  

Axiom eq_set_sym : forall A, symmetric _ (eq_set (A:=A)). 
    eq_set_sym is declared  

Axiom eq_set_trans : forall A, transitive _ (eq_set (A:=A)). 
    eq_set_trans is declared  

Axiom empty_neutral : forall A (S : set A), eq_set (union S (empty A)) S. 
    empty_neutral is declared
```

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

### Configure _CoqProject for package installation

Source: https://rocq-prover.org/doc/V9.1.0/refman/practical-tools/utilities.html

Example of a _CoqProject file configuration where the 'theories' directory path is omitted in the installed structure.

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

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

### SSReflect proof setup

Source: https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/ssreflect-proof-language.html

Initial configuration and axioms for natural number arithmetic proofs.

```Coq
From Corelib Require Import ssreflect. 


Set Implicit Arguments. 


Unset Strict Implicit. 


Unset Printing Implicit Defensive. 


Axiom addn0 : forall m, m + 0 = m. 


Axiom addnS : forall m n, m + S n = S (m + n). 


Axiom addSnnS : forall m n, S m + n = m + S n.
```

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

### Initialize SSReflect Proof Environment

Source: https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/ssreflect-proof-language.html

Standard setup commands for an SSReflect proof script.

```Coq
From Corelib Require Import ssreflect. 


Set Implicit Arguments. 


Unset Strict Implicit. 


Unset Printing Implicit Defensive. 


Lemma subnK : forall m n, n <= m -> m - n + n = m. 
    1 goal ============================ forall m n : nat, n <= m -> m - n + n = m
```

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

### Nested bigop proof example

Source: https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/ssreflect-proof-language.html

A proof example demonstrating the use of nested under tactics to rewrite within bigop summations.

```Coq
Lemma test_big_nested (m n : nat) : \sum_(0 <= a < m | prime a) \sum_(0 <= j < n | odd (j * 1)) (a + j) = \sum_(0 <= i < m | prime i) \sum_(0 <= j < n | odd j) (j + i). 
    1 goal m, n : nat ============================ \sum_(0 <= a < m | prime a) \sum_(0 <= j < n | odd (j * 1)) (a + j) = \sum_(0 <= i < m | prime i) \sum_(0 <= j < n | odd j) (j + i)  

under eq_bigr => i prime_i do under eq_big => [ j | j odd_j ] do [ rewrite (muln1 j) | rewrite (addnC i j) ]. 
    1 goal m, n : nat ============================ \sum_(0 <= i < m | prime i) \sum_(0 <= j < n | odd j) (j + i) = \sum_(0 <= i < m | prime i) \sum_(0 <= j < n | odd j) (j + i)
```

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

### Non-dependent Inversion Example

Source: https://rocq-prover.org/doc/V9.1.0/refman/proofs/writing-proofs/reasoning-inductives.html

Demonstrates using inversion_clear and inversion on a non-dependent goal.

```coq
Variable P : nat -> nat -> Prop.
Variable Q : forall n m:nat, Le n m -> Prop.
Goal forall n m, Le (S n) m -> P n m.
intros.
inversion_clear H.
intros.
inversion H.
```

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

### Example of goal reordering with selectors

Source: https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/ltac.html

Demonstrates how applying a tactic to specific goals reorders them.

```coq
Goal 1=0 /\ 2=0 /\ 3=0. 
    1 goal ============================ 1 = 0 /\ 2 = 0 /\ 3 = 0  

repeat split. 
    3 goals ============================ 1 = 0 goal 2 is: 2 = 0 goal 3 is: 3 = 0  

1,3: idtac. 
    3 goals ============================ 1 = 0 goal 2 is: 3 = 0 goal 3 is: 2 = 0 
```

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

### Demonstrate first-class backtracking

Source: https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/ltac2.html

Examples showing how to use backtracking primitives to handle branches and failures.

```Ltac2
From Ltac2 Require Import Printf.


(* `bs` holds a backtracking string *)


Ltac2 bs () := Control.plus (fun () => "x") (fun _ => "y").


(* Prints the first branch "x" and terminates successfully. *)


Ltac2 Eval (let s := bs () in printf "%s" s).
    x - : unit = ()

(* Prints both branches and returns the error. *)


Ltac2 print_and_fail (s : string) := printf "%s" s ; Control.zero (Tactic_failure None).


Ltac2 Eval (Control.case (fun () => let s := bs () in print_and_fail s)).
    x y - : ('a * (exn -> 'a)) result = Err (Tactic_failure None)
```

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

### SSReflect Clear Discipline Syntax

Source: https://rocq-prover.org/doc/V9.1.0/refman/changes.html

Examples of how clear switches are elaborated when applied to existing proof context entries.

```Coq
=> {x..} H -> => {x..H} H
```

```Coq
=> {x..} /H -> => /v {x..H}
```

```Coq
rewrite {x..} H -> rewrite E {x..H}
```

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

### Performing Head Reduction

Source: https://rocq-prover.org/doc/V9.1.0/refman/changes.html

Example of using the head flag with Eval to perform head reduction on a term.

```coq
Eval lazy head in (fun x => Some ((fun y => y) x)) 0
```

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

### Example _CoqProject configuration

Source: https://rocq-prover.org/doc/V9.1.0/refman/practical-tools/utilities.html

A sample configuration file defining project directories, compiler arguments, and plugin metadata generation.

```text
-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 environment for Ssreflect proof

Source: https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/ssreflect-proof-language.html

Initializes the environment with required modules, implicit argument settings, and custom notations.

```Coq
From Corelib Require Import ssreflect ssrfun ssrbool. 


Set Implicit Arguments. 


Unset Strict Implicit. 


Unset Printing Implicit Defensive. 


Axiom P : nat -> Prop. 
    P is declared  

Axioms eqn leqn : nat -> nat -> bool. 
    eqn is declared leqn is declared  

Declare Scope this_scope. 


Notation "a != b" := (eqn a b) (at level 70) : this_scope. 


Notation "a <= b" := (leqn a b) (at level 70) : this_scope. 
    Setting b constr at next level to match previous notation with longest common prefix: "_ <= _".  

Open Scope this_scope.
```

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

### SearchPattern examples

Source: https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/vernacular-commands.html

Examples of using SearchPattern to find theorems matching specific structural patterns.

```Rocq
From Stdlib Require Import Arith.
SearchPattern (_ + _ = _ + _).
SearchPattern (nat -> bool).
SearchPattern (forall l : list _, _ l l).
SearchPattern (?X1 + _ = _ + ?X1).
```

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

### Discriminate limitation example

Source: https://rocq-prover.org/doc/V9.1.0/refman/proofs/writing-proofs/reasoning-inductives.html

Example showing that discriminate cannot handle n <> S n, requiring induction instead.

```Rocq
Goal forall n:nat, n <> S n. 
    1 goal ============================ forall n : nat, n <> S n  

intro n. 
    1 goal n : nat ============================ n <> S n  

induction n. 
    2 goals ============================ 0 <> 1 goal 2 is: S n <> S (S n)
```

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

### Weakening Lemma Proof Setup

Source: https://rocq-prover.org/doc/V9.1.0/refman/proofs/writing-proofs/reasoning-inductives.html

Shows the manual approach to weakening proofs versus using dependent induction.

```coq
Lemma weakening : forall G D tau, term (G ; D) tau -> forall tau', term (G , tau' ; D) tau.
    1 goal ============================ forall (G D : ctx) (tau : type), term (G; D) tau -> forall tau' : type, term ((G, tau'); D) tau 

Lemma weakening' : forall G' tau, term G' tau -> forall G D, (G ; D) = G' -> forall tau', term (G, tau' ; D) tau.
    1 goal ============================ forall (G' : ctx) (tau : type), term G' tau -> forall G D : ctx, G; D = G' -> forall tau' : type, term ((G, tau'); D) tau
```

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

### Basic Module Import and Visibility

Source: https://rocq-prover.org/doc/V9.1.0/refman/language/core/modules.html

Demonstrates how to define a module and make its contents available via the Import command.

```coq
Module Mod. 
    Interactive Module Mod started  

Definition T:=nat. 
    T is defined  

Check T. 
    T : Set 

End Mod. 
    Module Mod is defined  

Check Mod.T. 
    Mod.T : Set 

Fail Check T. 
    The command has indeed failed with message: The reference T was not found in the current environment.  

Import Mod. 


Check T. 
    T : Set
```

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

### Reified arithmetic goal example

Source: https://rocq-prover.org/doc/V9.1.0/refman/addendum/micromega.html

Example of a reified arithmetic goal and its associated witness and variable map.

```Coq
example_lra = fun x y : Q => let __arith : forall __x2 __x1 : Q, __x1 + 2 * __x2 <= 4 -> 2 * __x1 + __x2 <= 4 -> __x1 + __x2 < 3 := fun __x2 __x1 : Q => let __wit := (PsatzAdd (PsatzIn Q 2) (PsatzAdd (PsatzIn Q 1) (PsatzMulE (PsatzC 3) (PsatzIn Q 0))) :: nil)%list in let __varmap := VarMap.Branch (VarMap.Elt __x2) __x1 VarMap.Empty in let __ff := IMPL (A isProp {| Flhs := PEadd (PEX 1) (PEmul (PEc 2) (PEX 2)); Fop := OpLe; Frhs := PEc 4 |} tt) None (IMPL (A isProp {| Flhs := PEadd (PEmul (PEc 2) (PEX 1)) (PEX 2); Fop := OpLe; Frhs := PEc 4 |} tt) None (A isProp {| Flhs := PEadd (PEX 1) (PEX 2); Fop := OpLt; Frhs := PEc 3 |} tt)) in QTautoChecker_sound __ff __wit (eq_refl <: QTautoChecker __ff __wit = true) (VarMap.find 0 __varmap) in __arith y x : forall x y : Q, x + 2 * y <= 4 -> 2 * x + y <= 4 -> x + y < 3 Arguments example_lra (x y)%_Q_scope _ _
```

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

### List installed Rocq packages

Source: https://rocq-prover.org/doc/V9.1.0/refman/practical-tools/utilities.html

Displays installed packages matching the coq-* pattern with their versions and descriptions.

```bash
$ opam list "coq-*" --installed
coq-bignums               8.15.0          Bignums, the Coq library of arbitrary large numbers
```

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

### Locate Objects and Notations

Source: https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/vernacular-commands.html

Examples demonstrating how to use the Locate command to find definitions, constructors, and verify object existence.

```Rocq
Locate nat.
    Inductive Corelib.Init.Datatypes.nat
```

```Rocq
Locate Datatypes.O.
    Constructor Corelib.Init.Datatypes.O (shorter name to refer to it in current context is O)
```

```Rocq
Locate Init.Datatypes.O.
    Constructor Corelib.Init.Datatypes.O (shorter name to refer to it in current context is O)
```

```Rocq
Locate Stdlib.Init.Datatypes.O.
    No object of suffix Stdlib.Init.Datatypes.O
```

```Rocq
Locate I.Dont.Exist.
    No object of suffix I.Dont.Exist
```

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

### Using dependent destruction

Source: https://rocq-prover.org/doc/V9.1.0/refman/proofs/writing-proofs/reasoning-inductives.html

Demonstrates the manual setup for dependent destruction using the provided lemma.

```coq
Lemma ex : forall n m:nat, Le (S n) m -> P n m. 
    intros n m H. 
```

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

### Example of Ring Expression Subterms

Source: https://rocq-prover.org/doc/V9.1.0/refman/addendum/ring.html

An example of a Gallina expression in the nat semiring and its corresponding concrete normal polynomial.

```Gallina
(plus (mult (plus (f (5)) x) x)
      (mult (if b then (4) else (f (3))) (2)))
```

```Gallina
(plus (mult (2) (if b then (4) else (f (3))))
      (plus (mult (f (5)) x) (mult x x)))
```

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

### Apply View Tactics in Proofs

Source: https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/ssreflect-proof-language.html

Examples demonstrating the use of view tactics like apply/andP and have/andP in proof scripts.

```Coq
From Corelib Require Import ssreflect ssrbool. 


Set Implicit Arguments. 


Unset Strict Implicit. 


Unset Printing Implicit Defensive. 


Section Test. 


Lemma test (a b : bool) (Ha : a) (Hb : b) : ~~ (a && b).
    1 goal a, b : bool Ha : a Hb : b ============================ ~~ (a && b)  

apply/andP.
    1 goal a, b : bool Ha : a Hb : b ============================ ~ (a /\ b)
```

```Coq
From Corelib Require Import ssreflect ssrbool. 


Set Implicit Arguments. 


Unset Strict Implicit. 


Unset Printing Implicit Defensive. 


Section Test. 


Lemma test (a b : bool) (pab : b && a) : b. 
    1 goal a, b : bool pab : b && a ============================ b  

have /andP [pa ->] : (a && b) by rewrite andbC. 
    1 goal a, b : bool pab : b && a pa : a ============================ true
```

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

### SearchRewrite examples

Source: https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/vernacular-commands.html

Examples of using SearchRewrite to find theorems where a pattern matches the left or right hand side of an equality.

```Rocq
From Stdlib Require Import Arith.
SearchRewrite (_ + _ + _).
```

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

### Initialize SSReflect Environment

Source: https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/ssreflect-proof-language.html

Load the required libraries and configure settings to match the SSReflect methodology.

```coq
From Corelib Require Import ssreflect ssrfun ssrbool.
```

```coq
Set Implicit Arguments.
```

```coq
Unset Strict Implicit.
```

```coq
Unset Printing Implicit Defensive.
```

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

### Define a Section

Source: https://rocq-prover.org/doc/V9.1.0/refman/addendum/type-classes.html

Starts a section for grouping definitions.

```Coq
Section EqDec_defs.
```

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

### Prove a goal using tauto without explicit intros

Source: https://rocq-prover.org/doc/V9.1.0/refman/proofs/automatic-tactics/logic.html

Shows that tauto performs introductions automatically when needed.

```coq
Goal forall (A:Prop) (P:nat -> Prop), A \/ (forall x:nat, ~ A -> P x) -> forall x:nat, ~ A -> P x. 
    1 goal ============================ forall (A : Prop) (P : nat -> Prop), A \/ (forall x : nat, ~ A -> P x) -> forall x : nat, ~ A -> P x  

tauto. 
    No more goals.
```

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

### Interactive under/over proof example

Source: https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/ssreflect-proof-language.html

Demonstrates the step-by-step process of using under to focus on a sub-term, rewriting it, and using over to return to the main goal.

```Coq
Lemma example_map l : sumlist (map (fun m => m - m) l) = 0.
```

```Coq
under eq_map => m.
```

```Coq
rewrite subnn.
```

```Coq
over.
```

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

### Check notation expression

Source: https://rocq-prover.org/doc/V9.1.0/refman/user-extensions/syntax-extensions.html

Example of checking a nested IF-then-else expression.

```Coq
Check (IF_then_else (IF_then_else True False True) (IF_then_else True False True) (IF_then_else True False True)). 
    If If True then False else True then If True then False else True else If True then False else True : Prop
```

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

### Define a parametric type

Source: https://rocq-prover.org/doc/V9.1.0/refman/language/extensions/match.html

Example of an inductive polymorphic list type.

```Coq
Inductive List (A:Set) : Set := | nil : List A | cons : A -> List A -> List A.
```

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

### Importing and checking LEQ module

Source: https://rocq-prover.org/doc/V9.1.0/refman/language/extensions/canonical.html

Initial setup to import the LEQ theory and verify the lele_eq lemma.

```coq
Import LEQ.theory. 


Check lele_eq. 
```

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

### Define multiple contextual implicit arguments

Source: https://rocq-prover.org/doc/V9.1.0/refman/language/extensions/implicit-arguments.html

Example where both arguments are contextual.

```coq
forall P:nat->Prop, forall n:nat, P n \/ n = 0
```

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

### Manage section-local variables and definitions

Source: https://rocq-prover.org/doc/V9.1.0/refman/language/core/sections.html

A complete example showing the lifecycle of section variables and definitions, including their generalization upon closing the section.

```coq
Section s1. 


Variables x y : nat. 
    x is declared y is declared 
The command `Let` introduces section-wide Let-in definitions. These definitions won't persist when the section is closed, and all persistent definitions which depend on `y'` will be prefixed with `let y' := y in`. 

Let y' := y. 
    y' is defined  

Definition x' := S x. 
    x' is defined  

Definition x'' := x' + y'. 
    x'' is defined  

Print x'. 
    x' = S x : nat x' uses section variable x.  

Print x''. 
    x'' = x' + y' : nat x'' uses section variables x y.  

End s1. 


Print x'. 
    x' = fun x : nat => S x : nat -> nat Arguments x' x%_nat_scope  

Print x''. 
    x'' = fun x y : nat => let y' := y in x' x + y' : nat -> nat -> nat Arguments x'' (x y)%_nat_scope
```

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

### Obligation natural of ident? with generic_tactic?

Source: https://rocq-prover.org/doc/V9.1.0/refman/addendum/program.html

Starts the proof of a specific obligation.

```APIDOC
## Obligation natural of ident? with generic_tactic?

### Description
Starts the proof of the obligation specified by its natural number index.
```

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

### Using intro and intros tactics

Source: https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/tactics.html

Demonstrates the step-by-step introduction of variables and hypotheses into the context, and the equivalent single-tactic approach.

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

intro m. 
    1 goal m : nat ============================ forall n : nat, m < n -> let x := 0 in True  

intro n. 
    1 goal m, n : nat ============================ m < n -> let x := 0 in True  

intro H. 
    1 goal m, n : nat H : m < n ============================ let x := 0 in True  

intro x. 
    1 goal m, n : nat H : m < n x := 0 : nat ============================ True
```

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

intros m n H x. 
    1 goal m, n : nat H : m < n x := 0 : nat ============================ True
```

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

### Defining boolean connectives

Source: https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/ssreflect-proof-language.html

Example of defining a boolean connective as a computable function.

```Coq
From Corelib Require Import ssreflect. 


Set Implicit Arguments. 


Unset Strict Implicit. 


Unset Printing Implicit Defensive. 


Section Test. 


Definition orb (b1 b2 : bool) := if b1 then true else b2. 
    orb is defined
```

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

### Configure and Print Pattern Matching

Source: https://rocq-prover.org/doc/V9.1.0/refman/language/extensions/match.html

Demonstrates how to toggle the printing of pattern matching for product types using 'Test Printing Let' and 'Remove Printing Let'.

```coq
Definition snd (A B:Set) (H:A * B) := match H with | pair x y => y end.
```

```coq
Test Printing Let for prod.
```

```coq
Print snd.
```

```coq
Remove Printing Let prod.
```

```coq
Unset Printing Synth.
```

```coq
Unset Printing Wildcard.
```

```coq
Print snd.
```

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

### Initialize SSReflect Environment

Source: https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/ssreflect-proof-language.html

Standard setup for loading SSReflect libraries and configuring implicit argument behavior.

```coq
From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat zify.
```

```coq
Set Implicit Arguments.
```

```coq
Unset Strict Implicit.
```

```coq
Unset Printing Implicit Defensive.
```

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

### Branching and destructuring patterns

Source: https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/ssreflect-proof-language.html

Examples of equivalent branching and destructuring patterns in SSReflect.

```Coq
move=> [a b].
case=> [a b].
case=> a b.
```

```Coq
case=> [] [a b] c.
move=> [[a b] c].
case; case=> a b c.
```

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

### Display build timing table

Source: https://rocq-prover.org/doc/V9.1.0/refman/practical-tools/utilities.html

Example output generated by the make pretty-timed target, showing build times and peak memory usage.

```text
ROCQ DEP VFILES
ROCQ C Slow.v
Slow.vo (real: 0.52, user: 0.39, sys: 0.12, mem: 394648 ko)
ROCQ C Fast.v
Fast.vo (real: 0.06, user: 0.02, sys: 0.03, mem: 56980 ko)
    Time |  Peak Mem | File Name
--------------------------------------------
0m00.41s | 394648 ko | Total Time / Peak Mem
--------------------------------------------
0m00.39s | 394648 ko | Slow.vo
0m00.02s |  56980 ko | Fast.vo
```

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

### Proving 1 <> 2

Source: https://rocq-prover.org/doc/V9.1.0/refman/proofs/writing-proofs/reasoning-inductives.html

Example demonstrating the use of discriminate to prove an inequality.

```Rocq
Goal 1 <> 2. 
    1 goal ============================ 1 <> 2  

discriminate. 
    No more goals.  

Qed.
```

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

### Trace tactic execution steps

Source: https://rocq-prover.org/doc/V9.1.0/refman/practical-tools/coqide.html

Example demonstrating the two-phase execution process for the tactic construct.

```coq
idtac "A"; idtac "B"; idtac "C".
```

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

### Match Expression Syntax

Source: https://rocq-prover.org/doc/V9.1.0/refman/language/core/inductive.html

Example of a match expression on a list in concrete syntax.

```Rocq
match t as l return P' with
| nil _ => t1
| cons _ hd tl => t2
end
```

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

### Define a singleton inductive type

Source: https://rocq-prover.org/doc/V9.1.0/refman/language/core/inductive.html

Example of a singleton inductive type definition.

```coq
Inductive prod (A B:Type) : Type := pair : A -> B -> prod A B.
```

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

### * intro pattern

Source: https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/tactics.html

Using the wildcard pattern to introduce all variables.

```Coq
Goal forall (A: Prop) (B: Prop), A -> B. 
    1 goal ============================ forall A B : Prop, A -> B  

intros *. 
    1 goal A, B : Prop ============================ A -> B
```

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

### Apply unsupported attribute warning

Source: https://rocq-prover.org/doc/V9.1.0/refman/language/core/basic.html

Example of triggering an unsupported attribute warning.

```Rocq
#[ foo ] Comments.
```

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

### Print All Command

Source: https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/vernacular-commands.html

Displays the current state of the environment, including sections and modules.

```vernacular
Print All
```

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

### Declare a Parametric Relation

Source: https://rocq-prover.org/doc/V9.1.0/refman/addendum/generalized-rewriting.html

Example of declaring Leibniz equality as a parametric relation.

```Coq
Add Parametric Relation (A : Type) : A (@eq A) [reflexivity proved by @refl_equal A] ...
```

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

### Control.plus

Source: https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/ltac2.html

Installs a backtracking point around a computation, providing a handler for exceptions.

```APIDOC
## val plus : (unit -> 'a) -> (exn -> 'a) -> 'a

### Description
Installs a backtracking point around the thunk `t`. If `t` raises an exception via `zero`, the `handler` is invoked to provide an alternative computation.

### Parameters
- **t** (unit -> 'a) - Required - The primary computation to execute.
- **handler** (exn -> 'a) - Required - The function to execute if `t` fails.
```

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

### Combined intro pattern using [=] -> and %

Source: https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/tactics.html

Applying injection, rewriting, and theorem application in one pattern.

```Coq
Require Import ListDef. 


Section IntroPatterns. 


Variables (A : Type) (xs ys : list A). 
    A is declared xs is declared ys is declared  

Axiom length_zero_iff_nil : forall [A] (l : list A), length l = 0 <-> l = nil. 
    length_zero_iff_nil is declared  

Example ThreeIntroPatternsCombined : S (length ys) = 1 -> xs ++ ys = xs. 
    1 goal A : Type xs, ys : list A ============================ S (length ys) = 1 -> xs ++ ys = xs  

intros [=->%length_zero_iff_nil]. 
    1 goal A : Type xs : list A ============================ xs ++ nil = xs
```
Tokens:
Raw