Live coding session for the third lecture of MPRI PRFA (2-7-2)

For this class we will look a bit more at the theory behind Coq (and other proof assistants like Agda or Lean): dependent type theory. We will see how this underlying theory comes into play when proving theorems and defining functions.

Dependent functions and type universes

Dependent types mean that types can depend on terms. See for instance the if in the type of the function below.

Another important part of the theory is the notion of universes. Essentially Type and Prop are universes. They contain respectively the types and propositions (as the names suggest).

Above you see that Type itself has type Type. It makes sense, after all Type is indeed a Type. However, assuming Type : Type actually leads to inconistencies (proofs of False) so instead, we have a hierarchy of universes: basically Type₀ : Type₁ : Type₂ …. You can ask Coq to show you universe levels by using the following command. If you are using VSCoq Legacy, it will not work and instead you need to use the command palette and choose "Coq: Display options" and then "Universe levels". Do exactly the same to switch it back.

This is not very easy to read but essentially it says that Typeᵢ lives in Typeᵢ₊₁. The fact that the universe levels are not displayed and inferred by the system is sometimes called: typical ambiguity. Even while hidden they still play an important role. If for instance we alias Type under some name T, we will run into an issue with the following definition.

Here you get what is called a "universe inconsistency" because you cannot quantify over a universe and stay within it essentially. Compare however with the following, seemingly equivalent, presentation.

This time it works because the Type on the right has a higher level that the one on the left so that it is able to contain it. You don't need to worry too much about universes at this point but know that they exist to forbid inconsistencies and that sometimes you will get universes inconsistencies that will require to look more closely at the definitions. Back to Prop now.

Prop is of type Type and actually Prop doens't have any hidden universe levels. It however has one interesting property which is that to create a proposition you can quantify over anything. This includes Prop itself. This propery is called impredicaitivity and is not present in Agda for instance.

Proof terms

Let us consider again the even predicate from last week.

As we showed you, constructor is actually applying the correct constructor between evenO and evenS. So when proving even 4 we can actually be explicit like below:

Now let us use Print to see what the proof is to Coq.

You see two uses of evenS followed by evenO. We also see that the numbers 2 and 0 are there because they appear as arguments to evenS but they're not really necessary so we can mark them as implicit so they don't bother us.

Now the proof of even 4 we write directly as follows:

Forall, implication

For now you saw what to do with ∀ and → interactively, and it was very similar: you use intro or intros to prove them, and apply to use them. When we prove something using tactics we can ask Coq to show how it built it with the command Show Proof. Let's see on an example.

We get what is called a proof term: it's a definition whose type is exactly the proposition we wanted to prove. We can use it directly to prove our lemma.

Coming up a with a proof term by hand is hard, and Coq can also help us write it using the refine tactics which accepts a partial term with some underscores (_) and then you can fill them interactively.

The proof in essence hasn't changed. All it comes down to is the typing rules of the theory. If you know the Curry-Howard correspondance for simple type theory this shouldn't be surprising: proving A → B is the same as defining a function from A to B. The introduction rule corresponds to λ-abstraction: Natural deduction Γ, A ⊢ B

---

Γ ⊢ A → B Simple type theory Γ, x : A ⊢ t : B

---

Γ ⊢ λ (x : A). t : A → B If you don't know λ-calculus, then think of λ x. t as a function taking an argument x and returning t where t might mention x. The elimination rule for implication then corresponds to application: Natural deduction Γ ⊢ A → B Γ ⊢ A

---

Γ ⊢ B Simple type theory Γ ⊢ f : A → B Γ ⊢ u : A

---

Γ ⊢ f u : B We mentioned before that we have dependent types, that lets us write things such as ∀ (x : A), B. This generalises the rules above to quantifiers: Dependent type theory Γ, x : A ⊢ t : B

---

Γ ⊢ λ (x : A). t : ∀ (x : A). B Γ ⊢ f : ∀ (x : A). B Γ ⊢ u : A

---

Γ ⊢ f u : Bx := u Notice how x mayb appear in B and thus needs to be replaced by u. Let us see how it works in practice:

