Adjusted formatting of provided spec in human_eval problem_2#73
Adjusted formatting of provided spec in human_eval problem_2#73amit9oct merged 1 commit intotrishullab:mainfrom
Conversation
There was a problem hiding this comment.
Pull request overview
This PR addresses issue #72 by making human_eval/problem_2’s problem_spec formatting/structure consistent with the rest of the human_eval suite, by moving the precondition into the local spec predicate.
Changes:
- Move
number > 0implication insidespec(instead of guarding the whole termination+postcondition). - Simplify the termination/property clause to
∃ result, ... ∧ spec result(consistent with other problems).
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| number > 0 → | ||
| 0 ≤ res ∧ | ||
| res < 1 ∧ | ||
| number.floor + res = number; | ||
| number > 0 → | ||
| -- program terminates | ||
| (∃ result, impl number = result ∧ | ||
| ∃ result, impl number = result ∧ | ||
| -- return value satisfies spec | ||
| spec result) | ||
| spec result |
There was a problem hiding this comment.
Moving the precondition number > 0 inside spec changes problem_spec from an outer implication (number > 0 → ...) to an existential with an inner implication (∃ result, ... ∧ (number > 0 → ...)). The existing theorem correctness proof below still does intro npos right after unfolding, which will no longer type-check because the goal is no longer an implication at the top level. Update the proof to first provide a witness (e.g., use result / refine ⟨result, rfl, ?_⟩) and then intro npos to discharge the inner implication.
There was a problem hiding this comment.
It type-checks on my machine, so either I am missing something, or Mr. Copilot here is hallucinating :(
There was a problem hiding this comment.
(build also succeeded in the automatic tests)
|
@amit9oct everything looks good on my side, should be ok to merge |
Hi @amit9oct,
me again, again...
PR addessing issue #72. Let me know if you agree with the edit, or if I'm missing anything.