Computer Aided Formal Reasoning Fall, 1995 Lecture notes 2 Rod Burstall and Judith Underwood

Reminder: The first exercise is due on 27 October – it can be found in:

http://www.dcs.ed.ac.uk/generated/package-links/lego/html/CAFR/programming.html

Refinement: deriving a program from a type

One difficulty with using recursion operators for programming is keeping track of what arguments you need to supply, since the functions involved often have more arguments than are used. This is essentially a matter of making sure that the arguments to the recursion operators all have the right types. To help us do this, we can derive the program top-down and use LEGO to keep track of what we have left to do.

For example, consider a program for testing whether one number is less than or equal to another.

An informal definition of i ≤ j is

    0 ≤ j          =  true
    suc i ≤ 0      =  false
    suc i ≤ suc j  =  i ≤ j

We can rewrite this as a function leq:

    leq 0 j              =  true
    leq (suc i) 0        =  false
    leq (suc i) (suc j)  =  leq i j

   The type of leq is nat ->nat ->bool.

Notice that this definition really involves two inductions, one on i and one on j. We can separate these by thinking of the induction on i as defining a function of type nat ->bool, such that the inductive case of this definition involves another induction on j.

We will now derive the program starting from the type, a process called “refinement”. We use the typing rules “upside down” to get a term of the desired type, by generating successive subgoals. The goal and subgoal types are in bold. The first step uses nat elimination (which is induction on nat). See below for further commentary.

Example leq Goal leq : nat ->nat ->bool nat rec (* define (leq i), of type nat ->bool, by induction on i *)

nat ->bool (* the leq zero function *)

[j0:nat] true (* leq 0 j = true *)

nat ->(nat ->bool) ->nat ->bool (* case for i= suc i1 – given i1, and leq i1, return leq i *) [i1:nat][leq i1]

nat ->bool (* define leq i by induction on its argument j *) nat rec

bool (* case for j=0 *)

false (* leq (suc i1) 0 = false *)

nat ->bool ->bool (* case for j=suc j1 –given j1, and leq i j1, return leq i j *) [j1:nat][leq i j1 : bool] bool (* i = suc i1, j = suc j1, so *) leq i1 j1 (* leq i j = leq i1 j1 *)

The non-bold entries give us the program. Here is the explanation. We want a function of type nat ->nat ->bool. We break this into two parts. We begin by thinking of a function from nat to nat ->bool, and then defining the nat ->bool portion as another function. The function from nat to nat ->bool is the function which, given i, returns a function (which we will call leq i) which is essentially [x:nat] leq i x, i.e. the function which returns true if i is less than or equal to its argument, and false otherwise. If i is zero, then leq i is the constant true function. Otherwise, if i=suc(i1),then leq i is defined by induction on its argument, using the value of the function leq i1.

Exercise: Annotate this derivation by saying what typing rule is used (backwards) at each step. “Refine” in Lego does something like this – given a term and a current goal type, it applies the typing rule for that term backwards to determine what hypotheses need to be satisfied in order to give the term that type. It’s actually more complicated than that – we’ll discuss refinement in more detail in a future lecture.

Exercise: Try a similar derivation for nat eq, the equality on nat.

Example: Summing the elements in a list, assuming plus: nat ->nat ->nat . Goal sum list:list nat ->nat [l:list nat]

nat

list rec nat zero list nat ->nat ->nat ->nat [k: list nat] [i: nat] [j: nat]

nat plus i j

list nat

l

Here i is the next element and j is the running total. The final program is

sumlist = list rec zero ([k: list nat] [i: nat] [j: nat plus i j]) l

Exercise: Annotate this derivation with comments describing the desired terms of each type.

Exercise: Derive the factorial function.

Exercise: Derive a function for appending two lists.

Exercise* means a harder / longer exercise

Exercise*: Derive a version of the unix command grep which tells you which lines of a file contain a given string. The function you derive should be a sort of list grep – it should determine which elements of a list of lists of nat contain a given list of nat, and return them in a list.

Thus the type of your function will be:

                grep: list nat ->list(list nat) ->list (list nat)

