Simple Parity Test

[nSchell4]

A simple test case to learn dafny by proving a familiar concept: if x is even or y is even, then x*y is even.

[Copilot]

Pull request overview

This PR introduces a Dafny proof for a parity property: if either x or y is even, then their product x*y is even. The implementation includes a predicate to check evenness and a test method with a corresponding proof lemma.

• Adds isEven predicate that recursively checks if a natural number is even
• Implements ParityTest method that asserts the parity property using ParityProof lemma
• Creates ParityProof lemma stub in the proofs directory

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated 1 comment.

File	Description
parity.dfy	Defines the isEven predicate and ParityTest method, but is located in the root directory instead of testcases/ where it should be according to the repository's build system
proofs/parity.dfy	Defines the ParityProof lemma with the appropriate ensures clause for the parity property

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

Pull request overview

Copilot reviewed 2 out of 2 changed files in this pull request and generated 2 comments.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[tapaswini-kodavanti]

As suggested by Copilot, the decreases clause is necessary for the predicate and proof skeleton to ensure there is a termination condition.

[amerikrainian]

As suggested by Copilot, the decreases clause is necessary for the predicate and proof skeleton to ensure there is a termination condition.

Have you verified this? Dafny can often infer decreasing quantities provided they are singular, like $n$. Consider, for example, the more.dfy test. Deleting decreases x from proofs/more.dfy still makes it pass.

[nSchell4]

As suggested by Copilot, the decreases clause is necessary for the predicate and proof skeleton to ensure there is a termination condition.

I have a proof which works without the decreases clause. Also, this file (proofs/parity.dfy) is for people to write their own proof, so this seems like an implementation-specific issue

[JohnEdwardJennings]

On my machine (Dafny 4.11.0+fcb2042d6d043a2634f0854338c08feeaaaf4ae2, WSL), I don't get an error saying it failed to prove termination for any loops. I think this is a good, simple-to-understand test case that people can get started with, so I'm approving it.

[JohnEdwardJennings]

LGTM

[Copilot]

Pull request overview

Copilot reviewed 2 out of 2 changed files in this pull request and generated no new comments.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.