Skip to content

Commit 955976e

Browse files
datokratdatokrat
authored
106 (#197)
This solves problem 106.
1 parent 4239884 commit 955976e

File tree

2 files changed

+296
-3
lines changed

2 files changed

+296
-3
lines changed

‎HumanEvalLean/HumanEval106.lean‎

Lines changed: 293 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,295 @@
1-
def f : Unit :=
2-
()
1+
module
2+
3+
import Lean.LibrarySuggestions.Default
4+
5+
import Std.Tactic.Do
6+
7+
/-!
8+
This file provides three solutions for problem 106, progressing from most simple to most efficient.
9+
-/
10+
11+
set_option mvcgen.warning false
12+
13+
open Std.Do
14+
15+
-- missing grind annotations
16+
attribute [grind =] Nat.length_toList_rco Nat.length_toList_rcc Std.PRange.Nat.succMany?_eq Nat.not_le
17+
18+
section NaiveImpl
19+
20+
/-!
21+
## A naïve implementation
22+
-/
23+
24+
def f (n : Nat) : List Nat := Id.run do
25+
let mut ret : List Nat := []
26+
for i in 1...=n do
27+
if i % 2 = 0 then
28+
let mut x := 1
29+
for j in 1...=i do x := x * j
30+
ret := x :: ret
31+
else
32+
let mut x := 0
33+
for j in 1...=i do x := x + j
34+
ret := x :: ret
35+
return ret.reverse
36+
37+
/-!
38+
### Tests
39+
-/
40+
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
45+
46+
/-!
47+
### Verification
48+
-/
49+
50+
@[grind =]
51+
def factorial : Nat → Nat
52+
| 0 => 1
53+
| n + 1 => factorial n * (n + 1)
54+
55+
@[grind =]
56+
def triangle : Nat → Nat
57+
| 0 => 0
58+
| n + 1 => triangle n + (n + 1)
59+
60+
example : factorial 1 = 1 := by decide
61+
example : factorial 4 = 24 := by decide
62+
example : triangle 1 = 1 := by decide
63+
example : triangle 4 = 10 := by decide
64+
65+
theorem length_f {n : Nat} :
66+
(f n).length = n := by
67+
generalize hwp : f n = w
68+
apply Std.Do.Id.of_wp_run_eq hwp
69+
mvcgen
70+
invariants
71+
| inv1 => ⇓⟨cur, xs⟩ => ⌜xs.length = cur.prefix.length⌝
72+
| inv2 => ⇓⟨cur, xs⟩ => ⌜True⌝ -- factorial loop
73+
| inv3 => ⇓⟨cur, xs⟩ => ⌜True⌝ -- sum loop
74+
with grind
75+
76+
theorem getElem_f {n : Nat} {k : Nat} (hlt : k < n) :
77+
(f n)[k]'(by grind [length_f]) = if k % 2 = 0 then triangle (k + 1) else factorial (k + 1) := by
78+
rw [List.getElem_eq_iff]
79+
generalize hwp : f n = w
80+
apply Std.Do.Id.of_wp_run_eq hwp
81+
mvcgen
82+
invariants
83+
-- outer loop
84+
| inv1 => ⇓⟨cur, xs⟩ => ⌜xs.length = cur.prefix.length ∧
85+
((_ : k < xs.length) → xs[xs.length - 1 - k] =
86+
if k % 2 = 0 then triangle (k + 1) else factorial (k + 1))⌝
87+
-- factorial loop
88+
| inv2 => ⇓⟨cur, x⟩ => ⌜x = factorial cur.prefix.length⌝
89+
-- sum loop
90+
| inv3 => ⇓⟨cur, x⟩ => ⌜x = triangle cur.prefix.length⌝
91+
92+
-- OUTER LOOP
93+
case vc7 => simp -- base case
94+
case vc8 => grind -- postcondition
95+
96+
-- FACTORIAL LOOP
97+
case vc3 => -- step
98+
have := Std.Rcc.eq_succMany?_of_toList_eq_append_cons ‹_›
99+
grind
100+
case vc1 => -- postcondition
101+
simp_all [Std.Rcc.eq_succMany?_of_toList_eq_append_cons ‹_›, factorial, Nat.add_comm 1]
102+
103+
-- SUM LOOP
104+
case vc6 => -- step
105+
have := Std.Rcc.eq_succMany?_of_toList_eq_append_cons ‹_›
106+
grind
107+
case vc4 => -- postcondition
108+
simp_all [Std.Rcc.eq_succMany?_of_toList_eq_append_cons ‹_›, triangle, Nat.add_comm 1]
109+
110+
end NaiveImpl
111+
112+
section EfficientImpl
113+
114+
/-!
115+
## An efficient implementation
116+
-/
117+
118+
def f' (n : Nat) : Array Nat := Id.run do
119+
if n ≤ 2 then
120+
return #[1, 2].take n
121+
let mut ret : Array Nat := .emptyWithCapacity n
122+
ret := ret.push 1 -- 1st entry should be `triangle 1`
123+
ret := ret.push 2 -- 2nd entry should be `factorial 2`
124+
for i in 3...=n do
125+
if i % 2 = 0 then
126+
-- It would be nicer if we could use `ret[i - 2]`, but it is unclear how to use the
127+
-- invariants `ret.size ≥ 2` and `i = ret.size` intrinsically.
128+
ret := ret.push (ret[i - 3]! * (i - 1) * i)
129+
else
130+
ret := ret.push (ret[i - 3]! + 2 * i - 1)
131+
return ret
132+
133+
/-!
134+
### Tests
135+
-/
136+
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
141+
142+
/-!
143+
### Verification
144+
-/
145+
146+
theorem size_f' {n : Nat} :
147+
(f' n).size = n := by
148+
generalize hwp : f' n = w
149+
apply Std.Do.Id.of_wp_run_eq hwp
150+
mvcgen
151+
all_goals try infer_instance
152+
case inv1 => exact ⇓⟨cur, xs⟩ => ⌜xs.size = cur.prefix.length + 2⌝
153+
all_goals try (simp_all; done) -- relies on `Nat.size_Rcc`
154+
grind
155+
156+
theorem getElem_f' {n : Nat} {k : Nat} (hlt : k < n) :
157+
(f' n)[k]'(by grind [size_f']) = if k % 2 = 0 then triangle (k + 1) else factorial (k + 1) := by
158+
rw [Array.getElem_eq_iff]
159+
generalize hwp : f' n = w
160+
apply Std.Do.Id.of_wp_run_eq hwp
161+
mvcgen
162+
invariants
163+
| inv1 => ⇓⟨cur, xs⟩ => ⌜xs.size = cur.prefix.length + 2 ∧ ∀ j : Nat, (_ : j < xs.size) →
164+
(j % 2 = 1 → xs[j] = factorial (j + 1)) ∧ (j % 2 = 0 → xs[j] = triangle (j + 1))⌝
165+
case vc1 hn => -- verification of the early return
166+
grind
167+
case vc4 => -- base case of the loop
168+
grind
169+
case vc2 hmod h => -- `then` branch
170+
have := Std.Rcc.eq_succMany?_of_toList_eq_append_cons ‹_›
171+
grind
172+
case vc3 => -- `else` branch
173+
have := Std.Rcc.eq_succMany?_of_toList_eq_append_cons ‹_›
174+
grind
175+
case vc5 => -- postcondition
176+
grind
177+
178+
end EfficientImpl
179+
180+
section MoreEfficientImpl
181+
182+
/-!
183+
## An efficient implementation avoiding `[·]!`
184+
-/
185+
186+
def f'' (n : Nat) : Array Nat := Id.run do
187+
if n ≤ 2 then
188+
return #[1, 2].take n
189+
let mut ret : Array Nat := .emptyWithCapacity n
190+
ret := ret.push 1 -- 1st entry should be `triangle 1`
191+
ret := ret.push 2 -- 2nd entry should be `factorial 2`
192+
let mut odd := 1 -- `triangle 1 = 1`
193+
let mut even := 2 -- `factorial 2 = 2`
194+
for i in 3...=n do
195+
if i % 2 = 0 then
196+
even := even * (i - 1) * i -- `factorial i = factorial (i - 2) * i * i + 1`
197+
ret := ret.push even
198+
else
199+
odd := odd + 2 * i - 1 -- `triangle i = triangle (i - 2) + 2 * i - 1`
200+
ret := ret.push odd
201+
return ret
202+
203+
/-!
204+
### Tests
205+
-/
206+
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
211+
212+
/-!
213+
### Verification
214+
-/
215+
216+
theorem size_f'' {n : Nat} :
217+
(f'' n).size = n := by
218+
generalize hwp : f'' n = w
219+
apply Std.Do.Id.of_wp_run_eq hwp
220+
mvcgen
221+
invariants
222+
| inv1 => ⇓⟨cur, _, _, xs⟩ => ⌜xs.size = cur.prefix.length + 2⌝
223+
with grind
224+
225+
def lastFactorial (n : Nat) := factorial (n / 2 * 2)
226+
def lastTriangle (n : Nat) := triangle ((n - 1) / 2 * 2 + 1)
227+
228+
@[grind =] theorem lastTriangle_two : lastTriangle 2 = 1 := by decide
229+
@[grind =] theorem lastFactorial_two : lastFactorial 2 = 2 := by decide
230+
231+
@[grind →]
232+
theorem lastTriangle_of_odd (h : n % 2 = 1) : lastTriangle n = triangle n := by
233+
grind [lastTriangle]
234+
235+
@[grind →]
236+
theorem lastFactorial_of_even (h : n % 2 = 0) : lastFactorial n = factorial n := by
237+
grind [lastFactorial]
238+
239+
theorem lastTriangle_add_one (h : n % 2 = 1) :
240+
lastTriangle (n + 1) = lastTriangle n := by
241+
grind [lastTriangle]
242+
243+
@[grind =]
244+
theorem lastFactorial_add_one_of_odd (h : n % 2 = 1) :
245+
lastFactorial (n + 1) = lastFactorial n * n * (n + 1) := by
246+
have : (n + 1) / 2 * 2 = n / 2 * 2 + 2 := by grind
247+
grind [lastFactorial]
248+
249+
@[grind =]
250+
theorem lastTriangle_add_one_of_odd (h : n % 2 = 1) :
251+
lastTriangle (n + 1) = lastTriangle n := by
252+
grind [lastTriangle]
253+
254+
@[grind =]
255+
theorem lastTriangle_add_one_of_even (h : n % 2 = 0) (h' : 0 < n) :
256+
lastTriangle (n + 1) = lastTriangle n + 2 * n + 1 := by
257+
have : n / 2 * 2 = (n - 1) / 2 * 2 + 2 := by grind
258+
grind [lastTriangle]
259+
260+
@[grind =]
261+
theorem lastFactorial_add_one_of_even (h : n % 2 = 0) :
262+
lastFactorial (n + 1) = lastFactorial n := by
263+
grind [lastFactorial]
264+
265+
theorem getElem_f'' {n : Nat} {k : Nat} (hlt : k < n) :
266+
(f'' n)[k]'(by grind [size_f'']) = if k % 2 = 0 then triangle (k + 1) else factorial (k + 1) := by
267+
rw [Array.getElem_eq_iff]
268+
generalize hwp : f'' n = w
269+
apply Std.Do.Id.of_wp_run_eq hwp
270+
mvcgen
271+
invariants
272+
| inv1 =>
273+
⇓⟨cur, even, odd, xs⟩ => ⌜xs.size = cur.prefix.length + 2 ∧ even = lastFactorial xs.size ∧ odd = lastTriangle xs.size ∧ ∀ j : Nat, (_ : j < xs.size) →
274+
(j % 2 = 1 → xs[j] = factorial (j + 1)) ∧ (j % 2 = 0 → xs[j] = triangle (j + 1))⌝
275+
case vc1 hn => -- verification of the early return
276+
-- the return value is a prefix of `[1, 2]` and `k` is the index that needs to be verified
277+
match k with
278+
| 0 => grind
279+
| 1 => grind
280+
| n + 2 => grind
281+
case vc4 => -- base case of the loop
282+
grind
283+
case vc2 hmod h => -- `then` branch
284+
have := Std.Rcc.eq_succMany?_of_toList_eq_append_cons ‹_›
285+
grind
286+
case vc3 => -- `else` branch
287+
have := Std.Rcc.eq_succMany?_of_toList_eq_append_cons ‹_›
288+
grind
289+
case vc5 => -- postcondition
290+
grind
291+
292+
end MoreEfficientImpl
3293

4294
/-!
5295
## Prompt
@@ -43,4 +333,4 @@ def check(candidate):
43333
assert candidate(1) == [1]
44334
assert candidate(3) == [1, 2, 6]
45335
```
46-
-/
336+
-/

‎lakefile.toml‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,9 @@ name = "human-eval-lean"
22
version = "0.1.0"
33
defaultTargets = ["HumanEvalLean", "create-scaffold"]
44

5+
[leanOptions]
6+
experimental.module = true
7+
58
[[lean_lib]]
69
name = "HumanEvalLean"
710
globs = ["HumanEvalLean.*"]

0 commit comments

Comments
 (0)