You will need some sub-functions.

Informally, for example

grep 23 (123 143 2233) = (123 2233)

and in formal notation grep((cons (two (cons three (nil nat))))

(cons ( cons (one (cons (two (cons three (nil nat))))))

(cons ( cons (one (cons (four (cons three (nil nat))))))

(cons (cons (two (cons (two (cons three (cons three (nil nat)))))))

(nil(list nat))))) )

=

(cons ( cons (one (cons (two (cons three (nil nat))))))

(cons ( cons (one (cons (four (cons three (nil nat))))))

(cons ( cons (two (cons (two (cons three (cons three (nil nat))))))) (nil(list nat)))) )

(give or take a few parentheses!) assuming one= suc(zero) and so on (as defined in the Lego library).

Running exercises in Lego

You can evaluate your functions in Lego, and you can derive them by refinement. The only two commands you will need for now are Refine and Intros.

To start a derivation, type Goal term:type, eg Goal leq: nat ->nat ->bool. When you type this to Lego, you get the response:

Lego> Goal leq:nat -> nat -> bool;
Goal
  ?0 : nat->nat->bool

The ?0 identifies the first goal, which is to produce a term of type nat ->nat ->bool. (If you’re familiar with logic programming, you can think of ?0 as a logical variable, standing for the term we want, which will be filled in as we go. Otherwise, just think of it as a label.) We want to define this term using nat rec, so we now type Refine nat rec;:

Lego> Refine nat_rec;
Refine by  nat_rec
  ?2 : nat->bool
  ?3 : nat->(nat->bool)->nat->bool

Lego has determined that if you provide something of type nat ->bool and something of type nat ->(nat ->bool) ->nat ->bool, then by putting them together using nat rec you will have satisfied your original goal (?0) of nat ->nat ->bool. Now we start to work on the first new goal, ?2. We want this to be the constant true function, so we introduce a name for the argument to the function :

Lego> Intros j0;
Intros (1)
  j0 : nat
  ?4 : bool

and now we fill in the bool with true

Lego> Refine true;
Refine by  true
Discharge..  j0
  ?3 : nat->(nat->bool)->nat->bool

The Discharge j0 indicates that Lego has unwound the derivation back to just before we introduced j0, since we have satisfied the goal we were working on then. Now we go to work on the new goal by introducing names for the first two arguments to the function:

Lego> Intros i1 leq_i1;
Intros (2) i1 leq_i1
  i1 : nat
  leq_i1 : nat->bool
  ?5 : nat->bool

and so on.

Exercise: finish this derivation in Lego. You should end up with Lego saying

*** QED ***

You can then save your proof:

Lego> Save;
"leq"  saved as global

and look at the resulting term:

Lego> leq;
value of leq = nat_rec ([_:nat]true) ([_:nat][leq_i1:nat->bool]nat_rec false
([j1:nat][_:bool]leq_i1 j1))
type  of leq = nat->nat->bool

Note that the variables which weren’t actually used have been replaced by dummy variables in the form of underscores ( ) in their lambda abstractions.

You can derive many of the functions we’ve looked at using only Refine and Intros. If you look at the LEGO reference card, you will see that there are many forms of intros/Intros, but they are all described as “Π introduction”. Π is a more general kind of function type which includes not only functions from, say, nat to nat, but also functions which take types as arguments and returns an argument which depends on that type , such as a function which, given T, returns the empty list of type list T, (nil T). In LEGO’s notation for Π types, the type of functions from nat to nat could be written { :nat}nat (which LEGO automatically simplifies to nat ->nat). The type of the second function would be { T: Type }list T, and the function itself would be [T:Type]nil T . This kind of parameterization by type is a very powerful tool – we’ll have a more formal introduction to Π types next week.

Lego is not a programming language; it is a proof language. So it evaluates very very slowly. Probably the grep example above will take forever (the fact that numbers are defined as successors of zero doesn’t help matters much). But evaluating (“normalising”) plus two two will give suc(suc(suc(suc zero))) fairly quickly. For proofs it is rather efficient.