6

HumanEvalLean/Common/Brackets.lean

@@ -64,12 +64,53 @@ theorem List.take_cons_eq_if {l : List α} {a : α} {n : Nat} :
 theorem List.take_singleton {a : α} {n : Nat} : [a].take n = if 0 < n then [a] else [] := by
   rw [List.take_cons_eq_if, List.take_nil]
 
-def minBalance (l : List Paren) : Int :=
-  (0...=l.length).toList.map (fun k => balance (l.take k)) |>.min (by simp)
+def maxBalance (l : List Paren) : Int :=
+  (0...=l.length).toList.map (fun k => balance (l.take k)) |>.max (by simp)
 
 attribute [-simp] Nat.toList_rcc_eq_append
 attribute [simp] Std.Rcc.mem_toList_iff_mem Std.Rcc.mem_iff
 
+@[grind! .]
+theorem maxBalance_nonneg (l : List Paren) : 0 ≤ maxBalance l := by
+  rw [maxBalance]
+  apply List.le_max_of_mem
+  simp only [List.mem_map, Std.Rcc.mem_toList_iff_mem, Std.Rcc.mem_iff, Nat.zero_le, true_and]
+  exact ⟨0, by simp⟩
+
+@[simp]
+theorem maxBalance_nil : maxBalance [] = 0 := by
+  simp [maxBalance]
+
+attribute [simp] Nat.le_max_left Nat.le_max_right
+
+@[simp]
+theorem maxBalance_cons {l : List Paren} {p : Paren} :
+    maxBalance (p :: l) = max 0 (p.toInt + maxBalance l) := by
+  rw [maxBalance]
+  simp [Nat.toList_rcc_succ_right_eq_cons_map]
+  rw [List.max_cons, List.max?_eq_some_max (by simp)]
+  simp only [Option.elim_some, maxBalance, ← (List.max_map_eq_max (f := (p.toInt + ·)) (by simp)),
+    List.map_map]
+  congr 1
+
+@[simp]
+theorem maxBalance_append_singleton {l : List Paren} {p : Paren} :
+    maxBalance (l ++ [p]) = max (maxBalance l) (balance l + p.toInt) := by
+  induction l with
+  | nil => simp
+  | cons hd tl ih =>
+    simp only [List.cons_append, maxBalance_cons, ih, balance_cons, Int.max_assoc]
+    grind
+
+theorem maxBalance_append {l m : List Paren} :
+    maxBalance (l ++ m) = max (maxBalance l) (balance l + maxBalance m) := by
+  induction l with
+  | nil => simpa using (Int.max_eq_right (maxBalance_nonneg _)).symm
+  | cons p l ih => grind [maxBalance_cons]
+
+def minBalance (l : List Paren) : Int :=
+  (0...=l.length).toList.map (fun k => balance (l.take k)) |>.min (by simp)
+
 @[grind! .]
 theorem minBalance_nonpos (l : List Paren) : minBalance l ≤ 0 := by
   rw [minBalance]

HumanEvalLean/HumanEval6.lean

@@ -1,7 +1,79 @@
 module
 
