Universes, Induction, Specifications

The source code for this module: PartI/Universes.ard, PartI/sort.ard
The source code for the exercises: PartI/UniversesEx.ard

In this module we take a closer look at the structure of the hierarchy of universes and explain how polymorphism works.

We discuss more advanced forms of induction and recursion: induction-recursion and recursion-recursion.

We conclude with remarks on writing specifications for functions.

Hierarchies of universes, polymorphism

As we mentioned earlier there is no actual type of all types in Arend. The type \Type behaves pretty much like the one, but not quite, and the difference is precisely that \Type cannot be used for contradictory circular definitions. This is so because \Type actually hides the hierarchy of universes \Type0, \Type1, … as we explain below.

The type \Type n, where the natural number n is called the predicative level of the universe, contains all types that do not refer to universes or refer to universes \Type i of lower predicative level i < n.

\func tt : \Type2 => \Type0 -> \Type1

In order to see how \Type works let us consider a definition parameterized by a type:

\func id (A : \Type) (a : A) => a

When \Type is written without an explicit level, it denotes the universe with the infinite predicative level, that is the universe that contains \Type n for every n. So the parameter A above ranges over this single infinite universe, which is convenient when we do not care about the level. Note that the infinite \Type is not itself a small type, hence it is not a member of any \Type n (in particular, not of itself); this is exactly what rules out contradictory circular definitions. For the same reason a definition such as \func bad : \Type => \Type is not allowed.

Thus id above is not polymorphic in the level. To make a definition genuinely polymorphic in the predicative level, we declare one or more named level parameters right after its name using the syntax .{...}, and refer to them in universes such as \Type l:

\func id.{l} (A : \Type l) (a : A) => a

Now id has a level parameter l and works uniformly for every predicative level. Level polymorphism is always explicit: a definition is polymorphic in the predicative level only if it declares a level parameter.

The level of a universe is one higher than the level of its elements: \Type l : \Type (\suc l), and n = \suc l is minimal such that \Type l : \Type n. So a function that returns the universe \Type l has result type \Type (\suc l):

\func type.{l} : \Type (\suc l) => \Type l

There are two operations that allow to form level expressions out of atomic ones: \suc l and \max l1 l2. Atomic level expressions are just nonnegative numerals and level parameters (such as l above). Therefore any level expression built from a single parameter l is either equivalent to a constant or to an expression of the form \max (l + c) c', where c, c' are constants and l + c is the c-fold \suc applied to l.

The level of a Pi-type or other type forming construction is the maximal level among all types contained in this construction:

\func test0.{l} : \Type (\max (\suc (\suc l)) 4) => \Type (\max l 3) -> \Type (\suc l)

We now illustrate the behaviour of universes and polymorphic definitions through a bunch of examples:

\func test1 => id Nat 0
\func test2 => id \Type0 Nat
\func test3 => id (\Type0 -> \Type1) (\lam X => X)
\func test4.{l} => id (\Pi (A : \Type l) -> A -> A) id

When invoking a definition it is possible to specify the values of its level parameters explicitly, again with the .{...} syntax. The arguments are level expressions, listed in the order in which the parameters were declared:

\func test5.{l} => id.{\suc l} (\Type l) Nat
\func test6 => id.{2} \Type1 \Type0

(The older ways of passing a level — positionally as an ordinary first argument, or via the \levels p h construct — no longer exist. Homotopy levels have been removed, so a level argument is now a single predicative level.)

In case a definition is invoked without explicit specification for the values of its levels, they will be inferred by the typechecker. In most cases there is no need to specify them explicitly.

The level of the universe of a data definition is the maximum among the levels of parameters of its constructors. Levels of parameters of the definition do not matter.

\data Magma.{l} (A : \Type l)
  | con (A -> A -> A)

\data MagmaEx.{l} (A : \Type l) (B : \Type5)
  | con (A -> A -> A)

\func test7.{l} : \Type l => MagmaEx.{l} Nat \Type4

The level of a class or a record is determined by its non-implemented fields and parameters (recall that parameters are just fields). For example, consider the definition of Magma as a class:

\class Magma.{l} (A : \Type l)
  | \infixl 6 ** : A -> A -> A

The level of Magma.{l} is \Type (\suc l) since the definition of Magma.{l} contains \Type l. Once the field A is implemented, that universe disappears from the non-implemented fields and the level drops by one: Magma.{l} Nat lives in \Type l (for instance Magma.{5} Nat : \Type5).

\func test8.{l} : \Type (\suc l) => Magma.{l}

\func test9.{l} : \Type l => Magma.{l} Nat

Consider one more example, the class Functor of functors. Unlike \Type, the universe \Set cannot be used with the infinite level, so it always requires an explicit predicative level:

