Blatt 6 —- Properties and Specifications

SemProg SoSe 2013, Set 6

Based on the material of the online course "Software Foundations" by Pierce et al. Submit your solutions to tadeusz.m.litak at cs.fau.de Please submit by Jun 9, anywhere on earth. However, you are strongly encouraged to do the exercise before the Wed lecture, even if additional bonus points for this have been entirely abolished. The file consists of 7 obligatory exercises, yielding 45 points altogether and one bonus exercise, which yields 10 additional points for those willing.

Exercise block: decidable equality

Our previous exercise Blatt hopefully drove home the message that the law of excluded middle and other classical tautologies are not available for free in Coq. However, for equality propositions the situation often looks better. Here is how we can define types with decidable equality in Coq.

From earlier chapters we also remember boolean equality for natural numbers beq_nat. Let us say that a type has boolean equality in such a situation.

Boolean equality should naturally imply decidable equality. Furthermore, our good friends like booleans and natsallow obvious boolean equality functions. This is an easy warm-up exercise.

Exercise 1: 5 points (natBooEq, booBooEq, Bool_Decid)

One would think that the converse implication will also be a piece of cake, i.e., decidable equality should yield a straightforward equality function: Try to uncomment this definition. What is the error message that you get? Why?

Exercise 2: 7.5 point (listDecEq, listBooEq)

Types with boolean/decidable equality can be used to construct new ones. The most obvious way of doing so is provided by lists.

To do the same with boolean equality, we first need to define a helper function.

<- FILL THIS IN SO THAT YOU CAN PROVE

How about other types? Can you think of any candidates for boolean/decidable equality for:

• functions nat -> nat
• real numbers (however you want to implement them in Coq)
• Prop itself?

Exercise block: specifications for lists

Exercise 3: 5 points (good_subseq_extend, maximal_strengthening)

For a warm-up, let us finish what we began at the beginning of PropRelInd lecture. Here are our definitions again.

A "good subsequence" for a given list l and a test is a subsequence of l all of whose members evaluate to true under the test.

Why, prove now the results we just stated w/o proof during the lecture...

Exercise 4: 7.5 points (forallb_matches_spec)

Let us try something more interesting. We can write down a specification for forallb using property all. Your job is to prove it works.

Exercise 5: 7.5 points (repeatslog_equivalent_repeatsind)

The following inductively defined proposition...

...gives us a precise way of saying that a value a appears at least once as a member of a list l. Here are a few warm-ups about appears_in.

We can use this property to definite inductively what it means that a list contains repeated occurrences of some element(s).

However, there is an obvious alternative definition...

In fact, this definition is a good excuse to define our first nontrivial tactical. Do you understand what it does?

You will most likely find it quite helpful in the proof that the two definitions are equivalent:

As this is an equivalence, you may of course prove first each of directions in separate lemmas.

Evaluating and optimizing polymorphic string expressions.

Exercise 6: 7.5 points (optimizetrim_sound)

Here is a definition of abstract syntax trees for (polymorphic) string expressions.

removal of the first char of the string, i.e., "trimming" the front Define functions evaluting these string expressions to lists.

<- FILL THIS IN! See many examples below if you want to double-check how exactly this function should be defined. Of course, there is a lot of redundancy in our expressions. Here is a function which tries to remove at least some. Do you understand what it does?

Just to double-check we understand what is going on there... a few examples with the intended output.

[ [1, 2, 1] : list nat ]

Now we can prove a theorem that our optimization is indeed correct:

Of course, tacticals can be used to make the proof this theorem much shorter and you are well advised to try some mentioned at the end of the Wed lecture. With a clever use of these, you should not need more than 6-7 lines... okay, maybe a bit longish lines.

Explicit Proof Objects for Induction and Improved Proofs

Exercise 7: 5 points (gorgeous_is_trivial')

This bit has not been explained in too much detail during the PropRelInd lecture... Hopefully the exercise will make up for it. Although tactic-based proofs are normally much easier to work with, the ability to write a proof term directly is sometimes very handy, particularly when we want Coq to do something slightly non-standard. Recall the induction principle on naturals that Coq generates for us automatically from the Inductive declation for nat.

There's nothing magic about this induction lemma: it's just another Coq lemma that requires a proof. Coq generates the proof automatically too...

We can read this as follows: Suppose we have evidence f that P holds on 0, and evidence f0 that forall n:nat, P n -> P (S n). Then we can prove that P holds of an arbitrary nat n via a recursive function F (here defined using the expression form Fix rather than by a top-level Fixpoint declaration). F pattern matches on n:

• If it finds 0, F uses f to show that P n holds.
• If it finds S n0, F applies itself recursively on n0 to obtain evidence that P n0 holds; then it applies f0 on that evidence to show that P (S n) holds.

F is just an ordinary recursive function that happens to operate on evidence in Prop rather than on terms in Set. Those interested in functional programming may notice that the match in F requires an annotation as n0 return (P n0) to help Coq's typechecker realize that the two arms of the match actually return the same type (namely P n). This is essentially like matching over a GADT (generalized algebraic datatype) in Haskell. In fact, F has a dependent type: its result type depends on its argument; GADT's can be used to describe simple dependent types like this. We can adapt this approach to proving nat_ind to help prove non-standard induction principles too. Recall our desire to prove that forall n : nat, even n -> ev n. Attempts to do this by standard induction on n fail, because the induction principle only lets us proceed when we can prove that even n -> even (S n) — which is of course never provable. What we did earlier in this chapter was a bit of a hack: Theorem even__ev : forall n : nat, (even n -> ev n) /\ (even (S n) -> ev (S n)). We can make a much better proof by defining and proving a non-standard induction principle that goes "by twos":

Once you get the hang of it, it is entirely straightforward to give an explicit proof term for induction principles like this. Proving this as a lemma using tactics is much less intuitive (try it!). The induction ... using tactic gives a convenient way to specify a non-standard induction principle like this.

Now, recall that in the previous Blatt we used a similar hack to show near-triviality of gorgeousness. Naturally, we can then hope to fix it in a similar way: defining an induction principle that goes "by three".

<- FILL THIS IN! Prove a similarly improved theorem using the new induction principle.

This is the end of obligatory exercises.

BONUSAUFGABE (10 points)

Still not fed up with proving properties and specifications of lists? Well, here is something more. Use appears_in to define an inductive proposition no_repeats X l, which should be provable exactly when l is a list (with elements of type X) where every member is different from every other. For example, no_repeats nat [1,2,3,4] and no_repeats bool [] should be provable, while no_repeats nat [1,2,1] and no_repeats bool [true,true] should not be.

<- Fill this in!

Here is one more natural notion:

Now prove the following theorem relating disjoint, no_repeats and ++.