MPRI 2-7-2 / 2024 / Live coding session 5

The goal of this lecture is

• understand more about sorts in Coq, i.e. about Type and Prop. This is helpful to decipher certain error messages that occasionally occur in practical developments.
• understand how induction principles are implemented and use this knowledge to implement induction principles for inductive types where Coq's automatic generation is too weak.

Sorts

We have already seen Type and Prop. They We are also called "universes" or "sorts". You have seen that seemingly Type : Type

but also that Type is actually a hierarchy of universes Type@{i} in order to avoid inconsistencies with Type : Type, which becomes visible once universe printing is enable. Note that in VSCoq you have to use the command palette (Ctrl/Cmd + Shift + P) and then "Coq: Display Universe levels".

Below we will see more about the typing rules of Type, in particular a reminder how the typing rule of forall works.

Universe of foralls. As you can see below, the type of a forall is the maximum of the types of the domain and codomain. See what it means for a forall containing Type.

Cumulativity Another property of Coq (and not present in Lean or Agda) is called cumulativity. It is a form of subtyping that says that Type@{i} is a subtype of Type@{j} when i ≤ j. See how A : Type@{i} also lives in Type@{j} but not the converse.

Prop lives in Type@{i} for all i.

Here you see Coq mentions a constraint that Set < i. There is indeed a third kind of universe we did not mention but you may have seen already. It's called Set. You can think of it as the lowest Type universe: Type@{0}, but in Coq it's actually Type@{Set} because the universe levels (i, j, k etc.) are not natural numbers but abstract variables with constraints like the one we added above. Set is the smallest Type and it is the only one which does not contain Prop. We do have cumulativity going from Prop to Set and Type however. An overview: Prop : Type@{Set+1} Set : Type@{Set+1} Prop <= Type@{Set+1} Set <= Type@{Set+1} Type@{i} : Type@{i+1} Type@{i} <= Type@{i+1}

Impredicativity. Prop has other particularities. When considering a forall that ends in a proposition, then the whole forall stays a proposition. This means that things like forall n, n = n or forall (P : Prop), P are propositions. This is impredicative because things like forall (P : Prop), P are actually quantifying over themselves. This is another big difference with Agda which is predicative instead. To remedy this they have to also add universe levels to Prop like Prop@{i}. In Coq, the universe of a forall ending in a proposition is always a proposition, regardless of the size of what we quantify over. This comes from the intuition (and models) that Prop is proof-irrelevant: all propositions are morally either empty (False) or contain only one element (True) so Prop can be seen (modelled) as a set with two elements so it is always small.

Again on VSCoq, use the palette to deactivate it. The same command works to disable universe printing.

Elimination restrictions Universes are also important when defining inductive types. When should you put your type in Prop or in Type? We have seen several examples: things like disjunction and conjunction are placed in Prop, but bool : Type for instance. The central reasons are the Prop is an impredicative sort (more on that below), but also that Prop can be axiomatically assumed to be "proof irrelevant".

In other words, this means that proofs cannot impqact computation in a meaningful way. That is, we cannot analyse a proof to build a a function that is supposed to compute a boolean.

As long as we remain in Prop, we can do pretty much the same as before.

We can also map the usual booleans into them.

But the converse we can't.

Coq complains that proofs can only be eliminated to build other proofs. The same happens in proof mode of course.

We can instead prove something weaker like this:

We can however not prove that there is a **function** inverting to_prop_bool, because this would be inconsistent with PI:

Singleton elimination However, there are crucial exceptions to the rule: If a type has at most one constructor and all the non-parameter arguments of the constructor are proofs, then such eliminations are allowed. This property is called (sub)singleton elimination because it essentially says that you can eliminate a proof, as long as there can be at most one such proof. So a term that depends on it, doesn't really depend on it in the end, but merely on the fact that there exists a proof. Note that they don't need to be in (sub)singletons but only in Prop. See the example below.

It also works with True, but it's not so interesting. Another more interesting case is equality. This means, you can use tactics such as rewrite on any type.

The above we can do in general:

Disjunction for instance does not fall under the exception:

Induction principles

Trees We can easily define binary trees (with labels in A) as follows. As for every inductive type, Coq generates induction principles corresponding to the various sorts:

• bintree_ind for Prop
• bintree_rect for Type
• bintree_rec for Set (but you can ignore it and use bintree_rect)

General trees Now say we don't want to limit ourselves to binary trees. The obvious way to define trees is to have nodes take a list of subtrees. Now as we're going to see, the induction principle that Coq generates is insufficient.

We have no induction hypopthesis at all!!

Indeed, see what Coq generated for us:

It essentially corresponds to a case analysis, but no induction hypotesis is avaiable. This is because we are using what we call *nested* inductive types. Coq does not know what to do with assumptions of type list so it just does nothing. Of course, this is stupid and we probably still have to suffer it because of backwards compatibility. Let's see how we can do better. First, notice that Coq still supports this kind of induction by using fixpoints. We can actually use them interactively.

Qed fails here because Coq cannot see our fixpoint terminates. Indeed, we used a recursive call on something completely unrelated. The reason we only know now is that Coq only checks for termination at Qed time, and not before. There is way to know beforehand though: the Guarded command checks that the guard condition (which verifies termination) holds up to the point where it's called.

This time it should actually work because morally we only use recursive calls on elements *in* the list, but Coq doesn't know it.

We in fact need to be able to recurse on the list, so we the same way we nested inductive types, we need to nest fixpoints. For this we can use the fix tactic which introduces a fixpoint. We need to revert the argument on which we want to recurse and then fix aux 1 will introduce a new hypothesis named aux corresponding to potential recursive calls.

This was rather painful because we have manually ensure that Coq recognises the proof to be structurally recursive. Ideally we would like to be able to do induction like always. In order to do so, we are going to use fixpoints to prove our own induction principle for trees. We'll start by copying the type of tree_ind.

We then add an induction hypothesis for all elements of the children list

Instead of using In, we can also use the Forall predicate

We can now use this induction principle by hand to prove tree_map_id again:

In fact, we can still use the induction tactic to do it. This is done with the special "using" keyword as below.

Size recursion

We have already seen size induction earlier. We can use the same idea to prove a size recursion principle:

Well-founded induction

The last topic how to do induction / recursion along *any* well-founded order. We define well-foundedness of an order on a point as the so-called Accessibility predicate:

We can prove that accessible points are not contained in loops:

And that accessible points are not the start of an infinite descending path

We give a proof that one can use recursion on proofs to write a function that "extracts" the witness from proofs of ∃ n, f n = true. This proof can be given using different ways. We show the easiest approach here, and leave a variant using Acc as exercise.