NOTE: I paused reading at chapter 6. Right now, this book is too advanced. I will read through Software Foundations before coming back. I ported the chapters 1-6 to Rocq 9.0.1.

2 Some Quick Examples

Given an overview of what is possible with Rocq for formal verification. A typed expression language is created with support for natural numbers and booleans, featuring type-indexed operations: addition, multiplication, equality comparison (for any type), and less-than comparison (for naturals). A compiler to a stack machine is created and proven to have correct translation for all possible programs. The compiler can be extracted to OCaml and executed with reasonable performance. The proofs introduce tactics for manual proving and automation techniques.

Type indexing allows encoding precise information directly in types. For example:

Inductive tbinop : type -> type -> type -> Set :=
| TPlus : tbinop Nat Nat Nat
| TTimes : tbinop Nat Nat Nat
| TEq : forall t, tbinop t t Bool
| TLt : tbinop Nat Nat Bool.

Here, TPlus takes two Nat operands and returns Nat, while TEq works on any type but requires both operands to match. This makes invalid programs like TBinop (TEq Nat) (TNConst 5) (TBConst true) impossible to construct. They’re rejected at compile time. While I was familiar with the concept of type indexing, this chapter deepened my understanding of its practical purpose.

The chapter explicitly states that not all concepts will be explained in detail, aiming instead to demonstrate what’s possible. Despite being unfamiliar with the Rocq proof assistant, I found the material approachable as key concepts and proof tactics were introduced progressively throughout the examples.

3 Introduction to Inductive Types

Proof Terms and Curry-Howard Correspondence

Coq unifies proofs and programs through the Curry-Howard correspondence: theorems are types, and proofs are programs that inhabit those types. The arrow -> represents both function types and logical implications. For example, fun x : True => x has type True -> True, making it simultaneously a function and a proof.

The type system distinguishes between:

• Set: Universe of computational types (programs like nat, bool)
• Prop: Universe of logical propositions (proofs like True, False)
• Type: The type of both Set and Prop

Key distinction: bool values (true/false) are decidable and always evaluate, while Prop propositions (True/False) represent undecidable logical statements. Both Prop and Set are primitive built-ins in Coq’s type system, not defined within the language.

Simple Inductive Types

unit - Singleton type with one value tt (“trivial term”).

• Curry-Howard equivalent of True
• Represents “trivially done” - like void in C or () in Haskell
• Every value of type unit equals tt, provable as: forall x : unit, x = tt
• Used when a function needs to return something but has no meaningful data
• In Curry-Howard: just as tt is the only value of unit, I is the only proof of True

Empty_set - Type with no constructors, hence no values can exist.

• Curry-Howard equivalent of False
• Represents impossible situations - like Haskell’s Void or Rust’s ! (never type)
• From Empty_set, you can prove anything (“from falsehood, anything follows”)
• Example: forall x : Empty_set, 2 + 2 = 5 is provable by case analysis with zero cases
• If you somehow had a value of Empty_set (or proof of False), the logical system is broken
• Pattern matching on Empty_set requires no branches: match e with end

bool - Two constructors: true and false. Pattern matching enables function definitions like negb (boolean negation). Proofs use case analysis (destruct) or induction.

More Inductive Types

• Enumerations - Simple types with multiple constructors (unit, Empty_set, bool)
• Simple Recursive Types - Self-referencing constructors (nat, lists, trees)
• Parameterized Types - Polymorphic types with type parameters (list T)
• Mutually Inductive Types - Types that reference each other (even_list/odd_list)
• Reflexive Types - Constructors taking functions of the type being defined (formula)
• Nested Inductive Types - Using the type as an argument to another type family (nat_tree with list nat_tree)

Tactics

Core Proof Tactics:

• induction x - Proof by induction on x. Generates subgoals for each constructor and provides inductive hypotheses (IH) for recursive arguments. For nat: creates base case P O and inductive step P n -> P (S n).
• destruct x - Case analysis on x without inductive hypotheses. Splits into one subgoal per constructor. Sufficient for non-recursive proofs; preferred over induction when IH isn’t needed.
• apply thm - Apply theorem/function thm to current goal. Replaces goal with the premises of thm. Used to manually apply induction principles: apply nat_ind instead of induction n.

Equality and Computation:

• reflexivity - Proves x = x by computational reduction. Automatically simplifies both sides until they’re syntactically identical.
• rewrite H - Replace using equality hypothesis H : a = b. Changes a to b in the goal. Use rewrite <- H to replace b with a.
• simpl - Computational simplification. Unfolds definitions and reduces match expressions when branches are obvious.

