Software Foundations Volume 1: Logical Foundations

2026/01/28

The following are my notes for Software Foundations Volume 1: Logical Foundations.

NOTE: It is not a comprehensive summary of the book. Some fundamental parts (like Polymorphism, Maps, and Imp) are not included while optional parts are. I highly recommend doing the exercises of the book.

Contents

Inductive Types

The number of built-in features in Rocq is very small. As a useful first approximation, types in Rocq can be thought of as sets. For example, the type day is defined as follows. In this case, the type is well-defined and finite.

Inductive day : Type :=
  | monday
  | tuesday
  | wednesday
  | thursday
  | friday
  | saturday
  | sunday.

Rocq also supports types with infinite size, such as the natural numbers, which are defined with two constructors: one for 0 and one for the successor of an object of type nat. Natural numbers are therefore represented in unary format, which differs from the decimal format humans use or the binary format computers use. The unary representation is chosen because it makes proofs simpler. The recursive structure of numbers directly mirrors how we structure proofs by induction. I find it interesting that even fundamental types like numbers are not a built-in feature but are defined in the standard library. The S constructor takes a parameter of type nat, but constructors can take parameters of any type, not necessarily the same type being defined.

Inductive nat : Type :=
  | O
  | S (n : nat).

Functions

Once we have defined inductive types, we write functions that operate on them using Definition and pattern matching with match expressions. A match expression examines the structure of a value and executes different code based on which constructor was used.

Example: the pred (predecessor) function on natural numbers:

Definition pred (n : nat) : nat :=
  match n with
  | O => O
  | S n' => n'
  end.

This function says: if n is O (zero), return O. If n has the form S n' (the successor of some number n'), return n' directly. This works by “peeling off” one S constructor from the unary representation.

However, this has a design flaw: there is no true predecessor of zero, but we’re forced to return something. A better approach uses the Option type, which represents whether a value exists or not (similar to Option in Rust or Optional in Python).

Option is polymorphic: it takes a type parameter A, so option nat, option bool, and option anything all use the same definition. Polymorphism is a very important feature in Rocq. It lets us write generic functions and types that work with any type, avoiding code duplication and enabling powerful abstractions.

Inductive option (A : Type) : Type :=
  | None
  | Some (a : A).

Definition pred' (n : nat) : option nat :=
  match n with
  | O => None nat
  | S n' => Some nat n'
  end.

