feat: Port 20 more numeric-only Dafny synthesis tasks (batch 7)

Author: alok

NumpySpec/DafnyBenchmarks/SynthesisTask101.lean

@@ -0,0 +1,15 @@
+-- Synthesis Task 101: Get the k-th element from an array (1-indexed)
+
+namespace NumpySpec.DafnyBenchmarks.SynthesisTask101
+
+/-- Returns the k-th element from an array (1-indexed) -/
+def kthElement (arr : Array Int) (k : Int) : Int :=
+  sorry
+
+/-- Specification: Returns the element at position k-1 (0-indexed) -/
+theorem kthElement_spec (arr : Array Int) (k : Int)
+    (h : 1 ≤ k ∧ k ≤ arr.size) :
+  kthElement arr k = arr[(k - 1).toNat]! :=
+  sorry
+
+end NumpySpec.DafnyBenchmarks.SynthesisTask101

NumpySpec/DafnyBenchmarks/SynthesisTask142.lean

@@ -0,0 +1,14 @@
+namespace NumpySpec.DafnyBenchmarks.SynthesisTask142
+
+/-- Count the number of positions where all three arrays have identical values -/
+def countIdenticalPositions (a b c : Array Int) : Nat :=
+  sorry
+
+/-- Specification: The count equals the number of indices where all three arrays have the same value -/
+theorem countIdenticalPositions_spec (a b c : Array Int) 
+    (h_len : a.size = b.size ∧ b.size = c.size) :
+    let count := (List.range a.size).filter (fun i => a[i]! = b[i]! ∧ b[i]! = c[i]!)
+    countIdenticalPositions a b c = count.length := by
+  sorry
+
+end NumpySpec.DafnyBenchmarks.SynthesisTask142

NumpySpec/DafnyBenchmarks/SynthesisTask143.lean

@@ -0,0 +1,12 @@
+namespace NumpySpec.DafnyBenchmarks.SynthesisTask143
+
+/-- Count the number of arrays in a list of arrays -/
+def countArrays (arrays : List (Array Int)) : Nat :=
+  sorry
+
+/-- Specification: The count equals the length of the list -/
+theorem countArrays_spec (arrays : List (Array Int)) :
+    countArrays arrays = arrays.length := by
+  sorry
+
+end NumpySpec.DafnyBenchmarks.SynthesisTask143

NumpySpec/DafnyBenchmarks/SynthesisTask145.lean

@@ -0,0 +1,26 @@
+import Std.Do.Triple
+import Std.Tactic.Do
+
+open Std.Do
+
+/-- MaxDifference: Find the maximum difference between any two elements in an array.
+    
+    Given an array with at least 2 elements, returns the maximum value of a[i] - a[j]
+    for any valid indices i and j.
+    
+    Example: maxDifference([1, 5, 3]) could return 4 (5 - 1)
+-/
+def maxDifference (a : Array Int) : Id Int :=
+  sorry
+
+/-- Specification: maxDifference returns a value that is greater than or equal to 
+    any difference between two elements in the array.
+    
+    Precondition: The array has at least 2 elements
+    Postcondition: For all pairs of indices i,j, the difference a[i] - a[j] is at most the result
+-/
+theorem maxDifference_spec (a : Array Int) :
+    ⦃⌜a.size > 1⌝⦄
+    maxDifference a
+    ⦃⇓diff => ⌜∀ i j : Fin a.size, a[i] - a[j] ≤ diff⌝⦄ := by
+  sorry

NumpySpec/DafnyBenchmarks/SynthesisTask290.lean

@@ -0,0 +1,16 @@
+-- Synthesis Task 290: Find the longest list from a sequence of lists
+
+namespace NumpySpec.DafnyBenchmarks.SynthesisTask290
+
+/-- Returns the longest list from a sequence of lists -/
+def maxLengthList (lists : List (List Int)) : List Int :=
+  sorry
+
+/-- Specification: The returned list is at least as long as any list in the input,
+    and it is one of the lists in the input -/
+theorem maxLengthList_spec (lists : List (List Int)) (h : lists.length > 0) :
+  let maxList := maxLengthList lists
+  (∀ l ∈ lists, l.length ≤ maxList.length) ∧ maxList ∈ lists :=
+  sorry
+
+end NumpySpec.DafnyBenchmarks.SynthesisTask290

NumpySpec/DafnyBenchmarks/SynthesisTask433.lean

@@ -0,0 +1,19 @@
+import Std.Do.Triple
+import Std.Tactic.Do
+
+open Std.Do
+
+namespace NumpySpec.DafnyBenchmarks.SynthesisTask433
+
+/-- Check if n is greater than all elements in array a -/
+def isGreater (n : Int) (a : Array Int) : Bool :=
+  sorry
+
+/-- Specification: If result is true, n is greater than all elements;
+    if false, there exists at least one element >= n -/
+theorem isGreater_spec (n : Int) (a : Array Int) :
+  (isGreater n a = true → ∀ i : Nat, i < a.size → n > a[i]!) ∧
+  (isGreater n a = false → ∃ i : Nat, i < a.size ∧ n ≤ a[i]!) := by
+  sorry
+
+end NumpySpec.DafnyBenchmarks.SynthesisTask433

NumpySpec/DafnyBenchmarks/SynthesisTask476.lean

