Update 125 and 129

src/lean4/human_eval/problem_125.lean

@@ -58,8 +58,9 @@ let rec is_valid_path (k': Nat) (path: List Nat) (grid: List (List Nat)) : Prop
 let spec (result: List Nat) :=
   let n := grid.length;
   (∀ i, i < n → (grid.get! i).length = n) →
-  (∀ i j, i < n → j < n ↔ ((grid.get! i).get! j) ∈ [1, n^2]) →
-  is_valid_path k result grid ∧ (∀ path, is_valid_path k path grid → lexographically_less result path);
+  (∀ i j, i < n → j < n → 1 ≤ (grid.get! i).get! j ∧ (grid.get! i).get! j ≤ n^2) →
+  grid.flatten.Nodup →
+  is_valid_path k result grid ∧ (∀ path, is_valid_path k path grid ∧ path ≠ result → lexographically_less result path)
 -- program terminates
 ∃ result, impl grid k = result ∧
 -- return value satisfies spec

src/lean4/human_eval/problem_129.lean

@@ -2,7 +2,7 @@ import Imports.AllImports
 
 -- start_def problem_details
 /--
-function_signature: "def split_words(txt)"
+function_signature: "def split_words(txt: str) -> Union[List[str], int]"
 docstring: |
     Given a string of words, return a list of words split on whitespace, if no whitespaces exists in the text you
     should split on commas ',' if no commas exists you should return the number of lower-case letters with odd order in the
@@ -16,44 +16,59 @@ test_cases:
     expected_output: 3
 -/
 -- end_def problem_details
-
 -- start_def problem_spec
 def problem_spec
 -- function signature
--- return a tuple of Option (List String) and Option Nat
-(impl: String → Option (List String) × Option Nat)
+(impl: String → List String ⊕ Int)
 -- inputs
-(text: String) :=
+(txt: String) :=
 -- spec
-let spec (result: Option (List String) × Option Nat) :=
-  -- both cannot be None
-  let words := result.fst;
-  let ord := result.snd;
-  0 < text.length →
-  ¬ (words = none ∧ ord = none) ∧
-    (words = none ↔ ∀ ch, ch ∈ text.toList →  (ch = ',' ∨ ch = ' ')) ∧
-    (∀ num, ord = some num → (text.get! 0).toNat = num) ∧
-    (∀ lst, words = some lst → ∀ i, i < lst.length →
-      let str := lst.get! i;
-      text.containsSubstr str) ∧
-    (∀ lst, words = some lst →
-      let first := text.takeWhile (fun c => c ≠ ',' ∧ c ≠ ' ');
-      let nextImpl := impl (text.drop (first.length + 1));
-      let nextWords := nextImpl.fst;
-      (∃ nextLst, nextWords = some nextLst ∧
-        lst = [first] ++ nextLst))
--- program terminates
-∃ result, impl text = result ∧
+let spec (result : List String ⊕ Int) :=
+match result with
+| Sum.inl lst =>
+  if txt.toList.any (fun x => x.isWhitespace) then
+    ∃ (left right: String) (whitespace: Char),
+      whitespace.isWhitespace ∧
+      left ++ whitespace.toString ++ right = txt ∧
+      (∀ c ∈ left.toList, ¬ c.isWhitespace) ∧
+      left = lst[0]! ∧
+      (if right.toList.any (fun x => x.isWhitespace) then
+        impl right = Sum.inl (lst.drop 1)
+      else
+        lst.drop 1 = (if right = "" then [] else [right]))
+  else if txt.toList.any (fun x => x = ',') then
+    ∃ left right,
+      left ++ "," ++ right = txt ∧
+      ',' ∉ left.toList ∧
+      left = lst[0]! ∧
+      (if right.toList.any (fun x => x = ',') then
+        impl right = Sum.inl (lst.drop 1)
+      else
+        lst.drop 1 = (if right = "" then [] else [right]))
+  else
+    false
+| Sum.inr count =>
+  ¬ (txt.toList.any (fun x => x.isWhitespace) ∨ txt.toList.any (fun x => x = ',')) ∧
+  (txt = "" → count = 0) ∧
+  (txt ≠ "" →
+    let letter := txt.get ⟨0⟩;
+    let order := letter.toNat - 'a'.toNat;
+    if letter.isLower ∧ Odd order then
+      Sum.inr (count - 1) = impl (txt.drop 1)
+    else
+      Sum.inr (count) = impl (txt.drop 1))
+-- program termination
+∃ result, impl txt = result ∧
 -- return value satisfies spec
 spec result
 -- end_def problem_spec
 
 -- start_def generated_spec
 def generated_spec
 -- function signature
-(impl: String → Option (List String) × Option Nat)
+(impl: String → List String ⊕ Int)
 -- inputs
-(text: String) : Prop :=
+(lst: String) : Prop :=
 -- end_def generated_spec
 --start_def generated_spec_body
 sorry
@@ -62,32 +77,30 @@ sorry
 -- start_def spec_isomorphism
 theorem spec_isomorphism:
 ∀ impl,
-(∀ text, problem_spec impl text) ↔
-(∀ text, generated_spec impl text) :=
+(∀ txt, problem_spec impl txt) ↔
+(∀ txt, generated_spec impl txt) :=
 -- end_def spec_isomorphism
 -- start_def spec_isomorphism_proof
 sorry
 -- end_def spec_isomorphism_proof
 
 -- start_def implementation_signature
-def implementation (text: String) : Option (List String) × Option Nat :=
+def implementation (txt: String) : List String ⊕ Int :=
 -- end_def implementation_signature
 -- start_def implementation
 sorry
 -- end_def implementation
 
--- Uncomment the following test cases after implementing the function
 -- start_def test_cases
--- #test implementation "Hello world!" = (some ["Hello", "world!"], none)
--- #test implementation "Hello,world!" = (some ["Hello", "world!"], none)
--- #test implementation "abcdef" = (none, some 3)
+-- #test implementation "Hello world!" = Sum.inl ["Hello", "world!"]
+-- #test implementation "Hello,world!" = Sum.inl ["Hello", "world!"]
+-- #test implementation "abcdef" = Sum.inr 3
 -- end_def test_cases
 
-
 -- start_def correctness_definition
 theorem correctness
-(text: String)
-: problem_spec implementation text :=
+(txt: String)
+: problem_spec implementation txt :=
 -- end_def correctness_definition
 -- start_def correctness_proof
 sorry