Blatt 4 —- More on Coq tactics and Prop

SemProg SoSe 2013, Set 4

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 the noon of Fri 24. However, you are strongly encouraged to do the exercise before the Wed lecture The file consists of 7 obligatory exercises, yielding 40 points altogether and one bonus exercise, which yields 10 additional points for those willing. Just like the previous sheets, this one is mostly binary—-either you did an exercise or did not—-but this time I reserve the right for occasionally deducing a stylistic point or so, e.g., for blatant violations of instructions and suggestions (I might look the other way if these violations resulted in an improved proof, of course. :-)

The first two exercises are leftovers from More About Coq lecture

Exercise 1: 7.5 points (bool_fn_applied_thrice)

Complete the following proof. You will need a lot of subcases, lots of destruction, but occasionally also you'll need to remember a thing or two.

☐

Exercise 2: 7.5 points (filter_exercise)

This nice exercise tests several elements from the More about Coq lecture. You will need to:

• think about your generality of the statement you want to prove by induction
• remember some of the things you want to destruct

☐

Now moving on to Prop..

Exercise 3: 2.5 points (oddI_oddC)

During the lecture, we provided two definitions of evenness, a computational and inductive one...

• Do the same thing for being odd: provide an inductive definition oddI and a computational one oddC, the latter using the boolean testing function
• Prove a theorem oddI_oddC which states the inductive definition implies the computational one.
• Not a part of the exercise: If you have time, try to show for yourself the converse direction. Can you do it without cheating, i.e., without using things we have not discussed during the lecture so far? What goes wrong? This is an excellent warm-up before the logic lecture

Exercise 4: 2.5 points (double_even)

*Recall we defined a function double on natural numbers which doubles its argument. Construct a tactic proof of the following proposition.

☐

Exercise block: CURTAIN NUMBERS

Durign the lecture, we defined a property of numbers which we misleadingly called beautiful (or gorgeous). In fact, it was neither beautiful nor gorgeous: it was stupid and uninteresting. Here a more entertaining one: If you were ever hanging curtains on old-fashioned curtain clips (I don't mean shower curtains), you know how it is done. First, you clip on both ends. Then you clip in the middle. The picture is like this: v___v___v if you have only 3 clips (the smallest curtain number) Then you do the procedure recursively, depending on the number of clips left: you clip in the middle of each interval: v_v_v_v_v (5 clips) ...and then again in the middle of each interval... vvvvvvvvv (9 clips) ... and so on, as long as you have the right number of clips to do the next step... We have determined that 3, 5 and 9 are "curtain numbers" and no other number smaller than 10 is. Can you guess further elements of the sequnce? If n is a curtain number, how do we define the next curtain number using n?

Exercise 5: 5 points (curtain)

Define inductively the curtain : nat -> Prop property. A function that you might fight useful for this appeared in an exercise above in this Blatt. Note that one of natural ways to do it—-using predecessor or restricted substraction—-is not necessarily a good one. You can try to prove some of theorems below using such a definition to see why it would be more difficult to work with.

Exercise 6: 2.5 points (nine_is_curtain)

Prove

Exercise 7: 5 points (curtain_is_odd)

Prove Note that for this purpose, you might find useful:

• formulating and proving a simple lemma on the relationship between the inductive definitions of being even and being odd
• a theorem proved in one of earlier exercises.

Just for comparision: from 8 on, every number is "beautiful" or "gorgeous". Try to prove it in Coq (it is not a part of this Blatt and not scored at all!). Can you do it with our toolbox so fax? Are we missing something?

Exercise 7: 7.5 points (seven_is_not_curtain)

This exercise is another good warm-up before the logic lecture. Rather than using bool and logical operators we'll see the next time, we can prove that a proposition does not hold in an alternative way. In this case, say we want to prove 7 is not a curtain number. Prove The best proof I was able to come up with seems slightly verbose: maybe you'll be able to improve on it? You can prove for yourself analogous theorem about gorgeous or beautiful. The proof should be simpler in this case. Note that in case of these properties, 7 is the largest number from which you would be able to reach a contradiction. On the other case, the proof you obtain in this exercise should not be difficult to extend to show that 11 is not a curtain number either. This is the end of obligatory exercises

Bonusaufgabe

Bonus exercise: 10 points (subsequence)

A list is a subsequence of another list if all of the elements in the first list occur in the same order in the second list, possibly with some extra elements in between. For example, 1,2,3 is a subsequence of each of the lists 1,2,3 1,1,1,2,2,3 1,2,7,3 5,6,1,9,9,2,7,3,8 but it is not a subsequence of any of the lists 1,2 1,3 5,6,2,1,7,3,8

• Define an inductive proposition subseq on list X that captures what it means to be a subsequence. (Hint: You'll need three cases.)
• Prove that subsequence is reflexive, that is, any list is a subsequence of itself.
• Prove that for any lists l1, l2 and l, if l1 is a subsequence of l2, then l ++ l1 is also a subsequence of l ++ l2 (you'll need just one of your constructors for it).
• Prove that for any lists l1, l2 and l, if l1 is a subsequence of l2, then l1 is also a subsequence of l ++ l2 (again, you'll need just one of your constructors for it, but other than in the previous item).
• Prove that for any lists l1, l2, l3 and l4, if l1 is a subsequence of l2 and l3 is a subsequence of l4, then l1 ++ l3 is also a subsequence of l2 ++ l4
• (Optional—-this means optional even for Bonusaufgabe! You don't have to do it even to get full bonus points, but if you have too much energy left in the week of Bergkirchweih... Prove that subsequence is transitive — that is, if l1 is a subsequence of l2 and l2 is a subsequence of l3, then l1 is a subsequence of l3. Hint: choose your induction carefully, both the level of generality and the thing you are actually doing the induction on!