From 94aa933c17d4103b941d35ba344452c51c07dbdc Mon Sep 17 00:00:00 2001
From: tiyn <tiyn@posteo.eu>
Date: Wed, 4 Mar 2026 00:41:30 +0100
Subject: [PATCH] programming language: added rocq

---
 wiki/programming_language/rocq.md | 75 +++++++++++++++++++++++++++++++
 1 file changed, 75 insertions(+)
 create mode 100644 wiki/programming_language/rocq.md

diff --git a/wiki/programming_language/rocq.md b/wiki/programming_language/rocq.md
new file mode 100644
index 0000000..21724fb
--- /dev/null
+++ b/wiki/programming_language/rocq.md
@@ -0,0 +1,75 @@
+# Rocq
+
+[Rocq](https://rocq-prover.org/) is an interactive theorem prover.
+It was formerly known as Coq.
+
+## Setup
+
+Rocq can be installed as explained on [the official website](https://rocq-prover.org/install).
+
+The easiest way to install Rocq is by using Opam due to it also being able to manage packages for
+Rocq.
+Opam needs to be installed for this.
+On most [Linux-based Systems](/wiki/linux.md) the [package manager](/wiki/linux/package_manager.md)
+contains a package called `opam`.
+If Opam was not initialized before, do it using the following commands.
+The command may ask to edit the config file for the shell.
+This is needed to function correctly.
+
+```sh
+opam init
+eval $(opam env)
+```
+
+Then Rocq can be installed using the following command.
+`<version>` has to be set to the desired version to install (for example `9.0.0`).
+
+```sh
+opam pin add rocq-prover <version>
+```
+
+## Usage
+
+This section addresses the usage of Rocq.
+
+### Basic Usage
+
+Rocq proves are saved in `.v` files.
+These can be compiled using the following command where `<file>` is a Rocq proof file.
+
+```sh 
+rocq c <file>
+```
+
+If nothing is shown as output and files like a `.vo` file are generated the proof was successful.
+Otherwise it was not successful.
+
+### Examples
+
+The following example proofs can be used to confirm the [Rocq setup](#setup) to work correctly.
+
+The following is a simple proof for commutativity of addition.
+This proof is correct.
+
+```v 
+Theorem plus_comm : forall n m : nat, n + m = m + n.
+Proof.
+  intros n m.
+  induction n as [| n' IH].
+  - simpl. rewrite <- plus_n_O. reflexivity.
+  - simpl. rewrite IH. rewrite <- plus_n_Sm. reflexivity.
+Qed.
+```
+
+The following proof attempts to proof that all natural numbers are equal to zero which is obviously
+false.
+
+```v 
+Theorem all_zero : forall n : nat, n = 0.
+Proof.
+  intros n.
+  destruct n.
+  - reflexivity.
+  - reflexivity.
+Qed.
+```