74 (#281)

This PR solves problem 74.

Author: datokrat

HumanEvalLean/HumanEval74.lean

@@ -1,7 +1,50 @@
 module
 
-def total_match : Unit :=
-  ()
+public import Std
+open Std
+
+public section
+
+/-! ## Missing API -/
+
+def Std.Iter.sum [Iterator α Id Nat] [IteratorLoop α Id Id] (it : Iter (α := α) Nat) :
+    Nat :=
+  it.fold (init := 0) (· + ·)
+
+theorem Std.Iter.sum_toList [Iterator α Id Nat] [IteratorLoop α Id Id]
+    [LawfulIteratorLoop α Id Id] [Iterators.Finite α Id] {it : Iter (α := α) Nat} :
+    it.toList.sum = it.sum := by
+  simp [sum, List.sum_eq_foldl, foldl_toList]
+
+theorem Std.Iter.sum_toArray [Iterator α Id Nat] [IteratorLoop α Id Id]
+    [LawfulIteratorLoop α Id Id] [Iterators.Finite α Id] {it : Iter (α := α) Nat} :
+    it.toArray.sum = it.sum := by
+  simp [← toArray_toList, sum_toList]
+
+/-! ## Implementation -/
+
+def totalMatch (xs ys : Array String) : Array String :=
+  minOn (fun zs => (zs.iter.map (·.length)).sum) xs ys
+
+/-! ## Tests -/
+
+example : totalMatch #[] #[] = #[] := by native_decide
+example : totalMatch #["hi", "admin"] #["hi", "hi"] = #["hi", "hi"] := by native_decide
+example : totalMatch #["hi", "admin"] #["hi", "hi", "admin", "project"] = #["hi", "admin"] := by
+  native_decide
+example : totalMatch #["4"] #["1", "2", "3", "4", "5"] = #["4"] := by native_decide
+example : totalMatch #["hi", "admin"] #["hI", "Hi"] = #["hI", "Hi"] := by native_decide
+example : totalMatch #["hi", "admin"] #["hI", "hi", "hi"] = #["hI", "hi", "hi"] := by
+  native_decide
+example : totalMatch #["hi", "admin"] #["hI", "hi", "hii"] = #["hi", "admin"] := by native_decide
+example : totalMatch #[] #["this"] = #[] := by native_decide
+example : totalMatch #["this"] #[] = #[] := by native_decide
+
+/-! ## Verification -/
+
+theorem totalMatch_spec :
+    totalMatch xs ys = if (xs.map (·.length)).sum ≤ (ys.map (·.length)).sum then xs else ys := by
+  simp [totalMatch, ← Iter.sum_toArray, minOn_eq_if]
 
 /-!
 ## Prompt
@@ -10,7 +53,7 @@ def total_match : Unit :=
 
 def total_match(lst1, lst2):
     '''
-    Write a function that accepts two lists of strings and returns the list that has 
+    Write a function that accepts two lists of strings and returns the list that has
     total number of chars in the all strings of the list less than the other list.
 
     if the two lists have the same number of chars, return the first list.
@@ -30,11 +73,11 @@ def total_match(lst1, lst2):
     l1 = 0
     for st in lst1:
         l1 += len(st)
-    
+
     l2 = 0
     for st in lst2:
         l2 += len(st)
-    
+
     if l1 <= l2:
         return lst1
     else:
@@ -63,4 +106,4 @@ def check(candidate):
     assert candidate(['this'], []) == []
 
 ```
--/
+-/