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

Computation with recursion operators

There are two parts to understanding functions written with the recursion operators bool_rec, nat_rec, and list_rec: understanding how to define functions and understanding how they compute.

Functions are defined inductively. First, we must specify the value of the function at some base case or cases – zero for the type nat, nil t for list t, and true and false for bool. Then, we specify how to compute the value of a more complex element of the type, using the value of the function at a simpler element as well as information about how the complex element was constructed from the simpler element. Thus, the value of the function on suc i can depend on i and the value of the function on i, and the value of the function on cons hd tail can depend on hd, tail, and the value of the function on tail. Writing functions is a matter of working out how to express the value you want in this way.

Computing the value of a function proceeds by cases. If we are in the base case, we return the appropriate value, as specified. If we are evaluating the function at a complex element of the type, we unwind the definition once, so that the argument to the recursion form is now the simpler element of the type. We continue in this way, at each step obtaining a term in which the recursion operator is applied to smaller and smaller elements of the type, until we reach the base case.

Five plus two : an annotated example.

Recall the definition of plus:

                 plus = [i:nat][j:nat] nat rec i ([k:nat] suc) j

Also recall the rules for evaluating nat rec:

                  nat rec m f zero     => m
                  nat rec m f (suc i)  => f i (nat rec m f i)

Let us calculate plus five two. The names for numbers are abbreviations, so that two =

suc (suc zero).
plus five two
 = ([i:nat][j:nat] nat_rec i ([k:nat] suc) j) five two

First, we beta-reduce, substituting five for i:

 = ([j:nat] nat_rec five ([k:nat] suc) j) two

Then we beta-reduce again, substituting two for j (and eliminating the outermost set of parentheses):

 =  nat_rec five ([k:nat] suc) two

Now let us expand the definition of two (not a computation step, just for clarity). We will not need to expand the definition of five.

 =  nat_rec five ([k:nat] suc) (suc (suc zero))

Now we look at the rules for nat rec. The last argument is not zero, so the second rule applies. The three arguments are

m = five
f = ([k:nat] suc)
(suc i) = (suc (suc zero))

Hence i = (suc zero). Applying the rule, we have

 = ([k:nat] suc) (suc zero) (nat_rec five ([k:nat] suc) (suc zero))

We reduce the application ([k:nat] suc) (suc zero) by substituting suc zero for k in suc. Since k does not appear in suc, we are left with suc, giving the whole term as:

 = suc (nat_rec five ([k:nat] suc) (suc zero))

Again we look at the rules for nat rec. The last argument to nat_rec is still not zero, so the second rule applies again. The three arguments this time are

m = five
f = ([k:nat] suc)
(suc i) = (suc zero)

Hence i = zero. Applying the rule, we have

 = suc (([k:nat] suc) zero (nat_rec five ([k:nat] suc) zero))

Again, reducing ([k:nat] suc) zero leaves only suc:

 = suc (suc (nat_rec five ([k:nat] suc) zero))

Looking at the rules for nat_rec, we see that the first rule applies – the arguments to nat_rec are:

m = five
f = ([k:nat] suc)
zero

Thus we apply the first rule, replacing nat_rec five ([k:nat] suc) zero) with five:

 = suc (suc five)

So, plus five two is suc (suc five), or 7. Here are the steps again:

plus five two
 = ([i:nat][j:nat] nat_rec i ([k:nat] suc) j) five two
 = ([j:nat] nat_rec five ([k:nat] suc) j) two
 =  nat_rec five ([k:nat] suc) two
 =  nat_rec five ([k:nat] suc) (suc (suc zero))
 = ([k:nat] suc) (suc zero) (nat_rec five ([k:nat] suc) (suc zero))
 = suc (nat_rec five ([k:nat] suc) (suc zero))
 = suc (([k:nat] suc) zero (nat_rec five ([k:nat] suc) zero))
 = suc (suc (nat_rec five ([k:nat] suc) zero))
 = suc (suc five)

Equality

