Lesson 1: Type Theory as a Mathematical Language

In our first steps with Coq, we start by importing the required libraries and setting some parameters. By default, Coq can only understand the quite bare-bones calculus of the Calculus of Inductive Constructions. This is a very "pure" language, but not very useful to do some more realistic examples. In this course, we will use a mature Coq library, "The Mathematical Components Library" which will provide us with a rich theory on data types and mathematics.

Interaction model:

Coq is an interactive theorem prover . That means that we submit commands to the system, and Coq will answer back with some feedback about our input. The first thing we need to understand in order to get familiar with Coq is how to use this interface. For this class, we will use the jsCoq web-based system, which has a "classical" 3-pane setup. The main window (left), contains a document with mixed text and Coq code. We can use the arrows in the right menu-bar to submit incrementally the code parts to Coq. jsCoq will highlight the code with different colors depending on the result Coq provides: - grey background means Coq accepted the sentence without problem - yellow background means Coq is processing the sentence - red means that Coq found a problem with the sentence You can also use the Alt-N (for next) and Alt-P (for previous) keys for a quicker navigation; on Mac, the command key is used instead. In addition to the colored feedback over the document, we have two panes in the right. The upper panel is usually called "goals panel", and is used to display the pending "proof obligations". The lower right panel is used to display miscellaneous information such as *error details*, search results, etc... To illustrate this, we can try to prove a quite logical theorem:

Basic Coq Commands:

Coq files are organized as mathematical documents using a vernacular language, which are basically a collection of definitions for top-level terms (or proofs) and their types (or propositions). We will precisely introduce what types and terms are next, but before, we also present some helper commands useful to develop interactive proofs. The basic ones are:

Definition / Theorem:

The core "vernacular" command to interact with Coq is the Theorem/Definition command, which is basically a wrapper to build a new definition that will be checked by Coq's kernel. The Theorem/Definition command has two forms:

• Interactive form:
  Theorem $name $arguments : $type. Proof. $tactics. Qed.
  In this form, the user specifies the definition / theorem to build, and Coq will switch to "interactive" mode where the user will employ a set of tactics to synthesize the desired term.
• Definitional form:
  Definition $name $arguments : $type := $term
  In this form, the user provides the full term directly.

The difference is best illustrated with an example:

It is possible to annotate arguments with types, so we can write:

Print:

The Print command allows us to inspect definitions, theorems, and data types. We can use it in the theorems we just defined:

About:

The About command allows us to print just the type of an object. This is useful as often we only care about the statement of a theorem, not about its proof. You can try with the previous examples and compare to Print:

Check:

About and Print display static metadata for Coq objects, the Check command allows us to actually run Coq's type checking and inference engine with arbitrary expressions. Some examples:

Search:

A very important command in practical use is Search, we will discuss Search more in the upcoming lessons, but we show a small example:

Documentation

Unfortunately Coq doesn't have commands to query documentation. The coqdoc tool is often used to generate, but this is an area that needs urgent improvement.

Section:

The last command we will survey here Section, which helps grouping arguments / hypothesis when several definitions share them. When a section is closed, the definitions inside it are generalized to include these arguments

Coq's Type theory and Functional Programming

As we have briefly discussed in the presentation, Coq is based on a functional calculus called the "Calculus of Constructions" which is a type theory. Type theories where invented in the early 20th century to avoid set-theoretical paradoxes, and were connected to logic and programming languages in the second half of the 20th century.

What is a type?

The exact definition of a type is an open research question. For the purposes of this tutorial, we can think of a type as a set. In TT it is common to use the colon symbol to denote "some object p is member of a set T", which we write as

   p : T

instead of the more traditional p ∈ T . From now on, we assume our objects to be programs. Then, we can write 3 : nat , true : bool , and fun x ⇒ x : nat → nat . We can also write true : nat which seems problematic! Coq's theory has the ability to assign types to objects under assumptions. This is in a sense the characterization of "functional". So we define environments Γ as lists of type assignments for variables x₁ ... xₙ such that Γ := (x₁ : T₁) ... (xₙ : Tₙ) . We call the resulting ternary relation "a typing judgment":

   Γ ⊢ p : T

which reads as "p is a program of type T under assumptions Γ". This the most important rule in the metatheory of Coq, and of many programming languages. Membership into the ⊢ relation is usually governed by a set of typing rules, usually written in deductive style. For example, we can write this rule for pairs:

   Γ ⊢ p₁ : T₁     Γ ⊢ p₂ : T₂
  ─────────────────────────────
    Γ ⊢ ⟨ p₁ , p₂ ⟩ : T₁ × T₂

which states that if the upper part of the rule is derivable, so is the conclusion or bottom part. Given a set of typing rules, a type-checker is a tool that will determine whether a triple Γ , p , T belongs to the ⊢ relation. This process can be decidable or not.

