Additional Exercises

Nostutter

Formulating inductive definitions of properties is an important skill that you will need in this course. Try to solve this exercise without any help.

We say that a list "stutters" if it repeats the same element consecutively. The property "Nostutter my_list" means that my_list does not stutter. Formulate an inductive definition for Nostutter. (This is different from the NoDup property in the exercise below; the sequence [1,4,1] repeats but does not stutter.)

type Nostutter <t> (l: List t) {
  RemoveMe : Nostutter []
}

Make sure each of these tests passes, but feel free to change the suggested proof (in comments) if it does not work for you. Your definition may be different from ours and still be correct; in that case, the examples may need a different proof. (You will notice that the suggested proofs use various tactics we have not discussed to make them more robust against the different possible ways of defining Nostutter. You can probably just uncomment them and use them as is, but you can also prove each example with more basic tactics.)

Test_nostutter_1 : Nostutter [3n,1n,4n,1n,5n,6n]
Test_nostutter_1 = ?
// Prova. repita o construtor; aplique beq_nat_false_iff; auto.

Test_nostutter_2 : Nostutter []
Test_nostutter_2 = ?
// Prova. repita o construtor; aplique beq_nat_false_iff; auto.

Test_nostutter_3 : Nostutter [5n]
Test_nostutter_3 = ?
// Prova. repita o construtor; aplique beq_nat_false; auto. Qed.

Test_nostutter_4 : Not (Nostutter [3n,1n,1n,4n])
Test_nostutter_4 = ?
// Prova. intro.
// repetir correspondência de metas com
// h: nostutter _ |- _ => inversão h; limpar h; subst
// end.
// contradição H1; auto.

Filter_challenge

Let's prove that our definition of filter from the Poly chapter corresponds to an abstract specification. Here is the specification, informally written in English:

A list l is an "ordered merge" of l1 and l2 if it contains all the same elements as l1 and l2, in the same order as l1 and l2, but possibly interleaved. For example,

[1n,4n,6n,2n,3n] is an ordered merge of [1n,6n,2n] and [4n,3n].

Now, suppose we have a set t, a function test: t -> Bool, and a list l of type List t. Suppose further that l is an ordered merge of two lists, l1 and l2, such that every item in l1 satisfies test and no item in l2 satisfies test. Then, filter test l = l1.

Translate this specification into a theorem in Kind and prove it. (You will need to start by defining what it means for a list to be an ordered merge of two lists. Do this with an inductive data type, not a function.)

Filter_challenge_2

A different way to characterize the behavior of filter is as follows: Among all the subsequences of l that have the property that test evaluates to True for all their elements, filter test l is the longest one. Formalize this statement and prove it.

Palindromes

A palindrome is a sequence that reads the same forwards and backwards.

Define an inductive proposition Pal about List t that captures what it means to be a palindrome. (Hint: You will need three cases. Your definition should be based on the structure of the list; having just a single constructor like
```
C <t> (l : List t)  (rev: Equal l (Rev l)) : Pal l
```
may seem obvious, but it won't work very well.)

Prove (pal_app_rev) that

(l : List t) : Pal (List.concat l (Rev l))

Prove (pal_rev) that

  (l : List t) (p: Pal l) : Equal l (Rev l)

Palindrome_converse

Again, the reverse direction is significantly harder, due to the lack of evidence. Using your definition of Pal from the previous exercise, prove that

(l : List t) ( Equal l (Rev l)) Pal l

NoDup

Remember the definition of the In property from the Logic chapter, which states that a value x appears at least once in a list l:

In <t> (x : t) (l : List t) : Type
In x List.nil = Empty
In x (List.concat xs.h xs.t) = Either (Equal x xs.h)  (In x xs)

Your first task is to use In to define an inductive proposition Disjoint <t> l1 l2, which should be provable exactly when l1 and l2 are lists (with elements of type t) that have no elements in common.

Next, use In to define an inductive proposition NoDup <t> l, which should be provable exactly when l is a list (with elements of type t) in which every member is different from all the others. For example, NoDup U60 [1,2,3,4] and NoDup Bool [] should be provable, while NoDup Nat [1n,2n,1n] and NoDup Bool [Bool.true,Bool.true] should not.

Finally, state and prove one or more interesting theorems that relate Disjoint, NoDup, and List.

Pigeonhole principle

The pigeonhole principle states a basic fact about counting: if we distribute more than n items into n pigeonholes, some pigeonhole must contain at least two items. As often happens, this seemingly trivial fact about numbers requires nontrivial machinery to prove, but now we have enough... First, prove an easy and useful lemma.

In_split 
  <t> 
  <x: t> 
  <l: List t> 
  (i: In x l) 
  : ([l1] -> [l2] -> ((Equal l (List.concat l1  (List.cons x  l2)))))
In_split i = ?

Now define a property Repeats in such a way that Repeats <t> l asserts that l contains at least one repeated element (of type t).

type  Repeats <t> (l: List t) {
  // PREENCHA AQUI
  RemoveMe' : Repeats [] // necessário para verificação de tipo, os dados não devem estar vazios
}

This proof is much easier if you use the excluded_middle hypothesis to show that In is decidable, i.e., Either (In x l) (Not (In x l)). However, it is also possible to do the proof without assuming that In is decidable; if you can do that, you won't need the excluded_middle hypothesis.

Here is one way to formalize the pigeonhole principle. Suppose the list l2 represents a list of pigeonhole labels, and the list l1 represents the labels assigned to a list of items. If there are more items than labels, at least two items must have the same label—i.e., the list l1 must contain repetitions.

Pigeonhole_principle <t> (x: t) 
 (l1: Data.List t) 
 (l2: Data.List t) 
 (i1: In x l1) 
 (i2: In x l2) 
 (lt: Lt (Data.List.length l1) (Data.List.length l2)) 
 : Repeats l1
Pigeonhole_principle t x l1 l2 i2 i2 lt = ?

Excluded_middle : (p : Type) : Either p (Not p)