Intro to ITPs, Part 2

Last time, we introduced Rocq, the notion of proof, and how Rocq serves as both a programming language and a proof assistant at the same time. Today, we're going to go into more detail about what Truth is, how it relates to Proof, and continue on our journey exploring what we can express in Rocq, moving from Minimal Propositional Logic to full Propositional Logic.

Truth and falsehood

In propositional logic, a formula or statement is valid if for all assignments of variables, the statement evaluates to T. In PBT, true statements are those for which we have not yet found a counter-example (thus, they are only possibly true). Sometimes our inputs are finite and thus we can exhaustively test, but this is pretty rare.

We can be a lot more precise in Rocq, but we also have to be a lot more careful: precision comes with a cost that small mistakes could render a so-called theorem not always true.

So let's talk about how to represent truth and falsehood in Rocq. These will be our second encounter with data definitions in Rocq (after Nat), also called inductive types. Inductive types are an important enough part of the system that the theory that underlies Rocq is called the Calculus of Inductive Constructions.

There is a lot more to them, but for now, will focus on a couple important examples. So what are true and false? Well, it turns out there are two different versions, and the difference is very important. First, we have the ordinary, boolean data definition that should be familiar from any number of programming languages, though perhaps written in an unfamiliar notation.

Inductive bool : Set :=
    true : bool
  | false : bool.

Let's read this, carefully. First, it says we are declaring a new Inductive type called bool. In Rocq, everything has a type, including types, which is what the : Set is saying: the type of bool is Set, which is the type of ordinary data types. This data definition has two cases: true and false.

Aside from the syntax, this should be very familiar. And indeed, we have familiar operations on type bool: and, or, not, if, etc. However, in Rocq, we have a separate, much more important definition of truth and falsehood that exists for a very important reason.

As we mentioned above, in theorem provers that subscribe to the types-as-theorems idea that originated in AUTOMATH, we should not be able to prove false! One of the oldest statements from logic is ex falso quodlibet. Translated as "from falsehood, anything follows", the idea is that if you have a proof of false, you can prove any theorem. As a result, any logical system in which you can prove false would not be very useful. That means if we use our type bool as our definition of logical truth and falsehood, we are in trouble, as we can easily "prove" false: we just use the constructor for false.

Why is this not an issue in PBT? Essentially, our only reasoning is based on evaluation and assertions (often, of equalities). Our only theorems are individual test cases, and their proofs are based on evaluation, which must terminate. We thus do not have the principle of explosion (ex falso quodlibet), along with just about any other logical reasoning! Indeed, we rarely have proofs: we simply have searches for counter-examples, though in certain limited cases it can be exhaustive (and thus form a proof) -- e.g., when we were writing truth tables for propositional formulas.

So how should we define logical truth and falsehood? Truth is the following:

Inductive True : Prop :=   I : True.

i.e., True is a inductive type that has type Prop that has a single constructer, I. Why Prop and not Set? Rocq distinguishes between types that are used for theorems, which have type Prop, and types that are used for computation, which have type Set. The actual situation is actually a bit more complicated, as there is an entire hierarchy of types, that exist to avoid circularities in the logic, but generally we'll be able to avoid worrying about that.

Why is True a type that has a single constructor? Well, logical truth is essentially trivial: it tells you nothing, on its own, and thus you can always construct a proof of it (you don't need to know anything).

Logical falsehood ends up being a lot more important. How do we define it?

Inductive False : Prop :=   .

This type is much more baffling, at first. It is a type, that has type Prop, but it has no constructors. Why does in have no constructors? Because it is impossible to construct. This is exactly what we want out of our logic, which is our programming language! Thus, we can formally write the statement "from false follows anything", without worrying, since there should be no way of constructing a value of type False. Note the importance of the distinction between the types (the theorem statements) and the terms (the proofs). The type False can easily be written down, and indeed, it is a very important type! We will often want to express that certain cases are impossible. How will we do that? We will write that if such cases occur, False will result, and as a result, we need not do anything more in those cases (as they become trivial).

If, in a proof, we end up with a term of type False, by inspecting the value, we can determine that we must be in an impossible case, because such a value could never have been constructed, and thus no further work is needed.

Propositional Logic

Now that we have a way to describe truth and falsehood, let's continue on with operators from propositional logic. We already have implication (which exists in minimal propositional logic) how about logical and?

Inductive and (A B : Prop) : Prop :=   conj : A -> B -> A /\ B.

And a separate infix notation definition, @rocq{/}.

There are two projection functions, proj1 and proj2, to get the two fields out.

To use it, we could write a statement like @rocq{ P /\ Q -> P} as:

Definition and_1 (p : P /\ Q) := proj1 p.

(Though this is quite redundant since proj1 already exists).

Despite the new syntax, this is entirely something you could have written in OCaml!

type ('x, 'y) and_type = Intro of 'x * 'y

let and_1 (Intro (a, _)) = a

What is that argument p? Well, it has type P /\ Q, i.e., it is a conjunction of two propositions. That is its type: the term is simply a pair, and so we can use projections (proj1) and proj2) to extract out fields from the pair; in this case, the first field is the proposition of type P.

So what this program does is, given a proof of a conjunction (a term of type @rocq{P /\ Q}), returns a proof of P (a term of that type).

Written in this style, both the theorem (the type) and the proof (the term) are somewhat mixed together.

In addition to logical and, we have logical or, defined as another inductive type:

Inductive or (A B : Prop) : Prop :=
  or_introl : A -> A \/ B | or_intror : B -> A \/ B.

Which similarly has infix syntax \/.

Again, this could be defined in OCaml:

type ('a, 'b) or_type =
  | Inl of 'a
  | Inr of 'b

let x : (int, string) or_type = Inl 42
let y : (int, string) or_type = Inr "hello"

Unlike and, logical or is an inductive type with two cases: or_introl and or_intror. This is a constructive view of logical disjunction: that if you have a proof of \(A \lor B\), that should mean that you either have a proof of \(A\) or a proof of \(B\). Thus, the two ways of constructing A \/ B are constructors that take terms of type A and B.

To use a disjunction, we end up having to consider the two cases: given a term (proof) of type A \/ B, we must handle the case that either we had a proof of A or we had a proof of B. This means that, unlike with and, there are no projections. If x : A \/ B, we don't have proj1 x : A and proj2 x : B. Rather, we have two possibilities for x: it is either or_introl a or or_intror b, where a : A and b : B.

We can deal with that in code using pattern matching, as follows:

Definition or_1 (pq : P \/ Q) (hp : P -> R) (hq : Q -> R) : R :=
  match pq with
  | or_introl p => hp p
  | or_intror q => hq q
  end.

Here, we handle the two possibilities, and invoke the corresponding function (hp or hq) accordingly.

This is exactly analogous to how we program with partial functions in OCaml. The same function could be defined with out data definition for Or above as:

let or_1 (pq : ('p, 'q) or_type) (hp : 'p -> 'r) (hq : 'q -> 'r) : 'r =
  match pq with
  | Inl p -> hp p
  | Inr q -> hq q

Logical not is defined not directly, but by way of logical falsehood:

not = fun A : Prop => A -> False : Prop -> Prop

extras

Let's actually write down the principle of explosion (ex falso quodlibet) if we could have an element of False:

Theorem ex_falso : forall P : Prop, False -> P.
Proof.
  intros P H. destruct H.
  (* alternatively: contradiction. *)
  (* fun P (H : False) => match H with end .*)
Qed.