Now pred' 0 returns None (no predecessor exists), while pred' (S n') returns Some n' (the predecessor is n'). This is more semantically correct, we explicitly distinguish the case where no valid predecessor exists. Pattern matching must be exhaustive: we must handle all constructors of the type.

When we don’t need to use the value bound by a pattern, we use the wildcard _ to avoid inventing an unused variable name. For example:

Definition is_zero (n : nat) : bool :=
  match n with
  | O => true
  | S _ => false
  end.

Simultaneous pattern matching allows us to match multiple values at once. This is useful when comparing two values, like checking equality of two natural numbers. We use the Fixpoint keyword to write recursive functions, and Rocq only accepts recursive definitions it can check will terminate (typically by structural recursion). In this case, Rocq can see that eqb is structurally recursive because the recursive call is on smaller arguments.

Fixpoint eqb (n m : nat) : bool :=
  match n, m with
  | O, O => true
  | O, S _ => false
  | S _, O => false
  | S n', S m' => eqb n' m'
  end.

Function Types

Functions in Rocq also have types and can therefore be thought of as part of a set. The function andb (logical AND) has type bool -> bool -> bool. It takes two arguments of type bool and returns a single bool. It is of the same type as the function orb (logical OR). They are in the same set of function types.

The arrow -> represents a function type. A -> B means “a function that takes an argument of type A and returns a result of type B”. (Function application is written by f x.) For example, bool -> bool is a function that takes a bool and returns a bool.

When we have multiple arrows, we read them right-to-left:

Example: the function andb that performs logical AND:

Definition andb (b1 : bool) (b2 : bool) : bool :=
  match b1 with
  | true => b2
  | false => false
  end.

This function has type bool -> bool -> bool. If the first argument b1 is true, we return b2 (the result depends on the second argument). If b1 is false, the result is false regardless of b2.

Proof Basics

Rocq is fundamentally about proofs. We define statements (propositions) about our types and then construct evidence that they hold. Proofs are introduced using the Example, Lemma, or Theorem keywords. These keywords are essentially equivalent from a technical standpoint. They all produce proven statements, but serve different naming conventions: Example for concrete test cases, Lemma for helper results used in larger proofs, and Theorem for main results.

Each proof has a goal (what we want to prove) and a context (facts and hypotheses we can use). We can reuse previously proven lemmas and theorems in our own proofs. Rocq accepts any proven statement without requiring us to reprove it.

Before diving into proofs, let’s first understand how proofs work by testing a simple concrete example:

Example eqb_refl_3 : eqb 3 3 = true.
Proof. reflexivity. Qed.

What’s happening here?

This is a simple proof that demonstrates the reflexivity principle. We’re claiming that when we compare the number 3 with itself using the eqb function, the result is true. The proof is trivial:

This works for a specific number, but what if we want to prove it for any natural number? That’s where we need induction.

induction is one of the most important tactics in Rocq. Like destruct, it performs case analysis on inductively defined types by creating a subgoal for each constructor. However, induction is more powerful: for recursive constructors, it adds an induction hypothesis to the context. This hypothesis states that the property we’re proving already holds for smaller values, allowing us to prove properties about infinite sets.

We use destruct for simple case analysis on a specific value, but use induction when you need to prove a property that holds for all values of a recursive type.

To prove a statement, we use tactics that manipulate the goal and context to move us closer to a proof. Here’s a detailed example of a general proof using induction:

(* Theorem: For any natural number n, comparing n with itself using eqb returns true.
   This demonstrates proof by mathematical induction. *)

Theorem eqb_refl : forall (n : nat), eqb n n = true. 
Proof. 
  (* Step 1: Introduce the universally quantified variable n into the context.
     After this, we have: n : nat  ⊢  eqb n n = true *)
  intros n.

  (* Step 2: Apply induction principle to n.
     This splits the proof into two cases:
     - Base case: n = O (zero)
     - Inductive case: n = S n' (successor), with induction hypothesis IHn' *)
  induction n as [|n' IHn']. 

  (* CASE 1: Base Case (n = 0)
     Goal: eqb 0 0 = true
     
     Strategy: Simplify the goal by unfolding the definition of eqb.
     Since both arguments are O, the pattern match returns true,
     reducing the goal to: true = true
     
     Then reflexivity closes the goal trivially. *)
  - simpl.                    (* eqb 0 0 unfolds to true = true *)
    reflexivity.              (* true = true is proven by reflexivity *)

  (* CASE 2: Inductive Case (n = S n')
     Context: n' : nat 
     Context: IHn' : eqb n' n' = true  (induction hypothesis)
     Goal: eqb (S n') (S n') = true
     
     Strategy: 
     1. Simplify unfolds the definition of eqb. Since both arguments are S n',
        the pattern match proceeds recursively and reduces to: eqb n' n' = true
     2. Rewrite using the induction hypothesis IHn' which states eqb n' n' = true.
        This transforms the goal to: true = true
     3. Reflexivity closes the remaining trivial goal.
     
     This completes the inductive step: if the property holds for n',
     it holds for S n' (the successor of n'). *)
  - simpl.                    (* eqb (S n') (S n') unfolds to eqb n' n' = true *)
    rewrite IHn'.             (* Replace eqb n' n' = true with true using IHn' *)
    reflexivity.              (* true = true is proven by reflexivity *)
Qed.

(* Conclusion:
   By mathematical induction:
   - We proved the base case: eqb 0 0 = true
   - We proved the inductive step: if eqb n' n' = true then eqb (S n') (S n') = true
   - Therefore, eqb n n = true for all natural numbers n. *)

The as clause specifies how to name the variables introduced in each case. This becomes especially important when we have more inductive cases and makes names explicit.

The pattern induction n as [| n' IHn'] has one “slot” per constructor of the type you are inducting on. For nat, there are two constructors (O and S), so there are two slots:

If you induct on a type with three constructors, you get three slots: induction x as [ ... | ... | ... ]. Each slot names the constructor arguments (and any induction hypotheses for recursive arguments).

One subtle point: when you introduce variables matters, because it changes the strength of your induction hypothesis.

Rule of thumb: if your goal looks like forall n m, P n m and you want to do induction on n, introduce n first, do induction n, and only then introduce m. That keeps m general in the IH.

(* weaker IH: m is fixed *)
intros n m. induction n as [|n IH].

(* stronger IH: IH works for any m *)
intros n. induction n as [|n IH]; intros m.

If you already introduced m “too early”, you can often recover by doing generalize dependent m. before induction.

Reusing Lemmas

One of the most powerful aspects of formal verification is the ability to build complex proofs by composing simpler, previously-proven results. Instead of reproving things, we reuse lemmas and theorems.

Consider this example. First, we prove a simple helper lemma:

Lemma app_nil_r : forall l : natlist,
  l ++ [] = l.
Proof.
  intros l.
  induction l as [|n l' IHl'].
  - reflexivity.              (* Base case: [] ++ [] = [] by reflexivity *)
  - simpl.                    (* Simplify: (n :: l') ++ [] becomes n :: (l' ++ []) *)
    rewrite -> IHl'.          (* Apply induction hypothesis: l' ++ [] = l' *)
    reflexivity.              (* Now we have n :: l' = n :: l', proven *)
Qed.

Now we can use this lemma in a more complex proof. When we have rewrite -> app_nil_r, Rocq searches for a pattern matching the left side of app_nil_r (which is l ++ []) in our goal and replaces it with the right side (l):

Theorem rev_length : forall l : natlist,
  length (rev l) = length l.
Proof.
  intros l.
  induction l as [|n l' IHl'].
  - reflexivity.              (* Base: length (rev []) = length [] *)
  - simpl.
    rewrite -> app_length.    (* Standard library lemma *)
    rewrite -> IHl'.          (* Apply induction hypothesis *)
    rewrite plus_comm.        (* length l' + 1 = 1 + length l' *)
    simpl. reflexivity.
Qed.

Once a lemma is proven with Qed, we can use it by name in rewrite, apply, or other tactics. Rocq maintains a library of proven results, allowing us to build increasingly complex proofs without reimplementing foundational facts.

When we use Qed to complete a proof, Rocq seals the proof. In particular, the resulting constant is typically opaque: other proofs can use the lemma statement, but the kernel will not unfold/reduce the proof term during computation. When you write rewrite -> app_nil_r, Rocq only cares about the statement l ++ [] = l, not how it was proven. We can change the proof script without affecting code that depends on it, as long as the statement stays the same.

Notation Declarations

Rocq allows us to define custom notation to make expressions more readable. The Notation command lets us create infix operators or change how terms are displayed.

For example, in the Lists chapter, we define custom notation for list operations:

Notation "x :: l" := (cons x l) (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).

These declarations mean:

The at level and associativity specifications control how Rocq parses and pretty-prints expressions. We can use these notations immediately after declaration:

Definition my_list := [1; 2; 3].
Definition prepend := 0 :: my_list.

Notation is purely syntactic sugar and just makes code more readable and closer to mathematical convention.

The Search Command

When working on proofs, we often need previously proven theorems but can’t remember their names. The Search command helps us find relevant theorems in the library.

Basic usage:

Search rev.           (* Find all theorems mentioning rev *)
Search (_ + _ = _).   (* Find all theorems about addition equalities *)

Wildcards (_) match any expression. To use a variable pattern instead:

Search (?x + ?y = ?y + ?x).  (* Find commutativity lemmas for + *)

You can restrict search to a specific module:

Search (_ + _) inside Induction.  (* Only search theorems from Induction module *)

Many IDEs (like VSRocq) provide graphical search interfaces that make this even more convenient.

Type Inference and Implicit Arguments

When we write polymorphic functions, Rocq can often infer type arguments automatically. Making arguments implicit avoids verbose type annotations.

In our earlier option with explicit type parameters, we had to write None nat and Some nat n'. A standard way to avoid that is to keep the datatype the same, but mark constructor arguments as implicit:

Inductive option (A : Type) : Type :=
  | None
  | Some (a : A).

Arguments None {A}.
Arguments Some {A} _.

Definition pred' (n : nat) : option nat :=
  match n with
  | O => None
  | S n' => Some n'
  end.

Higher Order Functions

Like many other programming languages, functions in Rocq can be passed as arguments to other functions, returned as a result, stored in a data structure, combined to create new functions, or used to build abstractions that work with any data type.

The most popular Higher Order functions filter, map and reduce fold are just a couple of lines in Rocq. In filter, the first explicit argument is a function which takes a variable of type X as input and returns a bool. In fold, the argument f is a function that takes an element of type X and an accumulator of type Y and returns a value of type Y.

Fixpoint filter {X : Type} (test : X -> bool) (l : list X) : list X :=
  match l with
  | [] => []
  | h :: t => if test h then h :: (filter test t) else filter test t
  end.

Fixpoint map {X Y : Type} (f : X -> Y) (l : list X) : list Y :=
  match l with
  | [] => []
  | h :: t => (f h) :: (map f t)
  end.
  
Fixpoint fold {X Y: Type} (f : X -> Y -> Y) (l : list X) (b : Y) : Y :=
  match l with
  | nil => b
  | h :: t => f h (fold f t b)
  end.

Often we need functions just once, for a single task. Rather than define them at the top level and give them names, Rocq lets us create functions “on the fly” using the fun keyword. An anonymous function like fun n => n * 2 is a function that takes n and returns n * 2, without needing a formal definition or name.

Here, filter selects even numbers using an anonymous predicate fun n => evenb n, then fold sums them with another anonymous function fun n acc => n + acc.

Fixpoint evenb (n : nat) : bool :=
  match n with
  | O => true
  | S O => false
  | S (S n') => evenb n'
  end.

Definition sum_evens (l : list nat) : nat :=
  fold (fun n acc => n + acc) (filter (fun n => evenb n) l) 0.

Currying and Uncurrying

Currying is the process of converting a function that takes a pair (product type) into a function that takes arguments one at a time. For example, a function f : (X × Y) → Z becomes f' : X → Y → Z. The curried version takes one argument, returns a function waiting for the second argument, and finally returns Z. This enables partial application. You can only pass the first argument and get back a specialized function.

Uncurrying is the reverse: converting X → Y → Z into (X × Y) → Z, where both arguments must be supplied together as a pair.

In Rocq, most functions are naturally curried (they take one argument at a time), which is why partial application works so well.

Destructing Compound Expressions

destruct can analyze not just variables, but the results of arbitrary expressions. Especially useful for boolean tests in if-then-else statements. When destructing a compound expression like (n =? 3), always use eqn: to preserve the equation, otherwise you lose critical information needed for the proof:

Definition is_three (n : nat) : bool :=
  if n =? 3 then true else false.

Theorem three_only : forall n, is_three n = true -> n = 3.
Proof.
  intros n H.
  unfold is_three in H.      (* H : (if n =? 3 then true else false) = true *)
  destruct (n =? 3) eqn:E.   (* CASE : (n =? 3) = true, H : true = true *)
  - apply Nat.eqb_eq in E.   (* E : n = 3 *)
    exact E.
  - discriminate H.          (* CASE : (n =? 3) = false, H : false = true *)
Qed.

Without eqn:E, the equation n =? 3 = true would be discarded, making it impossible to prove n = 3.

Constructive Logic

Rocq uses constructive logic. In constructive logic, proofs must be explicit and constructive: To prove that something exists, you must actually build or exhibit it, not just argue abstractly. This requirement fits the philosophy of machine-checked proofs. Only concrete, checkable evidence can be verified by a machine. As a result, several classical logic principles are not valid in Rocq’s constructive logic:

Law of Excluded Middle

The principle that every proposition is either true or false cannot be proven for arbitrary propositions. This is not derivable in Rocq because to prove P \/ ~ P, we’d need to use left (proving P) or right (proving ~ P), but we have no information about which side holds for an arbitrary proposition P.

Excluded middle is valid for decidable propositions where we can compute a boolean answer. For example, equality on natural numbers is decidable: forall (n m : nat), n = m \/ n <> m.

Definition excluded_middle := forall P : Prop,
  P \/ ~ P.

Double Negation Elimination

We cannot eliminate double negations for arbitrary propositions. We can prove P -> ~ ~ P (introducing double negation), but we cannot go from ~ ~ P back to P as this would require excluded middle.

Definition double_negation_elimination := forall P : Prop,
  ~ ~ P -> P.

Rocq is based on Intuitionistic type theory, a form of constructive logic whose foundation is the Curry-Howard correspondence. This principle equates propositions with types and proofs with programs: To prove a proposition is to construct a term of a certain type. Every proof is a program, and every program is a proof. This essential connection makes machine checking possible. Since proofs are executable objects, a computer can verify their correctness by type-checking and evaluation.

This is the fundamental core of Rocq: Its type checker is not just a tool for catching programming errors, but the very engine that guarantees the correctness of both programs and proofs.

The type A -> B is literally the type of functions from A to B. When A and B are propositions, a proof of A -> B is a function that transforms proofs of A into proofs of B. Consider this concrete example where a proof term is simultaneously a logical proof and an executable program:

(* A proof of implication IS a function *)
Definition modus_ponens (P Q : Prop) : (P -> Q) -> P -> Q :=
  fun (f : P -> Q) (p : P) => f p.

(* This is simultaneously:
   - A proof that ((P -> Q) -> P -> Q) is provable
   - A program that applies a function f to an argument p *)

This correspondence extends to all logical operations.

Propositions as Types

In Rocq, propositions have a special type called Prop. All well-formed propositions have type Prop, whether they are true, false, or unprovable. Propositions are first-class citizens. They can be named with Definition, parameterized (functions returning Prop), and manipulated like any other value in Rocq.

Check (forall n m : nat, n + m = m + n) : Prop.
Check 2 = 2 : Prop.
Check 3 = 2 : Prop.  (* false, but still has type Prop *)

(* Functions can return propositions *)
Fixpoint double (n : nat) : nat :=
  match n with
  | O => O
  | S n' => S (S (double n'))
  end.

