stuck with a proof

You need to do the math correctly first: find two functions that are inverse of each other.

You initial intent is correct: odd numbers to one side, even numbers to the other side, but what you store on each side should cover all the natural numbers, so you will probably have to divide by 2 somewhere.

For Coq usage, You should load the Arith package, by starting with the following line:

Require Import Arith.

This way, you can benefit from existing functions, like Nat.div2 and Nat.even and all the existing theorems about them. To find the relevant theorems, I suggest commands like:

Search Nat.even 2.
Search Nat.div2.

Last hint: proving properties of Nat.div2 by induction is rather difficult for beginners. Try to use the existing theorems as much as possible. If you choose to perform a proof by induction concerning div2, go look in the sources in file theories/Arith/Div2.v : the author of that file designed a specific induction theorem called ├Čnd_0_1_SS just for that purpose.

CLICK HERE to find out more related problems solutions.

Leave a Comment

Your email address will not be published.

Scroll to Top