Basics - Data and Functions

Rocq Proof Assistant

• Proof assistant for functional programming

• Verifies correctness of programs

• Uses Gallina for definitions, functions, proofs

• Named after Thierry Coquand

Functional Programming Characteristics

• Pure functions (no side effects)

• First-class functions

• Algebraic data types with pattern matching

• Polymorphic type systems

• Easier reasoning, testing, parallel programming

Functional vs Imperative Programming

• Functional: immutable state, recursion, no side effects
• Imperative: mutable variables, loops, side effects
• Functional enables easier reasoning and parallelism
• Imperative has harder-to-debug state changes

Rocq Basic Workflow

• Write Rocq code in .v files
• Process files interactively for definitions and proofs
• Available in browser, standalone IDE, or VS Code

Inductive Type Definition

• Defines new types by listing constructors
• Example: Inductive day : Type := | monday | tuesday …
• Each constructor creates a value of the type
• No arguments needed for simple enumerations

Pattern Matching Functions

• Defined with match statement
• Must be exhaustive (cover all constructors)
• Follows structure of data definition
• Example: nextworkingday (d:day) := match d with … end

Compute Command

• Evaluates expressions in Rocq
• Displays both result and type
• Used for testing
• Example: Compute (nextworkingday friday) returns ('monday : day')

Example Assertion

• Records expected result with a name
• Rocq verifies it with proof tactics
• Example: Example test: (nextworkingday saturday) = monday.

Proof State Display

• Shows current proof goal during interaction
• Example: (1/1) nextworkingday (nextworkingday saturday) = tuesday
• Transforms step by step until true

Wildcard Pattern

• Underscore _ matches any value
• Used when specific value doesn't matter
• Example: | _ => false matches all remaining cases

Boolean Type in Rocq

• Built-in Inductive bool : Type := | true | false
• Defined with pattern matching
• Example: andb (b1 b2:bool) := match b1 with … end

Custom Notation

• Defines syntactic sugar for readability
• Example: Notation "x && y" := (andb x y)
• Allows writing true && false instead of andb true false

Conditional Expressions

• if-then-else for boolean pattern matching
• Must have same type branches
• Example: def negb' (b:bool) := if b then false else true

Check Command

• Displays type of an expression
• Examples: Check true : bool
• Function types written with arrows

Constructors with Arguments

• Inductive types can have constructors carrying data
• Example: Inductive color : Type := | black | white | primary (p : rgb)
• Primary constructor takes rgb argument

Pattern Matching with Arguments

• Match on constructors with arguments
• Use variables or constants
• Example: | primary red => true | primary _ => false

Modules in Rocq

• Organize code into named spaces
• Example: Module Playground
• Access with dot notation: Playground.foo

Programs Are Data Principle

• Data has structure; functions follow that structure
• Inductive types define shapes
• Functions use pattern matching for processing