balanced-bracket-sequence.lean

import tactic.norm_num
import tactic.unfold_cases
import tactic.nth_rewrite
import tactic.linarith

universe u

inductive bracket_t
| left
| right

inductive balanced : list bracket_t → Prop
| empty : balanced []
| wrap (initial : list bracket_t) : balanced initial → balanced ([bracket_t.left] ++ initial ++ [bracket_t.right])
| append (initial1 initial2 : list bracket_t) : balanced initial1 → balanced initial2 → balanced (initial1 ++ initial2)

def balance_factor : ∀ length : ℕ, ∀ string : list bracket_t, ℤ
| 0 _ := 0
| _ [] := 0
| (n + 1) (bracket_t.left::rest) := 1 + balance_factor n rest
| (n + 1) (bracket_t.right::rest) := -1 + balance_factor n rest

def balance_factor_predicate (string : list bracket_t) := balance_factor string.length string = 0 ∧ ∀ n : ℕ, n < string.length → 0 ≤ balance_factor n string

def chop_head : list bracket_t → list bracket_t
| [] := []
| (head::rest) := rest

def chop_other_end : list bracket_t → list bracket_t
| [] := []
| (head::rest) := if rest.length = 0 then [] else head::chop_other_end rest

noncomputable def meaningless_element : bracket_t := @classical.choice bracket_t begin
  exact nonempty.intro bracket_t.left,
end

noncomputable def get_head : list bracket_t → bracket_t
| [] := meaningless_element
| (head::rest) := head

noncomputable def get_tail : list bracket_t → bracket_t
| [] := meaningless_element
| (head::rest) := if rest.length = 0 then head else get_tail rest

lemma reconstitute : ∀ string : list bracket_t, 0 < string.length → chop_other_end string ++ [get_tail string] = string
| [] h := begin
  rw (show ([] : list bracket_t).length = 0, by refl) at h,
  norm_num at h,
end
| (head::tail) h := begin
  rw chop_other_end,
  rw get_tail,
  split_ifs,
  have := list.length_eq_zero.mp h_1,
  rw this,
  rw list.nil_append,
  rw list.cons_append,
  rw list.cons_inj,
  exact reconstitute tail begin
    exact pos_iff_ne_zero.mpr h_1,
  end,
end

def chop_both_ends : list bracket_t → list bracket_t
| string := chop_head (chop_other_end string)

lemma head_open : ∀ string : list bracket_t, ∀ head : bracket_t, balance_factor_predicate (head::string) → head = bracket_t.left
| string head h := begin
  cases head,
  refl,
  rw balance_factor_predicate at h,
  have := h.right 1 begin
    rw list.length_cons,
    exact if h' : string.length = 0 then begin
      have h2 := list.eq_nil_of_length_eq_zero h',
      rw h2 at h,
      rw (show [bracket_t.right].length = 1, by refl) at h,
      have := h.left,
      rw balance_factor at this,
      rw balance_factor at this,
      norm_num at this,
    end else begin
      have := pos_iff_ne_zero.mpr h',
      exact nat.succ_lt_succ_iff.mpr this,
    end,
  end,
  rw balance_factor at this,
  cases string,
  rw balance_factor at this,
  norm_num at this,
  cases string_hd,
  rw balance_factor at this,
  norm_num at this,
  rw balance_factor at this,
  norm_num at this,
end

lemma ignores_garbage_left : ∀ z : list bracket_t, balance_factor z.length z = balance_factor z.length (z ++ [bracket_t.left])
| [] := begin
  rw (show ([] : list bracket_t).length = 0, by refl),
  rw list.nil_append,
  rw [balance_factor, balance_factor],
end
| (bracket_t.left::rest) := begin
  rw (show (bracket_t.left::rest).length = rest.length + 1, by refl),
  rw list.cons_append,
  rw [balance_factor, balance_factor],
  rw ignores_garbage_left rest,
end
| (bracket_t.right::rest) := begin
  rw (show (bracket_t.right::rest).length = rest.length + 1, by refl),
  rw list.cons_append,
  rw [balance_factor, balance_factor],
  rw ignores_garbage_left rest,
end

lemma minus_one : ∀ z : list bracket_t, (balance_factor (z ++ [bracket_t.right]).length (z ++ [bracket_t.right]) = balance_factor z.length z - 1)
| [] := begin
  rw list.nil_append,
  rw (show [bracket_t.right].length = 1, by refl),
  rw (show ([] : list bracket_t).length = 0, by refl),
  rw balance_factor,
  rw balance_factor,
  norm_num,
