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