## Description

In this assignment, you will assemble a few automatically verifiable inductive proofs about

pure functional code. All your solutions should be defined within a file named foldfiles.pf.

File names are case sensitive.

You will need to obtain the Haskell source files for the ibis lightweight proof verifier. Once

this is done, you can verify a proof script using a Haskell interpreter by loading the Main

module into the interpreter and evaluating:

ibis “filepath/filename.pf”

where filepath/filename.pf is a relative path from the location of the source files. If you

choose to compile the verifier using the provided Makefile, you can run it from the command

line using the same syntax as above.

Problem 1. (50 pts)

Suppose you have a large collection of files spread across many computers. Each computer

has its own processor and can run its own instance of a Haskell interpreter. You need to

produce an aggregate analysis of all the files as defined by a Haskell function called agg. In

other words, for all the files across all the computers, you must compute

f1 ‘agg‘ f2 ‘agg‘ … ‘agg‘ fN

You do not know anything about the function’s implementation, but you do know that there

is a Haskell value id that acts as both a left and right identity for the function agg, and agg

itself is associative. All this information is summarized in the following proof script.

Introduce agg, id.

Assume \forall f. f ‘agg‘ id = f

Assume \forall f. id ‘agg‘ f = f

Assume \forall f,g,h. f ‘agg‘ (g ‘agg‘ h) = (f ‘agg‘ g) ‘agg‘ h

1

You decide that the best way to accomplish this task is to perform a foldr over all the files.

However, you plan to distribute the workload over all the machines and then combine the

results at the end. You observe that this will be equivalent to folding over all the files on a

single machine only if for any pair of file lists xs and ys, it is the case that

foldr agg id (xs ++ ys) = (foldr agg id xs) ‘agg‘ (foldr agg id ys)

Thus, it is necessary to prove that this equation holds.

(a) A Haskell definition for foldr is provided below.

foldr f b (x:xs) = f x (foldr f b xs)

foldr f b [] = b

Add appropriate assumptions to the proof script that mathematically represent the

equations that constitute the definition of foldr.

(b) A Haskell definition for the list “append” operator is provided below.

(x:xs) ++ ys = x:(xs ++ ys)

[] ++ ys = ys

Add appropriate assumptions to the proof script that mathematically represent the

equations that constitute this definition.

Now that all the assumptions describing the circumstances have been added to the proof

script, it is possible to construct a proof of the desired mathematical statement. Because

the statement is quantified universally over two lists, the proof must proceed by induction.

In order to receive full credit, your solutions must contain no new assumptions and only

automatically verifiable assertions.

(c) First, the statement must be shown to hold in the base case for an empty list. Add

to your proof script and complete the following proof of the base case by replacing

… with an appropriate sequence of true statements, separated by the conjunction

operator.

Assert \forall ys.

…

/\ (foldr agg id []) ‘agg‘ (foldr agg id ys) = foldr agg id ([] ++ ys)

(d) Next, it remains to prove that the statement holds for any recursive case. It is sufficient

to show that given an inductive hypothesis about some list xs, it is possible to derive

the same statement for a list x:xs. Complete the following proof of the inductive case.

Assert \forall x,xs,ys.

(foldr agg id xs) ‘agg‘ (foldr agg id ys) = foldr agg id (xs ++ ys)

=> …

/\ (foldr agg id (x:xs)) ‘agg‘ (foldr agg id ys) = foldr agg id ((x:xs) ++ ys)

2

Problem 2. (50 pts)

As before, solutions that can receive full credit must contain no new assumptions and only

automatically verifiable assertions.

(a) Suppose you also want to prove that [] is a right identity for ++. That is, for any xs,

xs ++ [] = xs

Add two assertions to your proof script that correspond to a proof of this statement.

The first should be the base case, in which xs is []. The second should be the inductive

case, in which you assume that the statement holds for some xs and derive that it holds

for some x:xs:

Assert \forall x,xs.

xs ++ [] = xs

=> …

/\ (x:xs) ++ [] = x:xs

(b) Suppose we want to show that ++ is associative. This means that for any lists xs, ys,

and zs, it is the case that

(xs ++ ys) ++ zs = xs ++ (ys ++ zs)

Any case in which ys = [] or zs = [] is trivial, since [] is both a left and right identity

of ++. Thus, it is sufficient to prove that this holds for any xs by induction over the

structure of xs. Assemble two assertions that correspond to the base and inductive

cases of a proof of this statement. You must use an approach that is analogous to the

two previous proofs. You may not introduce any additional assumptions.

3