Bug fix of specs/implementations in benchmark

datasets/verina/verina_advanced_10/task.lean

@@ -15,7 +15,8 @@ def findExponents_precond (n : Nat) (primes : List Nat) : Prop :=
   n > 0 ∧
   primes.length > 0 ∧
   primes.all (fun p => Nat.Prime p) ∧
-  List.Nodup primes
+  List.Nodup primes ∧
+  (∀ p : Nat, Nat.Prime p → p ∣ n → p ∈ primes)
   -- !benchmark @end precond
 
 

datasets/verina/verina_advanced_12/task.lean

@@ -43,7 +43,10 @@ def firstDuplicate_postcond (lst : List Int) (result: Option Int) (h_precond : f
   | none => List.Nodup lst
   | some x =>
     lst.count x > 1 ∧
-    (lst.filter (fun y => lst.count y > 1)).head? = some x
+    ∃ i : Nat, i < lst.length ∧
+      lst[i]? = some x ∧
+      x ∈ lst.take i ∧
+      ∀ j : Nat, j < i → ∀ y, lst[j]? = some y → y ∉ lst.take j
   -- !benchmark @end postcond
 
 

datasets/verina/verina_advanced_15/task.lean

@@ -23,44 +23,24 @@ def increasingTriplet_precond (nums : List Int) : Prop :=
 
 def increasingTriplet (nums : List Int) (h_precond : increasingTriplet_precond (nums)) : Bool :=
   -- !benchmark @start code
-  -- must have at least 3 elements to form a triplet
-  let rec lengthCheck : List Int → Nat → Nat
-    | [], acc => acc
-    | _ :: rest, acc => lengthCheck rest (acc + 1)
-
-  let len := lengthCheck nums 0
-
-  if len < 3 then
-    false
-  else
-    -- scan for increasing triplet
-    let rec loop (xs : List Int) (first : Int) (second : Int) : Bool :=
-      match xs with
-      | [] => false
-      | x :: rest =>
-        let nextFirst := if x ≤ first then x else first
-        let nextSecond := if x > first ∧ x ≤ second then x else second
-        if x ≤ first then
-          loop rest nextFirst second
-        else if x ≤ second then
-          loop rest first nextSecond
-        else
-          true  -- found triplet
-    match nums with
+  -- scan for increasing triplet using Option for second to handle "not found yet"
+  let rec loop (xs : List Int) (first : Int) (secondOpt : Option Int) : Bool :=
+    match xs with
     | [] => false
-    | _ :: rest1 =>
-      match rest1 with
-      | [] => false
-      | _ :: rest2 =>
-        match rest2 with
-        | [] => false
-        | _ =>
-          -- Use Option to handle unbounded Int values instead of magic number
-          let initFirst := nums.head?
-          let initSecond := nums.head?
-          match initFirst, initSecond with
-          | some f, some s => loop nums f s
-          | _, _ => false
+    | x :: rest =>
+      if x ≤ first then
+        loop rest x secondOpt
+      else
+        match secondOpt with
+        | none => loop rest first (some x)
+        | some second =>
+          if x ≤ second then
+            loop rest first (some x)
+          else
+            true  -- found triplet
+  match nums with
+  | [] => false
+  | x :: rest => loop rest x none
   -- !benchmark @end code
 
 

datasets/verina/verina_advanced_44/task.lean

@@ -12,7 +12,7 @@
 @[reducible]
 def maxSubarraySumDivisibleByK_precond (arr : Array Int) (k : Int) : Prop :=
   -- !benchmark @start precond
-  k > 0
+  k > 1
   -- !benchmark @end precond
 
 
@@ -24,7 +24,7 @@ def maxSubarraySumDivisibleByK_precond (arr : Array Int) (k : Int) : Prop :=
 def maxSubarraySumDivisibleByK (arr : Array Int) (k : Int) : Int :=
   -- !benchmark @start code
   let n := arr.size
-  if n = 0 || k = 0 then 0
+  if n = 0 || k ≤ 0 then 0
   else
     --compute prefix sums for efficient subarray sum calculation
     let prefixSums := Id.run do
@@ -39,7 +39,7 @@ def maxSubarraySumDivisibleByK (arr : Array Int) (k : Int) : Int :=
         minElem := min minElem elem
       minElem
     let maxSum := Id.run do
-      let mut maxSum := minElem - 1
+      let mut maxSum := 0
       --check all subarrays with length divisible by k
       for len in List.range (n+1) do
         if len % k = 0 && len > 0 then
@@ -49,8 +49,7 @@ def maxSubarraySumDivisibleByK (arr : Array Int) (k : Int) : Int :=
             maxSum := max maxSum subarraySum
       maxSum
 
-    let default : Int := minElem - 1
-    if maxSum = default then 0 else maxSum
+    if maxSum ≤ 0 then 0 else maxSum
   -- !benchmark @end code
 
 
@@ -65,7 +64,7 @@ def maxSubarraySumDivisibleByK_postcond (arr : Array Int) (k : Int) (result: Int
   let subarrays := List.range (arr.size) |>.flatMap (fun start =>
     List.range (arr.size - start + 1) |>.map (fun len => arr.extract start (start + len)))
   let divisibleSubarrays := subarrays.filter (fun subarray => subarray.size % k.toNat = 0 && subarray.size > 0)
-  let subarraySums := divisibleSubarrays.map (fun subarray => subarray.toList.sum)
+  let subarraySums := (divisibleSubarrays.map (fun subarray => subarray.toList.sum)).filter (· > 0)
   -- No valid subarrays -> result is 0
   (subarraySums.length = 0 → result = 0) ∧
   -- Valid subarrays exist -> result is the maximum sum

datasets/verina/verina_basic_104/task.lean

@@ -23,12 +23,13 @@ def insert {K V : Type} [BEq K] [BEq V] (m : Map K V) (k : K) (v : V) : Map K V
 -- !benchmark @end solution_aux
 
 -- !benchmark @start precond_aux
-
+def unique_keys (m : Map Int Int) : Prop :=
+  ∀ p q, p ∈ m.entries → q ∈ m.entries → p.1 = q.1 → p = q
 -- !benchmark @end precond_aux
 @[reducible, simp]
 def update_map_precond (m1 : Map Int Int) (m2 : Map Int Int) : Prop :=
   -- !benchmark @start precond
-  True
+  unique_keys m1 ∧ unique_keys m2
   -- !benchmark @end precond
 
 

datasets/verina/verina_basic_40/task.lean

@@ -38,7 +38,7 @@ def secondSmallestAux (s : Array Int) (i minIdx secondIdx : Nat) : Int :=
     let smin := s[secondIdx]!
     if x < m then
       secondSmallestAux s (i + 1) i minIdx
-    else if x < smin then
+    else if m < x ∧ (x < smin ∨ smin ≤ m) then
       secondSmallestAux s (i + 1) minIdx i
     else
       secondSmallestAux s (i + 1) minIdx secondIdx