Rocq Project Template

This repository serves as my personal template for creating new Rocq projects. Rocq is a formal proof management system that provides a formal language to write mathematical definitions, executable algorithms, and theorems, together with an environment for semi-interactive development of machine-checked proofs.

🚀 Using This Template

To create a new project based on this template:

1. Click the "Use this template" button on GitHub
2. Choose a name for your new repository
3. Clone your new repository
4. Customize the project for your specific needs

📋 Prerequisites

Before using this template, ensure you have Rocq installed on your system:

Installation Options

Option 1: Using OPAM (Recommended)

opam install rocq

Option 2: Using Nix

nix-shell -p rocq

Option 3: From Source Follow the installation instructions at Rocq's official repository.

Verify Installation

rocq --version

📁 Project Structure

This template provides a standard Rocq project layout:

.
├── _CoqProject          # Project configuration file
├── Makefile            # Build automation
├── theories/           # Main development theories
├── instances/          # Concrete instances and examples
├── examples/           # Usage examples and demos
└── README.md          # This file

Directory Descriptions

• theories/: Contains the main theoretical development of your project. This is where you'll define abstract concepts, prove theorems, and develop the core mathematical content.

• instances/: Contains concrete instantiations of the abstract theories. This includes specific implementations and concrete examples of the general concepts defined in theories/. This might be a good place for instances of type classes.

• examples/: Contains example files demonstrating how to use your development. These serve as both documentation and tests for your theoretical work.

🔧 Development Workflow

Building the Project

To build the entire project:

make

To build a specific target:

make theories/YourFile.vo

Cleaning Build Artifacts

To clean all generated files:

make clean

Project Configuration

The _CoqProject file configures the project structure. It currently includes:

• Logical path mapping for the Tmpl namespace
• Include paths for all three main directories

You may want to customize this file by:

1. Changing the namespace from Tmpl to something more descriptive
2. Adding dependencies to other Rocq libraries
3. Setting compiler flags or options

Example customizations:

-R theories MyProject
-R instances MyProject  
-R examples MyProject

# Add dependencies
-Q path/to/some/lib SomeLib

# Set options
-arg -w -arg -notation-overridden

📝 Getting Started

1. Rename the namespace: Edit _CoqProject to replace Tmpl with your project name
2. Update the README: Customize this README.md file for your specific project
3. Add your first theory: Create a .v file in the theories/ directory
4. Build and test: Run make to ensure everything compiles
5. Add examples: Create demonstration files in examples/

Example First Theory

Create theories/BasicDefinitions.v:

(** * Basic Definitions *)

Definition my_constant : nat := 42.

Theorem example_theorem : my_constant = 42.
Proof.
  reflexivity.
Qed.

Then create theories/UsingBasic.v that uses the first file:

(** * Using Basic Definitions *)

From Tmpl Require Import BasicDefinitions.

Theorem my_constant_is_even : Nat.even my_constant = true.
Proof.
  reflexivity.
Qed.

🤝 Contributing

When contributing to a project based on this template:

1. Follow the established directory structure
2. Document your definitions and theorems
3. Provide examples in the examples/ directory
4. Ensure all proofs compile with make
5. Update this README as needed

📚 Resources

• Rocq Documentation
• Rocq Standard Library

📄 License

This template is provided as-is. Choose an appropriate license for your project when using this template.

---

Happy proving! 🎯