Definition is_even (n : nat) : Prop := exists k, n = double k.
Check is_even : nat -> Prop.

Being a proposition is different from being provable. A proposition can exist and be well-typed without having a proof.

Proof Irrelevance and Curry-Howard

The Curry-Howard correspondence tells us that “proofs are programs,” yet Rocq also embraces proof irrelevance: the principle that all proofs of the same proposition are indistinguishable.

Rocq distinguishes between Prop (the universe of propositions) and Type (the universe of computational types). Propositions live in Prop, which is designed for logical reasoning rather than computation. Proofs in Prop are treated as computationally irrelevant (for example, they are erased during extraction). We also assume proof irrelevance as an additional principle: that any two proofs of the same proposition are equal. When we prove a theorem, we mainly care that it is provable, not how it was proven (some mathematicians may find that offensive). The proof strategy (induction, case analysis, rewriting) becomes an implementation detail once sealed with Qed.

The computational content lives in other types like nat, bool, and list, where different constructions are distinct. When we extract executable programs from Rocq, all Prop terms are erased since they carry no runtime data. This gives us both logical rigor through precise proofs and computational efficiency by discarding proof details that don’t affect program behavior.

(* Example: Prop vs Type distinction *)
Fixpoint even_comp (n : nat) : bool :=
  match n with
  | O => true
  | S O => false
  | S (S n') => even_comp n'
  end.

Definition even (n : nat) : Prop :=
  exists k, n = double k.

Logical Connectives in Rocq

In Rocq, logical connectives are defined as inductive types. Proofs involving them are constructed using tactics that manipulate these types.

Conjunction

Conjunction (logical AND) of propositions A and B is written A /\ B, representing the claim that both are true. The infix notation /\ is syntactic sugar for and A B, where and : Prop -> Prop -> Prop. Under Curry-Howard, A /\ B corresponds to a product type (pair). A proof of A /\ B is literally a pair (proof_of_A, proof_of_B).

To prove a conjunction, use the split tactic to generate two subgoals, one for each part. To use a conjunctive hypothesis H : A /\ B, use destruct H as [HA HB] to split it into two separate hypotheses:

Lemma and_example : forall n m : nat, n = 0 /\ m = 0 -> n + m = 0.
Proof.
  intros n m [Hn Hm].  (* destruct the conjunction into two hypotheses *)
  rewrite Hn. rewrite Hm.
  reflexivity.
Qed.

Disjunction

Disjunction (logical OR) of propositions A and B is written A \/ B, true when either A or B holds. This stands for or A B, where or : Prop -> Prop -> Prop. Under Curry-Howard, A \/ B corresponds to a sum type (tagged union). A proof is either left proof_of_A or right proof_of_B.

To prove a disjunction, use left to prove the left side or right to prove the right side. To use a disjunctive hypothesis, perform case analysis with destruct or an intro pattern:

Lemma factor_is_O: forall n m : nat, n = 0 \/ m = 0 -> n * m = 0.
Proof.
  intros n m [Hn | Hm].
  - (* Case: n = 0 *)
    rewrite Hn. reflexivity.
  - (* Case: m = 0 *)
    rewrite Hm. rewrite <- mult_n_O. reflexivity.
Qed.

Falsehood and Negation

Negation ~ P is defined as P -> False, where False : Prop is a contradictory proposition with no proof. Since False cannot be proven, assuming it allows us to prove anything via the principle of explosion.

Inequality x <> y is notation for ~ (x = y), i.e., (x = y) -> False.

Theorem zero_not_one : 0 <> 1.
Proof.
  unfold not.
  intros contra.
  discriminate contra.  (* 0 = 1 contradicts constructor disjointness *)
Qed.

Universal Quantification

Universal quantification forall x : T, P x asserts that property P holds for every value x of type T. This is Rocq’s way of expressing “for all”. The type forall x : T, P x : Prop states that for any choice of x, the proposition P x holds. forall x : T, P x is a dependent function type, where the result type P x depends on the input value x. This is more general than simple function types like T -> U where the result type is always U.

To prove a universally quantified goal, use intros x to introduce an arbitrary value x into the context, then prove P x for this generic x. To use a universally quantified hypothesis H : forall x, P x, apply it to a specific value using apply H or specialize it with specialize H with (x := value).

Theorem forall_example : forall n m : nat,
  n + m = m + n.
Proof.
  intros n m.  (* Introduce arbitrary n and m *)
  (* Now prove n + m = m + n for these specific values *)
  apply add_comm.
Qed.

Logical Equivalence (If and Only If)

The iff connective P <-> Q asserts that two propositions have the same truth value. It’s defined as the conjunction of two implications: (P -> Q) /\ (Q -> P). You can often use a proven <-> to replace one side with the other.

Theorem iff_sym : forall P Q : Prop, (P <-> Q) -> (Q <-> P).
Proof.
  intros P Q [HAB HBA].
  split.
  - (* -> *) apply HBA.
  - (* <- *) apply HAB.
Qed.

Existential Quantification

Existential quantification exists x : T, P x asserts that there is at least one value x of type T for which property P holds. This is Rocq’s way of expressing “there exists.” Under Curry-Howard, exists x : T, P x corresponds to a dependent pair type (also called Sigma type). A proof is a pair (witness, proof_that_property_holds) where the second component’s type depends on the first component’s value.

Constructive requirement: In constructive logic, proving existence requires providing a witness. An actual value that satisfies the property. You cannot prove exists x, P x by arguing abstractly. You must exhibit a specific x and prove P x holds for it. This is the essence of constructive existence proofs.

To prove an existential goal, use exists value. to provide a concrete witness, then prove P value holds for that specific value. To use an existential hypothesis H : exists x, P x, destruct it with destruct H as [x Hx] to extract the witness x and the proof Hx : P x.

Theorem exists_example : forall n : nat,
  (exists m, n = 4 + m) -> (exists o, n = 2 + o).
Proof.
  intros n [m Hm].  (* Destruct existential: get witness m and proof Hm *)
  exists (2 + m).   (* Provide witness for goal *)
  apply Hm.
Qed.

Inductively Defined Propositions

Inductively Defined Propositions (IDP) is another very powerful feature of Rocq. Instead of expressing propositions using universal, existential, and logical connectives, propositions are defined inductively by a set of rules.

This makes perfect sense when considering that Rocq uses constructive logic. Proving a proposition is to construct evidence. The constructors of an IDP provide the specific rules for constructing this evidence. In fact, using these constructors is the only way to prove an IDP holds.

The ev Property

A classic example is the property of a number being even. We can define ev inductively:

Inductive ev : nat -> Prop :=
| ev_0 : ev 0
| ev_SS (n : nat) (H : ev n) : ev (S (S n)).

This definition says there are exactly two ways to prove a number is even:

  1. Rule ev_0: 0 is even.
  2. Rule ev_SS: If n is even, then S (S n) (i.e., n+2) is even.

Equivalence with Other Definitions

We can define the same proposition classically and inductively, prove their equivalence and when the proposition is part of the context of a new proof, interchange them. This can make proving new things a lot easier.

We previously defined evenness using a boolean function (evenb) or the existential proposition (exists k, n = 2 * k). We can prove that our inductive definition is equivalent to these.

We want to prove ev n <-> even n. The direction even n -> ev n is straightforward (induction on k). However, proving ev n -> even n requires a new technique.

Induction on Evidence

To prove forall n, ev n -> even n, standard induction on n is difficult. The inductive step would involve n and S n, but ev jumps by two (n to S (S n)). The induction hypothesis for n doesn’t help with S n generally.

Instead, we perform induction on the evidence E : ev n. Since E is built from constructors ev_0 and ev_SS, induction on E gives us cases corresponding exactly to these rules.

Theorem ev_even_iff : forall n,
  ev n <-> even n.
Proof.
  intros n. split.
  - (* -> *)
    unfold even. 
    intros E.
    (* We proceed by induction on the evidence E that ev n holds. *)
    induction E as [|n' E' IH].
    + (* Case E = ev_0: n is 0. *)
      exists 0. 
      reflexivity.
    + (* Case E = ev_SS n' E': n is S (S n').
         The IH tells us that n' is even (exists k, n' = double k). *)
      destruct IH as [k Hk].
      subst.
      exists (S k).
      simpl.
      reflexivity.
  - (* <- *) 
    unfold even.
    intros [k Hk].
    rewrite Hk.
    (* We use the helper lemma ev_double (prove by induction on k) *)
    apply ev_double.
Qed.

In the -> direction, we can see that Rocq produced an IH that corresponds to E', the single recursive occurrence of ev in its own definition. Since E' mentions n', the induction hypothesis talks about n', as opposed to n or some other number.

Tactics for Evidence

When we have a hypothesis H that is an IDP, we can use different tactics to analyze it:

With these tools, we can freely interchange between inductive (ev), boolean (evenb), and existential (even) definitions depending on which is most convenient for the current proof context. We can trivially prove the equivalence of ev and evenb using transitivity since we already know even <-> evenb and now ev <-> even.

Automation

Rocq’s auto tactic is proof search. It tries to solve the current goal by repeatedly applying hypotheses or lemmas from the context and from a hint database, together with simple steps like intros. It either solves the goal completely or does nothing.

If auto fails because it did not search deep enough, you can increase the search depth with auto n (default depth is 5), and you can inspect what it’s doing with debug auto (trace) or info_auto which shows which facts it used when it succeeds.

Hint databases are what make auto scale. Rocq ships with a default database called core, and you can add common lemmas, constructors, unfolding hints to a database:

(* Add objects to core. *)
Hint Resolve h : core.
Hint Constructors p : core.
Hint Unfold d : core.

(* Use your own database instead of polluting core. *)
Create HintDb db.
Hint Resolve h : db.

(* Use it when you need it. *)
auto with db.

eapply and eauto are variants that allow existential variables (placeholders like ?x) to be left for later instantiation. We use this when an intermediate value becomes obvious only after you solve a later subgoal.

Tactics Reference

apply · assert · assumption · auto · clear · constructor · contradiction · destruct · discriminate · eapply · eassumption · eauto · exists · exfalso · f_equal · generalize dependent · induction · injection · inversion · intros · left / right · lia · reflexivity · remember · rename · repeat · replace · rewrite · simpl · specialize · split · subst · symmetry · transitivity · try · unfold

apply

Uses a theorem or hypothesis to move between premises and conclusions.

assert

Introduces a “local lemma” into the context by stating a proposition and then proving it as a new subgoal. After the new subgoal is proved, the proposition becomes a hypothesis you can use. Usage: assert (H : P). creates a subgoal for P, then continues with H : P in the context.

assumption

Closes the goal if it exactly matches a hypothesis in the context.

auto

Attempts to solve the goal using proof search (roughly: combinations of intros and apply) using facts from the context and from hint databases (like core). It either solves the goal or does nothing. Increase depth with auto n (default 5). Use debug auto to see where it gets stuck, and info_auto to see what it used.

clear

clear H removes hypothesis H from the context.

constructor

If the goal is an inductive proposition, constructor tries to apply an appropriate constructor, leaving its premises as subgoals.

contradiction

Closes the goal if the context contains an explicit contradiction (e.g., both P and ~P, or a hypothesis equivalent to False).

destruct

Performs case analysis on an inductively defined value by creating a subgoal for each constructor. Use destruct x as [| n'] to name the variables in each case, and destruct x eqn:E to preserve the equation showing which constructor was matched.

discriminate

Proves the current goal immediately when the context contains a contradiction: an equality between values built from different constructors (e.g., true = false). Useful for eliminating impossible cases in proofs. This embodies: “From a false proposition, anything follows” (Principle of explosion), which states that from a contradictory hypothesis, any conclusion follows.

eapply

Like apply, but allows Rocq to leave some arguments as existential variables (placeholders like ?x) to be determined later. Useful when an intermediate term is hard to guess upfront, but becomes determined after solving subsequent subgoals.

eassumption

Like assumption, but also allows instantiating existential variables in the goal to match a hypothesis.

eauto

Like auto, but uses eapply during proof search, so it can solve goals that require deferring instantiation of some arguments. Typically slower than auto.

exists

When the goal is an existential exists x, P x, exists v provides the witness v and changes the goal to P v.

exfalso

Changes the current goal to False, useful when you want to prove something by deriving a contradiction.

f_equal

Transforms a goal of the form f x = f y into x = y, exploiting the property that function application preserves equality. Similar to injection, but works on goals rather than hypotheses. It reasoning backwards from an equality of constructed values to equalities of their arguments. Automatically discharged subgoals that are trivial (e.g., provable by reflexivity).

generalize dependent

Moves a variable from the context back into the goal as a universally quantified variable. Useful for strengthening induction hypotheses or reconsidering proof strategy when variables were introduced too early.

Usage: generalize dependent x. converts x : T in the context to forall x : T in the goal, allowing subsequent tactics to see x as a universally quantified variable.

induction

Proves goals involving recursive structures by breaking them into a base case (for the simplest constructor) and an inductive case (for recursive constructors), where you can assume the statement holds for smaller values via the induction hypothesis.

injection

Exploits the injectivity property of constructors: If two values built from the same constructor are equal, then their arguments must be equal. Given a hypothesis H : f x = f y where f is a constructor, injection H as Heq generates the equation x = y and adds it to the context. This works on hypotheses containing equalities, not on goals.

intros

Introduces universally quantified variables and hypotheses from the goal into the context, making them available for the proof.

inversion

inversion H is like destruct H, but smarter. Use it on a hypothesis that was built by an inductive definition.

It does two things:

In practice it is common to write inversion H; subst. so the generated equalities are immediately substituted.

left and right

When the goal is a disjunction P \/ Q, use left to change the goal to P, or right to change the goal to Q.

lia

Solves (or refutes) goals in linear integer arithmetic (equalities/inequalities with +, -, and logical connectives). Great for routine arithmetic side-conditions.

reflexivity

Proves equalities where both sides are identical or can be shown to be identical through computation and unfolding.

remember

remember e as x eqn:Hx replaces an expression e with a fresh name x and records the defining equation Hx : x = e. Useful before induction when e is not a variable.

rename

rename x into y renames a variable/hypothesis in the context (helpful when inversion/destruct picks awkward names).

repeat

Repeatedly applies a tactic until it fails (or stops making progress). Beware: repeat can loop if the tactic always succeeds and keeps making progress.

replace

Replaces a subexpression in the goal with another expression, creating two subgoals: one with the replacement applied, and one proving the two expressions are equal. Useful when rewrite cannot target the correct occurrence or when you want to guide the proof explicitly.

Usage: replace e1 with e2. produces subgoal 1 (goal with e1 replaced by e2) and subgoal 2 (proof that e1 = e2).

rewrite

Replaces occurrences in the goal using an equality hypothesis or theorem, allowing us to transform one expression into another. Use rewrite -> H to apply left-to-right or rewrite <- H to apply right-to-left. rewrite can be used on the goal or in the context with the in keyword (e.g., rewrite H in hyp).

simpl

Simplifies the goal by unfolding definitions and performing basic computation, reducing complex expressions to simpler forms.

specialize

Instantiates a universally quantified hypothesis in the context by providing concrete arguments. If H : ∀ x : T, P is a generic hypothesis, then specialize H with (x := e) replaces H with a specialized version where x is replaced by e. This is useful for narrowing down overly general assumptions to a specific case you care about. Can be combined with the as clause to name the resulting hypothesis: specialize H with (x := e) as H'.

split

When the goal is a conjunction P /\ Q, split generates two goals: P and Q.

subst

subst x replaces x everywhere using a hypothesis like x = e (or e = x) and clears that hypothesis; subst does this for all such equalities.

symmetry

Switches the left and right sides of an equality in the goal, converting ⊢ t = u into ⊢ u = t. Useful when apply fails because the equality is the wrong direction. Can be applied to hypotheses with symmetry in H.

transitivity

Proves a goal x = z by introducing an intermediate value y and splitting into two subgoals: x = y and y = z. Usage: transitivity y. where y is the intermediate value.

try

try T runs tactic T; if T fails, it succeeds doing nothing. Useful in scripts like induction ...; try (simpl; ...) to handle “most cases.”

unfold

Manually unfolds the definition of a name introduced by Definition so you can manipulate the underlying expression. This is useful when tactics like simpl are too conservative and don’t automatically unfold because they can’t simplify further.

Exercises for me To Do

Logic

IndProp

Imp

IndPrinciples

Rel