The Coq mailing list

[Paul Tarau <paul.tarau AT gmail.com>]

Hi Cedric,

Thanks for the code in test.v - it is a real "tour de force" of what
Coq can do in good hands!

Just curious why you say that

> And as well binary representation allow computing with other numbers
> that your representation cannot!

It turns out that the size binary tree representation for an n-bit
number is never larger than 2n+1 - the max occurs for Mersenne numbers
 of the form 2^n-1.

So the representation is quite practical - a sketch of an arbitrary
length integer package for Java using this representation - a possible
alternative to BigInteger class is at:

http://logic.csci.unt.edu/tarau/research/bijectiveNSF/

Paul

On Sun, Jun 19, 2011 at 10:21 AM, AUGER Cedric 
<Cedric.Auger AT lri.fr>
 wrote:
> Le Thu, 16 Jun 2011 11:20:51 -0500,
> Paul Tarau 
> <paul.tarau AT gmail.com>
>  a écrit :
>
>> My next challenge is to describe arithmetic computations directly on
>> binary trees - a kind of hereditary base 2 exponent notation - as used
>> in Goodstein's theorem). It is interesting because it allows computing
>> with gigantic numbers that binary representations cannot handle. The
>> intuition is that the first argument of the constructor C represents
>> an exponent of 2, recursively
>
> And as well binary representation allow computing with other numbers
> that your representation cannot!
>
>> Unfortunately, Coq rejects this with:
>>
>> Error: Cannot guess decreasing argument of fix.
>>
>> I think that termination of the mutually recursive Fixpoint
>> follows from the fact that at each step in every match
>> in every definition at least one argument becomes structurally
>> simpler - so every reduction in the mutually recursive
>> definition makes progress towards termination.
>
> It is the fact in coq, but not in your example.
>
>> Is it the mutual recursion that confuses Coq? Doest it make sense to
>> use the bijection to nat "t2n" as a measure? Defining a well founded
>> relation seems tricky as one needs successor/predecessor to work
>> first.
>
> It is tricky, but not impossible (I did it).
> I send what I did; do not expect it to be easy to read.
>
> I never use Program or Function; because it is not so often I would
> have use of it, there are some limitations, and I don't understand all
> what is performed (not because it is too complex, but because I have
> always been too lazy to try to use it). But I guess, that your example
> is a typical case where you may wish to use it.
>
> I also put a function to convert [nat] to [T], but I guess it can be
> simplified (by removing some of its specifications).
>
> I changed the definition of "exp2", so that all multiplications were
> removed.
>
>> P.S. The Haskell equivalent works as expected so it is unlikely that I
>> have any logical erros in my definition. Here it is:
>>
>> data T = E|C T T deriving (Eq,Read,Show)
>>
>> s0 E = E
>> s0 (C E y) = C (s0 (s0 y)) (s1 (s0 y))
>> s0 (C (C _ _) _) = E
>>
>> s1 E = E
>> s1 (C E y) = s1 y
>> s1 (C (C a b) y) = C (p2 a b) y
>>
>> p2 E E = E
>> p2 E (C a b) = C (C (s0 a) (s1 a)) b
>> p2 (C a b) y = C E (p2 (p2 a b) y)
>>
>> -- successor and predecessor on type T
>> s x = C (s0 x) (s1 x)
>> p (C x y) = p2 x y
>>
>> -- nat to T conversion
>> n2t 0 = E
>> n2t x | x>0 = s (n2t (x-1))
>>
>> -- T to nat conversion
>> t2n E = 0
>> t2n (C x y) = 2^(t2n x)*(2*(t2n y)+1)
>>
>> -- tests
>> check = map (t2n.n2t) [0..31]
>> pcheck = map (t2n.p.s.n2t) [0..31]
>
> In fact, assuming coq is consistant, your function is good and
> terminates.
>