12
\$\begingroup\$

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 , 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.

Improve this question
\$\endgroup\$
1
  • 1
    \$\begingroup\$ Would it be possible to constrain the length parameter in balance_factor to actually be equal to the length of string? Or maybe it could be implemented as sum(map foofun string) or something like that? \$\endgroup\$ Commented Oct 9, 2021 at 20:12

1 Answer 1

Reset to default
3
\$\begingroup\$

Lean 4 (non-competing), 1057 bytes

This is non-competing due to using Lean 4, instead of Lean 3 as required in the question. Specifically this utilizes the builtin grind tactic a lot, which was only released at the beginning of this month. I am not counting the size of the formalized statement in the byte count, only stuff I added (and the import Mathlib line).

import Mathlib

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

attribute [grind,simp] balance_factor balance_factor_predicate
macro"g":tactic=>`(tactic|first|grind|simp_all)
@[simp,grind]
theorem A:∀n≤a.length,balance_factor n (a++b)=balance_factor n a:=by
induction' a with a
g
rintro(_|_)<;>cases a<;>g
@[simp,grind]
lemma B:∀n>a.length,balance_factor n (a++b)=balance_factor a.length a+balance_factor (n-a.length) b:=by
induction' a with a
g
rintro(_|_)<;>cases a<;>g
lemma X (string : List bracket_t) : balanced string ↔ balance_factor_predicate string :=
⟨λh↦by induction h;g;simp_all;rintro(_|_)_<;>g;g,λh↦by
by_cases H:∃n<string.length,0<n∧balance_factor n string=0
obtain⟨n,o,t⟩:=H
obtain⟨a,b,rfl,rfl⟩:∃a b,a++b=_∧a.length=n:= ⟨_,_,string.take_append_drop n,by g⟩
simp at o h
apply balanced.append<;>(rw[X];g;intro n;have:=h.2 n;have:=h.2 (a.length + n);g)
rcases string with _|⟨a,b⟩<;>simp_all[balanced.empty]
have:0≤balance_factor 1 (a::b):=by g
cases a<;>g
cases b using List.reverseRecOn<;>g
rename_i b a
cases a
have:=h.2 (b.length+1)
g
apply balanced.wrap
rw [X]
g
intro n
have:=h.2 (n+1)
g⟩
termination_by string.length
decreasing_by
g;g;g

Try it online!

Ungolfed:

import Mathlib

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 : ℕ → 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

attribute [grind,simp] balance_factor balance_factor_predicate

@[simp,grind]
lemma balance_factor_of_le  : ∀ n ≤ a.length, balance_factor n (a ++ b) = balance_factor n a := by
  induction' a with a _
  · simp
  · rintro (_|_) <;> cases a <;> grind

@[simp,grind]
lemma balance_factor_of_lt : ∀ n > a.length, balance_factor n (a ++ b) = balance_factor a.length a + balance_factor (n - a.length) b := by
  induction' a with a _
  · simp
  · rintro (_|_) <;> cases a <;> grind

lemma X (string : List bracket_t) : balanced string ↔ balance_factor_predicate string := by
  constructor <;> intro h
  · induction h
    · grind
    · simp_all
      rintro (_|_) _ <;> grind
    · grind
  · by_cases hs : ∃ n < string.length, 0 < n ∧ balance_factor n string = 0
    · obtain ⟨n, h1, h2⟩ := hs
      obtain ⟨a, b, rfl, rfl⟩ : ∃ a b, a ++ b = string ∧ a.length = n := ⟨_, _, string.take_append_drop n, by grind⟩
      simp at h1
      apply balanced.append <;> rw [X]
      · simp at h
        simp_all
        intro n
        have := h.2 n
        grind
      · simp at h
        simp_all
        intro n
        have := h.2 (a.length + n)
        grind
    · rcases string with _|⟨a,b⟩ <;> simp_all [balanced.empty]
      have : 0 ≤ balance_factor 1 (a :: b) := by grind
      cases a <;> simp_all
      cases b using List.reverseRecOn <;> simp_all [-List.cons_append_fun, ← List.cons_append]
      rename_i b a
      cases a
      · have := h.2 (b.length + 1) (by grind)
        grind
      · apply balanced.wrap
        rw [X]
        simp_all
        intro n _
        have := h.2 (n + 1) (by grind)
        grind
termination_by string.length
decreasing_by
  all_goals grind

Try it online!

Improve this answer
\$\endgroup\$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.