The Coq mailing list

[Michel Levy <michel.levy1948 AT gmail.com>]

On 16/02/2015 21:36, 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.

--

Jakub

The main difficulty is to write in Coq the definition of f.
I give first the librairies where you will find the definition of div2 : nat -> nat, even : nat -> bool, log2 : nat -> nat.
Require Import Coq.Arith.Div2.
(* div2 *)
Require Import Coq.Numbers.Natural.Peano.NPeano.
(* even  log2*)

But there is another difficulty. In Coq, you should write the recursive function with a "clearly" decreasing argument, for example (S k) decreases in k.
But it's not clear to Coq that x/2 (i.e. div2 x) < x.
What decreases is the "binary" length of x. So I suggest to introduce this length as a third argument.
f(x,y) = g(1+log2 x,x,y)
g(l,x, y):= if l=0 then 0 else if (x is even) then 2*g(l-1,x/2,y) else 2*g(l-1,x/2,y)+y
It's easy to translate, with a match _expression_, the definition of g in Coq, with the first argument clearly decreasing.

-- 
email : michel.levy1948 AT gmail.com
http://membres-liglab.imag.fr/michel.levy