@@ -0,0 +1,54 @@
+import Std.Do.Triple
+import Std.Tactic.Do
+
+open Std.Do
+
+/-- Min: Find the minimum element in a non-empty list.
+    
+    Recursively finds the minimum element by comparing the last element
+    with the minimum of the prefix.
+-/
+def min : List Int → Int
+  | [] => 0  -- Should not happen given precondition
+  | [a] => a
+  | l => 
+    let minPrefix := min (l.take (l.length - 1))
+    let lastElem := l.getLast!
+    if lastElem ≤ minPrefix then lastElem else minPrefix
+termination_by l => l.length
+decreasing_by sorry
+
+/-- Max: Find the maximum element in a non-empty list.
+    
+    Recursively finds the maximum element by comparing the last element
+    with the maximum of the prefix.
+-/
+def max : List Int → Int
+  | [] => 0  -- Should not happen given precondition
+  | [a] => a
+  | l => 
+    let maxPrefix := max (l.take (l.length - 1))
+    let lastElem := l.getLast!
+    if lastElem ≥ maxPrefix then lastElem else maxPrefix
+termination_by l => l.length
+decreasing_by sorry
+
+/-- SumMinMax: Return the sum of the minimum and maximum elements in an array.
+    
+    Given a non-empty array, returns the sum of its minimum and maximum elements.
+    
+    Example: sumMinMax([3, 1, 4, 1, 5]) = 1 + 5 = 6
+-/
+def sumMinMax (a : Array Int) : Id Int :=
+  sorry
+
+/-- Specification: sumMinMax returns the sum of the minimum and maximum elements.
+    
+    Precondition: The array is non-empty
+    Postcondition: The result equals max(a.toList) + min(a.toList)
+-/
+theorem sumMinMax_spec (a : Array Int) :
+    ⦃⌜a.size > 0⌝⦄
+    sumMinMax a
+    ⦃⇓sum => ⌜sum = max a.toList + min a.toList⌝⦄ := by
+  sorry

NumpySpec/DafnyBenchmarks/SynthesisTask566.lean

@@ -0,0 +1,53 @@
+import Std.Do.Triple
+import Std.Tactic.Do
+
+open Std.Do
+
+namespace NumpySpec.DafnyBenchmarks.SynthesisTask566
+
+/-- Helper function: power of 10 -/
+def power10 (n : Nat) : Nat :=
+  sorry
+
+/-- Helper function: number of digits in a natural number -/
+def numberOfDigits (n : Nat) : Nat :=
+  sorry
+
+/-- Helper function: sum of digits recursive implementation -/
+def sumDigitsRecursive (n : Nat) (p : Nat) : Nat :=
+  sorry
+
+/-- Helper function: sum of digits -/
+def sumDigits (n : Nat) : Nat :=
+  sorry
+
+/-- Compute the sum of digits of a natural number -/
+def sumOfDigits (number : Nat) : Nat :=
+  sorry
+
+/-- Specification: The sum of digits is non-negative and equals sumDigits -/
+theorem sumOfDigits_spec (number : Nat) :
+  sumOfDigits number ≥ 0 ∧ sumOfDigits number = sumDigits number := by
+  sorry
+
+/-- Power of 10 is at least 1 -/
+theorem power10_ge_one (n : Nat) :
+  power10 n ≥ 1 := by
+  sorry
+
+/-- Power of 10 for positive n is divisible by 10 -/
+theorem power10_div_ten (n : Nat) (h : n > 0) :
+  power10 n % 10 = 0 := by
+  sorry
+
+/-- Number of digits is at least 1 -/
+theorem numberOfDigits_ge_one (n : Nat) :
+  numberOfDigits n ≥ 1 := by
+  sorry
+
+/-- Single digit characterization -/
+theorem numberOfDigits_single (n : Nat) :
+  numberOfDigits n = 1 ↔ 0 ≤ n ∧ n ≤ 9 := by
+  sorry
+
+end NumpySpec.DafnyBenchmarks.SynthesisTask566

NumpySpec/DafnyBenchmarks/SynthesisTask573.lean

@@ -0,0 +1,17 @@
+-- Synthesis Task 573: Product of unique elements
+
+namespace NumpySpec.DafnyBenchmarks.SynthesisTask573
+
+/-- Calculate the product of unique elements in an array -/
+def uniqueProduct (arr : Array Int) : Int :=
+  sorry
+
+/-- Specification: Product includes each distinct element exactly once -/
+theorem uniqueProduct_spec (arr : Array Int) :
+    ∃ uniqueElems : List Int,
+      (∀ x : Int, x ∈ uniqueElems ↔ ∃ i : Nat, i < arr.size ∧ arr[i]! = x) ∧
+      (∀ i j : Nat, i < j → j < uniqueElems.length → uniqueElems[i]! ≠ uniqueElems[j]!) ∧
+      uniqueProduct arr = uniqueElems.foldl (· * ·) 1 :=
+  sorry
+
+end NumpySpec.DafnyBenchmarks.SynthesisTask573

NumpySpec/DafnyBenchmarks/SynthesisTask579.lean

@@ -0,0 +1,24 @@
+import Std.Do.Triple
+import Std.Tactic.Do
+
+open Std.Do
+
+namespace NumpySpec.DafnyBenchmarks.SynthesisTask579
+
+/-- Predicate to check if x is in array a -/
+def inArray (a : Array Int) (x : Int) : Prop :=
+  ∃ i : Nat, i < a.size ∧ a[i]! = x
+
+/-- Find elements that are in exactly one of the two arrays (symmetric difference) -/
+def dissimilarElements (a : Array Int) (b : Array Int) : List Int :=
+  sorry
+
+/-- Specification: All elements in result are in exactly one array (not both, not neither),
+    and all elements in the result are distinct -/
+theorem dissimilarElements_spec (a : Array Int) (b : Array Int) :
+  let result := dissimilarElements a b
+  (∀ x ∈ result, (inArray a x) ≠ (inArray b x)) ∧
+  (∀ i j : Nat, i < result.length → j < result.length → i < j → result[i]! ≠ result[j]!) := by
+  sorry
+
+end NumpySpec.DafnyBenchmarks.SynthesisTask579