Computer Aided Formal Reasoning 1996/7 Lecture notes 10 Judith Underwood

Quantification over types

Today we will look at type universes and quantification (both universal and existential) over Type. We have used universal quantification over both Prop and Type, but we have not looked carefully at the rules for Type. We have also not seen how existential quantification extends to Type.

We will introduce rules two new type constructors, called Π and Σ. We are already familiar with Π – it is just another name for the dependent function type we have been using to describe quantification. Σ types are a different form of existential types.

We will first look at typing rules for terms in Π types, then Σ types. We will then give formation rules for Π and Σ types. It is in the formation rules that we shall see how the Π and Σ types differ from the universal and existential quantification in Prop.

Π types

We will begin with Π types, since we are already familiar with them. In Lego, the rules for introduction and elimination of Π are as follows:

                               \frac{G, x:A ⊢ b:B}{G ⊢ [x:A]b :\{x:A\}B}

The Lego notation [x:A]b : {x:A}B is written elsewhere λx:A.b : Πx:A.B. (Here, Lego has a certain advantage in that it is easier to parse.) In this rule, x may be free in B (but not in G). If x is free in B, it becomes bound in {x:A}.B.

                            \frac{G ⊢ f:\{x:A\}B   G ⊢ a:A}{G ⊢ f a:B[a/x]}

Note that if x is not free in B, these rules are the same as those for the function type A →B. Because of this, Π types are sometimes called “dependent function types”. (They are also called “dependent product types” by those who consider that the operator describes the (possibly infinite) Cartesian product of all the B[x] as x ranges over A.)

The terms in Π types compute the same way that the ordinary functions do – the difference is solely in the fact that the type of the result may depend on the argument to the function. This is the Type version of universal quantification; we’ll compare it to universal quantification in Prop later.

Σ types

