Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

# [Proof Ground 2020] My Favourite Computer Game

M. is looking through his day-by-day record on how many hours he spent on his favourite computer game. As he skims through it he finds that it is a very long list, with long periods of stable frenzy. He decides to use "run-length-encoding" to both compress the list and identify long streaks.
After doing so, he realizes that he later may want to add more data points to the compressed list, how could he do that? Also he is more interested in the latest data, so he wants to reverse the compressed list. But is it then still representing the correct data?

Submitted by: Manuel Eberl

Coq: Fabian Kunze

Lean: Simon Hudon & Kevin Kappelmann

Isabelle: Manuel Eberl & (Simon Wimmer)

## Resources

### Definitions File

```theory Defs
imports Main
begin

lemmas [termination_simp] = length_dropWhile_le

fun rle where
"rle [] = []"
| "rle (x # xs) = (x, length (takeWhile (\<lambda>y. y = x) xs) + 1) # rle (dropWhile (\<lambda>y. y = x) xs)"

end```

### Template File

```theory Submission
imports Defs
begin

(* The append lemma - gives 30% of the points.
Note: While this lemma gives less points, it's actually harder to prove! *)

lemma rle_append: "xs = [] \<or> ys = [] \<or> last xs \<noteq> hd ys \<Longrightarrow> rle (xs @ ys) = rle xs @ rle ys"
sorry

(* Given the append lemma show the reverse lemma - gives 70% of the points.
Note: While this lemma gives more points, it might actually be easier to prove *)
lemma rle_rev_if_rle_append: "(xs = [] \<or> ys = [] \<or> last xs \<noteq> hd ys \<Longrightarrow> rle (xs @ ys) = rle xs @ rle ys)
\<Longrightarrow> rle (rev xs) = rev (rle xs)"
sorry

end```

### Check File

```theory Check
imports Submission
begin

lemma "xs = [] \<or> ys = [] \<or> last xs \<noteq> hd ys \<Longrightarrow> rle (xs @ ys) = rle xs @ rle ys"
by (fact Submission.rle_append)

lemma "(xs = [] \<or> ys = [] \<or> last xs \<noteq> hd ys \<Longrightarrow> rle (xs @ ys) = rle xs @ rle ys)
\<Longrightarrow> rle (rev xs) = rev (rle xs)"
by (fact Submission.rle_rev_if_rle_append)

end```

### Definitions File

```import tactic data.list.basic

/-

section Run_length_encoding

The following function performs run-length encoding of a list,
converting each run of `n > 0` successive equal elements
`x` into a single element `(x, n)`.
-/

variables {α : Type*}
variables [decidable_eq α]
variables {xs : list α}

open list

lemma sizeof_append {xs ys : list α} : 1 + sizeof (xs ++ ys) = sizeof xs + sizeof ys :=
by { well_founded_tactics.unfold_sizeof,
induction xs; simp [list.sizeof,*]; linarith }

lemma sizeof_pos (xs : list α) : 0 < sizeof xs :=
by { well_founded_tactics.unfold_sizeof,
induction xs; simp [list.sizeof], linarith }

lemma sizeof_lt_size_append {xs ys : list α} : sizeof xs < 1 + sizeof (xs ++ ys) :=
by { well_founded_tactics.unfold_sizeof,
induction xs; simp [list.sizeof,*], apply sizeof_pos, linarith }

def rle : list α → list (α × ℕ)
| [] := []
| (x :: xs) :=
have (drop_while (eq x) xs).sizeof < 1 + xs.sizeof,  -- for termination
by { apply @lt_of_lt_of_le _ _ _ ((take_while (eq x) xs).sizeof + (drop_while (eq x) xs).sizeof),
{ linarith! [sizeof_pos (take_while (eq x) xs)], },
{ erw [← sizeof_append,take_while_append_drop], refl } },
(x, length \$ take_while (eq x) xs) :: rle (drop_while (eq x) xs)

----------------------just some definitions to prevent cheating------------------------

open list

-- def rle_reverse_prop : Prop := ∀ xs : list α, rle (reverse xs) = reverse (rle xs)
def rle_append_prop [inhabited α] : Prop := ∀ {xs ys : list α} (hxs : xs = [] ∨ ys = [] ∨ ilast xs ≠ head ys), rle (xs ++ ys) = rle xs ++ rle ys
def rle_rev_if_rle_append_prop [inhabited α] : Prop := ∀ {xs : list α}, (∀ {xs ys : list α} (hxs : xs = [] ∨ ys = [] ∨ ilast xs ≠ head ys),
rle (xs ++ ys) = rle xs ++ rle ys) → rle (reverse xs) = reverse (rle xs)

-- notation `rle_reverse_prop` := @rle_reverse_prop
notation `rle_append_prop` := @rle_append_prop
notation `rle_rev_if_rle_append_prop` := @rle_rev_if_rle_append_prop
```