We have been working towards predicate logic, i.e. a way of forming propositions which depend on variables (of some kind). In Lego, a predicate on a type T is a function from T to Prop. Thus, a predicate depends on a variable in just the same way as a function depends on its argument. Predicate logic is used to describe logical properties of some domain, e.g. natural numbers. One such property (a particularly important one) is equality. Lego can be configured to use any one of several different notions of equality, but for now we’ll just be using the basic properties given in the rules below.

Rules for Equality

Equality is, like many other operations, implicitly quantified over types. (There is an explanation of implicit quantification at the end of today’s notes.) So, the type of Eq (the equality symbol) is {t|Type}t->t->Prop. This means that two objects of different types cannot be compared for equality.

The most fundamental property of equality is that it is an equivalence relation; that is, equality is reflexive, symmetric, and transitive. The axioms which specify this are:

Eq_refl: {t|Type}refl (Eq|t)
Eq_sym: {t|Type}sym (Eq|t)
Eq_trans: {t|Type}trans (Eq|t)

where refl, sym, and trans are defined for general relations R:T->T->Prop:

Lego> refl;
value of refl = [T|Type][R:T->T->Prop]{t:T}R t t
type  of refl = {T|Type}(T->T->Prop)->Prop
Lego> sym;
value of sym = [T|Type][R:T->T->Prop]{t,u|T}(R t u)->R u t
type  of sym = {T|Type}(T->T->Prop)->Prop
Lego> trans;
value of trans = [T|Type][R:T->T->Prop]{t,u,v|T}(R t u)->(R u v)->R t v
type  of trans = {T|Type}(T->T->Prop)->Prop

Written as rules, these are:

                             G, t:T ⊢ Eq refl:Eq t t
                      G,t:T,u:T ⊢ Eq sym:(Eq t u) ->Eq u t
              G,t:T,u:T,v:T ⊢ Eq trans:(Eq t u)->(Eq u v)->(Eq t v)

Two more axioms for equality are more easily understood as rules than as axioms. They describe the fact that predicates and functions must respect equality. The first actually says that if m and n are equal in type T, then P m implies P n for all P:

               \frac{G, m:T, n:T ⊢ M: (Eq m n)}{G, m:T, n:T ⊢ Eq subst M :\{P: T ->Type\}(P m) ->P n}

The second rule says that if a function is applied to equal inputs, the results must be equal (in the range type):

                        \frac{G ⊢ f:T->S   G ⊢ M:Eq t1 t2}{G ⊢ Eq resp f M :Eq (f t1) (f t2)}

Some examples

Here are some examples of proofs in Lego using these rules. The Lego file containing these examples is available from the lecture notes web page.

First we define the function bool_to_nat:

[bool_to_nat = bool_rec one zero];

This function returns one if applied to true and zero if applied to false. We can now check this formally:

Lego> Goal  Eq (bool_to_nat true) one;
Goal
  ?0 : Eq (bool_to_nat true) one
Lego> Refine Eq_refl;
Refine by  Eq_refl
*** QED ***

Refining by Eq_refl caused Lego to simplify the goal by evaluating (bool_to_nat true) to get one. Since Eq_refl proves Eq one one, the proof is finished.

Here is a proof using Eq_trans:

Lego> Goal  (and (Eq zero one) (Eq one two)) -> Eq zero two;
Goal
  ?0 : (and (Eq zero one) (Eq one two))->Eq zero two
Lego> intros H;
intros (1) H
  H : and (Eq zero one) (Eq one two)
  ?1 : Eq zero two
Lego> Refine Eq_trans;
Refine by  Eq_trans
  ?4 : nat
  ?6 : Eq|nat zero ?4
  ?7 : Eq|nat ?4 two

Lego prompts for the natural number used as an “intermediate step” in the link between zero and two. According to my assumptions, that link is the natural number one:

Lego> Refine one;
Refine by  one
  ?6 : Eq|nat zero one
  ?7 : Eq|nat one two

Now these are part of my assumptions:

Lego> Refine fst H;
Refine by  fst H
  ?7 : Eq|nat one two
