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

alok · alok · commit 2e5225c97191 · 2025-07-10T19:00:02.000-04:00
diff --git a/NumpySpec/DafnyBenchmarks/SynthesisTask135.lean b/NumpySpec/DafnyBenchmarks/SynthesisTask135.lean
@@ -0,0 +1,14 @@
+-- Synthesis Task 135: Calculate nth hexagonal number
+
+namespace NumpySpec.DafnyBenchmarks.SynthesisTask135
+
+/-- Calculate the nth hexagonal number -/
+def nthHexagonalNumber (n : Nat) : Nat :=
+  sorry
+
+/-- Specification: The nth hexagonal number is n(2n-1) -/
+theorem nthHexagonalNumber_spec (n : Nat) :
+    nthHexagonalNumber n = n * (2 * n - 1) :=
+  sorry
+
+end NumpySpec.DafnyBenchmarks.SynthesisTask135
diff --git a/NumpySpec/DafnyBenchmarks/SynthesisTask14.lean b/NumpySpec/DafnyBenchmarks/SynthesisTask14.lean
@@ -0,0 +1,15 @@
+-- Synthesis Task 14: Calculate triangular prism volume
+
+namespace NumpySpec.DafnyBenchmarks.SynthesisTask14
+
+/-- Calculate the volume of a triangular prism -/
+def triangularPrismVolume (base height length : Nat) : Nat :=
+  sorry
+
+/-- Specification: Volume = (base * height * length) / 2 -/
+theorem triangularPrismVolume_spec (base height length : Nat) 
+    (hb : base > 0) (hh : height > 0) (hl : length > 0) :
+    triangularPrismVolume base height length = (base * height * length) / 2 :=
+  sorry
+
+end NumpySpec.DafnyBenchmarks.SynthesisTask14
diff --git a/NumpySpec/DafnyBenchmarks/SynthesisTask17.lean b/NumpySpec/DafnyBenchmarks/SynthesisTask17.lean
@@ -0,0 +1,14 @@
+-- Synthesis Task 17: Calculate square perimeter
+
+namespace NumpySpec.DafnyBenchmarks.SynthesisTask17
+
+/-- Calculate the perimeter of a square given its side length -/
+def squarePerimeter (side : Nat) : Nat :=
+  sorry
+
+/-- Specification: Perimeter is 4 times the side length -/
+theorem squarePerimeter_spec (side : Nat) (h : side > 0) :
+    squarePerimeter side = 4 * side :=
+  sorry
+
+end NumpySpec.DafnyBenchmarks.SynthesisTask17
diff --git a/NumpySpec/DafnyBenchmarks/SynthesisTask227.lean b/NumpySpec/DafnyBenchmarks/SynthesisTask227.lean
@@ -0,0 +1,16 @@
+-- Synthesis Task 227: Find minimum of three integers
+
+namespace NumpySpec.DafnyBenchmarks.SynthesisTask227
+
+/-- Find the minimum of three integers -/
+def minOfThree (a b c : Int) : Int :=
+  sorry
+
+/-- Specification: Result is the minimum and is one of the inputs -/
+theorem minOfThree_spec (a b c : Int) :
+    let min := minOfThree a b c
+    min ≤ a ∧ min ≤ b ∧ min ≤ c ∧
+    (min = a ∨ min = b ∨ min = c) :=
+  sorry
+
+end NumpySpec.DafnyBenchmarks.SynthesisTask227
diff --git a/NumpySpec/DafnyBenchmarks/SynthesisTask264.lean b/NumpySpec/DafnyBenchmarks/SynthesisTask264.lean
@@ -0,0 +1,14 @@
+-- Synthesis Task 264: Calculate dog years
+
+namespace NumpySpec.DafnyBenchmarks.SynthesisTask264
+
+/-- Convert human years to dog years -/
+def dogYears (humanYears : Nat) : Nat :=
+  sorry
+
+/-- Specification: Dog years = 7 * human years -/
+theorem dogYears_spec (humanYears : Nat) :
+    dogYears humanYears = 7 * humanYears :=
+  sorry
+
+end NumpySpec.DafnyBenchmarks.SynthesisTask264
diff --git a/NumpySpec/DafnyBenchmarks/SynthesisTask268.lean b/NumpySpec/DafnyBenchmarks/SynthesisTask268.lean
@@ -0,0 +1,14 @@
+-- Synthesis Task 268: Calculate star number
+
+namespace NumpySpec.DafnyBenchmarks.SynthesisTask268
+
+/-- Calculate the nth star number -/
+def starNumber (n : Nat) : Nat :=
+  sorry
+
+/-- Specification: The nth star number is 6n(n-1)+1 -/
+theorem starNumber_spec (n : Nat) :
+    starNumber n = 6 * n * (n - 1) + 1 :=
+  sorry
+
+end NumpySpec.DafnyBenchmarks.SynthesisTask268
diff --git a/NumpySpec/DafnyBenchmarks/SynthesisTask279.lean b/NumpySpec/DafnyBenchmarks/SynthesisTask279.lean
@@ -0,0 +1,14 @@
+-- Synthesis Task 279: Calculate nth decagonal number
+
+namespace NumpySpec.DafnyBenchmarks.SynthesisTask279
+
+/-- Calculate the nth decagonal number -/
+def nthDecagonalNumber (n : Nat) : Int :=
+  sorry
+
+/-- Specification: The nth decagonal number is 4n²-3n -/
+theorem nthDecagonalNumber_spec (n : Nat) :
+    nthDecagonalNumber n = 4 * n * n - 3 * n :=
+  sorry
+
+end NumpySpec.DafnyBenchmarks.SynthesisTask279
diff --git a/NumpySpec/DafnyBenchmarks/SynthesisTask3.lean b/NumpySpec/DafnyBenchmarks/SynthesisTask3.lean
@@ -0,0 +1,14 @@
+-- Synthesis Task 3: Check if number is non-prime
+
+namespace NumpySpec.DafnyBenchmarks.SynthesisTask3
+
+/-- Check if a number is non-prime (composite) -/
+def isNonPrime (n : Nat) : Bool :=
+  sorry
+
+/-- Specification: Returns true iff n has a divisor between 2 and n-1 -/
+theorem isNonPrime_spec (n : Nat) (h : n ≥ 2) :
+    isNonPrime n = ∃ k : Nat, 2 ≤ k ∧ k < n ∧ n % k = 0 :=
+  sorry
+
+end NumpySpec.DafnyBenchmarks.SynthesisTask3
diff --git a/NumpySpec/DafnyBenchmarks/SynthesisTask406.lean b/NumpySpec/DafnyBenchmarks/SynthesisTask406.lean
@@ -0,0 +1,14 @@
+-- Synthesis Task 406: Check if integer is odd
+
+namespace NumpySpec.DafnyBenchmarks.SynthesisTask406
+
+/-- Check if an integer is odd -/
+def isOdd (n : Int) : Bool :=
+  sorry
+
+/-- Specification: Returns true iff n is odd -/
+theorem isOdd_spec (n : Int) :
+    isOdd n = (n % 2 = 1) :=
+  sorry
+
+end NumpySpec.DafnyBenchmarks.SynthesisTask406
diff --git a/NumpySpec/DafnyBenchmarks/SynthesisTask432.lean b/NumpySpec/DafnyBenchmarks/SynthesisTask432.lean
@@ -0,0 +1,14 @@
+-- Synthesis Task 432: Calculate median of two lengths
+
+namespace NumpySpec.DafnyBenchmarks.SynthesisTask432
+
+/-- Calculate the median (average) of two positive integers -/
+def medianLength (a b : Nat) : Nat :=
+  sorry
+
+/-- Specification: Median is the average of the two values -/
+theorem medianLength_spec (a b : Nat) (ha : a > 0) (hb : b > 0) :
+    medianLength a b = (a + b) / 2 :=
+  sorry
+
+end NumpySpec.DafnyBenchmarks.SynthesisTask432
diff --git a/NumpySpec/DafnyBenchmarks/SynthesisTask435.lean b/NumpySpec/DafnyBenchmarks/SynthesisTask435.lean
@@ -0,0 +1,15 @@
+-- Synthesis Task 435: Get last digit of integer
+
+namespace NumpySpec.DafnyBenchmarks.SynthesisTask435
+
+/-- Get the last digit of a non-negative integer -/
+def lastDigit (n : Nat) : Nat :=
+  sorry
+
+/-- Specification: Last digit is n % 10 and is between 0 and 9 -/
+theorem lastDigit_spec (n : Nat) :
+    let d := lastDigit n
+    0 ≤ d ∧ d < 10 ∧ n % 10 = d :=
+  sorry
+
+end NumpySpec.DafnyBenchmarks.SynthesisTask435
diff --git a/NumpySpec/DafnyBenchmarks/SynthesisTask574.lean b/NumpySpec/DafnyBenchmarks/SynthesisTask574.lean
@@ -0,0 +1,15 @@
+-- Synthesis Task 574: Calculate cylinder surface area
+
+namespace NumpySpec.DafnyBenchmarks.SynthesisTask574
+
+/-- Calculate the surface area of a cylinder -/
+def cylinderSurfaceArea (radius height : Float) : Float :=
+  sorry
+
+/-- Specification: Surface area = 2πr(r+h) -/
+theorem cylinderSurfaceArea_spec (radius height : Float) 
+    (hr : radius > 0) (hh : height > 0) :
+    cylinderSurfaceArea radius height = 2 * 3.14159265358979323846 * radius * (radius + height) :=
+  sorry
+
+end NumpySpec.DafnyBenchmarks.SynthesisTask574
diff --git a/NumpySpec/DafnyBenchmarks/SynthesisTask58.lean b/NumpySpec/DafnyBenchmarks/SynthesisTask58.lean
@@ -0,0 +1,14 @@
+-- Synthesis Task 58: Check if two integers have opposite signs
+
+namespace NumpySpec.DafnyBenchmarks.SynthesisTask58
+
+/-- Check if two integers have opposite signs -/
+def hasOppositeSign (a b : Int) : Bool :=
+  sorry
+
+/-- Specification: Returns true iff one is positive and the other is negative -/
+theorem hasOppositeSign_spec (a b : Int) :
+    hasOppositeSign a b = ((a < 0 ∧ b > 0) ∨ (a > 0 ∧ b < 0)) :=
+  sorry
+
+end NumpySpec.DafnyBenchmarks.SynthesisTask58
diff --git a/NumpySpec/DafnyBenchmarks/SynthesisTask59.lean b/NumpySpec/DafnyBenchmarks/SynthesisTask59.lean
@@ -0,0 +1,14 @@
+-- Synthesis Task 59: Calculate nth octagonal number
+
+namespace NumpySpec.DafnyBenchmarks.SynthesisTask59
+
+/-- Calculate the nth octagonal number -/
+def nthOctagonalNumber (n : Nat) : Nat :=
+  sorry
+
+/-- Specification: The nth octagonal number is n(3n-2) -/
+theorem nthOctagonalNumber_spec (n : Nat) :
+    nthOctagonalNumber n = n * (3 * n - 2) :=
+  sorry
+
+end NumpySpec.DafnyBenchmarks.SynthesisTask59
diff --git a/NumpySpec/DafnyBenchmarks/SynthesisTask606.lean b/NumpySpec/DafnyBenchmarks/SynthesisTask606.lean
@@ -0,0 +1,14 @@
+-- Synthesis Task 606: Convert degrees to radians
+
+namespace NumpySpec.DafnyBenchmarks.SynthesisTask606
+
+/-- Convert degrees to radians -/
+def degreesToRadians (degrees : Float) : Float :=
+  sorry
+
+/-- Specification: radians = degrees * π / 180 -/
+theorem degreesToRadians_spec (degrees : Float) :
+    degreesToRadians degrees = degrees * 3.14159265358979323846 / 180 :=
+  sorry
+
+end NumpySpec.DafnyBenchmarks.SynthesisTask606
diff --git a/NumpySpec/DafnyBenchmarks/SynthesisTask77.lean b/NumpySpec/DafnyBenchmarks/SynthesisTask77.lean
@@ -0,0 +1,14 @@
+-- Synthesis Task 77: Check if divisible by 11
+
+namespace NumpySpec.DafnyBenchmarks.SynthesisTask77
+
+/-- Check if an integer is divisible by 11 -/
+def isDivisibleBy11 (n : Int) : Bool :=
+  sorry
+
+/-- Specification: Returns true iff n is divisible by 11 -/
+theorem isDivisibleBy11_spec (n : Int) :
+    isDivisibleBy11 n = (n % 11 = 0) :=
+  sorry
+
+end NumpySpec.DafnyBenchmarks.SynthesisTask77
diff --git a/NumpySpec/DafnyBenchmarks/SynthesisTask82.lean b/NumpySpec/DafnyBenchmarks/SynthesisTask82.lean
@@ -0,0 +1,14 @@
+-- Synthesis Task 82: Calculate sphere volume
+
+namespace NumpySpec.DafnyBenchmarks.SynthesisTask82
+
+/-- Calculate the volume of a sphere given its radius -/
+def sphereVolume (radius : Float) : Float :=
+  sorry
+
+/-- Specification: Volume = (4/3)πr³ -/
+theorem sphereVolume_spec (radius : Float) (h : radius > 0) :
+    sphereVolume radius = (4 / 3) * 3.1415926535 * radius * radius * radius :=
+  sorry
+
+end NumpySpec.DafnyBenchmarks.SynthesisTask82
diff --git a/NumpySpec/DafnyBenchmarks/SynthesisTask85.lean b/NumpySpec/DafnyBenchmarks/SynthesisTask85.lean
@@ -0,0 +1,14 @@
+-- Synthesis Task 85: Calculate sphere surface area
+
+namespace NumpySpec.DafnyBenchmarks.SynthesisTask85
+
+/-- Calculate the surface area of a sphere given its radius -/
+def sphereSurfaceArea (radius : Float) : Float :=
+  sorry
+
+/-- Specification: Surface area = 4πr² -/
+theorem sphereSurfaceArea_spec (radius : Float) (h : radius > 0) :
+    sphereSurfaceArea radius = 4 * 3.14159265358979323846 * radius * radius :=
+  sorry
+
+end NumpySpec.DafnyBenchmarks.SynthesisTask85
diff --git a/NumpySpec/DafnyBenchmarks/SynthesisTask89.lean b/NumpySpec/DafnyBenchmarks/SynthesisTask89.lean
@@ -0,0 +1,14 @@
+-- Synthesis Task 89: Find closest smaller integer
+
+namespace NumpySpec.DafnyBenchmarks.SynthesisTask89
+
+/-- Find the closest smaller integer (n-1) -/
+def closestSmaller (n : Nat) : Nat :=
+  sorry
+
+/-- Specification: Result is n-1 -/
+theorem closestSmaller_spec (n : Nat) (h : n > 0) :
+    closestSmaller n + 1 = n :=
+  sorry
+
+end NumpySpec.DafnyBenchmarks.SynthesisTask89