\class Functor.{l} (F : \Set l -> \Set l) -- \Set is almost the same as \Type, we will discuss the difference later

  | fmap {A B : \Set l} : (A -> B) -> F A -> F B

The level of Functor.{l} will be \Type (\suc l) even if the field F is implemented since fmap also refers to \Set l.

\data Maybe.{l} (A : \Set l) | nothing | just A

\func test10.{l} : \Type (\suc l) => Functor.{l} Maybe

Exercise 1: Calculate the levels in each of the invocations of id'' below. Specify explicitly the result types for all idTest* (giving a result type also pins down the levels).

\func id''.{l} {A : \Type l} (a : A) => a

\func idTest1 => id'' (id'' id)
\func idTest2 => id'' Maybe
\func idTest3 => id'' Functor
\func idTest4 => id'' (Functor Maybe)
\func idTest5.{l} (f : \Pi {A B : \Set l} -> (A -> B) -> Maybe A -> Maybe B) => id'' (Functor Maybe f)

Induction principles

We have already seen that data types have canonical eliminators associated with them and that non-dependent and dependent eliminators correspond to recursion and induction principles respectively. It is also possible to define custom eliminators and, thus, custom induction principles that in some case are more convenient to use. For example, we can define an induction principle for natural numbers that allows to use induction hypothesis for any number less than the current one, not just for the number less by one:

\func Nat-ind (E : Nat -> \Type)
  (r : \Pi (n : Nat) -> (\Pi (k : Nat) -> T (k < n) -> E k) -> E n)
  (n : Nat) : E n => {?} -- prove this as an exercise

Exercise 2: Define div via Nat-ind.

\func div (n k : Nat) (p : T (0 < k)) : Nat => {?}

Exercise 3: Prove the following induction principle for lists:

\func List-ind
  {A : \Type}
  (E : List A -> \Type)
  (r : \Pi (xs : List A) -> (\Pi (ys : List A) -> T (length ys < length xs) -> E ys) -> E xs)
  (xs : List A) : E xs => {?}

Induction-recursion

Recursion-recursion – is a principle, allowing to define mutually recursive functions. For example, consider function isOdd and isEven:

\func isEven (n : Nat) : Bool
  | 0 => true
  | suc n => isOdd n

\func isOdd (n : Nat) : Bool
  | 0 => false
  | suc n => isEven n

Induction-induction – is a principle, allowing to define mutually recursive data types. In case a data type is a part of mutually inductive definition, its type must be specified explicitly. Consider the types IsOdd and IsEven:

\data IsEven (n : Nat) : \Type \with
  | 0 => zero-isEven
  | suc n => suc-isEven (IsOdd n)

\data IsOdd (n : Nat) : \Type \with
  | suc n => suc-isOdd (IsEven n)

Induction-recursion – is a principle, allowing to define data types and functions that are mutually recursive. For example, this construct allows to define universes of types as data types. We will explain how it can be done below.

Universes via induction-recursion

Let us define a custom universe containing some custom set of types:

\data Type
  | nat
  | list Type
  | arr Type Type

The type Type can be thought of as a type that contains codes of types. We should also define a function that realizes them as actual types:

\func El (t : Type) : \Set0 \elim t
  | nat => Nat
  | list t => List (El t)
  | arr t1 t2 => El t1 -> El t2

\func idc (t : Type) (x : El t) : El t => x

The universe Type contains just non-dependent types. If we want to include also dependent types to the universe, we should use induction-recursion:

\data Type' : \Set0
  | nat'
  | list' Type'
  | pi' (a : Type') (El' a -> Type')

\func El' (t : Type') : \Set0 \elim t
  | nat' => Nat
  | list' t => List (El' t)
  | pi' t1 t2 => \Pi (a : El' t1) -> El' (t2 a)

Completeness of specifications

Specification for an element of type A is simply a predicate P : A -> \Type, describing the property of an element that we want to prove.

A specification P is correct for a : A if P a is provable. A specification P is complete for a : A if P x implies x=a for all x : A.

For example, assume we want to write specification for a function fac : Nat -> Nat that computes the factorial of a number:

-- P1 is correct specification for 'fac', but incomplete.

\func P1 (f : Nat -> Nat) => f 3 = 6
-- P2 is complete, but not correct.

\func P2 (f : Nat -> Nat) => Empty
-- P3 -- correct and complete specification for 'fac'.

\func P3 (f : Nat -> Nat) => \Sigma (f 0 = 1) (\Pi (n : Nat) -> f (suc n) = suc n * f n)

Another example of a correct and complete specification for a sort function:

\func P (f : List A -> List A) => \Pi (xs : List A) -> \Sigma (isSorted (f xs)) (isPerm (f xs) xs)
-- where 'isSorted xs' is true iff  'xs' is sorted and

