Fun.lean

section 
parameters {α : Type} 
variable [ a_dec  : decidable_eq α]
include a_dec
open nat 

definition replicate (a : α) : ℕ → list α 
| 0 := []
| (succ n) := a :: replicate n

definition expand (l : list (α × ℕ) ) : list α := 
  list.bind l (λ xn, replicate (prod.fst xn) (prod.snd xn))

theorem replicate_append 
  : ∀ a n₁ n₂, (replicate a n₁ ++ replicate a n₂ = replicate a (n₁ + n₂)) :=
by intros; induction n₁; simp [replicate, *]

inductive wellformed : list (α × ℕ) → Prop 
| nil : wellformed []
| one : ∀ a n, wellformed [(a, succ n)]
| ind : ∀ xs a n b m, (a ≠ b) → wellformed ((b,succ m)::xs) → wellformed ((a,succ n)::(b,succ m)::xs) 

definition cons_c (h : (α × ℕ)) : list (α × ℕ) → list (α × ℕ)
| [] := [h] 
| ((x,n)::xs) := if (prod.fst h = x) then (x,n+prod.snd h)::xs else h::(x,n)::xs 

theorem cons_c_wf 
  : ∀ a n xs, wellformed xs → wellformed (cons_c (a,succ n) xs) := 
by intros; cases a_1; simp [cons_c]; try {cases (decidable.em (a = a_1_a))}; 
   simp [*, wellformed.one, wellformed.nil, wellformed.ind] 

theorem wf_induct 
  : ∀ xs (wf : wellformed xs) (P : list (α × ℕ) → Prop),
     P []
  → (∀ xs (wf : wellformed xs) x n, P xs → P (cons_c (x, succ n) xs))
  → P xs :=
begin 
intros xs wf P case_nil case_cons,
induction xs, simp *,
cases wf,
{ let one := case_cons [] wellformed.nil, simp [cons_c, *] at one, 
  apply one, apply case_nil },
{ let step := case_cons _ wf_a_2 wf_a, simp [cons_c, *] at step,  apply step }
end

theorem cons_c_cons_c 
  : ∀ l a n m, cons_c (a, n) (cons_c (a, m) l) = cons_c (a, n + m) l := 
begin 
intros; cases l,
{ simp [cons_c] },
{ cases l_hd, cases (decidable.em (a = l_hd_fst)); simp [cons_c, *] },
end

definition app_c :  list (α × ℕ) → list (α × ℕ) → list (α × ℕ) 
| [] := λ ys, ys
| (x :: xs) := λ ys, cons_c x (app_c xs ys) 

theorem app_c_cons_c : ∀ x l₁ l₂, app_c (cons_c x l₁) l₂ = cons_c x (app_c l₁ l₂) :=
begin 
intros, induction l₁; simp [app_c, *, cons_c],
cases (l₁_hd); cases (x); simp [app_c, cons_c], 
cases (decidable.em (x_fst = l₁_hd_fst)); simp [*, app_c, cons_c_cons_c],
end

theorem app_c_nil: ∀ l (wf : wellformed l), app_c l [] = l := 
by intros; apply (wf_induct _ wf); try { intros }; simp [*, app_c, app_c_cons_c]

theorem app_c_wf : ∀ l₁ ( wf₁ : wellformed l₁) l₂ (wf₂ : wellformed l₂), wellformed (app_c l₁ l₂) :=
begin 
intros, apply (wf_induct _ wf₁); try {intros }; simp [*,app_c,app_c_cons_c], 
apply cons_c_wf, simp *,
end

theorem expand_nil : expand [] = [] := 
by simp [expand]


theorem expand_cons : ∀ a n xs, expand ((a, n)::xs) = replicate a n ++ expand xs := 
by intros; simp[expand]

theorem cons_c_refinement : ∀  l₁ a n, expand (cons_c (a , n) l₁) = replicate a n ++ expand l₁ := 
begin 
intros; cases l₁, 
{ simp [expand_nil, expand_cons, cons_c] },
{ cases l₁_hd; simp [cons_c]; cases (decidable.em (a = l₁_hd_fst ));
  simp [*, expand_cons]; rw [<-replicate_append, list.append_assoc]
}
end

theorem app_c_refinement : ∀ l₁ l₂, expand (app_c l₁ l₂) = (expand l₁) ++ (expand l₂) := 
begin 
intros, induction l₁,
{ simp [expand_nil, app_c] },
{ cases (l₁_hd); simp [expand_cons, app_c, cons_c_refinement,l₁_ih] }
end 

definition drop_c : ℕ → list (α × ℕ) → list (α × ℕ)
| 0 l                          := l 
| (succ n) []                      := []
| (succ n) ((x , zero)      :: xs) := drop_c n xs
| (succ n) ((x , succ zero) :: xs) := drop_c n xs
| (succ n) ((x , succ (succ m))    :: xs) := drop_c n ((x, succ m) :: xs) 

theorem drop_c_wf : ∀ n xs (wf : wellformed xs), wellformed (drop_c n xs) := 
begin 
intro, induction n; intros, 
{ simp[drop_c,wf] },
{ cases wf; cases n_n; 
  repeat { simp[drop_c, wellformed.nil, wellformed.one, wellformed.ind, *] <|> cases wf_n }}
end 

theorem drop_c_refinement : ∀  n l (wf : wellformed l) , expand (drop_c n l) = list.drop n (expand l) := 
begin 
intro, induction n; intros,
{ simp[drop_c] },
{ cases wf; cases n_n;
  repeat {  simp[drop_c, expand_nil, expand_cons, *, wellformed.one, wellformed.ind, replicate] 
        <|> rewrite [n_ih] 
        <|> cases wf_n 
         }
}
end

definition compress (l : list α) : list (α × ℕ) := 
   list.foldr app_c [] (list.map (λx, [(x,1)]) l) 

theorem compress_nil : compress [] = [] := 
by simp [compress]
 
theorem compress_cons : ∀ x ys, compress (x :: ys) = cons_c (x , 1) (compress ys) := 
by intros; simp [compress, app_c]

theorem compress_wf : ∀ xs, wellformed (compress xs) := 
by intros; induction xs; 
   simp [compress_nil, compress_cons, app_c_wf, cons_c_wf, wellformed.nil, *]

theorem compress_app : ∀ xs ys, compress (xs ++ ys) = app_c (compress xs) (compress ys) := 
by intros; induction xs; simp [compress_nil, app_c, compress_cons, *, app_c_cons_c]

theorem compress_replicate : ∀ x n, compress (replicate x (succ n)) = [(x , succ n)] :=
by intros; induction n; 
   repeat { simp [replicate, compress_cons, compress_nil, cons_c] at * <|> rewrite n_ih }

theorem compress_expand :  ∀ xs, wellformed xs → compress (expand xs) = xs :=
by intros; apply (wf_induct xs); try { intros };
   simp [expand_nil, compress_nil, *, cons_c_refinement, compress_app, compress_app, compress_replicate, app_c]

theorem expand_compress : ∀ xs, expand (compress xs) = xs := 
by intros; induction xs; 
   simp [compress_nil,expand_nil, compress_cons, cons_c_refinement, replicate, *]

theorem drop_c_compress :  ∀ n xs, drop_c n (compress xs) = compress (list.drop n xs) := 
by intros; rw [← expand_compress xs]; rw [← drop_c_refinement];
   simp[compress_expand, compress_wf,drop_c_wf]
end