/- Exercise 2.1: Functional Programming — Lists -/
/- Question 1: Counting elements -/
/- 1.1. Define a function `count` that counts the number of occurrences of an element in a list. It
should be similar to `bcount` from the lecture, except that it takes a value `α` instead of a
predicate `α → bool`.
`decidable_eq` is the type class of types whose equality is decidable. -/
def count {α : Type} (a : α) [decidable_eq α] : list α → ℕ
| [] := 0
| (x :: xs) := count xs + (if x = a then 1 else 0)
/- 1.2. Test your definition of `count` on a few examples to convince yourself that it is
correct. This is something you should always do regardless of whether we ask for it.
You can use `#reduce` or (if `#reduce` fails) `#eval` to do this. -/
#reduce count 5 [] -- expected: 0
#reduce count 5 [1, 2, 5, 1] -- expected: 1
#reduce count 5 [5, 2, 5, 1] -- expected: 2
#reduce count 10 [10, 10, 9, 10, 10] -- expected: 4
/- 1.3. Complete the following proof (or replace it with a new proof structure of your own).
Hints: Some of the following lemmas might be useful to reason about `≤`. Moreover, if it helps you
carry out the proof, you could reconsider revising your answer to question 1.1. -/
#check nat.le_add_left
#check nat.le_add_right
#check add_le_add_left
#check add_le_add_right
lemma count_le_length {α : Type} (a : α) [decidable_eq α] :
∀xs : list α, count a xs ≤ list.length xs
| [] :=
by refl
| (x :: xs) :=
calc count a (x :: xs) = count a xs + (if x = a then 1 else 0) :
by refl
... ≤ list.length xs + (if x = a then 1 else 0) :
begin
apply add_le_add_right,
apply (count_le_length xs)
end
... ≤ list.length (x :: xs) :
begin
by_cases (x = a),
{ simp [h, list.length] },
{ simp [h, list.length], apply nat.le_add_left }
end
/- Question 2: Removing duplicates -/
/- 2.1. Define a predicate `mem x xs` that returns true if `x` is an element of `xs`. -/
def mem {α : Type} (a : α) (xs : list α) [decidable_eq α] : Prop :=
count a xs ≠ 0
/- The above `mem` predicate is not quite as convenient as the predefined `list.mem`, for which
theorems and a nice notation (infix `∈`) are available, including a proof of decidability. Let's use
`list.mem` from now on. -/
#print list.has_mem
#check list.mem
#check list.decidable_mem
/- 2.2. Define a function `remdups` that removes duplicate elements in a list. For example,
`remdups [1, 2, 1, 3]` could return either `[1, 2, 3]` or `[2, 1, 3]`, depending of which of the two
occurrences of `1` is kept.
Hint: One of the two behaviors is easier to implement. -/
def remdups {α : Type} [decidable_eq α] : list α → list α
| [] := []
| (x :: xs) := if x ∈ xs then remdups xs else x :: remdups xs
/- 2.3. Test your implementation on more than two input values, using `#reduce` or `#eval`, and put
the expected value in a comment. -/
#reduce remdups [] -- expected: []
#reduce remdups [1] -- expected: [1]
#reduce remdups [1, 2, 3, 4, 5, 6, 7, 10, 9, 8] -- expected: [1, 2, 3, 4, 5, 6, 7, 10, 9, 8]
#reduce remdups [1, 2, 1, 3] -- expected: [2, 1, 3]
#reduce remdups [1, 1, 2, 1, 1, 2, 4, 1, 1, 2, 1, 1, 2, 4, 8] -- expected: [1, 2, 4, 8]
/- Do you find yourself copy-pasting the outcome of `#reduce` into the comment? If so, this defeats
the point of writing a test. You should first think for yourself of the expected result, write it
down, and then compare the actual result with it. -/
/- 2.4. Define a function `remdups_adj` that compresses adjacent duplicates. For example, it would
leave `[1, 2, 1, 3]` unchanged but compress `[1, 1, 2, 2, 2, 1, 3, 3]` to `[1, 2, 1, 3]`. -/
def remdups_adj {α : Type} [decidable_eq α] : list α → list α
| [] := []
| [x] := [x]
| (x :: y :: xs) := if x = y then remdups_adj (x :: xs) else x :: remdups_adj (y :: xs)
/- 2.5. Test your implementation on the same values as you used for question 2.3. -/
#reduce remdups_adj [] -- expected: []
#reduce remdups_adj [1] -- expected: [1]
#reduce remdups_adj [1, 2, 3, 4, 5, 6, 7, 10, 9, 8] -- expected: [1, 2, 3, 4, 5, 6, 7, 10, 9, 8]
#reduce remdups_adj [1, 2, 1, 3] -- expected: [1, 2, 1, 3]
#reduce remdups_adj [1, 1, 2, 1, 1, 2, 4, 1, 1, 2, 1, 1, 2, 4, 8]
-- expected: [1, 2, 1, 2, 4, 1, 2, 1, 2, 4, 8]
/- Do the tests detect any difference in behavior between `remdups` and `remdups_adj`? If the answer
is no, this is a strong indication that your tests were incomplete to start with. -/
/- 2.6. Prove that `remdups` does not influence the behavior of `list.mem`.
Hint: Use `by_cases` to distinguish between the case where a given element is kept and the case
where it is removed. -/
@[simp] lemma mem_remdups {α : Type} (a : α) [decidable_eq α] :
∀xs : list α, a ∈ remdups xs ↔ a ∈ xs
| [] := by refl
| (x :: xs) :=
begin
simp [remdups],
by_cases (x ∈ xs),
{ simp [h, mem_remdups xs],
apply iff.intro,
{ intro, apply or.intro_right, assumption },
{ intro hor,
apply hor.elim,
{ intro a_eq_x, rw a_eq_x, assumption },
{ intro, assumption } } },
{ simp [h, mem_remdups xs] }
end
/- 2.7. State and prove that `remdups_adj` does not influence the behavior of `list.mem`. -/
@[simp] lemma mem_remdups_adj {α : Type} (a : α) [decidable_eq α] :
∀xs : list α, a ∈ remdups_adj xs ↔ a ∈ xs
| [] := by refl
| [x] := by refl
| (x :: y :: xs) :=
begin
by_cases (x = y); simp [h, remdups_adj, mem_remdups_adj (y :: xs)],
rw ←or.assoc,
rw or_self
end
/- 2.8. State and prove that `remdups` is idempotent (i.e., that applying it twice has the same
effect as applying it only once). -/
lemma remdups_idem {α : Type} [decidable_eq α] :
∀xs : list α, remdups (remdups xs) = remdups xs
| [] := by refl
| (x :: xs) :=
begin
simp [remdups],
by_cases (x ∈ xs),
{ simp [h], apply remdups_idem },
{ simp [h, remdups], apply remdups_idem }
end
/- 2.9 (**optional bonus**). State and prove that `remdups_adj` is idempotent.
Warning: This one is difficult. -/
lemma remdups_adj_middle {α : Type} (y : α) (xs : list α) [decidable_eq α] :
∀ws : list α, remdups_adj (ws ++ y :: y :: xs) = remdups_adj (ws ++ y :: xs)
| [] := by simp [remdups_adj]
| [w] := by by_cases w = y; simp [h, remdups_adj]
| (w :: w' :: ws) :=
begin
simp [remdups_adj],
by_cases w = w';
{ simp [h],
show remdups_adj ((w' :: ws) ++ y :: y :: xs) = remdups_adj ((w' :: ws) ++ y :: xs),
by rw remdups_adj_middle }
end
lemma remdups_adj_append_idem {α : Type} [decidable_eq α] :
∀xs ws : list α, remdups_adj (ws ++ remdups_adj xs) = remdups_adj (ws ++ xs)
| [] ws := by simp [remdups_adj]
| [_] ws := by simp [remdups_adj]
| (x :: y :: xs) ws :=
begin
simp [remdups_adj],
by_cases (x = y); simp [h],
{ simp [remdups_adj_middle, remdups_adj_append_idem] },
{ calc remdups_adj (ws ++ x :: remdups_adj (y :: xs)) =
remdups_adj ((ws ++ [x]) ++ remdups_adj (y :: xs)) : by simp
... = remdups_adj ((ws ++ [x]) ++ y :: xs) : by rw remdups_adj_append_idem
... = remdups_adj (ws ++ x :: y :: xs) : by simp }
end
lemma remdups_adj_idem {α : Type} [decidable_eq α] :
∀xs : list α, remdups_adj (remdups_adj xs) = remdups_adj xs :=
assume xs,
show remdups_adj ([] ++ remdups_adj xs) = remdups_adj ([] ++ xs),
from remdups_adj_append_idem _ []