coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Equality proof of a simple computation, Jakub Arnold, 02/16/2015
- Re: [Coq-Club] Equality proof of a simple computation, Adam Chlipala, 02/16/2015
- Re: [Coq-Club] Equality proof of a simple computation, Kyle Stemen, 02/17/2015
- Re: [Coq-Club] Equality proof of a simple computation, Kyle Stemen, 02/17/2015
- Re: [Coq-Club] Equality proof of a simple computation, Michel Levy, 02/17/2015
- Re: [Coq-Club] Equality proof of a simple computation, Adam Chlipala, 02/16/2015
Archive powered by MHonArc 2.6.18.