From dc40978affd428d3e0776bae67b3b7cbd7fee1f8 Mon Sep 17 00:00:00 2001 From: Alessandro Sosso Date: Thu, 5 Mar 2026 14:49:25 +0100 Subject: [PATCH 1/2] Bug fixes (basic_40, basic_104, advanced_10, advanced_12, advanced_15) --- datasets/verina/verina_advanced_10/task.lean | 3 +- datasets/verina/verina_advanced_12/task.lean | 5 +- datasets/verina/verina_advanced_15/task.lean | 54 ++++++-------------- datasets/verina/verina_basic_104/task.lean | 5 +- datasets/verina/verina_basic_40/task.lean | 2 +- 5 files changed, 27 insertions(+), 42 deletions(-) diff --git a/datasets/verina/verina_advanced_10/task.lean b/datasets/verina/verina_advanced_10/task.lean index f631e8e..d63871a 100644 --- a/datasets/verina/verina_advanced_10/task.lean +++ b/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 diff --git a/datasets/verina/verina_advanced_12/task.lean b/datasets/verina/verina_advanced_12/task.lean index 2b5e7e3..229372d 100644 --- a/datasets/verina/verina_advanced_12/task.lean +++ b/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 diff --git a/datasets/verina/verina_advanced_15/task.lean b/datasets/verina/verina_advanced_15/task.lean index 155288b..20d8fb7 100644 --- a/datasets/verina/verina_advanced_15/task.lean +++ b/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 diff --git a/datasets/verina/verina_basic_104/task.lean b/datasets/verina/verina_basic_104/task.lean index 5347ecf..b571a64 100644 --- a/datasets/verina/verina_basic_104/task.lean +++ b/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 diff --git a/datasets/verina/verina_basic_40/task.lean b/datasets/verina/verina_basic_40/task.lean index c46e0ea..6096028 100644 --- a/datasets/verina/verina_basic_40/task.lean +++ b/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 From b02dd758617234bf125d0d55cbff28637c270d22 Mon Sep 17 00:00:00 2001 From: Alessandro Sosso Date: Thu, 5 Mar 2026 14:49:38 +0100 Subject: [PATCH 2/2] Bug fixes (advanced_44) --- datasets/verina/verina_advanced_44/task.lean | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/datasets/verina/verina_advanced_44/task.lean b/datasets/verina/verina_advanced_44/task.lean index 8c5f8da..d5d9b58 100644 --- a/datasets/verina/verina_advanced_44/task.lean +++ b/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