I agree 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.

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)

Download Files
### Definitions File

### Template File

### Check 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

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

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

Download Files
### Definitions File

### Template File

### Check 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

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

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 α _ _

Download Files
### Definitions File

### Template 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). You probably need [size_induction] to reason about this definition. *) 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.

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. Admitted. (** 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. Admitted.

Terms and Conditions