end
| (bracket_t.left::rest) := begin
  rw list.cons_append,
  rw (show (bracket_t.left :: (rest ++ [bracket_t.right])).length = (rest ++ [bracket_t.right]).length + 1, by refl),
  rw balance_factor,
  have := minus_one rest,
  rw this,
  rw (show (bracket_t.left :: rest).length = rest.length + 1, by refl),
  rw balance_factor,
  norm_num,
end
| (bracket_t.right::rest) := begin
rw list.cons_append,
  rw (show (bracket_t.right :: (rest ++ [bracket_t.right])).length = (rest ++ [bracket_t.right]).length + 1, by refl),
  rw balance_factor,
  have := minus_one rest,
  rw this,
  rw (show (bracket_t.right :: rest).length = rest.length + 1, by refl),
  rw balance_factor,
  rw int.sub_eq_add_neg,
  rw int.sub_eq_add_neg,
  rw (int.add_assoc _ _ _).symm,
end

lemma ignores_garbage : ∀ n_n : ℕ, ∀ z : list bracket_t, n_n < z.length → balance_factor n_n (z ++ [bracket_t.right]) = balance_factor n_n z
| 0 anything h := begin
  cases anything,
  rw list.nil_append,
  rw balance_factor,
  rw balance_factor,
  rw list.cons_append,
  rw balance_factor,
  rw balance_factor,
end
| anything [] h := begin
  rw (show ([] : list bracket_t).length = 0, by refl) at h,
  exact false.elim ((not_lt_of_ge anything.zero_le) h),
end
| (n + 1) (bracket_t.left::rest) h := begin
  rw [list.cons_append, balance_factor, balance_factor],
  rw (show (bracket_t.left::rest).length = rest.length + 1, by refl) at h,
  rw ignores_garbage n rest (nat.lt_of_succ_lt_succ h),
end
| (n + 1) (bracket_t.right::rest) h := begin
  rw [list.cons_append, balance_factor, balance_factor],
  rw (show (bracket_t.right::rest).length = rest.length + 1, by refl) at h,
  rw ignores_garbage n rest (nat.lt_of_succ_lt_succ h),
end

lemma ignores_garbage' : ∀ z : list bracket_t, balance_factor z.length z = balance_factor z.length (z ++ [bracket_t.right])
| [] := begin
  rw (show ([] : list bracket_t).length = 0, by refl),
  rw list.nil_append,
  rw [balance_factor, balance_factor],
end
| (bracket_t.left::rest) := begin
  rw (show (bracket_t.left::rest).length = rest.length + 1, by refl),
  rw list.cons_append,
  rw [balance_factor, balance_factor],
  rw ignores_garbage' rest,
end
| (bracket_t.right::rest) := begin
  rw (show (bracket_t.right::rest).length = rest.length + 1, by refl),
  rw list.cons_append,
  rw [balance_factor, balance_factor],
  rw ignores_garbage' rest,
end

lemma sandwich1 (rest2 : list bracket_t) : ∀ rest1 : list bracket_t, balance_factor (rest1 ++ bracket_t.left :: rest2).length (rest1 ++ bracket_t.left :: rest2) = balance_factor (rest1 ++ rest2).length (rest1 ++ rest2) + 1
| [] := begin
  rw list.nil_append,
  rw list.nil_append,
  rw (show (bracket_t.left::rest2).length = rest2.length + 1, by refl),
  rw balance_factor,
  rw int.add_comm,
end
| (bracket_t.left::rest) := begin
  rw list.cons_append,
  rw (show (bracket_t.left :: (rest ++ bracket_t.left :: rest2)).length = (rest ++ bracket_t.left :: rest2).length + 1, by refl),
  rw balance_factor,
  rw sandwich1 rest,
  rw list.cons_append,
  rw (show (bracket_t.left :: (rest ++ rest2)).length = (rest ++ rest2).length + 1, by refl),
  rw balance_factor,
  rw add_assoc,
end
| (bracket_t.right::rest) := begin
  rw list.cons_append,
  rw (show (bracket_t.right :: (rest ++ bracket_t.left :: rest2)).length = (rest ++ bracket_t.left :: rest2).length + 1, by refl),
  rw balance_factor,
  rw sandwich1 rest,
  rw list.cons_append,
  rw (show (bracket_t.right :: (rest ++ rest2)).length = (rest ++ rest2).length + 1, by refl),
  rw balance_factor,
  rw add_assoc,
end

