The Coq mailing list

["Vincent Siles" <vsiles AT lix.polytechnique.fr>]

Hi Tambet,

I think you ask the wrong questions:
1) do you know how to prove this "on paper" without Coq or Isabelle ?
if not, you should start here.
2) if you do, do you manage to correctly state the lemmas inside Coq
(datastructes & so on) ?
if you don't, you should ask help for that precisely before going on
3) if you do, what are the technical points that you don't manage to solve ?

This is a list about proving things "with" coq, so you should be a little
more precise about your issues.

Best regards,
Vincent

> I also played with Isabelle and playing with both helped to formalize,
> what
> I want to prove. Anyway, I am unable to enter this proof to either of
> those
> ...at leas reading this would help you to help me ;) This needs creating
> some class, defining Collatz sequence next number, "follows" concept and
> "is
> followed by 1" concept; also it needs, possibly, a binary analysis of a
> number?
>
> Thus, the following is what I want to formalize (and check):
>
>
> fun p(a) = if (p(a) % 2 = 0) then (p(a div 2)) else (a).
> The greatest divisor of a, which is power of two = p(a).
>
> I want to show that the number of multiplication-addition series always
> equals p(a+1) and gives odd result for odd, even result for even and
> follows
> the formula (((3/2)**(p(a+1)))*a+1)-1.
> This should be trivial by binary analysis.
>
> I want to show that because of this even-odd differentiation, 3n+1 series
> is
> never called more than twice in a row. This follows from upper.
>
> I want to show that for any even number, all following even numbers will
> have p(n) >= a(n) and that when looked from the position of n/2, that will
> come back to even if n/2 it started with was odd and vice versa, because
> div2 can't possibly change oddity of any upper level.
>
> Thus, starting from even it leads to odd (next number) and starting from
> odd
> it leads to even (smaller number). Modulus is built in such way that p(n)
> for each even number is p(n)+1 related to it's division by two and this
> p(n)
> is how many times it will be divided by two, thus p(n) for any following
> even is big enough to lead to smaller number (n/2+1 for next one, as
> numbers
> grow, also this p(n) grows and thus, even leads to following(n)<=n+1).
>
> I want, thus, to show that the sequence always eventually leads to smaller
> number than it started from or 1.
>
>
> Python check for those claims for first 100000 numbers (or just make the
> constant larger) is
> available<https://docs.google.com/leaf?id=0B3C-f_zmS2XoMDM3OGM4YmUtNWE2OS00M2M0LWFiOTAtNTVkYWVkZjEyOTRl&hl=en&authkey=CLOM7pQM>
> .
>
> Tambet
>