Just as Π types represent universal quantification, Σ types represent existential quantification at the level of Type. (Recall that Ex creates things of type Prop. The introduction rule for Σ is:

                            \frac{G ⊢ a:A   G ⊢ b:B[a/x]}{G ⊢ (a,b):<x:A>B}

Again, x may be free in B. If x is free in B, it becomes bound in <x:A>B.

The idea is that <x:A>B means “there exists an x:A such that B,” and, to prove this, we must supply both an a:A and a proof of B[a/x].

Unlike Ex, the Prop level existential quantifier, from a proof of <x:A>B we can directly extract both the witness and the proof that the witness satisfies B:

                                  \frac{G ⊢ M:<x:A>B}{G ⊢ M.1:A}

                                \frac{G ⊢ M:<x:A>B}{G ⊢ M.2:B[M.1/x]}

Note that if x is not free in B, these rules just describe a cartesian product type A × B. Because of this, Σ types are sometimes called “dependent product types”. (Recall that Π types are also sometimes called dependent product types. Those who call Π dependent product will call Σ a “dependent sum type,” considering it as a disjoint union of the B[x] as x ranges over A, represented by tagging elements with the associated element of A.)

The terms in Σ types compute the same way that the ordinary pairs do, except instead of fst and snd we have .1 and .2. Computationally, the difference is only in the fact that the type of the second component of the pair may depend on the first component.

Σ and Π as quantification

The dependent Σ and Π types can be interpreted as representing predicative quantification over types. The fundamental difference between Prop and Type lies in precisely what the quantified variables range over. Specifically, the difference lies in whether or not the formula/type being defined is included in the scope of the quantification. In Type, we are actually quantifying over type universes Type(0),Type(1), ... as explained below.

As with Prop, we can consider Π types to represent universal quantification. {x:A}B asserts that for all x of type A, B holds (really B is inhabited). Thus an element of this type produces something in B[a/x] for every a:A. The type <x:A>B corresponds to ∃x : A.B in the sense that <x:A>B has an inhabitant if there exists a of type A such that we can construct an inhabitant of

B[a/x].

Unlike Prop, when quantifying over Type we do not wish to include the type currently being defined in the range of the quantified variable. To do this, we construct a hierarchy of universe types (types which contain other types as elements). The idea is to begin with a lowest type universe Prop containing base objects and building on top of it universes Type(i) where in Type(i) types which are defined by quantification over elements of universes Type(j) where j < i. More formally, we can write this as the following type construction rules:

                      \frac{G ⊢ A:Type(i)   G, x:A ⊢ B:Type(i)}{G ⊢ \{x:A\}B : Type(i)}

Note that this Π is created by quantifying over an element of Type(i), not all of Type(i) itself. This means that the quantified type is still in Type(i).

It may be easier to understand this if we consider a different rule:

                   (*)  \frac{G ⊢ A:Type(i)   G, x:A ⊢ B:Type(j)}{G ⊢ \{x:A\}B : Type(max(i,j))}

We have a similar rule for Σ:

                      \frac{G ⊢ A:Type(i)   G, x:A ⊢ B:Type(i)}{G ⊢ <x:A>B : Type(i)}

These rules describe the relationship between the universes:

                                \frac{G ⊢ A:Type(i)}{G ⊢ A:Type(i+1)}

                              \frac{i < j}{G ⊢ Type(i):Type(j)}

Exercise: Show that (each instance of) rule (*) is derivable from the other rules.

Note that we have lost some of the distinction between terms and types, since types are elements of types as well as having terms being elements of types. Nevertheless, we can make some distinction by declaring those things in some universe type (including Prop) to be types.

In this system, we can only define a type T by quantifying over types T′ which may not contain T. This is called a predicative definition. Compare this with Prop, where we have the rule

                              \frac{G, x:Prop ⊢ B:Prop}{G ⊢ \{x:Prop\}B : Prop}

In other words, we are defining an element of Prop by quantifying over all elements of Prop – including the one we are currently defining. This is impredicative quantification.

Application

Using Σ types, we can write a specification as a type. For instance, consider the integer square root function, which, given x, returns the greatest integer y less than or equal to \sqrt{x}. In other words, we must have y^{2} ≤ x and x < (y + 1)^{2}. We can now write the type of this function as a logical statement “For all x, there exists y such that y^{2} ≤ x and x < (y + 1)^{2}.” In Lego, this is

{x:nat}<y:nat> (and (Le (times y y) x)
                    (Lt x (times (suc y) (suc y))))

Considered as a type, any element of this type is an integer square root function, i.e. if we have that f is in this type, then for any n, we have

(and (Le (times (f n) (f n)) n)
     (Lt n (times (suc (f n)) (suc (f n)))))

A big proof

As an example of a medium-sized development, I will derive an element of the type

{x:nat}<y:nat> (and (Le (times y y) x)
                    (Lt x (times (suc y) (suc y)))).

I am going to use a number library functions and lemmas, in particular:

Le_zero_n : {n:nat}Le zero n
zero_Lt_suc_n : {n:nat}Lt zero (suc n)
Le_trans : {x,y,z|nat}(Le x y)->(Le y z)->Le x z
Le_suc : {x:nat}Le x (suc x)
lt_true_imp_Lt : {n,m:nat}(Eq (lt n m) true)->Lt n m
lt_false_imp_Le : {n,m:nat}(Eq (lt n m) false)->Le m n
plus_commutes : {m,n:nat}Eq (plus m n) (plus n m)

These lemmas live in various libraries. They are all imported by lib_nat_rels, which defines various relations on the natural numbers. Note that the relations are both propositional valued and boolean valued; we have both

Lt : nat -> nat -> Prop

and

lt : nat -> nat -> bool.

I will also use a lemma (“here’s one I prepared earlier”):

Lt_lemma :  {x,y:nat}(Lt x (times (suc y) (suc y)))->
              Lt (suc x) (times (suc (suc y)) (suc (suc y)))

The Lego module containing the proof of this lemma will be available with these lecture notes from the course web page.

Goal
  ?0 : {x:nat}<y:nat>and (Le (times y y) x) (Lt x (times (suc y) (suc y)))
Lego> Refine nat_elim [x:nat]<y:nat>
(and (Le (times y y) x) (Lt x (times (suc y) (suc y))));
Refine by
  nat_elim ([x:nat]<y:nat>
            and (Le (times y y) x) (Lt x (times (suc y) (suc y))))
  ?1 : <y:nat>and (Le (times y y) zero) (Lt zero (times (suc y) (suc y)))
  ?2 : {x1:nat}
       (<y:nat>and (Le (times y y) x1) (Lt x1 (times (suc y) (suc y))))->
       <y:nat>
       and (Le (times y y) (suc x1)) (Lt (suc x1) (times (suc y) (suc y)))

The rule for Sigma introduction is Intros # (though actually regular intros will work as well.) This breaks down a goal of the form <x:A>B into its two parts:

Lego> Intros #;
Intros (0) #
  ?3 : nat
  ?4 : and (Le (times ?3 ?3) zero) (Lt zero (times (suc ?3) (suc ?3)))

Note that the second goal depends on the first, as expected. This is the base case, i.e. the value of the function on zero, which is zero:

Lego> Refine zero;  (* base case -- y=0 when x=0 *)
Refine by  zero
  ?4 : and (Le (times zero zero) zero) (Lt zero (times (suc zero) (suc zero)))

Now we verify that zero satisfies the specification.

Refine by  pair
  ?7 : Le (times zero zero) zero
  ?8 : Lt zero (times (suc zero) (suc zero))
Lego> Refine Le_zero_n;
Refine by  Le_zero_n
  ?8 : Lt zero (times (suc zero) (suc zero))
Lego> Refine zero_Lt_suc_n; (* done with base case *)
Refine by  zero_Lt_suc_n

Now we begin the inductive case. (The goal actually appeared at each step above but I removed it for ease of reading.) Here is the goal:

  ?2 : {x1:nat}
       (<y:nat>and (Le (times y y) x1) (Lt x1 (times (suc y) (suc y))))->
       <y:nat>
       and (Le (times y y) (suc x1)) (Lt (suc x1) (times (suc y) (suc y)))
Lego> intros __;
intros (2) __
  x1 : nat

  x1_ih : <y:nat>and (Le (times y y) x1) (Lt x1 (times (suc y) (suc y)))
  ?11 : <y:nat>
        and (Le (times y y) (suc x1)) (Lt (suc x1) (times (suc y) (suc y)))

Given the integer square root of x1, we now need to calculate the integer square root of suc x1. The value of the square root of x1 is going to be important, so we will give it a name:

Lego> [y1 = x1_ih.1];
defn  y1 = x1_ih.1
      y1 : nat

Now we have the critical step. The value of the square root of suc x1 is either y1 (for example, 3 is the integer square root of both 9 and 10) or suc y1 (for example, 3 is the integer square root of 15 but 4 is the integer square root of 16). We need to create a case split depending on whether or not suc x1 is still less than times (suc y1) (suc y1). How can we create this case split from nothing?

We can create case splits on boolean values with bool_elim; but Lt (suc x1) (times (suc y1) (suc y1)) is a Prop, not a bool. However, “less than” is a decidable predicate on (pairs of) natural numbers – hence we could write a function lt:nat->nat->bool such that lt a b is true if and only if Lt a b is provable. In fact, this function exists in the library, along with several theorems describing the connection between Lt and lt.

So now we know we want a case split on the boolean value lt (suc x1) (times (suc y1) (suc y1)). To create this, we use bool_elim with a new variable b, and add, as an extra

hypothesis, that b equals lt (suc x1) (times (suc y1) (suc y1)) Then bool_elim gives us

the two cases

Eq (lt (suc x1) (times (suc y1) (suc y1))) true
Eq (lt (suc x1) (times (suc y1) (suc y1))) false

Here is what happens in Lego:

Refine bool_elim [b:bool](Eq (lt (suc x1) (times (suc y1)(suc y1))) b)->
<y:nat>and (Le (times y y) (suc x1)) (Lt (suc x1) (times (suc y) (suc y)));
Refine by
  bool_elim ([b:bool](Eq (lt (suc x1) (times (suc y1) (suc y1))) b)-><y:nat>
             and (Le (times y y) (suc x1))
                 (Lt (suc x1) (times (suc y) (suc y))))
  ?13 : (Eq (lt (suc x1) (times (suc y1) (suc y1))) true)-><y:nat>
        and (Le (times y y) (suc x1)) (Lt (suc x1) (times (suc y) (suc y)))
  ?14 : (Eq (lt (suc x1) (times (suc y1) (suc y1))) false)-><y:nat>
        and (Le (times y y) (suc x1)) (Lt (suc x1) (times (suc y) (suc y)))
  ?15 : bool
  ?16 : Eq (lt (suc x1) (times (suc y1) (suc y1))) ?15

These last two goals come from the fact that we’ve added

(Eq (lt (suc x1) (times (suc y1)(suc y1))) b)

as an extra hypothesis – we must supply a proof of this hypothesis to get our original goal back. Fortunately, finding the appropriate b is easy – we can do it by reflexivity of equality:

Lego> Refine -0 Eq_refl;
Refine 16 by  Eq_refl
  ?13 : (Eq (lt (suc x1) (times (suc y1) (suc y1))) true)-><y:nat>
        and (Le (times y y) (suc x1)) (Lt (suc x1) (times (suc y) (suc y)))
  ?14 : (Eq (lt (suc x1) (times (suc y1) (suc y1))) false)-><y:nat>
        and (Le (times y y) (suc x1)) (Lt (suc x1) (times (suc y) (suc y)))

The Refine -0 means “work on the last goal”. Note this gets rid of goal ?15 as well.

Now we work on the first case, where suc x1 is still less than y1+1 squared. This fact appears as H:

Lego> intros;  (* case 1 -- (suc x1) < (suc y1) * (suc y1) *)
intros (1)
H : Eq (lt (suc x1) (times (suc y1) (suc y1))) true
?20 : nat
?21 : and (Le (times ?20 ?20) (suc x1))
          (Lt (suc x1) (times (suc ?20) (suc ?20)))

In this case, the result for suc x1 is the same as the result for x1:

Lego> Refine y1;
Refine by  y1
?21 : and (Le (times y1 y1) (suc x1))
          (Lt (suc x1) (times (suc y1) (suc y1)))

Now we must check that y1 meets the specification. The proof of the first part uses the inductive hypothesis and a lemma about Lt; the proof of the second uses the extra assumption H.

Lego> Refine pair;
Refine by  pair
?24 : Le (times y1 y1) (suc x1)
?25 : Lt (suc x1) (times (suc y1) (suc y1))
Lego> Refine Le_trans;
Refine by  Le_trans
?27 : nat
?29 : Le (times y1 y1) ?27
?30 : Le ?27 (suc x1)
?25 : Lt (suc x1) (times (suc y1) (suc y1))
Lego> Refine x1;
Refine by  x1
?29 : Le (times y1 y1) x1
?30 : Le x1 (suc x1)
?25 : Lt (suc x1) (times (suc y1) (suc y1))
Lego> Prf;
x1 : nat
x1_ih : <y:nat>and (Le (times y y) x1) (Lt x1 (times (suc y) (suc y)))
y1 = ... : nat
H : Eq (lt (suc x1) (times (suc y1) (suc y1))) true
?29 : Le (times y1 y1) x1
?30 : Le x1 (suc x1)
?25 : Lt (suc x1) (times (suc y1) (suc y1))
Lego> Refine fst x1_ih.2;
Refine by  fst x1_ih.2
?30 : Le x1 (suc x1)
?25 : Lt (suc x1) (times (suc y1) (suc y1))
Lego> Refine Le_suc;
Refine by  Le_suc
?25 : Lt (suc x1) (times (suc y1) (suc y1))
Lego> Refine lt_true_imp_Lt ? ? H;
Refine by  lt_true_imp_Lt (suc x1) (times (suc y1) (suc y1)) H
Discharge..  H
x1 : nat
x1_ih : <y:nat>and (Le (times y y) x1) (Lt x1 (times (suc y) (suc y)))

  y1 = ... : nat
  ?14 : (Eq (lt (suc x1) (times (suc y1) (suc y1))) false)-><y:nat>
        and (Le (times y y) (suc x1)) (Lt (suc x1) (times (suc y) (suc y)))
Lego> (* end of first case *)

The second case proceeds much like the first.

(* second case -- not (suc x1) < (suc y1) * (suc y1) *)
intros;
Lego> intros (1)
  H : Eq (lt (suc x1) (times (suc y1) (suc y1))) false
  ?37 : nat
  ?38 : and (Le (times ?37 ?37) (suc x1))
            (Lt (suc x1) (times (suc ?37) (suc ?37)))

In this case, the result for x1 is now too small, so it must be increased:

Lego> Refine (suc y1);
Refine by  suc y1
  ?38 : and (Le (times (suc y1) (suc y1)) (suc x1))
            (Lt (suc x1) (times (suc (suc y1)) (suc (suc y1))))
Lego> Refine pair;
Refine by  pair
  ?41 : Le (times (suc y1) (suc y1)) (suc x1)
  ?42 : Lt (suc x1) (times (suc (suc y1)) (suc (suc y1)))
Lego> Refine lt_false_imp_Le;
Refine by  lt_false_imp_Le
  ?45 : Eq (lt (suc x1) (times (suc y1) (suc y1))) false
  ?42 : Lt (suc x1) (times (suc (suc y1)) (suc (suc y1)))
Lego> Immed;
Immediate
  ?42 : Lt (suc x1) (times (suc (suc y1)) (suc (suc y1)))
Lego> Refine Lt_lemma;
Refine by  Lt_lemma
  ?48 : Lt x1 (times (suc y1) (suc y1))
Lego> Prf;
  x1 : nat
  x1_ih : <y:nat>and (Le (times y y) x1) (Lt x1 (times (suc y) (suc y)))
  y1 = ... : nat
  H : Eq (lt (suc x1) (times (suc y1) (suc y1))) false
  ?48 : Lt x1 (times (suc y1) (suc y1))
Lego> Refine snd x1_ih.2;
Refine by  snd x1_ih.2
Discharge..  H
Discharge..  y1 x1_ih x1
*** QED ***   (* time= 0.800000  gc= 0.030000  sys= 0.080000 *)

Three part exercise:

1. Meditate on the ways in which Π is a product type and the ways in which it is a function type.

2. Meditate on the ways in which Σ is a sum type and the ways in which it is a product type.

3. Decide to call them Π and Σ types.