-def parse_nested_parens : Unit :=
-  ()
+import HumanEvalLean.Common.Brackets
+import Std.Tactic.Do
+
+def computeMaxDepth (s : String.Slice) : Int := Id.run do
+  let mut depth : Int := 0
+  let mut maxDepth : Int := 0
+  for c in s do
+    if c == '(' then
+      depth := depth + 1
+      maxDepth := max maxDepth depth
+    else if c == ')' then
+      depth := depth - 1
+      maxDepth := max maxDepth depth
+  return maxDepth
+
+def parseNestedParens (parenString : String.Slice) : Array Int :=
+  (parenString.split ' ').map computeMaxDepth |>.toArray
+
+example : parseNestedParens "(()()) ((())) () ((())()())" = #[2, 3, 1, 3] := by native_decide
+example : parseNestedParens "() (()) ((())) (((())))" = #[1, 2, 3, 4] := by native_decide
+example : parseNestedParens "(()(())((())))" = #[4] := by native_decide
+
+open Std.Do
+
+set_option mvcgen.warning false
+theorem computeMaxDepth_eq {s : String.Slice} :
+    computeMaxDepth s = maxBalance (parens '(' ')' s.copy) := by
+  generalize hwp : computeMaxDepth s = w
+  apply Std.Do.Id.of_wp_run_eq hwp
+  mvcgen
+  case inv => exact (⇓(pos, ⟨bal, maxBal⟩) => ⌜∀ (t₁ t₂ : String), pos.Splits t₁ t₂ →
+    bal = balance (parens '(' ')' t₁) ∧ maxBal = maxBalance (parens '(' ')' t₁)⌝)
+  next pos _ hp bal minBal h newBal newMinBal ih =>
+    simp only [↓Char.isValue, SPred.down_pure] at ⊢ ih
+    intro t₁ t₂ hsp
+    obtain ⟨t₁, rfl⟩ := hsp.exists_eq_append_singleton
+    simp only [↓Char.isValue, beq_iff_eq] at h
+    simp only [↓Char.isValue, h, String.append_singleton, parens_push, ↓reduceIte,
+      Option.toList_some, balance_append, balance_cons, Paren.toInt_open, balance_nil, Int.add_zero,
+      maxBalance_append_singleton]
+    have := ih _ _ hsp.of_next
+    grind
+  next pos _ hp bal minBal h₁ h₂ newBal newMinBal ih =>
+    simp only [↓Char.isValue, SPred.down_pure] at ⊢ ih
+    intro t₁ t₂ hsp
+    obtain ⟨t₁, rfl⟩ := hsp.exists_eq_append_singleton
+    simp only [↓Char.isValue, beq_iff_eq] at h₂
+    simp only [↓Char.isValue, h₂, String.append_singleton, parens_push, Char.reduceEq, ↓reduceIte,
+      Option.toList_some, balance_append, balance_cons, Paren.toInt_close, Int.reduceNeg,
+      balance_nil, Int.add_zero, maxBalance_append_singleton]
+    have := ih _ _ hsp.of_next
+    grind
+  next pos _ hp bal minBal h₁ h₂ ih =>
+    simp only [↓Char.isValue, SPred.down_pure] at ⊢ ih
+    intro t₁ t₂ hsp
+    obtain ⟨t₁, rfl⟩ := hsp.exists_eq_append_singleton
+    simp only [↓Char.isValue, beq_iff_eq] at h₁ h₂
+    simp only [↓Char.isValue, String.append_singleton, parens_push, h₁, ↓reduceIte, h₂,
+      Option.toList_none, List.append_nil]
+    have := ih _ _ hsp.of_next
+    grind
+  next => simp
+  next => simp_all
+
+theorem computeMaxDepth_eq_comp : computeMaxDepth = (maxBalance <| parens '(' ')' ·) ∘ String.Slice.copy := by
+  funext s
+  exact computeMaxDepth_eq
+
+theorem parseNestedParens_intercalate (l : List String) (hl : l ≠ [])
+    (hl' : ∀ s ∈ l, ∀ c ∈ s.toList, c = '(' ∨ c = ')')  :
+    parseNestedParens (" ".intercalate l) = (l.map (maxBalance <| parens '(' ')' ·)).toArray := by
+  simp only [parseNestedParens, ↓Char.isValue, Std.Iter.toArray_map, computeMaxDepth_eq_comp,
+    ← Array.toList_inj, Array.toList_map, Std.Iter.toList_toArray, ← List.map_map]
+  erw [← String.split_eq_split_toSlice, String.toList_split_intercalate (by grind), if_neg hl]
 
 /-!
 ## Prompt
@@ -54,4 +126,4 @@ def check(candidate):
     assert candidate('() (()) ((())) (((())))') == [1, 2, 3, 4]
     assert candidate('(()(())((())))') == [4]
 ```
--/
+-/