lemma sandwich2 (rest2 : list bracket_t) : ∀ rest1 : list bracket_t, balance_factor (rest1 ++ bracket_t.right :: rest2).length (rest1 ++ bracket_t.right :: rest2) = balance_factor (rest1 ++ rest2).length (rest1 ++ rest2) - 1
| [] := begin
  rw list.nil_append,
  rw list.nil_append,
  rw (show (bracket_t.right::rest2).length = rest2.length + 1, by refl),
  rw balance_factor,
  rw int.add_comm,
  norm_num,
end
| (bracket_t.left::rest) := begin
  rw list.cons_append,
  rw (show (bracket_t.left :: (rest ++ bracket_t.right :: rest2)).length = (rest ++ bracket_t.right :: rest2).length + 1, by refl),
  rw balance_factor,
  rw sandwich2 rest,
  rw list.cons_append,
  rw (show (bracket_t.left :: (rest ++ rest2)).length = (rest ++ rest2).length + 1, by refl),
  rw balance_factor,
  rw [int.sub_eq_add_neg, int.sub_eq_add_neg],
  rw add_assoc,
end
| (bracket_t.right::rest) := begin
  rw list.cons_append,
  rw (show (bracket_t.right :: (rest ++ bracket_t.right :: rest2)).length = (rest ++ bracket_t.right :: rest2).length + 1, by refl),
  rw balance_factor,
  rw sandwich2 rest,
  rw list.cons_append,
  rw (show (bracket_t.right :: (rest ++ rest2)).length = (rest ++ rest2).length + 1, by refl),
  rw balance_factor,
  rw [int.sub_eq_add_neg, int.sub_eq_add_neg],
  rw add_assoc,
end

lemma append_add_balance_factor : ∀ a b : list bracket_t, balance_factor a.length a + balance_factor b.length b = balance_factor ((a ++ b).length) (a ++ b)
| [] [] := begin
  rw (show ([] : list bracket_t) ++ [] = [], by refl),
  rw (show ([] : list bracket_t).length = 0, by refl),
  rw balance_factor,
  norm_num,
end
| [] anything := begin
  rw (show ([] : list bracket_t).length = 0, by refl),
  rw (show ([] : list bracket_t) ++ anything = anything, by refl),
  rw balance_factor,
  norm_num,
end
| anything [] := begin
  rw (show ([] : list bracket_t).length = 0, by refl),
  rw (show anything ++ ([] : list bracket_t) = anything, by exact list.append_nil anything),
  rw balance_factor,
  norm_num,
end
| (head1::rest1) (head2::rest2) := begin
  cases head1,
  repeat {
    cases head2,
    repeat {
      rw (show ∀ x : bracket_t, (x::rest1).length = rest1.length + 1, begin intro, refl, end),
      rw (show ∀ x : bracket_t, (x::rest2).length = rest2.length + 1, begin intro, refl, end),
      rw balance_factor,
      rw balance_factor,
      try { rw sandwich1, },
      try { rw sandwich2, },
      rw list.cons_append,
      rw (show ∀ x : bracket_t, ∀ y : list bracket_t, (x::y).length = y.length + 1, begin intros, refl end),
      rw balance_factor,
      rw (append_add_balance_factor rest1 rest2).symm,
      try { rw int.sub_eq_add_neg, },
      nth_rewrite 2 int.add_comm,
      nth_rewrite 0 int.add_assoc,
      nth_rewrite 0 int.add_assoc,
      nth_rewrite 1 (int.add_assoc _ _ _).symm,
    },
  },
end


lemma tail_close : ∀ string : list bracket_t, ∀ tail : bracket_t, balance_factor_predicate (string ++ [tail]) → tail = bracket_t.right
| string tail h := begin
  cases tail,
  {
    rw balance_factor_predicate at h,
    cases h,
    have := h_right string.length begin
      rw list.length_append,
      rw (show [bracket_t.left].length = 1, by refl),
      exact nat.lt_succ_self _,
    end,
    rw (ignores_garbage_left string).symm at this,
    rw (append_add_balance_factor string [bracket_t.left]).symm at h_left,
    rw (show [bracket_t.left].length = 1, by refl) at h_left,
    rw balance_factor at h_left,
    rw balance_factor at h_left,
    norm_num at h_left,
    have h1 := eq_sub_of_add_eq h_left,
    norm_num at h1,
    rw h1 at this,
    norm_num at this,
  },
  refl,
end

lemma ignores_garbage'' : ∀ a b : list bracket_t, ∀ n : ℕ, n ≤ a.length → balance_factor n (a ++ b) = balance_factor n a
| a b 0 h := begin
  generalize : a ++ b = x,
  cases x,
  repeat {
    cases a,
    repeat {
      rw balance_factor,
    }
  },
