The Coq mailing list

["Kyle Stemen" <ncyms8r3x2 AT snkmail.com>]

You can use even_odd_dec for the even/odd check. If you're dealing with natural numbers, you still need general recursion to recursively call the function with x/2, as Adam pointed out.

Note that if you use integers instead of natural numbers, the x/2 recursion is easier. Integers are already stored in binary in Coq.

On Mon, Feb 16, 2015 at 12:49 PM, Adam Chlipala adamc-at-csail.mit.edu |coq-club/Example Allow| <qhp3ztn3ot AT sneakemail.com> wrote:

You might find it helpful to read Chapter 7 of CPDT <http://adam.chlipala.net/cpdt/>, which explains several approaches to general-recursive function definitions in Coq.  There's going to be a catch, no matter which method you choose!

On 02/16/2015 03:36 PM, Jakub Arnold wrote:

Hey guys,

I've came across a few excercises in one of my classes and thought I could try proving them in Coq, but I can't find a way to represent them. The simplest one looks like this.

Prove that the following function does multiplication on natural numbers

f(x,y) := if x = 0 then 0

             else if (x is even) then 2 * f(x/2, y)

                     else 2 * f(x/2, y) + y

I've managed to find the Arith.Div2.div2 function, which seems it could take care of the division, but I'm not really sure how to represent this as a Fixpoint, since the conditional requires a bool, but even is a Prop, though what I'm trying to prove feels more like a computation than a Prop.

Thanks for any tips! Sorry if this question is too easy, this is my first post on the mailing list.