Proofs as types

The key idea that makes Coq usable as a proof checker is the "Curry-Howard" correspondence, which states that types can be understood as logical propositions, and programs can be understood as proofs. Then, we can read:

   Γ ⊢ p : T

as "p is a proof for proposition T under assumptions Γ", and our typing rules determine our logical theory. It is usually desired for our logical theory to be consistent, that is to say, to require it can't derive a type T and its negation. This is often not the case for type-systems in programming languages, and they for example allow well-typed programs not to terminate, which amounts to a circular proof. Under this optic, Coq is a tool that is often used to write down a theorem T, and synthesize a suitable p, such that "∅ ⊢ p : T" is derivable. In addition to the Curry-Howard correspondence, it is also useful to think of truth in the Coq system as an equivalent principle named the Brouwer–Heyting–Kolmogorov interpretation of intuitionistic logic, sometimes called BHK of "realizability" interpretation. Let's assume that propositions T are drawn from the language of first-order logic. Then assume that we have some Turing-complete language such as the untyped lambda calculus or a Partial Combinatory Algebra, with a distinguished pairing operator, then:

• a proof of "P₁ ∧ P₂" is a tuple < p₁, p₂ > where pᵢ is a proof of i.
• a proof of "P₁ ∨ P₂" is a pair <s,p> where if s (a boolean) is true then p is a proof of P₁, else p is a proof of P₂.
• a proof of "P -> Q" is a function that takes as input a proof of P and returns a proof of Q.
• a proof of "∀ x : S, ϕ(x)" is a function that converts an element s of S into a proof of "ϕ(s)"; note the similarity with the interpretation of implication !
• a proof of "∃ x : S, ϕ(x)" is a tuple <w,p> where w is an element of S and p is a proof of "ϕ(w)"

In the next section, we will codify this intuition using typing rules.

Coq's programs and types

For better or worse, users need to have a basic understanding of the typing judgment of Coq as to be able to debug errors and generally have a mental model of how their program or proof is going to be checked. This is "leaky" in a sense, but provides the very important advantage of having proofs objects that can be checked by a minimal kernel implementing Coq's typing rules.

The type universe

The first rule of Coq is that we have two special types Prop and Type, for types that are "logical" and types that are "computational". This is a key feature of Coq, and often confuses users. So for example, Coq validates nat : Type and P : Prop, Q : Prop ⊢ P ∧ Q : Prop The distinction between Prop and Type is quite technical, and at some point the Coq user will be required to learn more about it. We can summarize the intuition briefly here: types that are propositions "hide" their proofs, thus it is not possible to observe externally when two proofs are different. This provides the advantage of allowing "logical impredicativity", where the class of formulas is itself a formula. Types in Type do allow observation, but then the class of such types becomes necessarily stratified.

A type inside a type?

Indeed, you may have guessed that Prop and Type are quite strange animals, they are set of types, that contain types! That seems a bit paradoxical. Indeed, Prop and Type are special in Coq's calculus and can be thought of as proper classes instead of sets. Moreover, the typing relation is asserted usually twice, for example imagine 3 : nat and nat : Type , so in a sense we have 3 ∈ nat ∈ Type . It is a common error when starting with Coq to arrive to situation where we send to the system 3 : Type, which will fail, nat : nat :

Type formation rules

The main type formation rule for Coq is:

    Γ ⊢ P : Prop   Γ, (x : P) ⊢ Q : Prop
    ────────────────────────────────────
       Γ ⊢ forall (x : P), Q : Prop

Prop vs bool

A common question is whether propositions in Coq are boolean valued. For example, assume n m : nat, should n = m in bool or in Prop ? Recall that a proof in Coq is a program. Thus, if we place n = m in bool it means that when we assign a value to these variables, the proof will be an element of bool that is say, true or false. Thus, we have just declared with our types that equality of natural numbers is decidable. However, Coq is not limited to decidable propositions at all, and this is where Prop is required. In modern practice, there is a tendency to assign the type bool to most constructively boolean propositions. For example, for the main formation rule, we can only assign the type bool to ∀ (x : P), Q when P is a type of finite cardinality and Q can be assigned type bool too.

Gallina, Coq's programming language

We now proceed to introduce Coq's programming language "Gallina". Gallina allows the definition of functions, propositions, and data in a way that is well-suited for the construction of proof objects. Recall that the main goal of Coq's type-checker is to verify that a given Gallina program is valid, that is to say, can be assigned some type T. Given the input Γ ⊢ p : T, Coq's type checker will return yes/no. Let's now see Gallina's syntax and typing rules.

Variables

Variables in Gallina are just identifiers, and the typing rule will check that they are bound by doing a lookup in the environment, which will determine its type:

   (x : T) ∈ Γ
  ─────────────
    Γ ⊢ x : T

Creating functions / reasoning under hypotheses