end
| a b (n + 1) h := begin
  generalize_hyp h1 : a ++ b = x,
  cases x,
  repeat {
    cases a,
    repeat {
      rw balance_factor,
    }
  },
  cases a_hd,
  rw balance_factor,
  rw (show ∀ a : bracket_t, ∀ b : list bracket_t, (a::b).length = b.length + 1, by begin intros, refl, end) at h,
  have := ignores_garbage'' a_tl b n (nat.le_of_succ_le_succ h),
  rw list.cons_append at h1,
  exact false.elim (list.cons_ne_nil _ _ h1),
  exact false.elim (list.cons_ne_nil _ _ h1),
  rw (show ([] : list bracket_t).length = 0, by refl) at h,
  have := nat.succ_pos n,
  have : false := nat.lt_le_antisymm this h,
  exact false.elim this,
  cases x_hd,
  {
    cases a_hd,
    {
      rw balance_factor,
      rw balance_factor,
      rw list.cons_append at h1,
      rw (list.cons.inj_eq bracket_t.left (a_tl ++ b) bracket_t.left x_tl) at h1,
      rw h1.right.symm,
      rw (show ∀ a : bracket_t, ∀ b : list bracket_t, (a::b).length = b.length + 1, by begin intros, refl, end) at h,
      have := ignores_garbage'' a_tl b n (nat.le_of_succ_le_succ h),
      rw this,
    },
    {
      rw h1.symm,
      rw list.cons_append,
      rw balance_factor,
      rw balance_factor,
      rw (show ∀ a : bracket_t, ∀ b : list bracket_t, (a::b).length = b.length + 1, by begin intros, refl, end) at h,
      have := ignores_garbage'' a_tl b n (nat.le_of_succ_le_succ h),
      rw this,
    },
  },
  rw h1.symm,
  rw list.cons_append,
  cases a_hd,
  repeat {
    rw balance_factor,
    rw balance_factor,
    rw (show ∀ a : bracket_t, ∀ b : list bracket_t, (a::b).length = b.length + 1, by begin intros, refl, end) at h,
    have := ignores_garbage'' a_tl b n (nat.le_of_succ_le_succ h),
    rw this,
  },
end

lemma decompose : ∀ a b : list bracket_t, ∀ n : ℕ, ¬(n ≤ a.length) → balance_factor n (a ++ b) = balance_factor a.length a + balance_factor (n - a.length) b
| a b 0 h := begin
  have h1 := nat.zero_le a.length,
  have := lt_or_eq_of_le h1,
  cases this,
  exact false.elim (h h1),
  rw this.symm,
  norm_num,
  generalize : a ++ b = x,
  have : ∀ x : list bracket_t, balance_factor 0 x = 0 := begin
    intro x,
    cases x,
    rw balance_factor,
    cases x_hd,
    repeat {
      rw balance_factor,
    },
  end,
  rw this,
  rw this,
  rw this,
  norm_num,
end
| a b (n + 1) h := begin
  cases a,
  {
    rw list.nil_append,
    rw (show ([] : list bracket_t).length = 0, by refl),
    norm_num,
    rw balance_factor,
  },
  {
    rw list.cons_append,
    rw (show (a_hd :: a_tl).length = a_tl.length + 1, by refl),
    cases a_hd,
    repeat {
      rw balance_factor,
      rw nat.succ_sub_succ n a_tl.length,
      rw balance_factor,
      rw (show ∀ a : bracket_t, ∀ b : list bracket_t, (a::b).length = b.length + 1, by begin intros, refl, end) at h,
      have : n ≤ a_tl.length → n.succ ≤ a_tl.length.succ := begin
        intro h,
        exact nat.succ_le_succ h,
      end,
      have : ¬n.succ ≤ a_tl.length.succ → ¬n ≤ a_tl.length := begin
        intros h h1,
        have := this h1,
        exact false.elim (h this),
      end,
      have := this h,
      have := decompose a_tl b n this,
      rw this,
      rw int.add_assoc,
    }
  },
end

lemma append_nonnegative_condition : ∀ a b : list bracket_t, (∀ n : ℕ, n ≤ a.length → 0 ≤ balance_factor n a) → (∀ n : ℕ, n ≤ b.length → 0 ≤ balance_factor n b) → (∀ n : ℕ, n ≤ (a ++ b).length → 0 ≤ balance_factor n (a ++ b)) := begin
  intros a b h1 h2 n h3,
  exact if h : n ≤ a.length then begin
    have h4 := h1 n h,
    have := ignores_garbage'' a b n,
    rw this,
    exact h4,
    exact h,
  end else begin
    rw decompose a b n h,
    have := h1 a.length (nat.le_refl _),
    rw list.length_append a b at h3,
    have := (@nat.sub_le_sub_right_iff n (a.length + b.length) a.length (le_self_add)).mpr h3,
    rw (norm_num.sub_nat_pos (a.length + b.length) a.length b.length rfl) at this,
    have := h2 (n - a.length) this,
    exact add_nonneg (by tauto) (by tauto),
  end,
