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 thebalanced 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 thebalanced
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.
length
parameter inbalance_factor
to actually be equal to the length ofstring
? Or maybe it could be implemented assum(map foofun string)
or something like that? \$\endgroup\$