Functions in Gallina are specified using a "lambda notation". For example, the identity function is written λ x → x , or in textual form fun x ⇒ x. In words of Dana Scott, "the lambda calculus captures the intuition of reasoning under a hypothesis". And indeed, we can see that in its typing rule:

   Γ, (x : T) ⊢ e : U     Γ ⊢ T : Prop    Γ, (x : T) ⊢ U: Prop
  ─────────────────────────────────────────────────────────────
           Γ ⊢ λ (x : T) . e : forall (x : T), U

which reads "λ x . e" has type "forall (x : T), U" under Γ if "e" has type "U" under Γ extended with assumption (x : T), and the types are properly built. When U doesn't depend on x, Coq will render ∀ (x : T), U as T → U. We can resort to Coq to check some lambda terms:

Function application / modus-ponens

   Γ ⊢ f : ∀ (x : T), U      Γ ⊢ e : T
  ─────────────────────────────────────
           Γ ⊢ f e : U[e/x]

which reads "e applied to f has type U with e substituted for x if f has the right functional type and e has the right argument type". We can just check some of the above terms, now with an argument applied:

In the case where the type doesn't depend on the argument (non-dependent case), we have:

   Γ ⊢ f : T → U   Γ ⊢ e : T
  ───────────────────────────
        Γ ⊢ f e : U

we can combine some rules to get:

   Γ ⊢ f : T → U     Γ ⊢ e : U → V
  ─────────────────────────────────
   Γ ⊢ λ (x : T) , e (f x) : T → V

which is the familiar modus-ponens rule.

Inductive Data Types

The above rules complete the presentation of the Calculus of Constructions! While we are missing some details related to Type, it is indeed remarkable how minimal it is, for the amount of logical power it packs. You may wonder "but what about the logical primitives?" "Where is negation, where is or? Where is bool?" That's a great question, and indeed so far we have been using some primitives that are not part of the above presentation. The reason is that types such as bool, and connectives such as or, or negation, can be encoded in the calculus we presented. For example, not and bool can be defined by using their "elimination principle":

The other connectives are encoded similarly. However, these encoding are pretty cumbersome to work with, and moreover they have bad computational properties. Thus, the original Coq Calculus is the extension of the core with inductively defined "data types", similar to the "algebraic data types" found in languages such as OCaml, Haskell, or Rust. Coq's inductives tho have some unique features due to the proof-theoretic nature of Coq which we will explore in the next lesson. Today, we will focus on more "vanilla" inductive data types.

Inductive definition

While so far we have been using Gallina to define programs, inductives are truly "pieces of data". For example, we can define the natural numbers in Coq in the following way:

Let's examine the definition carefully: the first line declares to Coq natural as a type, thus extending the typing rules to admit natural : Type. The second part of the declaration is what we call "constructors", that is to say, ways to build a natural number. The first constructor is the constant `O` , which is by itself a natural, and the second constructor is S, which takes a natural. So, if x : nat, then S x : nat. Coq's typing rules are extended so o : natural, and x : natural ⊢ s x : natural. Constructors can be seen as "tags" that represent different cases, so their name is a user choice. We can as well write:

or even

The key point is that this specification fully determines what the elements of the natural type are. For the first case, we have that if x : natural, x has to be either O or S x', where x' is another natural. Coq allows us to define quite arbitrary inductives, and they don't necessarily have be possible to inhabit. For example, this is a valid definition:

The elements of opus are all the proofs of 0 = 1, and as we know Coq is consistent, there is no such proof. So while we could define the data type, we will never be able to build one of its elements. So inductives extend the "programs are proof" motto to "data is proof". Inductive data types one of the key points in the success of Coq as a tool, as they allow us to model mathematical universes pretty precisely, while at the same time keeping the guarantee that we can't build some data that would lead us to inconsistency. This is not so easy, given that you may have noticed that for example the natural is recursive in nature. Indeed, Coq places some extra conditions on which inductives are admissible. Most common one is called "the positivity condition". Dually, when analyzing / consuming some data that is recursive, now Coq has to check that the function doing this is well-founded and thus it will terminate.

Case analysis

Provided some element of an inductive data type, we want to be able to analyze it in base of its declared constructors. For example, given a natural number, we may want to compute if the number is even. Or if our data represents some possible behaviors of a system, equivalently we may want to do a proof by case analysis. Coq supports by means of the match statement:

Note that instead of Definition, here we use the Fixpoint keyword, which does tell Coq that our definition is recursive. Coq will check that the definition indeed does terminate. If we try a definition that Coq can't see terminating, Coq will complain:

We can disable this check and get a proof of false

We can do case analysis for the bad datatype too:

Logic as Data

Coq's core calculus only has the ∀ logical connective, how can we define the rest of operations as data? Indeed, we can define them as follows:

Specifications in the Coq's Mathematical Universe

A very interesting and powerful use case of inductive definitions is building models of our specifications and logical theories. Imagine we have the axioms for a commutative magma, that is to say, a type with a binary endo-operator which happens to be commutative. We can specify that as:

As far as we are concerned, this is just a piece of data that packs a type, an operator, and an axiom of the operator. Can we construct such a structure with a type that is not void? The answer is yes:

We will dwell into this more in the next lesson, but in general we can understand elements of inductive types like elements of a model of Coq's coherent mathematical universe.

Computation and equality

So far, we have been using "computation" and equality in a quite informal sense. The notion of computation in Coq mainly corresponds to the notion of computation for the lambda calculus, that is to way, provided a function f : U → T and a term x : T, the application f u : T will compute by substituting u for the variable in the definition of f. There are several strategies in terms of evaluation strategies, but the main tricky part is that case analysis can't progress when a variable is in a match position:

The first result tells us that the if is waiting on b to get a value, and thus we can't progres as we do in the second case. This is logical and expected. However, it is well-known that in the presence of multiple parameters, we have to bias evaluation. Something we skimmed over (on purpose) so far was the question of equality of Coq programs. But if you look at the typing rules, it turns out that Coq needs to decide when typing when two types and programs are equal. Usually, we say that t1 is convertible to t2 if there is a term t such that t1 and t2 will evaluate to it, that is to say:

   ∃ t, t₁ ↦ t ∧ t₂ ↦ t
  ──────────────────────
         t₁ ≈ t₂

for example true || false ≈ true, 3 + 3 ≈ 6, and n.+1 ! ≈ n.+1 × n!, etc... Thus, when typing, Coq will consider two types equal when they are convertible:

   T ≈ U      Γ ⊢ p : T
  ──────────────────────
        Γ ⊢ p : U

Having convertibility in the type rules as a built-in is extremely useful and another reason for the success of Coq. However, there is a great tension between equality and computation, as we will short illustrate.

Equality, briefly

Equality in type theory is also an advanced research topic, with many possible definitions. Coq defines "user-level" or "propositional" (as opposed to computational) equality as a data type

When combined with the conversion typing rule, we have that all terms that are convertible are equal. However the converse doesn't hold, as we can strictly equate more terms propositionality than by conversion. We will see more examples in the next lesson, but the following example illustrates the problem:

In the second case, computation blocks. That may be surprising but it is due to + checking the left argument first. As it is a variable, it can't decide which case it is. Another way to understand this mismatch is by thinking of computation as directed vs equality as undirected.

Proofs by computation

Despite its shortcoming, computation inside Coq is extremely useful to do proofs; when our term is variable-free, we will get a normal form, and that has been used extensively to automate large proofs. Moreover, we can write algorithms inside Coq and prove their properties, then run them, and obtain a proof over the result. To do a proof by computation, we just need to tell Coq that our proof term is the equality constructor, erefl:

Coq's front-end

We will finish this lesson by looking into some more internal Coq implementation details, but that arise quite often in the real world. In particular, we will describe the two "elaboration passes" which are used by Coq to go from parsing to core "kernel" terms. Extensive use in the real world of Coq parsing extension and notations and type inference requires even the casual user to have some knowledge of this layers.

Notations and Implicit Arguments

Contrary to most programming languages, Coq's syntax and parser is highly extensible. This is a must in order to formalize non-trivial mathematics, as good readability is required. Users and libraries can declare Notations, which extend the parser, and will add some unsugaring rules Coq's first elaboration pass. Notations can mask some arguments, which then Coq will interpret as holes, to be resolved in the next phase. Example of notations are numbers, lists, logical operators, etc... The command Set Printing All. is of great help in the cases where the unsugared output is required to understand why something doesn't work.

Another important feature that users face a lot are implicit arguments. In many cases, like in equality, the first argument (base type of the equality) will be uniquely determined by the next argument. Thus, Coq allows us to declare this argument as "implicit", and a hole will be inserted for it automatically. Implicits are marked by using braces on the argument declaration, or by a explicit command. Thus, these two expressions are equivalent eq 3 and @eq nat 3.

Type inference

Coq has a quite advanced type inference engine. By virtue of Coq types containing terms, Coq's type inference engine is also a program synthesis engine on its own. Type inference is very important as Coq's kernel does require every lambda abstraction to be annotated with the type in order to type-check it. Moreover, it is often common to omit types of arguments for better readability and let Coq figure out using constraints and unification, and the first phase of implicit argument resolution will produce many "type holes" to be filled by the inference engine. While it is out of scope for this tutorial, making an effective use of Coq's type inference engine is essential to achieve an efficient proof style in the real world, both at the user level and at the tactic level. Among others, Coq's type inference engine support bidirectional inference, coercions, type classes, type-directed synthesis of records, and higher-order unification.