end

lemma balance_factor_append : ∀ a b : list bracket_t, balance_factor_predicate a → balance_factor_predicate b → balance_factor_predicate (a ++ b) := begin
  intros a b h1 h2,
  rw balance_factor_predicate at h1,
  rw balance_factor_predicate at h2,
  rw balance_factor_predicate,
  split,
  rw (append_add_balance_factor _ _).symm,
  rw [h1.left, h2.left],
  norm_num,
  intros n h,
  exact append_nonnegative_condition a b begin
    intros n h,
    have := lt_or_eq_of_le h,
    cases this,
    exact h1.right n this,
    rw this,
    apply le_of_lt_or_eq,
    right,
    exact h1.left.symm,
  end begin
    intros n h,
    have := lt_or_eq_of_le h,
    cases this,
    exact h2.right n this,
    rw this,
    apply le_of_lt_or_eq,
    right,
    exact h2.left.symm,
  end n (le_of_lt h),
end

lemma balanced_implies_balance_factor (string : list bracket_t) : balanced string → balance_factor_predicate string := begin
  intro h,
  induction h with z x c v b q w e r,
  rw balance_factor_predicate,
  rw (show ([] : list bracket_t).length = 0, by refl),
  rw balance_factor,
  split,
  refl,
  intro n,
  intro absurdity,
  exact false.elim ((not_lt_of_ge n.zero_le) absurdity),
  rw balance_factor_predicate,
  rw list.append_assoc,
  rw list.cons_append,
  rw list.nil_append,
  rw (show (bracket_t.left :: (z ++ [bracket_t.right])).length = (z ++ [bracket_t.right]).length + 1, by refl),
  rw balance_factor,
  split,
  rw minus_one z,
  rw balance_factor_predicate at c,
  rw c.left,
  norm_num,
  intro n,
  intro h,
  rw balance_factor_predicate at c,
  have h1 := c.right,
  induction n,
  rw balance_factor,
  have ha := n_ih (nat.lt_trans (nat.lt_succ_self n_n) h),
  rw balance_factor,
  have hb := h1 n_n,
  exact if cond : n_n < z.length then begin
    have hc := hb cond,
    have hd := c.left,
    rw ignores_garbage n_n z cond,
    have := le_trans hc (le_of_lt (int.lt_succ_self (balance_factor n_n z))),
    rw (show (balance_factor n_n z).succ = 1 + balance_factor n_n z, begin
      rw add_comm,
      refl,
    end) at this,
    exact this,
  end else begin
    have := (add_lt_add_iff_right 1).mp h,
    rw list.length_append z [bracket_t.right] at this,
    rw (show [bracket_t.right].length = 1, by refl) at this,
    have := nat.le_of_lt_succ this,
    have := lt_or_eq_of_le this,
    cases this,
    exact false.elim (cond this_1),
    rw this_1,
    rw (ignores_garbage' z).symm,
    rw c.left,
    norm_num,
  end,
  exact balance_factor_append v b e r,
end

def dropN : ∀ string : list bracket_t, ∀ n : ℕ, list bracket_t
| [] _ := []
| x 0 := x
| (head::tail) (n + 1) := dropN tail n

def takeN : ∀ string : list bracket_t, ∀ n : ℕ, list bracket_t
| [] _ := []
| _ 0 := []
| (head::tail) (n + 1) := head::takeN tail n

lemma takeN_calc : ∀ string : list bracket_t, ∀ n : ℕ, balance_factor n string = balance_factor (takeN string n).length (takeN string n)
| [] x := begin
  cases x,
  rw balance_factor,
  have : takeN [] 0 = [] := by refl,
  rw this,
  norm_num,
  rw balance_factor,
  rw balance_factor,
  rw takeN,
  norm_num,
  rw balance_factor,
  norm_num,
end
| x 0 := begin
  have : balance_factor 0 x = 0 := begin
    cases x,
    rw balance_factor,
    rw balance_factor,
  end,
  rw this,
  have : takeN x 0 = [] := begin
    cases x,
    refl,
    rw takeN,
  end,
  rw this,
  norm_num,
  rw balance_factor,
end
| (head::tail) (n + 1) := begin
  cases head,
  repeat {
    rw balance_factor,
    rw takeN,
    rw list.length_cons,
    rw balance_factor,
    have := takeN_calc tail n,
    rw this,
  },
end

lemma lt_of_ne : ∀ n : ℕ, n ≠ 0 → n ≠ 1 → 1 < n
| 0 h h' := false.elim (h rfl)
| 1 h h' := false.elim (h' rfl)
| (n + 2) h h' := by norm_num

