Lean golf: Balanced Bracket Sequence

Question

Ungolfed, ugly, horrible proof to help you make progress on this challenge: https://gist.github.com/huynhtrankhanh/dff7036a45073735305caedc891dedf2

A bracket sequence is a string that consists of the characters ( and ). There are two definitions of a balanced bracket sequence.

Definition 1

• The empty string is balanced.
• If a string x is balanced, "(" + x + ")" is also balanced.
• If x and y are two balanced strings, x + y is also balanced.

Definition 2

The balance factor of a string is the difference between the number of ( characters and the number of ) characters. A string is balanced if its balance factor is zero and the balance factor of every prefix is nonnegative.

Your task is to prove the two definitions are equivalent in the Lean theorem prover, specifically Lean 3. You're allowed to use the mathlib library.

Formalized statement:

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

lemma X (string : list bracket_t) : balanced string ↔ balance_factor_predicate string := begin
  -- your proof here
  sorry,
end

This is code-golf, shortest code in bytes wins.

How to solve this challenge:

• The balanced string -> balance_factor_predicate part can be solved relatively easily by "running at it"—do induction on the balanced string predicate, keep your head, and you are done.
• The balance_factor_predicate -> balanced string part is slightly harder. I used well founded recursion to prove this part. I cleverly mimicked each constructor of the balanced predicate and stitched the constructors together with well founded recursion. Read the complete proof for more details.

Remember to ping me in chat (The Nineteenth Byte or The Lean-to) if you need help. Thanks.