Let us see again proof terms in action and how it compares to tactics.

We can just do it in direct style.

And, or, exists

First, we'll have a look at the definitions of various logical connectives and propositions we've used over the course of the lecture.

You can also get them using Print.

To eliminate a proof of False, one can just match on it and provide the exactly zero cases that are needed.

The rest should be easier to understand.

Using tactics to build definitions.

In fact there is no rule that says that tactics are reserved for proofs. Proving and programming are essentially the same thing in Coq! Note that instead of Qed we need to put Defined to tell Coq we care about the content of the definition.

Modulo some simplication, we get the same thing as what we would have written by hand.

Proofs using terms can be quite short.

Guard condition

If you remember, when we talked about Fixpoint we mentioned {struct n} and how it was necessary to tell Coq which argument was structurally recursive but we never explicitly said why termination is so important in the first place. Actually, if we deactivate the termination checking, we can derive a proof of False very easily.

False is simply proven via a loop!

We get back a proof of False by applying the function f.

The termination checker is not the only important part of the system. One such criterion is called positivity and is imposed on inductive types definitions. It says that a constructor to an inductive type cannot mention said inductive type on the left of an arrow (→). See the following example when deactivating positivity checking from which we can derive False.

It already looks fishy because C here has type ¬ bad → bad.

Recursors

Induction principles in Coq are primitives, they actually unfold to a combination of Fixpoint and match. See below how we define them for nat and list.

Reduction

Up till now we've been using simpl a lot without really telling you what it does. Essentially it triggers what we call reduction rules. Those correspond to the evaluation of programs. The first rule that applies is called β-reduction. What it does is turn `(fun x => t) u` into `tx := u`. We can see it in action by using the Eval command. It takes as argument a reduction strategy (such as simpl).

Now simpl does much more than β so if we want to only perform β we do:

cbn stands for call-by-name and is a strategy that can be parametrised by flags such as beta to limit its action. Here we have limited it to β-reduction. Indeed, one can notice that neither + nor × have been reduced. This way we get control over computation.

---

We have not really seen them, but it's also possible to introduce let bindings in definitions as a way to name intermediary results. Expression let x := u in t can be reduced (using ζ-reduction) by substituting u for x in t.

Unfolding definitions There are several ways to unfold definitions. The first one is with the unfold strategy. unfold foo will unfold the constant foo. Another one is to perform δ-reduction which simply replaces names by the corresponding definitions. A list of names can be provided but is optional. If no name is provided then all possible δ-reductions are performed. To use delta we switch to cbv which stands for call-by-value. Note: δ is like definition.

The output from the previous function might be surprising to you. Let's look at a simpler example to understand what is happening.

What happened is that Coq here also unfolded the definition of + (which is add) which is defined through a combination of Fixpoint (or fix) and pattern matching (match). fix and match have their own set of reduction rules of the same name. The combination of the two is called ι-reduction (ι like inductive). We will see how it goes in interactive mode where we can also use unfold, cbn or cbv as tactics (exactly like simpl).

Control of unfoldings Somethimes we want to simplify an expression but only focusing on some parts. Say in the expression (S n + m) - m from last week where we only wanted to reduce the + part. We showed simpl add but there are other ways to do it.

Sometimes we'd rather provide a list of exceptions not to be unfolded:

There are more strategies like lazy, hnf, or vm_compute… More detail in the reference manual: https://coq.inria.fr/doc/v8.18/refman/proofs/writing-proofs/equality.htmlapplying-conversion-rules * Here is a demo of examples of proof terms. In particular we show you cases where the proof term is much shorter than using tactics.

Note implicit argument overloading of or_introl and or_intror

ADVANCED

Mutual inductive types

It is also possible to define several inductive types at the same time. You just combine them with the with keyword. This way we can define the type of trees mutually with that of forests (which are basically lists of trees).

You can then define mutual definitions over such types by using Fixpoint and the with keyword.

Nested inductive types

Finally, you can define more inductive types by using what is called nesting. In the type below, you define a tree as something that contains a list of trees.