3 Lecture 3: Basics of Rocq – SoSe 26 Type Theory & Logic & Functional Programming Notes

Basics of Lambda Calculus

In lambda calculus, the basic syntactic forms are:

variables: $x, y, f, \dots$. These are atomic terms
lambda abstractions: $\lambda x. t$. These create functions by binding a variable
Applicaitons: $t\, u$: Uses a function by applying it to an argument.

So the two central operations are:

abstraction: $\lambda x. t$. ($t$ is called the function body)
application: $t\, u$.

These can be seen as complementary operations. For example:

\[ \labs{x}{x\cdot 2 + 1} \]

is the function $x \to x \cdot 2 + 1$, and applying it to 3 gives:

\[ \begin{aligned} \lapp{(\labs{x}{x\cdot 2 + 1})}{3} &\to 3 \cdot 2 + 1 &&\text{($\to$ denotes reduction)}\\ &\to 7 \end{aligned} \]

This reduction rule is called $\beta$-reduction:

Definition 3.1 ($\beta$-reduction) \[ \lapp{\labs{x}{t}}{a} \betared t[x := a] \]

It says: applying a lambda abstraction to an argument means substituting the argument for the bound variable in the body.

Why is it called abstraction?

abstraction: generalize an expression into a function
application: specialize a function to a concrete argument

Bound and Free Variables

In a term like:

\[ \labs{x}{x\cdot 2 + 1} \]

The variable $x$ is bound the $\lambda$. Its scope is the body $x\cdot 2 + 1$.

In constrast consider:

\[ \labs{x}{x\cdot y + 1} \]

Here $x$ is bound and $y$ is not. The variable $y$ is free. Nevertheless this term is still syntactically meaningful. It represents a function of $x$, but one that depends on an external parameter $y$. For example, consider the reduction:

\[ \lapp{(\labs{x}{x\cdot y + 1})}{3} \betared 3\cdot y + 1 \]

The result still contains the free variable $y$, and this term is not automatically interpreted as a function of two variables. For a function with $x$ and $y$, we must bind both variables explicitly:

\[ \labs{x}{\labs{y}{x \cdot y + 1}} \]

This is a curried two argument function: It first takes $x$, then returns a function that takes $y$. Consider the following reduction:

\[ \begin{aligned} \lapp{(\lapp{(\labs{x}{\labs{y}{x\cdot y + 1}})}{3})}{4} &\betared \lapp{(\labs{y}{3\cdot y + 1})}{4} \\ &\betared 3 \cdot 4 + 1 \\ &\betared 13 \end{aligned} \]

Typed Lambda Calculus

In typed lambda calculus, variables and functions have types.

\[ \tlabs{x}{\Nat}{x \cdot 2 + 1} : \Nat \to \Nat \]

A two-argument function can be written as:

\[ \tlabs{x}{\Nat}{\tlabs{y}{\Nat}{x\cdot y + 1}} : \Nat \to \Nat \to \Nat \]

By convention, arrow types associate to the right, so

\[ \Nat \to \Nat \to \Nat \]

means:

\[ \Nat \to (\Nat \to \Nat) \]

So a two-argument function is really a function that takes one argument and returns another function. (Curried function notation)

Open Terms and Contexts

The term

\[ \tlabs{x}{\Nat}{x \cdot y + 1} \]

contains the free variable $y$. In typed lambda calculus, this term is not typeable in the empty context, because the type of $y$ is unknown. But it is typeable in a context where $y : \Nat$ is assumed.

We can write this as

\[ y : \Nat \vdash \tlabs{x}{\Nat}{x \cdot y + 1} : \Nat \to \Nat \]

This means:

\[ \text{Assuming $y$ is a natural number} \\ \tlabs{x}{\Nat}{x \cdot y + 1} \, \text{is a function from $\Nat$ to $\Nat$} \]

By contrast,

\[ \vdash \tlabs{x}{\Nat}{x \cdot 2 + 1} : \Nat \to \Nat \]

has no assumptions. It is a closed term.

