Skip to content

Commit ebb161b

Browse files
wkrozowskiwkrozowski
authored
feat: further use of cbv (#311)
1 parent 76a1a47 commit ebb161b

File tree

5 files changed

+64
-64
lines changed

5 files changed

+64
-64
lines changed

‎HumanEvalLean/HumanEval100.lean‎

Lines changed: 17 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -19,23 +19,23 @@ def makeAPile₂ (n : Nat) : List Nat :=
1919
## Tests
2020
-/
2121

22-
example : makeAPile₁ 0 = [] := by native_decide
23-
example : makeAPile₁ 1 = [1] := by native_decide
24-
example : makeAPile₁ 2 = [2, 4] := by native_decide
25-
example : makeAPile₁ 3 = [3, 5, 7] := by native_decide
26-
example : makeAPile₁ 4 = [4, 6, 8, 10] := by native_decide
27-
example : makeAPile₁ 5 = [5, 7, 9, 11, 13] := by native_decide
28-
example : makeAPile₁ 6 = [6, 8, 10, 12, 14, 16] := by native_decide
29-
example : makeAPile₁ 8 = [8, 10, 12, 14, 16, 18, 20, 22] := by native_decide
30-
31-
example : makeAPile₂ 0 = [] := by native_decide
32-
example : makeAPile₂ 1 = [1] := by native_decide
33-
example : makeAPile₂ 2 = [2, 4] := by native_decide
34-
example : makeAPile₂ 3 = [3, 5, 7] := by native_decide
35-
example : makeAPile₂ 4 = [4, 6, 8, 10] := by native_decide
36-
example : makeAPile₂ 5 = [5, 7, 9, 11, 13] := by native_decide
37-
example : makeAPile₂ 6 = [6, 8, 10, 12, 14, 16] := by native_decide
38-
example : makeAPile₂ 8 = [8, 10, 12, 14, 16, 18, 20, 22] := by native_decide
22+
example : makeAPile₁ 0 = [] := by cbv
23+
example : makeAPile₁ 1 = [1] := by cbv
24+
example : makeAPile₁ 2 = [2, 4] := by cbv
25+
example : makeAPile₁ 3 = [3, 5, 7] := by cbv
26+
example : makeAPile₁ 4 = [4, 6, 8, 10] := by cbv
27+
example : makeAPile₁ 5 = [5, 7, 9, 11, 13] := by cbv
28+
example : makeAPile₁ 6 = [6, 8, 10, 12, 14, 16] := by cbv
29+
example : makeAPile₁ 8 = [8, 10, 12, 14, 16, 18, 20, 22] := by cbv
30+
31+
example : makeAPile₂ 0 = [] := by cbv
32+
example : makeAPile₂ 1 = [1] := by cbv
33+
example : makeAPile₂ 2 = [2, 4] := by cbv
34+
example : makeAPile₂ 3 = [3, 5, 7] := by cbv
35+
example : makeAPile₂ 4 = [4, 6, 8, 10] := by cbv
36+
example : makeAPile₂ 5 = [5, 7, 9, 11, 13] := by cbv
37+
example : makeAPile₂ 6 = [6, 8, 10, 12, 14, 16] := by cbv
38+
example : makeAPile₂ 8 = [8, 10, 12, 14, 16, 18, 20, 22] := by cbv
3939

4040
/-!
4141
## Verification

‎HumanEvalLean/HumanEval126.lean‎

Lines changed: 13 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -31,19 +31,19 @@ def isSorted (xs : Array Nat) : Bool := Id.run do
3131
## Tests
3232
-/
3333

34-
example : isSorted #[5] = true := by native_decide
35-
example : isSorted #[1, 2, 3, 4, 5] = true := by native_decide
36-
example : isSorted #[1, 3, 2, 4, 5] = false := by native_decide
37-
example : isSorted #[1, 2, 3, 4, 5, 6] = true := by native_decide
38-
example : isSorted #[1, 2, 3, 4, 5, 6, 7] = true := by native_decide
39-
example : isSorted #[1, 3, 2, 4, 5, 6, 7] = false := by native_decide
40-
example : isSorted #[] = true := by native_decide
41-
example : isSorted #[1] = true := by native_decide
42-
example : isSorted #[3, 2, 1] = false := by native_decide
43-
example : isSorted #[1, 2, 2, 2, 3, 4] = false := by native_decide
44-
example : isSorted #[1, 2, 3, 3, 3, 4] = false := by native_decide
45-
example : isSorted #[1, 2, 2, 3, 3, 4] = true := by native_decide
46-
example : isSorted #[1, 2, 3, 4] = true := by native_decide
34+
example : isSorted #[5] = true := by cbv
35+
example : isSorted #[1, 2, 3, 4, 5] = true := by cbv
36+
example : isSorted #[1, 3, 2, 4, 5] = false := by cbv
37+
example : isSorted #[1, 2, 3, 4, 5, 6] = true := by cbv
38+
example : isSorted #[1, 2, 3, 4, 5, 6, 7] = true := by cbv
39+
example : isSorted #[1, 3, 2, 4, 5, 6, 7] = false := by cbv
40+
example : isSorted #[] = true := by cbv
41+
example : isSorted #[1] = true := by cbv
42+
example : isSorted #[3, 2, 1] = false := by cbv
43+
example : isSorted #[1, 2, 2, 2, 3, 4] = false := by cbv
44+
example : isSorted #[1, 2, 3, 3, 3, 4] = false := by cbv
45+
example : isSorted #[1, 2, 2, 3, 3, 4] = true := by cbv
46+
example : isSorted #[1, 2, 3, 4] = true := by cbv
4747

4848
/-!
4949
## Missing API

‎HumanEvalLean/HumanEval35.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,8 @@ def maxElement (xs : Array Int) : Int :=
77

88
/-! ## Tests -/
99

10-
example : maxElement #[1, 2, 3] = 3 := by native_decide
11-
example : maxElement #[5, 3, -5, 2, -3, 3, 9, 0, 124, 1, -10] = 124 := by native_decide
10+
example : maxElement #[1, 2, 3] = 3 := by cbv
11+
example : maxElement #[5, 3, -5, 2, -3, 3, 9, 0, 124, 1, -10] = 124 := by cbv
1212

1313
/-! ## Verification -/
1414

‎HumanEvalLean/HumanEval48.lean‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -6,13 +6,13 @@ open Std
66
def isPalindrome (s : String) : Bool :=
77
s.chars.zip s.revChars |>.all (fun p => p.1 == p.2)
88

9-
example : isPalindrome "" = true := by native_decide
10-
example : isPalindrome "aba" = true := by native_decide
11-
example : isPalindrome "aaaaa" = true := by native_decide
12-
example : isPalindrome "zbcd" = false := by native_decide
13-
example : isPalindrome "xywyx" = true := by native_decide
14-
example : isPalindrome "xywyz" = false := by native_decide
15-
example : isPalindrome "xywxz" = false := by native_decide
9+
example : isPalindrome "" = true := by cbv
10+
example : isPalindrome "aba" = true := by cbv
11+
example : isPalindrome "aaaaa" = true := by cbv
12+
example : isPalindrome "zbcd" = false := by cbv
13+
example : isPalindrome "xywyx" = true := by cbv
14+
example : isPalindrome "xywyz" = false := by cbv
15+
example : isPalindrome "xywxz" = false := by cbv
1616

1717
theorem isPalindome_iff {s : String} : isPalindrome s ↔ s.toList = s.toList.reverse := by
1818
simp [isPalindrome, ← Iter.all_toList, List.mem_iff_getElem, List.ext_getElem_iff]

‎HumanEvalLean/HumanEval69.lean‎

Lines changed: 25 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -21,31 +21,31 @@ def search (xs : List Nat) : Int :=
2121

2222
/-! ## Tests -/
2323

24-
example : search [5, 5, 5, 5, 1] = 1 := by native_decide
25-
example : search [4, 1, 4, 1, 4, 4] = 4 := by native_decide
26-
example : search [3, 3] = -1 := by native_decide
27-
example : search [8, 8, 8, 8, 8, 8, 8, 8] = 8 := by native_decide
28-
example : search [2, 3, 3, 2, 2] = 2 := by native_decide
29-
example : search [2, 7, 8, 8, 4, 8, 7, 3, 9, 6, 5, 10, 4, 3, 6, 7, 1, 7, 4, 10, 8, 1] = 1 := by native_decide
30-
example : search [3, 2, 8, 2] = 2 := by native_decide
31-
example : search [6, 7, 1, 8, 8, 10, 5, 8, 5, 3, 10] = 1 := by native_decide
32-
example : search [8, 8, 3, 6, 5, 6, 4] = -1 := by native_decide
33-
example : search [6, 9, 6, 7, 1, 4, 7, 1, 8, 8, 9, 8, 10, 10, 8, 4, 10, 4, 10, 1, 2, 9, 5, 7, 9] = 1 := by native_decide
34-
example : search [1, 9, 10, 1, 3] = 1 := by native_decide
35-
example : search [6, 9, 7, 5, 8, 7, 5, 3, 7, 5, 10, 10, 3, 6, 10, 2, 8, 6, 5, 4, 9, 5, 3, 10] = 5 := by native_decide
36-
example : search [1] = 1 := by native_decide
37-
example : search [8, 8, 10, 6, 4, 3, 5, 8, 2, 4, 2, 8, 4, 6, 10, 4, 2, 1, 10, 2, 1, 1, 5] = 4 := by native_decide
38-
example : search [2, 10, 4, 8, 2, 10, 5, 1, 2, 9, 5, 5, 6, 3, 8, 6, 4, 10] = 2 := by native_decide
39-
example : search [1, 6, 10, 1, 6, 9, 10, 8, 6, 8, 7, 3] = 1 := by native_decide
40-
example : search [9, 2, 4, 1, 5, 1, 5, 2, 5, 7, 7, 7, 3, 10, 1, 5, 4, 2, 8, 4, 1, 9, 10, 7, 10, 2, 8, 10, 9, 4] = 4 := by native_decide
41-
example : search [2, 6, 4, 2, 8, 7, 5, 6, 4, 10, 4, 6, 3, 7, 8, 8, 3, 1, 4, 2, 2, 10, 7] = 4 := by native_decide
42-
example : search [9, 8, 6, 10, 2, 6, 10, 2, 7, 8, 10, 3, 8, 2, 6, 2, 3, 1] = 2 := by native_decide
43-
example : search [5, 5, 3, 9, 5, 6, 3, 2, 8, 5, 6, 10, 10, 6, 8, 4, 10, 7, 7, 10, 8] = -1 := by native_decide
44-
example : search [10] = -1 := by native_decide
45-
example : search [9, 7, 7, 2, 4, 7, 2, 10, 9, 7, 5, 7, 2] = 2 := by native_decide
46-
example : search [5, 4, 10, 2, 1, 1, 10, 3, 6, 1, 8] = 1 := by native_decide
47-
example : search [7, 9, 9, 9, 3, 4, 1, 5, 9, 1, 2, 1, 1, 10, 7, 5, 6, 7, 6, 7, 7, 6] = 1 := by native_decide
48-
example : search [3, 10, 10, 9, 2] = -1 := by native_decide
24+
example : search [5, 5, 5, 5, 1] = 1 := by cbv
25+
example : search [4, 1, 4, 1, 4, 4] = 4 := by cbv
26+
example : search [3, 3] = -1 := by cbv
27+
example : search [8, 8, 8, 8, 8, 8, 8, 8] = 8 := by cbv
28+
example : search [2, 3, 3, 2, 2] = 2 := by cbv
29+
example : search [2, 7, 8, 8, 4, 8, 7, 3, 9, 6, 5, 10, 4, 3, 6, 7, 1, 7, 4, 10, 8, 1] = 1 := by cbv
30+
example : search [3, 2, 8, 2] = 2 := by cbv
31+
example : search [6, 7, 1, 8, 8, 10, 5, 8, 5, 3, 10] = 1 := by cbv
32+
example : search [8, 8, 3, 6, 5, 6, 4] = -1 := by cbv
33+
example : search [6, 9, 6, 7, 1, 4, 7, 1, 8, 8, 9, 8, 10, 10, 8, 4, 10, 4, 10, 1, 2, 9, 5, 7, 9] = 1 := by cbv
34+
example : search [1, 9, 10, 1, 3] = 1 := by cbv
35+
example : search [6, 9, 7, 5, 8, 7, 5, 3, 7, 5, 10, 10, 3, 6, 10, 2, 8, 6, 5, 4, 9, 5, 3, 10] = 5 := by cbv
36+
example : search [1] = 1 := by cbv
37+
example : search [8, 8, 10, 6, 4, 3, 5, 8, 2, 4, 2, 8, 4, 6, 10, 4, 2, 1, 10, 2, 1, 1, 5] = 4 := by cbv
38+
example : search [2, 10, 4, 8, 2, 10, 5, 1, 2, 9, 5, 5, 6, 3, 8, 6, 4, 10] = 2 := by cbv
39+
example : search [1, 6, 10, 1, 6, 9, 10, 8, 6, 8, 7, 3] = 1 := by cbv
40+
example : search [9, 2, 4, 1, 5, 1, 5, 2, 5, 7, 7, 7, 3, 10, 1, 5, 4, 2, 8, 4, 1, 9, 10, 7, 10, 2, 8, 10, 9, 4] = 4 := by cbv
41+
example : search [2, 6, 4, 2, 8, 7, 5, 6, 4, 10, 4, 6, 3, 7, 8, 8, 3, 1, 4, 2, 2, 10, 7] = 4 := by cbv
42+
example : search [9, 8, 6, 10, 2, 6, 10, 2, 7, 8, 10, 3, 8, 2, 6, 2, 3, 1] = 2 := by cbv
43+
example : search [5, 5, 3, 9, 5, 6, 3, 2, 8, 5, 6, 10, 10, 6, 8, 4, 10, 7, 7, 10, 8] = -1 := by cbv
44+
example : search [10] = -1 := by cbv
45+
example : search [9, 7, 7, 2, 4, 7, 2, 10, 9, 7, 5, 7, 2] = 2 := by cbv
46+
example : search [5, 4, 10, 2, 1, 1, 10, 3, 6, 1, 8] = 1 := by cbv
47+
example : search [7, 9, 9, 9, 3, 4, 1, 5, 9, 1, 2, 1, 1, 10, 7, 5, 6, 7, 6, 7, 7, 6] = 1 := by cbv
48+
example : search [3, 10, 10, 9, 2] = -1 := by cbv
4949

5050
/-! ## Missing API -/
5151

0 commit comments

Comments
 (0)
⚡