Skip to content

Commit 1d2260f

Browse files
wkrozowskiwkrozowski
authored
feat: use cbv in several examples (#304)
1 parent 0a3752e commit 1d2260f

27 files changed

+167
-167
lines changed

‎HumanEvalLean/HumanEval0.lean‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -33,13 +33,13 @@ def hasCloseElements (xs : Array Rat) (threshold : Rat) : Bool := Id.run do
3333
## Tests
3434
-/
3535

36-
example : hasCloseElements #[1.0, 2.0, 3.9, 4.0, 5.0, 2.2] 0.3 = true := by native_decide
37-
example : hasCloseElements #[1.0, 2.0, 3.9, 4.0, 5.0, 2.2] 0.05 = false := by native_decide
38-
example : hasCloseElements #[1.0, 2.0, 5.9, 4.0, 5.0] 0.95 = true := by native_decide
39-
example : hasCloseElements #[1.0, 2.0, 5.9, 4.0, 5.0] 0.8 = false := by native_decide
40-
example : hasCloseElements #[1.0, 2.0, 3.0, 4.0, 5.0, 2.0] 0.1 = true := by native_decide
41-
example : hasCloseElements #[1.1, 2.2, 3.1, 4.1, 5.1] 1.0 = true := by native_decide
42-
example : hasCloseElements #[1.1, 2.2, 3.1, 4.1, 5.1] 0.5 = false := by native_decide
36+
example : hasCloseElements #[1.0, 2.0, 3.9, 4.0, 5.0, 2.2] 0.3 = true := by cbv
37+
example : hasCloseElements #[1.0, 2.0, 3.9, 4.0, 5.0, 2.2] 0.05 = false := by cbv
38+
example : hasCloseElements #[1.0, 2.0, 5.9, 4.0, 5.0] 0.95 = true := by cbv
39+
example : hasCloseElements #[1.0, 2.0, 5.9, 4.0, 5.0] 0.8 = false := by cbv
40+
example : hasCloseElements #[1.0, 2.0, 3.0, 4.0, 5.0, 2.0] 0.1 = true := by cbv
41+
example : hasCloseElements #[1.1, 2.2, 3.1, 4.1, 5.1] 1.0 = true := by cbv
42+
example : hasCloseElements #[1.1, 2.2, 3.1, 4.1, 5.1] 0.5 = false := by cbv
4343

4444
/-!
4545
## Verification

‎HumanEvalLean/HumanEval106.lean‎

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -38,10 +38,10 @@ def f (n : Nat) : List Nat := Id.run do
3838
### Tests
3939
-/
4040

41-
example : f 5 = [1, 2, 6, 24, 15] := by native_decide
42-
example : f 7 = [1, 2, 6, 24, 15, 720, 28] := by native_decide
43-
example : f 1 = [1] := by native_decide
44-
example : f 3 = [1, 2, 6] := by native_decide
41+
example : f 5 = [1, 2, 6, 24, 15] := by cbv
42+
example : f 7 = [1, 2, 6, 24, 15, 720, 28] := by cbv
43+
example : f 1 = [1] := by cbv
44+
example : f 3 = [1, 2, 6] := by cbv
4545

4646
/-!
4747
### Verification
@@ -134,10 +134,10 @@ def f' (n : Nat) : Array Nat := Id.run do
134134
### Tests
135135
-/
136136

137-
example : f' 5 = #[1, 2, 6, 24, 15] := by native_decide
138-
example : f' 7 = #[1, 2, 6, 24, 15, 720, 28] := by native_decide
139-
example : f' 1 = #[1] := by native_decide
140-
example : f' 3 = #[1, 2, 6] := by native_decide
137+
example : f' 5 = #[1, 2, 6, 24, 15] := by cbv
138+
example : f' 7 = #[1, 2, 6, 24, 15, 720, 28] := by cbv
139+
example : f' 1 = #[1] := by cbv
140+
example : f' 3 = #[1, 2, 6] := by cbv
141141

142142
/-!
143143
### Verification
@@ -204,10 +204,10 @@ def f'' (n : Nat) : Array Nat := Id.run do
204204
### Tests
205205
-/
206206

207-
example : f'' 5 = #[1, 2, 6, 24, 15] := by native_decide
208-
example : f'' 7 = #[1, 2, 6, 24, 15, 720, 28] := by native_decide
209-
example : f'' 1 = #[1] := by native_decide
210-
example : f'' 3 = #[1, 2, 6] := by native_decide
207+
example : f'' 5 = #[1, 2, 6, 24, 15] := by cbv
208+
example : f'' 7 = #[1, 2, 6, 24, 15, 720, 28] := by cbv
209+
example : f'' 1 = #[1] := by cbv
210+
example : f'' 3 = #[1, 2, 6] := by cbv
211211

212212
/-!
213213
### Verification

‎HumanEvalLean/HumanEval115.lean‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -16,11 +16,11 @@ def maxFill (grid : Vector (Vector Nat n) m) (capacity : Nat) : Nat :=
1616
# Tests
1717
-/
1818

19-
example : maxFill #v[#v[0,0,1,0], #v[0,1,0,0], #v[1,1,1,1]] 1 = 6 := by native_decide
20-
example : maxFill #v[#v[0,0,1,1], #v[0,0,0,0], #v[1,1,1,1], #v[0,1,1,1]] 2 = 5 := by native_decide
21-
example : maxFill #v[#v[0,0,0], #v[0,0,0]] 5 = 0 := by native_decide
22-
example : maxFill #v[#v[1,1,1,1], #v[1,1,1,1]] 2 = 4 := by native_decide
23-
example : maxFill #v[#v[1,1,1,1], #v[1,1,1,1]] 9 = 2 := by native_decide
19+
example : maxFill #v[#v[0,0,1,0], #v[0,1,0,0], #v[1,1,1,1]] 1 = 6 := by cbv
20+
example : maxFill #v[#v[0,0,1,1], #v[0,0,0,0], #v[1,1,1,1], #v[0,1,1,1]] 2 = 5 := by cbv
21+
example : maxFill #v[#v[0,0,0], #v[0,0,0]] 5 = 0 := by cbv
22+
example : maxFill #v[#v[1,1,1,1], #v[1,1,1,1]] 2 = 4 := by cbv
23+
example : maxFill #v[#v[1,1,1,1], #v[1,1,1,1]] 9 = 2 := by cbv
2424

2525
/-!
2626
## Verification

‎HumanEvalLean/HumanEval12.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -37,9 +37,9 @@ def longest? (xs : List String) : Option String :=
3737
## Tests
3838
-/
3939

40-
example : longest? [] = none := by native_decide
41-
example : longest? ["x", "y", "z"] = some "x" := by native_decide
42-
example : longest? ["x", "yyy", "zzzz", "www", "kkkk", "abc"] = some "zzzz" := by native_decide
40+
example : longest? [] = none := by cbv
41+
example : longest? ["x", "y", "z"] = some "x" := by cbv
42+
example : longest? ["x", "yyy", "zzzz", "www", "kkkk", "abc"] = some "zzzz" := by cbv
4343

4444
/-!
4545
## Verification

‎HumanEvalLean/HumanEval122.lean‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -25,11 +25,11 @@ def addElements (xs : Array Int) (k : Nat) : Int :=
2525
## Tests
2626
-/
2727

28-
example : addElements #[1,-2,-3,41,57,76,87,88,99] 3 = -4 := by native_decide
29-
example : addElements #[111,121,3,4000,5,6] 2 = 0 := by native_decide
30-
example : addElements #[11,21,3,90,5,6,7,8,9] 4 = 125 := by native_decide
31-
example : addElements #[111,21,3,4000,5,6,7,8,9] 4 = 24 := by native_decide
32-
example : addElements #[1] 1 = 1 := by native_decide
28+
example : addElements #[1,-2,-3,41,57,76,87,88,99] 3 = -4 := by cbv
29+
example : addElements #[111,121,3,4000,5,6] 2 = 0 := by cbv
30+
example : addElements #[11,21,3,90,5,6,7,8,9] 4 = 125 := by cbv
31+
example : addElements #[111,21,3,4000,5,6,7,8,9] 4 = 24 := by cbv
32+
example : addElements #[1] 1 = 1 := by cbv
3333

3434
/-!
3535
## Verification

‎HumanEvalLean/HumanEval128.lean‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -68,14 +68,14 @@ def prodSigns (arr : List Int) : Option Int := do
6868
## Tests
6969
-/
7070

71-
example : prodSigns [1, 2, 2, -4] = some (-9) := by native_decide
72-
example : prodSigns [0, 1] = some 0 := by native_decide
73-
example : prodSigns [] = none := by native_decide
74-
example : prodSigns [1, 1, 1, 2, 3, -1, 1] = some (-10) := by native_decide
75-
example : prodSigns [2, 4, 1, 2, -1, -1, 9] = some 20 := by native_decide
76-
example : prodSigns [-1, 1, -1, 1] = some 4 := by native_decide
77-
example : prodSigns [-1, 1, 1, 1] = some (-4) := by native_decide
78-
example : prodSigns [-1, 1, 1, 0] = some 0 := by native_decide
71+
example : prodSigns [1, 2, 2, -4] = some (-9) := by cbv
72+
example : prodSigns [0, 1] = some 0 := by cbv
73+
example : prodSigns [] = none := by cbv
74+
example : prodSigns [1, 1, 1, 2, 3, -1, 1] = some (-10) := by cbv
75+
example : prodSigns [2, 4, 1, 2, -1, -1, 9] = some 20 := by cbv
76+
example : prodSigns [-1, 1, -1, 1] = some 4 := by cbv
77+
example : prodSigns [-1, 1, 1, 1] = some (-4) := by cbv
78+
example : prodSigns [-1, 1, 1, 0] = some 0 := by cbv
7979

8080
/-!
8181
## Verification

‎HumanEvalLean/HumanEval13.lean‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -8,10 +8,10 @@ There is nothing to implement: The standard library provides `Int.gcd` out of th
88
## Tests
99
-/
1010

11-
example : Int.gcd 3 7 = 1 := by native_decide
12-
example : Int.gcd 10 15 = 5 := by native_decide
13-
example : Int.gcd 49 14 = 7 := by native_decide
14-
example : Int.gcd 144 60 = 12 := by native_decide
11+
example : Int.gcd 3 7 = 1 := by cbv
12+
example : Int.gcd 10 15 = 5 := by cbv
13+
example : Int.gcd 49 14 = 7 := by cbv
14+
example : Int.gcd 144 60 = 12 := by cbv
1515

1616
/-!
1717
## Verification

‎HumanEvalLean/HumanEval133.lean‎

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -5,18 +5,18 @@ def sumSquares (xs : List Rat) : Int :=
55

66
/-! ## Tests -/
77

8-
example : sumSquares [1, 2, 3] = 14 := by native_decide
9-
example : sumSquares [1.0, 2, 3] = 14 := by native_decide
10-
example : sumSquares [1, 3, 5, 7] = 84 := by native_decide
11-
example : sumSquares [1.4, 4.2, 0] = 29 := by native_decide
12-
example : sumSquares [-2.4, 1, 1] = 6 := by native_decide
13-
example : sumSquares [100, 1, 15, 2] = 10230 := by native_decide
14-
example : sumSquares [10000, 10000] = 200000000 := by native_decide
15-
example : sumSquares [-1.4, 4.6, 6.3] = 75 := by native_decide
16-
example : sumSquares [-1.4, 17.9, 18.9, 19.9] = 1086 := by native_decide
17-
example : sumSquares [0] = 0 := by native_decide
18-
example : sumSquares [-1] = 1 := by native_decide
19-
example : sumSquares [-1, 1, 0] = 2 := by native_decide
8+
example : sumSquares [1, 2, 3] = 14 := by cbv
9+
example : sumSquares [1.0, 2, 3] = 14 := by cbv
10+
example : sumSquares [1, 3, 5, 7] = 84 := by cbv
11+
example : sumSquares [1.4, 4.2, 0] = 29 := by cbv
12+
example : sumSquares [-2.4, 1, 1] = 6 := by cbv
13+
example : sumSquares [100, 1, 15, 2] = 10230 := by cbv
14+
example : sumSquares [10000, 10000] = 200000000 := by cbv
15+
example : sumSquares [-1.4, 4.6, 6.3] = 75 := by cbv
16+
example : sumSquares [-1.4, 17.9, 18.9, 19.9] = 1086 := by cbv
17+
example : sumSquares [0] = 0 := by cbv
18+
example : sumSquares [-1] = 1 := by cbv
19+
example : sumSquares [-1, 1, 0] = 2 := by cbv
2020

2121
/-!
2222
## Verification

‎HumanEvalLean/HumanEval139.lean‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -45,10 +45,10 @@ theorem special_factorial_func_correct {n : Nat} :
4545
apply this <;> simp [Nat.factorial, Nat.brazilianFactorial]
4646
intros; fun_induction special_factorial.go <;> grind [Nat.factorial, Nat.brazilianFactorial]
4747

48-
theorem test1 : special_factorial 4 = 288 := by native_decide
49-
theorem test2 : special_factorial 5 = 34560 := by native_decide
50-
theorem test3 : special_factorial 7 = 125411328000 := by native_decide
51-
theorem test4 : special_factorial 1 = 1 := by native_decide
48+
theorem test1 : special_factorial 4 = 288 := by cbv
49+
theorem test2 : special_factorial 5 = 34560 := by cbv
50+
theorem test3 : special_factorial 7 = 125411328000 := by cbv
51+
theorem test4 : special_factorial 1 = 1 := by cbv
5252

5353
/-!
5454
## Prompt

‎HumanEvalLean/HumanEval2.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -13,9 +13,9 @@ def truncateNumber (x : Rat) : Rat :=
1313
## Tests
1414
-/
1515

16-
example : truncateNumber (7/2) = 1/2 := by native_decide
17-
example : truncateNumber (133/100) = 33/100 := by native_decide
18-
example : truncateNumber (123456/1000) = 456/1000 := by native_decide
16+
example : truncateNumber (7/2) = 1/2 := by cbv
17+
example : truncateNumber (133/100) = 33/100 := by cbv
18+
example : truncateNumber (123456/1000) = 456/1000 := by cbv
1919

2020
/-!
2121
## Verification

0 commit comments

Comments
 (0)
⚡