Lambda Abstraction and Application as Introduction and Elimination

In type theory, abstraction and application can be understood as the introduction and elimination forms for function types, analogous to introduction and elimination of implication symbol in natural deduction calculus.

These should be understood as type judgment rules.

Fur a function type $A \to B$ consider:

Introduction

Consider the following:

\[ \Gamma, x : A \vdash t : B \]

This judgment means:

Assuming the type judgments in $\Gamma$ (the context) and that the additional variable $x$ has type $A$, then the term $t$ has the type $B$ in the same context $\Gamma$.

The lambda-introduction rule says:

\[ \infrule{ \Gamma, x : A \vdash t : B }{ \Gamma \vdash \labs{x}{t} : A \to B } \]

Meaning:

if $t$ has type $B$ under temporary assumptions $x : A$ and context $\Gamma$, then $\labs{x}{t}$ has type $A \to B$ under the original context $\Gamma$.

Elimination

The elimination rule for the function type $A \to B$ (also called function application and implication elimination):

With context, the rule is written as

\[ \infrule{ \Gamma \vdash f : A \to B \qquad \Gamma \vdash a : A }{ \Gamma \vdash \lapp{f}{a} : B } \]

The first premise

\[ \Gamma \vdash f : A \to B \]

says:

Under the assumptions $\Gamma$, $f$ is a function that takes input $A$ and produces output of type $B$.

The second premise

\[ \Gamma \vdash a : A \]

says:

Under the same assumptions in $\Gamma$, $a$ is a term of type $A$.

The conclusion

\[ \Gamma \vdash \lapp{f}{a} : B \]

says:

Applying $f$ to $a$ gives a term of type $B$.

Lambda Abstraction in Rocq

Rocq uses they keyword fun for $\lambda$. So the lambda term:

\[ \tlabs{x}{\Nat}{x \cdot 2 + 1} \]

is written in Rocq as:

fun x : nat => x * 2 + 1

So in general

\[ \tlabs{x}{A}{t} \]

corresponds to

fun x : A => t

Lambda Abstraction in Rocq Function Definitions

Rocq lets us define fucntions in two equivalent styles. For example, Boolean negation can be written in the familiar argument style:

Definition negb(b : bool) : bool :=
  match b with
  | true => false
  | false => true
  end.

But it also can be written by explicitly giving a function value:

Definition negb : bool -> bool :=
  fun b : bool =>
    match b with
    | true => false
    | false => true
    end.

These two definitions are equivalent. So in general

Definition f (x : A) : B :=
  body.

Definition f : A -> B :=
  fun x : A => body.

are equivalent.

Multiple Arguments

Same idea applies. For example:

Definition g (x y : nat) : nat := 
  x * y + 1.

is shorthand for

Definition g : nat -> nat -> nat :=
  fun x y : nat => x * y + 1

where fun x y : nat => x * y + 1 is itself a shorthand for:

fun x : nat => fun y : nat => x * y + 1.

Or in lambda calculus notation:

\[ \labs{x\, y}{x * y + 1} \]

is a shorthand for:

\[ \labs{x}{\labs{y}{x * y + 1}} \]

Booleans in Rocq’s Core Library

Boolean values are available without any imports in Rocq. There are two canonical Boolean values:

true
false

Both are values of type bool.

Check true.
Check false.

true
     : bool

false
     : bool

Cell evaluated.

In Rocq, every expression has a type. The expressions true and false have type bool. The type bool itself also has a type: Rocq classifies it as Set.

Roughly speaking, Set is the universe of computational data types, such as Booleans, natural numbers, lists, and other datatypes. More generally, Set itself lives in a larger universe called Type.

Check bool.
About bool.
Check Set.
Check Type.

bool
     : Set

bool : Set

bool is not universe polymorphic
Expands to: Inductive Corelib.Init.Datatypes.bool
Declared in library Corelib.Init.Datatypes, line 39, characters 10-14

Set
     : Type

Type
     : Type

Cell evaluated.

A useful first picture is:

true  : bool
false : bool
bool  : Set
Set   : Type

So the hierarchy starts with ordinary values, then their types, and then universes classifying those types.

Note

In type theory, types are themselves objects that can be checked and classified. This is why commands like Check bool, Check Set, and Check Type are meaningful.

Certain pre-defined functions are also available out of the box and can be used to compute expressions. For example, negb is Boolean negation.

Check negb.
About negb.

Check negb false.
Compute negb false.

negb
     : bool -> bool

negb : bool -> bool

negb is not universe polymorphic
Arguments negb b%bool_scope
negb is transparent
Expands to: Constant Corelib.Init.Datatypes.negb
Declared in library Corelib.Init.Datatypes, line 84, characters 11-15

negb false
     : bool

     = true
     : bool

Cell evaluated.

Curried Notation

A function of two variables like orb is written in curried notation. This means that the value of orb on two Boolean arguments is written as

orb true false

not as

orb (true, false)

The second expression would suggest that orb takes a pair as input. But Rocq’s orb takes one Boolean argument first, and then returns a new function waiting for the second Boolean argument.

Check orb true false.
Check orb.
Check bool -> (bool -> bool).
Check orb true.

(true || false)%bool
     : bool

orb
     : bool -> bool -> bool

bool -> bool -> bool
     : Set

orb true
     : bool -> bool

Cell evaluated.

The type

bool -> bool -> bool

should be read as

bool -> (bool -> bool)

because arrow types associate to the right. Therefore, orb true is a function of type bool -> bool.

Note

A function type A -> B -> C means A -> (B -> C). A function of two arguments is therefore a function that takes one argument and returns another function.

We can compute using this syntax.

Compute negb (orb true false).

     = false
     : bool

Cell evaluated.

In the rest of the file, we construct basic functions from bool to bool and from bool to bool -> bool. Most of them are already contained in Rocq’s core library, but redefining them is a good way to learn pattern matching.

Basic Pattern Matching

To avoid conflicts with Rocq’s core library, we wrap everything in a module called BooleanValues. This is optional here, since we do not intend to use the current file as a library later on.

Module BooleanValues.

Cell evaluated.

Inside the module, our own definitions can have the same names as functions from Rocq’s core library. For example, when we define our own negb, it shadows the library function of the same name inside this module. The original library function still exists, but the unqualified name negb will refer to our local definition.

Note

A module gives us a local namespace. This lets us experiment with names like negb, andb, and orb without permanently overwriting Rocq’s library definitions.

Boolean Negation

Let us start with the definition of the negb function, which sends true to false and false to true. We define it by pattern matching on Boolean values.

Definition negb (b : bool) : bool :=
  match b with
  | true  => false
  | false => true
  end.

Check negb.

negb
     : bool -> bool

Cell evaluated.

The definition says: to compute negb b, inspect the possible forms of b.

If b is true, return false.
If b is false, return true.

Since bool has exactly two constructors, true and false, these two cases are exhaustive.

About negb.
Compute negb false.

negb : bool -> bool

negb is not universe polymorphic
Arguments negb b%bool_scope
negb is transparent
Expands to: Constant Top.BooleanValues.negb
Declared in toplevel input, characters 11-15

     = true
     : bool

Cell evaluated.

We can also give expressions a name and then use that name in later computations.

Compute negb (negb false).

Definition example_bool := negb false.

Compute negb example_bool.

     = false
     : bool

     = false
     : bool

Cell evaluated.

Note

Pattern matching is Rocq’s way of defining functions by cases. For bool, there are exactly two cases: true and false.

Boolean Conjunction

Now we define an andb function. It takes two Booleans b and b', and returns their Boolean conjunction.

The truth table for Boolean conjunction is:

`b`	`b'`	`andb b b'`
`true`	`true`	`true`
`true`	`false`	`false`
`false`	`true`	`false`
`false`	`false`	`false`

This truth table can be translated directly into a pattern match with four cases.