lemma preserve_length : ∀ string : list bracket_t, ∀ n : ℕ, n ≤ string.length → (takeN string n).length = n
| [] x h := begin
  have : takeN [] x = [] := begin
    cases x,
    refl,
    refl,
  end,
  rw this,
  norm_num,
  norm_num at h,
  exact h.symm,
end
| x 0 h := begin
  have : takeN x 0 = [] := begin
    cases x,
    refl,
    refl,
  end,
  rw this,
  norm_num,
end
| (head::tail) (n + 1) h := begin
  rw list.length_cons at h,
  rw takeN,
  rw list.length_cons,
  rw nat.succ_inj',
  have := preserve_length tail n begin
    exact nat.succ_le_succ_iff.mp h,
  end,
  exact this,
end

lemma sane : ∀ string : list bracket_t, ∀ n x : ℕ, n < x → balance_factor n string = balance_factor n (takeN string x) := begin
  intro string,
  induction string with head tail sane,
  intros a b c,
  cases a,
  rw balance_factor,
  generalize : takeN list.nil b = h,
  cases h,
  rw balance_factor,
  rw balance_factor,
  rw balance_factor,
  have : takeN [] b = [] := begin
    cases b,
    rw takeN,
    norm_num at c,
    rw takeN,
    norm_num,
  end,
  rw this,
  rw balance_factor,
  intros a b c,
    cases b,
  norm_num at c,
  rw takeN,
  cases a,
  rw balance_factor,
  cases head,
  rw balance_factor,
  rw balance_factor,
  cases head,
  rw balance_factor,
  rw balance_factor,
  have := sane a b (nat.succ_lt_succ_iff.mp c),
  rw this,
  rw balance_factor,
  rw balance_factor,
  have := sane a b (nat.succ_lt_succ_iff.mp c),
  rw this,
end

