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
). There are two definitions of a balanced bracket sequence.
- The empty string is balanced.
- If a string x is balanced,
"(" + x + ")"is also balanced.
- If x and y are two balanced strings,
x + yis also balanced.
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.
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:
balanced string -> balance_factor_predicatepart can be solved relatively easily by "running at it"—do induction on the
balanced stringpredicate, keep your head, and you are done.
balance_factor_predicate -> balanced stringpart is slightly harder. I used well founded recursion to prove this part. I cleverly mimicked each constructor of the
balancedpredicate 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.