The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

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.