showdown-fulcrum.lean

-- These are pretty general lemmas about lists.
-- We could find them in the standard library
namespace list

universes u v w

variables {α : Type u} {β : Type v} {γ : Type w}
variables (f : α → β → γ)
variables {x : α} {y : β} {xs : list α} {ys : list β}

open function

@[simp]
lemma map_eq_nil {f : α → γ} :
  map f xs = nil ↔ xs = nil :=
by cases xs ; simp

@[simp]
lemma zip_eq_nil :
  zip xs ys = nil ↔ xs = nil ∨ ys = nil :=
by cases xs ; cases ys ; simp

lemma map₂_eq_map_zip :
  map₂ f xs ys = map (uncurry f) (zip xs ys) :=
begin
  induction xs generalizing ys,
  { cases ys ; simp, },
  { cases ys ; simp [*,uncurry], }
end

lemma mem_map₂
  (h : (x,y) ∈ zip xs ys) :
  f x y ∈ map₂ f xs ys :=
by { rw map₂_eq_map_zip,
     refine @mem_map_of_mem _ _ (uncurry f) (x,y) _ h, }

@[simp]
lemma cons_tail_tails :
  xs :: tail (tails xs) = tails xs :=
by cases xs ; simp

lemma tails_append {xs' : list α} :
  tails (xs ++ xs') = map (++ xs') (tails xs) ++ (tails xs').tail :=
by induction xs ; simp *

lemma tails_reverse :
  tails (reverse xs) = reverse (map reverse (inits xs)) :=
by induction xs with x xs; simp [tails_append,*,comp]

lemma inits_reverse :
  inits (reverse xs) = reverse (map reverse (tails xs)) :=
by { rw ← reverse_reverse xs,
     generalize : reverse xs = ys,
     simp [tails_reverse,comp],
     symmetry, apply map_id }

@[simp]
lemma sum_reverse [add_comm_monoid α] :
  sum (reverse xs) = sum xs :=
by induction xs ; simp *

end list

section minimum

variables {α : Type*} [decidable_linear_order α] [inhabited α]

def minimum (xs : list α) : α :=
list.foldl min xs.head xs.tail

@[simp]
lemma minimum_single (x : α) :
  minimum [x] = x :=
rfl

open list

@[simp]
lemma minimum_cons (x : α) (xs : list α)
  (h : xs ≠ []) :
  minimum (x :: xs) = min x (minimum xs) :=
by { cases xs with y ys, contradiction,
     simp [minimum], rw ← foldl_hom,
     simp [min_assoc], }

lemma le_minimum {x : α} {xs : list α}
  (h : xs ≠ [])
  (h' : ∀ i, i ∈ xs → x ≤ i) :
  x ≤ minimum xs :=
begin
  induction xs, contradiction,
  by_cases xs_tl = list.nil,
  { subst xs_tl, apply h', simp, },
  simp *, apply le_min,
  { apply h', simp },
  { apply xs_ih h, introv h'',
    apply h', right, apply h'' },
end

@[simp]
lemma minimum_cons_le_self {i : α} {xs : list α} :
  minimum (i :: xs) ≤ i :=
by cases xs ; simp [min_le_left]

lemma minimum_le {i : α} {xs : list α}
  (h : i ∈ xs) :
  minimum xs ≤ i :=
by { induction xs ; cases h,
     { subst i, simp [min_le_left], },
     { have : xs_tl ≠ [],
       { intro, subst xs_tl, cases h },
       simp *, transitivity, apply min_le_right,
       solve_by_elim } }

end minimum

local attribute [instance] classical.prop_decidable

-- Here are the specifics of our solution.
-- It hinges on computing lists of partial sums
-- forward (`inits_sums`) and backward (`tails_sums`)
section fulcrum

open list int function

instance : inhabited ℤ :=
⟨ 0 ⟩

def inits_sums.f : list ℤ × ℤ → ℤ → list ℤ × ℤ
 | (xs,acc) x := ((acc+x) :: xs, acc+x)

def partial_sums (xs : list ℤ) : list ℤ :=
(list.foldl inits_sums.f ([0],0) xs).1

def tails_sums (xs : list ℤ) : list ℤ :=
partial_sums xs.reverse

def inits_sums (xs : list ℤ) : list ℤ :=
(partial_sums xs).reverse

def fulcrum (xs : list ℤ) : ℤ :=
let xs' := map₂ (λ i j, abs (i - j)) (inits_sums xs) (tails_sums xs) in
minimum xs'

variables (xs : list ℤ)

@[simp]
def partial_sums_def :
  partial_sums xs.reverse = xs.tails.map sum :=
begin
  simp [partial_sums],
  suffices : foldl inits_sums.f ([0], 0) (reverse xs)
           = (map sum (tails xs), sum xs),            { simpa * },
  induction xs ; simp [*,foldl_reverse,inits_sums.f],
end

@[simp]
def tails_sums_def :
  tails_sums xs = xs.tails.map sum :=
by simp [tails_sums]

@[simp]
def inits_sums_def :
  inits_sums xs = xs.inits.map sum :=
by { rw ← reverse_reverse xs,
     generalize : reverse xs = ys,
     simp [inits_sums,inits_reverse,comp], }

lemma le_fulcrum (x : ℤ)
  (h : ∀ i j, (i,j) ∈ zip (xs.inits.map sum) (xs.tails.map sum) → x ≤ abs (i - j)) :
  x ≤ fulcrum xs :=
begin
  apply le_minimum,
  { simp [map₂_eq_map_zip,decidable.not_or_iff_and_not],
    cases xs ; simp, },
  { simp, introv h', simp [map₂_eq_map_zip,uncurry] at h',
    rcases h' with ⟨ a, b, h₀, h₁ ⟩, subst i,
    apply h _ _ h₀, }
end

lemma fulcrum_le (i j : ℤ)
  (h : (i,j) ∈ zip (xs.inits.map sum) (xs.tails.map sum)) :
  fulcrum xs ≤ abs (i - j) :=
minimum_le $
by { simp, refine mem_map₂ (λ i j, abs (i + -j)) h, }

end fulcrum