Lego> Refine snd H;
Refine by  snd H
Discharge..  H
*** QED ***

A similar proof gives an example of Eq_sym. The goal is almost the same, but instead of Eq one two as part of my assumption, I have Eq two one:

Lego> Goal  (and (Eq zero one) (Eq two one)) -> Eq zero two;
Goal
  ?0 : (and (Eq zero one) (Eq two one))->Eq zero two
Lego> intros H;
intros (1) H
  H : and (Eq zero one) (Eq two one)
  ?1 : Eq zero two
Lego> Refine Eq_trans;
Refine by  Eq_trans
  ?4 : nat
  ?6 : Eq|nat zero ?4
  ?7 : Eq|nat ?4 two

Lego> Refine one;
Refine by  one
  ?6 : Eq|nat zero one
  ?7 : Eq|nat one two
Lego> Refine fst H;
Refine by  fst H
  ?7 : Eq|nat one two

I have Eq two one as part of my assumption – what I want to do is apply Eq_sym to this to get

Eq one two:
Lego> Refine Eq_sym (snd H);
Refine by  Eq_sym (snd H)
Discharge..  H
*** QED ***

Finally, an illustration of Eq_resp:

Lego> Goal  (Eq true false) -> Eq one zero;
Goal
  ?0 : (Eq true false)->Eq one zero
Lego> intros H;
intros (1) H
  H : Eq true false
  ?1 : Eq one zero

Since bool_to_nat takes true and false to one and zero respectively, we use it as an argument

to Eq_resp:
Lego> Refine Eq_resp bool_to_nat H;
Refine by  Eq_resp bool_to_nat H
Discharge..  H
*** QED ***

Implicit syntax for quantification

In many cases where something is quantified over types, the appropriate type instance can be deduced from the types of the arguments. For example, although the recursion forms for defining functions over booleans, etc. are parametrized by a type variable, the instantiation of this variable can be inferred from the types of the arguments. So, Lego can deduce that the function definition [b:bool]bool_rec zero one b uses an instance of bool_rec where the type variable is replaced by nat, since the first argument has type nat.

All of the recursion forms have this property. Their types are

bool_rec : {t|Type}t->t->bool->t
nat_rec :  {t|Type}t->(nat->t->t)->nat->t
list_rec : {s,t|Type}t->(s->(list s)->t->t)->(list s)->t

Equality proof terms also use implicit quantification, not only over types but also over terms. For example, the type of Eq_sym simplifies to:

{T|Type}{t,u|T}(Eq|T t u)->Eq|T u t

As well as the type T, the terms t and u of type T are implicit.

As mentioned last time, a term f of type {t|T}A is like one of type {t:T}A, except that the argument t need not be given explicitly when f is used. For example, if you have a goal Eq a b and an assumption x : Eq b a, you need only say Refine Eq_sym x rather than providing all the arguments, as Refine Eq_sym T a b x – Lego will work out that t should be a and u should be b.

Sometimes, however, Lego will be unable to tell what an implicit argument was meant to be. In this case, an implicit argument may given explicitly by using a special application operator, also denoted |. This is why we see Eq|T in the type of Eq_sym above.

As another example, consider these two versions of the polymorphic identity function:

Id_imp = [t|Type][a:t]a : {t|Type}t->t
Id_exp = [t:Type][a:t]a : {t:Type}t->t

The first version is implicitly parameterized by t, the second is explicitly parameterized. The first does not generally need to be given a type argument, so that we have

Id_imp zero : nat

However, Id_exp zero gives an error, because zero is not a type. To apply Id_exp to zero, we must supply the type nat explicitly:

Id_exp nat zero : nat

Sometimes a formula has been implicitly quantified but Lego is not able to determine what all of the types should be. This happened with the example at the end of lecture notes three, with the command Refine snd;, and it often happens when using Eq_trans – the “middle formula” (u in the rules above) will need to be supplied. In such cases, Lego will ask for the formula or type by generating new goals. If you want to provide an implicit argument explicitly, the application is denoted | also, so that, for example:

Id_imp|nat = Id_exp nat.