Definition andb (b b' : bool) : bool :=
  match b, b' with
  | true,  true  => true
  | true,  false => false
  | false, true  => false
  | false, false => false
  end.

Cell evaluated.

In fact, some simplifications are possible. If the first Boolean is true, then the result is just the second Boolean. If the first Boolean is false, then the result is always false, regardless of the second Boolean.

match b, b' with
| true,  b' => b'
| false, _  => false
end

The symbol _ is a wildcard pattern. It means: there is some value here, but we do not need to name it because the result does not depend on it.

Another possible, but less readable, way is to pattern match first on b and then on b'. This produces a nested program. It typechecks, but it is more verbose. Note that only the final end is followed by a period.

match b with
| true =>
  match b' with
  | true  => true
  | false => false
  end
| false =>
  match b' with
  | true  => false
  | false => false
  end
end.

As with negb, we can use andb to compute Boolean values.

Compute andb true false.
Compute andb true (negb example_bool).

     = false
     : bool

     = false
     : bool

Cell evaluated.

Recall that andb is a function of two variables, but it is written in curried notation. If we ask Rocq to check its type, we get bool -> bool -> bool, not a function type from pairs.

Check andb.
Check andb true.
Compute andb true.

andb
     : bool -> bool -> bool

andb true
     : bool -> bool

     = fun b' : bool => if b' then true else false
     : bool -> bool

Cell evaluated.

The expression andb true is a partially applied function. It is the function that takes a Boolean b' and returns andb true b', which is just b'.

We see in particular that arrow types associate to the right:

bool -> bool -> bool
=
bool -> (bool -> bool)

This means that an expression like

andb b b'

is parsed as

(andb b) b'

In contrast, the arrow type (bool -> bool) -> bool describes a function which takes a Boolean function as input and returns a Boolean value. We can define an example by evaluating a function f : bool -> bool at a given Boolean value.

Definition eval_at_true : (bool -> bool) -> bool :=
  fun f => f true.

Compute eval_at_true negb.
Compute eval_at_true (andb true).

Definition eval_at (b : bool) : (bool -> bool) -> bool :=
  fun f => f b.

Compute eval_at false negb.
Compute eval_at false (andb true).

     = false
     : bool

     = true
     : bool

     = true
     : bool

     = false
     : bool

Cell evaluated.

Boolean Disjunction

Let us define an orb function on Booleans.

The truth table for Boolean disjunction is:

`b`	`b'`	`orb b b'`
`true`	`true`	`true`
`true`	`false`	`true`
`false`	`true`	`true`
`false`	`false`	`false`

If the first Boolean is true, then the result is always true. If the first Boolean is false, then the result is the second Boolean.

Definition orb (b b' : bool) : bool :=
  match b, b' with
  | true,  _  => true
  | false, b' => b'
  end.

Cell evaluated.

Since the first branch does not actually use b', and the second branch only returns b', we can also write the same idea as a match on b alone.

match b with
| true  => true
| false => b'
end

Compute orb false false.
Compute orb false (negb false).

     = false
     : bool

     = true
     : bool

Cell evaluated.

Boolean Implication

Let us define Boolean implication. The intended truth table is:

`b`	`b'`	`implb b b'`
`true`	`true`	`true`
`true`	`false`	`false`
`false`	`true`	`true`
`false`	`false`	`true`

This corresponds to the classical idea that P -> Q is false only when P is true and Q is false.

For this one, we use Rocq’s if ... then ... else ... syntax.

Definition implb (b b' : bool) : bool :=
  if b then b' else true.

Cell evaluated.

Here

if b then b' else true

is essentially shorthand for the following pattern match:

match b with
| true  => b'
| false => true
end

So if ... then ... else ... is not a separate mysterious mechanism. For Booleans, it is a convenient notation for pattern matching on a Boolean condition.

Exercise: implement the function implb using pattern matching. The result of the following computation should be the Boolean true.

Compute implb false true.

     = true
     : bool

Cell evaluated.

Exercise: implement the Boolean if-then-else function as a function with type signature

bool -> bool -> bool -> bool

It should take three Boolean arguments:

condition -> then_branch -> else_branch -> result

One possible implementation is:

Definition ifb (b x y : bool) : bool :=
  match b with
  | true  => x
  | false => y
  end.

Theorem Proving

Next, we start using Rocq as a tool for proving properties of the functions we have defined. The syntax looks different at first, but in type theory stating a theorem is closely related to declaring a type, and proving a theorem is closely related to constructing a term of that type.

For example, the statement

negb (negb true) = true

is an equality proposition. To prove it means to construct a proof object inhabiting that proposition.

Note

In Rocq, a theorem statement is a type. Proving the theorem means constructing a term whose type is the theorem statement.

Negation Is Involutive

The first property that we prove is that, for every Boolean value b, we have

negb (negb b) = b

In ordinary language: applying Boolean negation twice gives us back the original Boolean value.

Let us start with some special cases, in which we prove our equality by direct computation. When using an interactive Rocq editor, the tactic state shows the current goal and helps guide the proof.

Theorem negb_negb_true_eq_true : negb (negb true) = true.
Proof.
  simpl.

Proving: negb_negb_true_eq_true

1 subgoal

-------------- (1/1)
true = true

Cell evaluated.

The simpl tactic simplifies the goal by computation. In this case, negb (negb true) computes to true.

  reflexivity.

Proving: negb_negb_true_eq_true

No more subgoals

Cell evaluated.

The reflexivity tactic proves goals where the two sides of an equality reduce to the same expression. It is stronger than a purely textual check: it can unfold definitions and compute enough to see that both sides are definitionally equal.

Qed.

Cell evaluated.

If you are just getting started with theorem provers, focus here on the block that starts with Proof and ends with Qed. This is a Rocq proof script. It is written in the tactic language, while function definitions like negb and andb are written in the core term language, called Gallina.

In this simple example, simpl is not actually necessary, because reflexivity can perform the needed computation itself.

Theorem negb_negb_false_eq_false : negb (negb false) = false.
Proof.
  reflexivity.
Qed.

Cell evaluated.

Here is the same proof written directly as a Gallina term. Note that we use Definition rather than Theorem.

Definition negb_negb_false_eq_false' :
    negb (negb false) = false :=
  eq_refl.

Cell evaluated.

The term eq_refl is the canonical proof that an expression is equal to itself. Since both sides reduce to the same Boolean, eq_refl is accepted.

You can check that the theorem and the definition produce essentially the same proof object using the Print command.

Print negb_negb_false_eq_false.
Print negb_negb_false_eq_false'.

negb_negb_false_eq_false = eq_refl
     : negb (negb false) = false

negb_negb_false_eq_false' = eq_refl
     : negb (negb false) = false

Cell evaluated.

If you try to prove something incorrect, the prover will let you know.

Theorem fail_to_unify : negb (negb false) = true.
Proof.
  Fail reflexivity.
Admitted.

The command has indeed failed with message:
Unable to unify "true" with "negb (negb false)".

Cell evaluated.

The command Fail reflexivity. asks Rocq to check that reflexivity fails. This is useful for experimentation. The theorem is then closed with Admitted, which means that the statement is accepted without proof.

Warning

Admitted is not a real proof. It is useful while experimenting or developing a file, but admitted theorems should not be treated as established results in finished work.

Now let us prove the general theorem. We need to prove the statement for an arbitrary Boolean b. Since b can only be true or false, it is natural to split the proof into two cases.

The destruct tactic plays the same role in proofs that the match keyword plays in function definitions.

In a function definition, match b with ... end defines a result by considering all possible forms of b.
In a proof, destruct b proves the current goal by considering all possible forms of b.

Since bool has exactly two constructors, destruct b creates two subgoals: one for b = true and one for b = false.

Theorem negb_inv (b : bool) : negb (negb b) = b.
Proof.
  destruct b.

Proving: negb_inv

2 subgoals

-------------- (1/2)
negb (negb true) = true
-------------- (2/2)
negb (negb false) = false

Cell evaluated.

After destruct b, the goal has been modified. In the first case, b has been replaced by true; in the second case, b has been replaced by false.

We use focusing dashes to separate the two subgoals.

  - simpl. reflexivity.

Proving: negb_inv

This subproof is complete, but there are some unfocused goals:

-------------- (1/1)
negb (negb false) = false

Cell evaluated.

The second case can be solved by reflexivity alone.

  - reflexivity.

Instead of using reflexivity, we can also reuse a previous proof with the exact tactic. The theorem negb_negb_false_eq_false has exactly the type needed for the second goal.

  - exact negb_negb_false_eq_false.
Qed.

Cell evaluated.

One may observe that negb_inv true is a proof of the equality

negb (negb true) = true

and that negb_inv itself is a proof of the universally quantified proposition

forall b : bool, negb (negb b) = b

Check negb_inv true.
Check negb_inv.

negb_inv true
     : negb (negb true) = true

negb_inv
     : forall b : bool, negb (negb b) = b

Cell evaluated.

Note

A theorem with a variable, such as Theorem negb_inv (b : bool) : ..., behaves like a function that takes an argument b : bool and returns a proof of the corresponding statement.

Equivalent Definitions of Implication

Recall the formulas from classical logic:

(P ⇒ Q) ⇔ ¬P ∨ Q
(P ⇒ Q) ⇔ ¬(P ∧ ¬Q)

The first formula is often taken as a definition of implication in classical logic.

In this section, we interpret the logical connectives as Boolean functions:

Logical notation	Boolean function
`P ⇒ Q`	`implb b b'`
`¬P`	`negb b`
`P ∨ Q`	`orb b b'`
`P ∧ Q`	`andb b b'`

Since we are working with Boolean-valued functions, saying that two Boolean formulas are equivalent means saying that they compute to the same Boolean value for all inputs. Therefore, we express equivalence here using equality of Booleans.

Later, when working directly with propositions in Prop, logical equivalence will be expressed differently, for example using <->.

We first prove the Boolean version of

(P ⇒ Q) ⇔ ¬P ∨ Q

This exercise also shows how to structure a proof with pattern matching on several variables. First, we present a nested version: we destruct b, and then destruct b' in each branch. This gives two cases corresponding to the possible values of b, with two subcases corresponding to the possible values of b'.

Theorem implb_eq_orb_negb (b b' : bool) :
    implb b b' = orb (negb b) b'.
Proof.
  destruct b.
  - destruct b'.
    + reflexivity.
    + reflexivity.
  - destruct b'.
    all: reflexivity.
Qed.

Cell evaluated.

The tactic all: reflexivity applies reflexivity to all remaining subgoals. Here, after destructing b', both remaining cases can be solved in the same way.

Next, we prove the Boolean version of

(P ⇒ Q) ⇔ ¬(P ∧ ¬Q)

Here we destruct b and b' simultaneously. This immediately creates four cases, much like the simultaneous pattern matching used in the definition of andb.

Theorem implb_eq_negb_andb_negb (b b' : bool) :
    implb b b' = negb (andb b (negb b')).
Proof.
  destruct b, b'.
  all: reflexivity.
Qed.

Cell evaluated.

Notice that we used explicit parameters (b b' : bool) rather than implicit parameters {b b' : bool}. Braces introduce implicit arguments, which Rocq tries to infer from context. This is useful later, but explicit parameters are clearer at this introductory stage.

End BooleanValues.

Cell evaluated.

Curry-Howard Correspondence

In Rocq, there is a deep analogy between ordinary functions and theorem with parameters. This is an instance of the Curry-Howard correspondence:

Propositions behave like types Proofs behave like terms/values inhabiting those types

For example bool is a type, and its inhabitants are the Boolean values:

true : bool
false : bool

Similarly, a proposition such as

neg (neg b) = b

can be understood as a type. Its inhabitants are proofs of that proposition. So if we have

p : negb (negb b) = b

Then p is a proof object whose type is the proposition

negb (negb b) = b

Analogy between Ordinary Functions and Theorems

Consider the ordinary boolean function:

Definition f (b : bool) : bool :=
  negb b.

This says:

f takes an input b : bool and returns an output of type bool

it’s type is

f : bool -> bool

And compare with the theorem:

Theorem negb_inv (b : bool) : negb (negb b) = b.

This can be understood as saying:

negb_inv takes b : bool and returns a proof of negb (negb b) = b.

After the theorem is proved, Rocq gives it the type:

negb_inv : forall b : bool, negb (negb b) = b

This is a dependent function type. It is called dependent becaus the result type depends on the input b. For example, if we apply negb_inv to true, we get:

negb_inv true : negb (negb true) = true

If we apply it to false, we get:

negb_inv false : negb (negb false) = false.

The important point is that negb_inv true is not a Boolean value. It is a proof object. More precisely, it s a proof of the proposition.

negb (negb true) = true

We can compare theorems and functions as follows:

Expression	Input	Output
`f`	`b : bool`	`negb b : bool`
`negb_inv`	`b : bool`	proof of `negb (negb b) = b`

The theorem

Theorem negb_inv (b : bool) : negb (negb b) = b.
Proof.
  destruct b.
  - reflexivity.
  - reflexivity.
Qed.

is conceptually similar to:

Definition negb_inv : forall b : bool, negb (negb b) = b :=
  fun b =>
    match b with
    | true => eq_refl
    | false => eq_refl
    end.

Set vs Type

The type bool lives in the universe Set:

Check bool.

bool
     : Set

Cell evaluated.

whereas propositions such as equalities live in Prop:

Check negb (negb true) = true.

negb (negb true) = true
     : Prop

Cell evaluated.

Both are type-like objects, but they have different roles:

Set: computational objects
Prop: logical propositions / proof types

Meaning of `Destruct`

The tactic destruct performs case analysis on an object according to the possible ways that object could have been constructed.

For example, if

b : bool

then b has only two possible constructors:

true : bool
false : bool

So when we write

destruct b.

Rocq splits the proof into two cases:

Case 1: b = true
Case 2: b = false

The word destruct is therefore connected to the idea of deconstructing a value: we inspect its outermost constructor and split into the corresponding cases.

The same idea applies to other inductive types. For natural numbers, a value of type nat is constructed either as 0 or as the successor of antoher natural nubmer. Therefore destruct n. splits the proof into the cases

Case 1: n = 0
Case 2: n = S n’

This is closely related to pattern matching. In a function definition, we write:

match b with
| true => ...
| false => ...
end.

In a proof, we write:

destruct b.

The difference is:

match: case-splits inside a term/program
destruct: case-splits inside an interactive proof

Summary

In this lecture, we saw the following ideas:

true and false are the two canonical values of type bool.
bool is classified by the universe Set.
Boolean functions can be defined by pattern matching.
Functions of several arguments are usually curried in Rocq.
The wildcard pattern _ means that the value is irrelevant in that branch.
if ... then ... else ... is a convenient notation for pattern matching on Booleans.
Theorems are types, and proofs are terms inhabiting those types.
simpl computes in the goal, while reflexivity proves equalities whose two sides reduce to the same expression.
destruct performs case distinction in proofs, analogous to match in programs.
Boolean equivalence of Boolean-valued expressions can be expressed as equality of Booleans.

Basics of Lambda Calculus

Bound and Free Variables

Typed Lambda Calculus

Open Terms and Contexts

Lambda Abstraction and Application as Introduction and Elimination

Introduction

Elimination

Lambda Abstraction in Rocq

Lambda Abstraction in Rocq Function Definitions

Multiple Arguments

Booleans in Rocq’s Core Library

Curried Notation

Basic Pattern Matching

Boolean Negation

Boolean Conjunction

Boolean Disjunction

Boolean Implication

Theorem Proving

Negation Is Involutive

Equivalent Definitions of Implication

Curry-Howard Correspondence

Analogy between Ordinary Functions and Theorems

Set vs Type

Meaning of Destruct

Summary

Meaning of `Destruct`