LARA

In this third lab, you will be considering properties that Stainless is not able to prove on its own and may require certain hints. You will therefore be using Welder, a proof engine that lets you manually construct and manipulate theorems in order to prove more complex properties.

You are given 2 weeks for this assignment.

Deadline: Monday, Mar. 27, 23:59.

Send your solutions by mail to nicolas.voirol@epfl.ch.

Download the zip file: labs03.zip

The archive consists of the following files:

• build.sbt
• src/main/scala/FoldLeftRight.scala
• src/main/scala/FoldContent.scala
• src/main/scala/Main.scala

The FoldLeftRight.scala file corresponds to Exercise 1 and FoldContent.scala corresponds to Exercise 2. The provided main simply tests whether your solutions are valid and prints out a successful message if this is the case.

You can compile and run the project by using sbt compile and sbt run. Note that the first call to sbt compile may be quite slow as it will need to download and compile welder.

To get an idea of what welder is and how it works, you should start by reading the Tutorial. It can also be useful to consider the following example ListAndTrees.scala to get an idea of how more complicated proofs can be constructed.

Lab 03 Solutions

In this first exercise, we will start with a *simpler* theorem. We will be showing that in a monoid (z,f), left and right folds starting with the zero element z produce identical results.

In other words, ∀z,f,l. isMonoid(z, f) ⇒ (foldl(f, z, l) = foldr(f, z, l)).

Fill in the values/functions annotated with TODO in the file located at src/main/scala/FoldLeftRight.scala in the provided zip.

You can check your solution by issuing the sbt run command in the project's root directory and checking for the output:

“The fold left-right correspondance theorem has been proved!”

In this second exercise, you will construct a slightly more complicated proof. We will show that given a function f that is associative, commutative and idempotent, the result of folding over two lists l1 and l2 are identical if the lists have same content.

In other words, ∀z,f,l1,l2. (isAssociative(f) && isCommutative(f) && isIdempotent(f) && content(l1) = content(l2)) ⇒ (fold(f, z, l1) = fold(f, z, l2)).

We assume associativity and commutativity to be well known (see Associativity and Commutativity for a refresher), but let us consider idempotence. For a binary function f, we say f is idempotent iff for all x,y we have f(x, y) = f(x, f(x, y)). This is the case, for example, of the max function defined on two values.

Fill in the values/functions annotated with TODO in the file located at src/main/scala/FoldContent.scala in the provided zip.

You can check your solution by issuing the sbt run command in the project's root directory and checking for the output:

“The fold with equal content correspondance theorem has been proved!”

Hint: it may be useful to introduce an auxiliary lemma that talks about the result of folding over certain interesting reorderings of a list. You may also need some extra function definitions in this lemma. Don't forget to add any new function definition to the symbols!