Skip to content

Fix to test case (problem_103) and formatting issues in sample_examples #71

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
amit9oct merged 3 commits into from
Apr 3, 2026
Merged

Fix to test case (problem_103) and formatting issues in sample_examples #71

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
019a998
fixed test case in problem_103.lean
barabbs Mar 28, 2026
1fb6e4f
added missing generated_spec_body section in problem 3 and 5 in sampl…
barabbs Mar 28, 2026
6a2917a
removed inconsistent by at the end of spec_isomorphism section in sam…
barabbs Mar 28, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/lean4/human_eval/problem_103.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -82,7 +82,7 @@ else
-- #test implementation 7 13 = some "0b1010"
-- #test implementation 964 977 = some "0b1111001010"
-- #test implementation 996 997 = some "0b1111100100"
-- #test implementation 185 546 = some "0b101101110"
-- #test implementation 185 546 = some "0b101101101"

Copilot AI Mar 28, 2026

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The updated expected output matches the current implementation/problem_spec behavior (it uses xs.sum / xs.length, i.e., integer division/floor). However, the problem docstring still says "Round the answer to the nearest integer", which conflicts with the floor-rounding used by all existing tests (e.g., (964, 977) → 970.5 → 970). Please update the docstring to reflect floor rounding (or change the spec/implementation to do nearest-integer rounding and update the tests accordingly).

Copilot uses AI. Check for mistakes.
-- #test implementation 362 496 = some "0b110101101"
-- #test implementation 350 902 = some "0b1001110010"
-- #test implementation 197 233 = some "0b11010111"
Expand Down
2 changes: 1 addition & 1 deletion src/lean4/sample_examples/problem_1.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -413,7 +413,7 @@ linarith
theorem spec_isomorphism:
∀ impl,
(∀ score_changes threshold, problem_spec impl score_changes threshold) ↔
(∀ score_changes threshold, generated_spec impl score_changes threshold) := by
(∀ score_changes threshold, generated_spec impl score_changes threshold) :=
-- end_def spec_isomorphism
-- start_def spec_isomorphism_proof
sorry
Expand Down
4 changes: 3 additions & 1 deletion src/lean4/sample_examples/problem_3.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,8 @@ def generated_spec
(impl: Nat → Nat)
-- inputs
(n: Nat) : Prop :=
--end_def generated_spec
--start_def generated_spec_body
-- spec
let spec (result: Nat) :=
match n with
Expand All @@ -62,7 +64,7 @@ match n with
-- return value satisfies spec
∃ result, impl n = result ∧
spec result
-- end_def generated_spec
-- end_def generated_spec_body

-- start_def iso_helper_lemmas
lemma fib0_unique (n : ℕ) (h : fibonacci_non_computable 0 n) : n = 0 :=
Expand Down
4 changes: 3 additions & 1 deletion src/lean4/sample_examples/problem_5.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,9 +50,11 @@ def generated_spec
(impl: Nat → Nat)
-- inputs
(n: Nat) : Prop :=
--end_def generated_spec
--start_def generated_spec_body
-- spec
sorry
-- end_def generated_spec
-- end_def generated_spec_body

-- start_def spec_isomorphism
theorem spec_isomorphism:
Expand Down
Loading