-- 'isPerm xs ys' is true iff 'xs' is a permutation of 'ys'.

Of course, specifications must always be correct, but one may opt for working with incomplete specifications since sometimes it is too hard to write and prove a complete one. Nevertheless, it is useful to understand, when a specification is complete. One useful necessary and sufficient condition of completeness for correct specifications can be formulated as follows:

\Pi (x y : A) -> P x -> P y -> x = y

Exercise 4: Implement function filter and prove that it is correct, that is that the following holds: a) filter p xs is a sublist of xs, b) All elements of filter p xs satisfy the predicate p, c) Any sublist of xs with property (b) is a sublist of filter p xs.

Correctness of Insertion Sort

We now finally prove the correctness of the insertion sort algorithm, defined in Indexed Data Types:

\func sort {A : TotalPreorder} (xs : List A) : List A
  | nil => nil
  | cons a xs => insert a (sort xs)
  \where
    \func insert {A : TotalPreorder} (a : A) (xs : List A) : List A \elim xs
      | nil => cons a nil
      | cons x xs => \case totality x a \with {
        | inl _ => cons x (insert a xs)
        | inr _ => cons a (cons x xs)
      }

The full specification of the sort function consists of two properties:

• sort xs is a sorted list.
• sort xs is a permutation of xs. We begin with the latter property. It can be defined in several different (but equivalent) ways. We will use an interesting option: instead of giving its definition from the start, we begin with an empty data type and add more constructors as needed:

\data Perm {A : \Type} (xs ys : List A)

Of course, the proof proceeds by induction on the list:

\func sort-perm {A : TotalPreorder} (xs : List A) : Perm xs (sort xs) \elim xs
  | nil => {?}
  | cons a l => {?}

In the first goal, we need to show that the empty list is a permutation of itself. To do this, we need to add the first constructor to Perm:

\data Perm {A : \Type} (xs ys : List A) \elim xs, ys
  | nil, nil => perm-nil

In the second goal, we need to show that cons a l is a permutation of insert a (sort l). Clearly, we need to use the induction hypothesis and we also need to prove some lemma about insert function. There is an obvious property of this function related to permutation:

\func insert-perm {A : TotalPreorder} (a : A) (xs : List A) : Perm (cons a xs) (sort.insert a xs) => {?}

This lemma implies that insert a (sort l) is a permutation of cons a (sort l). We can combine this property with the induction hypothesis to obtain the required result. To do this, we need to know the following facts:

• Permutations are closed under cons a so that we can conclude that cons a (sort l) is a permutation of cons a l,
• Perm is a transitive relation so that we can combine two proofs.

We add two new constructors to Perm which reflect these properties. At this point, our proof looks like this:

\data Perm {A : \Type} (xs ys : List A) \elim xs, ys
  | nil, nil => perm-nil
  | cons x xs, cons y ys => perm-cons (x = y) (Perm xs ys)
  | xs, ys => perm-trans {zs : List A} (Perm xs zs) (Perm zs ys)

\func sort-perm {A : TotalPreorder} (xs : List A) : Perm xs (sort xs) \elim xs
  | nil => perm-nil
  | cons a l => perm-trans (perm-cons idp (sort-perm l)) (insert-perm a (sort l))
  \where
    \func insert-perm {A : TotalPreorder} (a : A) (xs : List A) : Perm (cons a xs) (sort.insert a xs) => {?}

The proof of insert-perm also proceeds by induction on the list. The nil case is easy: we just need to show that cons a nil is a permutation of itself. In the cons case, we need to decide whether b <= a or a <= b. We can do this by using \case:

\func insert-perm {A : TotalPreorder} (a : A) (xs : List A) : Perm (cons a xs) (sort.insert a xs) \elim xs
  | nil => perm-cons idp perm-nil
  | cons b l => \case totality b a \as r \return
                                          Perm (cons a (cons b l)) (\case r \with {
                                            | inl _ => cons b (sort.insert a l)
                                            | inr _ => cons a (cons b l)
                                          }) \with {
    | inl b<=a => {?}
    | inr a<=b => {?}
  }

The second subgoal is easy: we need to prove that cons a (cons b l) is a permutation of itself. We can show that Perm is reflexive using constructors that we already added:

\func perm-refl {A : \Type} {xs : List A} : Perm xs xs \elim xs
  | nil => perm-nil
  | cons a l => perm-cons idp perm-refl

In the first subgoal, we need to prove that cons a (cons b l) is a permutation of cons b (insert a l). By the induction hypothesis and transitivity of Perm, we can reduce this problem to the problem of showing that cons a (cons b l) is a permutation of cons b (cons a l). To prove this, we need to add yet another constructor to Perm:

\data Perm {A : \Type} (xs ys : List A) \elim xs, ys
  | nil, nil => perm-nil
  | cons x xs, cons y ys => perm-cons (x = y) (Perm xs ys)
  | xs, ys => perm-trans {zs : List A} (Perm xs zs) (Perm zs ys)
  | cons x (cons x' xs), cons y (cons y' ys) => perm-perm (x = y') (x' = y) (xs = ys)

Now, we can finish the proof of insert-perm:

\func insert-perm {A : TotalPreorder} (a : A) (xs : List A) : Perm (cons a xs) (sort.insert a xs) \elim xs
  | nil => perm-cons idp perm-nil
  | cons b l => \case totality b a \as r \return
                                          Perm (cons a (cons b l)) (\case r \with {
                                            | inl _ => cons b (sort.insert a l)
                                            | inr _ => cons a (cons b l)
                                          }) \with {
    | inl b<=a => perm-trans (perm-perm idp idp idp) (perm-cons idp (insert-perm a l))
    | inr a<=b => perm-refl
  }

Our definition of Perm might look like cheating, but it is a perfectly valid definition of this predicate. It might happen that we already have some fixed definition Perm' of this predicate and we want to prove that our sort function satisfies the required property with respect to Perm'. In this case, we just need to prove that Perm xs ys implies Perm' xs ys. It is easy to do this: we just need to show that Perm' satisfies 4 properties corresponding to 4 constructors of Perm. We can even omit the intermediate step and replace Perm with Perm' and constructors of Perm with the proofs of corresponding properties.

Now, let us prove the remaining property of the sort function. We will define predicate IsSorted inductively. The empty list is always sorted and cons x xs is sorted if xs is sorted and x is less than or equal to the head of xs. The problem is that xs might be empty, in which case the last property does not make sense. We can consider three cases instead of two and define IsSorted as follows:

\data IsSorted {A : Preorder} (xs : List A) \with
  | nil => nil-sorted
  | cons _ nil => single-sorted
  | cons x (cons y _ \as xs) => cons-sorted (x <= y) (IsSorted xs)

It turns out that this definition is not very convenient because we need to consider more cases when proving things about sorted lists. There is another option: we can define the head that returns some default value when the list is empty:

\func head {A : \Type} (def : A) (xs : List A) : A \elim xs
  | nil => def
  | cons a _ => a

Now, we can define predicate IsSorted as follows:

\data IsSorted {A : Preorder} (xs : List A) \elim xs
  | nil => nil-sorted
  | cons x xs => cons-sorted (x <= head x xs) (IsSorted xs)

If xs is not empty, then condition x <= head x xs asserts that x is less than or equal to the head of xs. If xs is empty, then condition x <= head x xs is always true by reflexivity of <=.

The rest of the proof is straightforward. We formulate an obvious lemma about the insert function and prove the required property by induction:

\func sort-sorted {A : TotalPreorder} (xs : List A) : IsSorted (sort xs) \elim xs
  | nil => nil-sorted
  | cons a l => insert-sorted a (sort-sorted l)
  \where {
    \func insert-sorted {A : TotalPreorder} (x : A) {xs : List A} (xs-sorted : IsSorted xs) : IsSorted (sort.insert x xs) => {?}
  }

The proof of the lemma is also a straightforward induction:

\func insert-sorted {A : TotalPreorder} (x : A) {xs : List A} (xs-sorted : IsSorted xs) : IsSorted (sort.insert x xs) \elim xs
  | nil => cons-sorted <=-refl nil-sorted
  | cons a l => \case totality a x \as r \return
                                          IsSorted (\case r \with {
                                            | inl _ => cons a (sort.insert x l)
                                            | inr _ => cons x (cons a l)
                                          }) \with {
    | inl a<=x => \case xs-sorted \with {
      | cons-sorted a<=l l-sorted => cons-sorted (insert-lem a x l a<=x a<=l) (insert-sorted x l-sorted)
    }
    | inr x<=a => cons-sorted x<=a xs-sorted
  }

In the case inl a<=x, we need another auxiliary lemma with a simple proof by case analysis:

\func insert-lem {A : TotalPreorder} (a x : A) (l : List A) (a<=x : a <= x) (a<=l : a <= head a l) : a <= head a (sort.insert x l) \elim l
  | nil => a<=x
  | cons b l => \case totality b x \as r \return
                                          a <= head a (\case r \with {
                                            | inl _ => cons b (sort.insert x l)
                                            | inr _ => cons x (cons b l)
                                          }) \with {
    | inl _ => a<=l
    | inr _ => a<=x
  }

This completes the proof of correctness of sort. The full proof can be found here.

Exercise: Implement another sorting algorithm and prove its correctness.