lemma balance_factor_implies_balanced : ∀ string : list bracket_t, balance_factor_predicate string → balanced string
| string := begin
  intro h,
  rw balance_factor_predicate at h,
  cases h,
  classical,
  exact if hempty : string.length = 0 then begin
    have := list.length_eq_zero.mp hempty,
    rw this,
    exact balanced.empty,
  end else if hsingleton : string.length = 1 then begin
    cases string,
    exact balanced.empty,
    cases string_tl,
    norm_num at h_left,
    cases string_hd,
    rw balance_factor at h_left,
    rw balance_factor at h_left,
    norm_num at h_left,
    rw balance_factor at h_left,
    rw balance_factor at h_left,
    norm_num at h_left,
    rw list.length_cons at hsingleton,
    rw list.length_cons at hsingleton,
    norm_num at hsingleton,
  end else if hnotequal : ∀ (n : ℕ), n < string.length → 0 < n → 0 < balance_factor n string then begin
    have split_things : string = [get_head string] ++ chop_both_ends string ++ [get_tail string] := begin
      clear_except hempty hsingleton,
      cases string,
      norm_num at hempty,
      cases string_hd,
      repeat {
        rw get_head,
        rw chop_both_ends,
        rw chop_other_end,
        rw get_tail,
        split_ifs,
        have : 1 < (bracket_t.left :: string_tl).length := begin
          apply lt_of_ne, assumption, assumption,
        end,
        norm_num at this,
        exact false.elim (ne_of_lt this h.symm),
        rw chop_head,
        rw list.append_assoc,
        rw reconstitute string_tl (pos_iff_ne_zero.mpr h),
        rw list.cons_append,
        rw list.nil_append,
      },
    end,
    have := head_open (chop_both_ends string ++ [get_tail string]) (get_head string) begin
      rw list.singleton_append.symm,
      rw (list.append_assoc _ _ _).symm,
      rw split_things.symm,
      rw balance_factor_predicate,
      tauto,
    end,
    rw this at split_things,
    clear this,
    have := tail_close ([bracket_t.left] ++ chop_both_ends string) (get_tail string) begin
      rw split_things.symm,
      rw balance_factor_predicate,
      tauto,
    end,
    rw this at split_things,
    clear this,
    rw split_things,
    apply balanced.wrap _,
    have := have wf : (chop_both_ends string).length < string.length, from begin
      have : ∀ string : list bracket_t, 1 < string.length → (chop_both_ends string).length + 2 = string.length := begin
        clear_except,
        intros string h,
        cases string,
        norm_num at h,
        rw chop_both_ends,
        rw chop_other_end,
        split_ifs,
        have : string_tl = [] := list.length_eq_zero.mp h_1,
        rw this at h,
        norm_num at h,
        rw chop_head,
        have := reconstitute string_tl (pos_iff_ne_zero.mpr h_1),
        norm_num,
        conv begin
          to_rhs,
          rw this.symm,
        end,
        rw list.length_append,
        norm_num,
      end,
      have := this string begin
        apply lt_of_ne _ _ _, assumption, assumption,
      end,
      rw this.symm,
      norm_num,
    end, balance_factor_implies_balanced (chop_both_ends string) begin
      rw balance_factor_predicate,
      split,
      have help := append_add_balance_factor ([bracket_t.left] ++ chop_both_ends string) [bracket_t.right],
      rw split_things.symm at help,
      rw (append_add_balance_factor [bracket_t.left] (chop_both_ends string)).symm at help,
      norm_num at help,
      rw balance_factor at help,
      rw balance_factor at help,
      rw balance_factor at help,
      norm_num at help,
      rw h_left at help,
      exact help,
      intros n limit,
      have := hnotequal (n + 1) begin
        have : ∀ string : list bracket_t, 1 < string.length → (chop_both_ends string).length + 2 = string.length := begin
          clear_except,
          intros string h,
          cases string,
          norm_num at h,
          rw chop_both_ends,
          rw chop_other_end,
          split_ifs,
          have : string_tl = [] := list.length_eq_zero.mp h_1,
          rw this at h,
          norm_num at h,
          rw chop_head,
          have := reconstitute string_tl (pos_iff_ne_zero.mpr h_1),
          norm_num,
          conv begin
            to_rhs,
            rw this.symm,
          end,
          rw list.length_append,
          norm_num,
        end,
        have := this string begin
          apply lt_of_ne _ _ _, assumption, assumption,
        end,
        rw this.symm,
        apply nat.succ_lt_succ,
        exact limit.trans (nat.lt_succ_self _),
      end (nat.succ_pos n),
      rw split_things at this,
      rw list.append_assoc at this,
      rw list.singleton_append at this,
      rw balance_factor at this,
      have := int.add_one_le_iff.mpr this,
      norm_num at this,
      have help := ignores_garbage n (chop_both_ends string) limit,
      rw help at this,
      exact this,
    end,
    exact this,
  end else begin
    push_neg at hnotequal,
    cases hnotequal with x h1,
    have hwellfounded := h1.left,
    have := le_antisymm h1.right.right (h_right x h1.left),
    have left := have wf : (takeN string x).length < string.length, from begin
      clear_except hwellfounded,
      induction string generalizing x,
      norm_num at hwellfounded,
      norm_num at hwellfounded,
      norm_num,
      cases x,
      rw takeN,
      norm_num,
      rw takeN,
      have := string_ih x (nat.succ_lt_succ_iff.mp hwellfounded),
      norm_num,
      exact this,
    end, balance_factor_implies_balanced (takeN string x) begin
      rw balance_factor_predicate,
      split,
      rw (takeN_calc _ _).symm,
      exact this,
      have := preserve_length string x (le_of_lt hwellfounded),
      rw this,
      intros n h',
      have := h_right n (lt_trans h' hwellfounded),
      rw (sane string n x h').symm,
      exact this,
    end,
    have right := have wf : (dropN string x).length < string.length, from begin
      have := h1.right.left,
      clear_except hempty this,
      induction string generalizing x this,
      norm_num at hempty,
      cases x,
      exact false.elim (@nat.le_lt_antisymm 0 0 (rfl.ge) this),
      rw dropN,
      norm_num,
      have to_split := em (string_tl.length = 0),
      cases to_split,
      rw to_split,
      norm_num,
      rw list.length_eq_zero.mp to_split,
      have : dropN [] x = [] := begin
        cases x, refl, rw dropN, clear_except,
        exact nat.succ_ne_zero x,
      end,
      rw this,
      norm_num,
      have := string_ih to_split x,
      have split2 := em (x = 0),
      cases split2,
      rw split2,
      have : dropN string_tl 0 = string_tl := begin
        cases string_tl,
        refl, rw dropN,
      end,
      rw this,
      exact lt_add_one (list.length string_tl),
      have := (this (pos_iff_ne_zero.mpr split2)).trans (nat.lt_succ_self string_tl.length),
      exact this,
    end, balance_factor_implies_balanced (dropN string x) begin
      rw balance_factor_predicate,
      split,
      have : ∀ string : list bracket_t, ∀ x : ℕ, takeN string x ++ dropN string x = string := begin
        clear_except,
        intros,
        induction string generalizing x,
        have : takeN [] x = [] := begin
          cases x,
          refl,
          refl,
        end,
        rw this,
        have : dropN [] x = [] := begin
          cases x,
          refl,
          refl,
        end,
        rw this,
        refl,
        cases x,
        rw takeN,
        rw dropN,
        rw list.nil_append,
        rw takeN,
        rw dropN,
        rw list.cons_append,
        rw list.cons_inj,
        exact string_ih x,
      end,
      have : ∀ string : list bracket_t, ∀ x : ℕ, balance_factor (dropN string x).length (dropN string x) + balance_factor (takeN string x).length (takeN string x) = balance_factor string.length string := begin
        clear_except this,
        intros,
        have destruct := (this string x).symm,
        conv begin
          to_rhs,
          rw destruct,
        end,
        have := append_add_balance_factor (takeN string x) (dropN string x),
        rw add_comm,
        exact this,
      end,
      have := this string x,
      rw h_left at this,
      have help := takeN_calc string x,
      rw (show balance_factor x string = 0, by assumption) at help,
      rw help.symm at this,
      norm_num at this,
      exact this,
      intros n h,
      have := h_right (x + n),
      have : ∀ string : list bracket_t, ∀ x : ℕ, x < string.length → (dropN string x).length = string.length - x := begin
        clear_except,
        intros string x h,
        induction string generalizing x,
        norm_num at h,
        cases x,
        rw dropN,
        norm_num,
        rw dropN,
        rw list.length_cons,
        rw list.length_cons at h,
        have := string_ih x (nat.succ_lt_succ_iff.mp h),
        rw this,
        have := nat.succ_sub_succ string_tl.length x,
        rw this,
      end,
      rw this string x hwellfounded at h,
      clear this,
      have := this (nat.add_lt_of_lt_sub_left h),
      have help : ∀ string : list bracket_t, ∀ x n : ℕ, balance_factor (takeN string x).length (takeN string x) + balance_factor n (dropN string x) = balance_factor (x + n) string := begin
        clear_except,
        intros,
        induction string generalizing x n,
        have : takeN [] x = [] := begin
          cases x,
          refl,
          refl,
        end,
        rw this,
        have : dropN [] x = [] := begin
          cases x,
          refl,
          refl,
        end,
        rw this,
        norm_num,
        have : ∀ x : ℕ, balance_factor x [] = 0 := begin
          clear_except,
          intros,
          cases x,
          refl,
          refl,
        end,
        rw this,
        rw this,
        rw this,
        norm_num,
        cases x,
        rw takeN,
        rw dropN,
        norm_num,
        rw balance_factor,
        rw takeN,
        rw dropN,
        rw nat.succ_add,
        cases string_hd,
        rw balance_factor,
        norm_num,
        rw balance_factor,
        have := string_ih x n,
        rw this.symm,
        have := int.add_assoc 1 (balance_factor (takeN string_tl x).length (takeN string_tl x)) (balance_factor n (dropN string_tl x)),
        conv begin
          to_lhs,
          rw this,
        end,
        rw balance_factor,
        norm_num,
        rw balance_factor,
        rw int.add_assoc,
        have := string_ih x n,
        rw this,
      end,
      rw (help string x n).symm at this,
      rw ((show balance_factor x string = 0, by assumption).symm.trans (takeN_calc string x)).symm at this,
      norm_num at this,
      exact this,
    end,
    have goal := balanced.append _ _ left right,
    have : ∀ string : list bracket_t, ∀ x : ℕ, takeN string x ++ dropN string x = string := begin
      clear_except,
      intros,
      induction string generalizing x,
      have : takeN [] x = [] := begin
        cases x,
        refl,
        refl,
      end,
      rw this,
      have : dropN [] x = [] := begin
        cases x,
        refl,
        refl,
      end,
      rw this,
      refl,
      cases x,
      rw takeN,
      rw dropN,
      rw list.nil_append,
      rw takeN,
      rw dropN,
      rw list.cons_append,
      rw list.cons_inj,
      exact string_ih x,
    end,
    have := this string x,
    rw this at goal,
    exact goal,
  end,
end
using_well_founded {
  rel_tac := λ_ _, `[exact ⟨_, inv_image.wf list.length nat.lt_wf⟩],
  dec_tac := tactic.assumption }

lemma balanced_iff_balance_factor (string : list bracket_t) : balanced string ↔ balance_factor_predicate string := begin
  split,
  exact balanced_implies_balance_factor _,
  exact balance_factor_implies_balanced _,
end