Constructor Reasoning:

• discriminate - Proves inequality between different constructors. Solves goals like true = false -> False or O = S n -> False immediately. Based on injectivity of constructors.
• injection H - From equality of constructor applications (e.g., S n = S m), derives equalities of arguments (n = m). Adds new equalities as hypotheses.
• congruence - Complete decision procedure for equality with uninterpreted functions. Combines discriminate, injection, and congruence closure. Very powerful for equality reasoning.

Basic Goal Management:

• intro / intros - Move hypotheses from goal to context. intro H names one hypothesis; intros introduces all. Turns forall x, P x into context x : T with goal P x.
• red - One step of reduction/unfolding. Useful for exposing structure (e.g., unfolding not to see implication).
• change e - Replace goal with computationally equivalent expression e. Manual control over what form the goal takes.

4 Inductive Predicates

How to define logical properties as inductive types in Prop. Instead of data types like lists or numbers, we define judgments like “n is even” or “n equals zero” using inference rules. The key insight: use rule induction instead of regular induction on data. For example, when proving something about even numbers, induct on the proof that a number is even, not on the number itself. Covers basic logic connectives with automation (tauto, intuition), existential quantification, and recursive predicates. When using induction, variables that appear before what you’re inducting on stay fixed, while variables after it can vary.

Tactics:

• inversion H - Smart case analysis that detects impossible cases. When destruct would lose information, inversion preserves it and can immediately solve contradictions.
• tauto - Automatic solver for propositional logic. Proves any valid formula using only ->, /\, \/, ~.
• intuition - Like tauto but works with arbitrary goals. Uses propositional reasoning to simplify, then leaves remaining non-logical facts for you.
• constructor - Apply the (only) constructor that fits. Shortcut when there’s one obvious way to build the goal.
• left / right - Prove a disjunction P \/ Q by proving the left or right side.
• split - Break a conjunction P /\ Q into two separate goals.
• exists x - Prove exists x, P x by providing witness x.
• unfold def - Replace def with its definition. Useful for expanding definitions like not.
• eapply thm - Like apply but allows unknowns. Lets eauto fill in the missing pieces later.
• eauto - Smarter version of auto that can use eapply. Better at finding complex proofs automatically.

5 Infinate Data and Proofs

In programming languages like Haskell (or any other lazy evaluated language) we can define infinite data structures. For example in a binary tree or list in python, a value is only evaluated when needed. This can lead to non-terminism which we do not have in formal verification. Rocq also supports lazy data structures.

Keywords

• CoInductive: Like Inductive but for infinite constructors (like an infinite stream of numbers)
• CoFixPoint: Like FixPoint but for infinite objects (like an infinite list of zeros)

Recursive calls in a type must be guarded by the constructor of their type. This prevents infinite loops (WHY?). In practice any co-recursive definition must be able to evaluate to a finite result in finite time. You can not write a function filter because it might remove every element and never terminate.

Equality of co-recursive definitions can not use the normal eq predicate. Instead we define a new one which checks the equality of head and tail. We can check equality explicitly or implicit

CoInductive stream_eq_bool : stream bool -> stream bool -> Prop :=
  | Stream_eq_bool : forall (h1 h2 : bool) (t1 t2 : stream bool),
      h1 = h2 ->
      stream_eq_bool t1 t2
      -> stream_eq_bool (Cons h1 t1) (Cons h2 t2).

We reuse h for the head of both.

CoInductive stream_eq_bool : stream bool -> stream bool -> Prop :=
  | Stream_eq_bool : forall (h : bool) (t1 t2 : stream bool),
      stream_eq_bool t1 t2
      -> stream_eq_bool (Cons h t1) (Cons h t2).

The section continues with a proof of equality for two factorial steams and how to generalize these proofs (SHOULD REVISIT!). It ends with a motivation for co-inductive types. We define a simple imperative programming language and prove the correctness of an optimization (x + 0 = x).

The last third of this chapter was hard. I did not understand the generalizations of the stream equality proofs. The motivation of co-inductive types is very useful in the context of program verification.

Tactics:

• cofix Structure proof as a co-fixpoint

6 Subset Types and Variations

This chapter introduces dependent types known from other proof assistants. The chapter motivates dependent types with the promise of easier program verification. Using the predecessor function, the default version in Rocq returns 0 for 0. In program verification however, we might be interested verifying that pred is not called on 0.

We reimplement dependent types using subset types from the standard library including defining syntactic sugar to arrive at a natural syntax. It is shown that proof code is erased in extraction to OCaml (just like in to F*).