### Template File

```import .defs

variables {α : Type*}
variables [decidable_eq α]
variables {xs : list α}
open list

-- lemma rle_rev : rle (reverse xs) = reverse (rle xs) := sorry

lemma rle_append [inhabited α] {xs ys : list α}
(hxs : xs = [] ∨ ys = [] ∨ ilast xs ≠ head ys) :
rle (xs ++ ys) = rle xs ++ rle ys :=
sorry

lemma rle_rev_if_rle_append [inhabited α] {xs : list α} : (∀ {xs ys : list α} (hxs : xs = [] ∨ ys = [] ∨ ilast xs ≠ head ys),
rle (xs ++ ys) = rle xs ++ rle ys) → rle (reverse xs) = reverse (rle xs) := sorry

```

### Check File

```import .defs
import .submission

variables {α : Type*}
variables [decidable_eq α]

variables [inhabited α]

-- The append subtask - gives 30% of the points.
-- Note: While this subtask gives less points, it's actually harder to prove!
lemma rle_append_safe1 : rle_append_prop α _ _ := @rle_append α _ _
lemma rle_append_safe2 : rle_append_prop α _ _ := @rle_append α _ _
lemma rle_append_safe3 : rle_append_prop α _ _ := @rle_append α _ _

-- Given the append subtask show the reverse subtask - gives 70% of the points.
-- Note: While this subtask gives more points, it might actually be easier to prove
lemma rle_rev_if_rle_append_safe1 : rle_rev_if_rle_append_prop α _ _ := @rle_rev_if_rle_append α _ _
lemma rle_rev_if_rle_append_safe2 : rle_rev_if_rle_append_prop α _ _ := @rle_rev_if_rle_append α _ _
lemma rle_rev_if_rle_append_safe3 : rle_rev_if_rle_append_prop α _ _ := @rle_rev_if_rle_append α _ _
lemma rle_rev_if_rle_append_safe4 : rle_rev_if_rle_append_prop α _ _ := @rle_rev_if_rle_append α _ _
lemma rle_rev_if_rle_append_safe5 : rle_rev_if_rle_append_prop α _ _ := @rle_rev_if_rle_append α _ _
lemma rle_rev_if_rle_append_safe6 : rle_rev_if_rle_append_prop α _ _ := @rle_rev_if_rle_append α _ _
lemma rle_rev_if_rle_append_safe7 : rle_rev_if_rle_append_prop α _ _ := @rle_rev_if_rle_append α _ _

```

### Definitions File

```From Coq Require Export Lists.List.
Export List.ListNotations.
Require Export PeanoNat.

Fixpoint takeWhile {X} (f: X -> bool) (xs:list X) :=
match xs with
[] => xs
| x::xs' =>
if f x then x::takeWhile f xs' else []
end.

Fixpoint dropWhile {X} (f: X -> bool) (xs:list X) :=
match xs with
[] => xs
| x::xs' =>
if f x then dropWhile f xs' else xs
end.

(** Not structurally recursive, but dropWhile is carefully crafted and this still works (similar to https://github.com/coq/coq/issues/10724).
Fixpoint rle (xs:list nat) : list (nat*nat) :=
match xs with
[] => []
| x :: xs => (x,1 + length (takeWhile (Nat.eqb x) xs)) :: rle (dropWhile (Nat.eqb x) xs)
end.

(*Needed for spec of app-lemma: *)

Fixpoint last_error {X} (xs:list X) :=
match xs with
[] => None
| [x] => Some x
| _::xs => last_error xs
end.

Require Import Wf_nat.
(* Helper lemma for size induction *)
Lemma size_ind {X} (P:X -> Prop) (f: X -> nat) (H: forall x, (forall x', f x' < f x -> P x') -> P x) : forall x, P x.
Proof.
eapply induction_ltof1. unfold ltof. eassumption.
Qed.
```

### Template File

```Require Import Defs.

(** The append lemma - gives 30% of the points.
Note: While this lemma gives less points, it's actually harder to prove! *)
Lemma rle_app (xs ys : list nat):
(forall x, ~ (last_error xs = Some x
/\ hd_error ys = Some x))
-> rle (xs++ys) = rle xs ++ rle ys.
Proof.

(** Given the append lemma show the reverse lemma - gives 70% of the points.
Note: While this lemma gives more points, it might actually be easier to prove *)
Lemma rle_rev_if_rle_app:
(forall xs ys,
(forall x, ~ (last_error xs = Some x
/\ hd_error ys = Some x))
-> rle (xs++ys) = rle xs ++ rle ys)
-> forall xs, rev (rle xs) = rle (rev xs).
Proof.