Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Equality proof of a simple computation

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Equality proof of a simple computation


Chronological Thread 
  • From: Jakub Arnold <darthdeus AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Equality proof of a simple computation
  • Date: Mon, 16 Feb 2015 21:36:26 +0100

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



Archive powered by MHonArc 2.6.18.

Top of Page