Re: [isabelle] Questions about Isabelle



If you do not need negative numbers, I suggest to use nat instead of int.

Tobias

Tambet schrieb:
> Sorry for reposting, but I had a few errors (whole day played with Isabelle,
> now a bit blurry). This is the same message with errors fixed (hope that
> moderator catches the previous one).
> 
> Hello!
> 
> 
> I would like to ask a few questions about Isabelle, because in a day of
> reading manuals and testing things, I have some questions needed to do
> anything at all left unanswered.
> 
> I did, in previous few days, study about Coq, but found out that Isabelle
> language use is much more intuitive to me and it has some tools built-in,
> which Coq lacks.
> 
> 
> However, now I have a number of problems:
> 
>    - Loading built-in libraries is extremely slow. Is there any kind of
>    caching, compilation or preloading technique to make it faster?
>    - Built-in heuristics tool does not solve things and I think that this is
>    related to some bias in my understanding of semantics, because things are
>    really trivial.
>    - Search of patterns is extremely slow - is Isabelle meant only for
>    supercomputers and clusters?
> 
> 
> Next thing that I quite much do not understand the Class semantics. I am
> used to programming languages, mostly imperative, but with many plays with
> others, but it's a first try I try to use prover. I am actually completely
> lost with that.
> 
> 
> I give concrete examples about what I want to do to get on track:
> 
> I want to prove several things about Collatz sequences. For that, I tried
> (taking fibonaccy series and primes theories as examples) to just formulate
> a class, which contains all positive naturals. I did write fixes clause with
> 'a => bool and definition that it's over zero. After that I tried to prove
> with heuristics, that even integers of that class are bigger than one - this
> failed. I tried to unfold the definition from class, but wasn't able to do
> that. Now I think that maybe this class does not provide me that check at
> all? It's basically copy of similar class from primes with definitions for
> naturals removed as I thought that maybe it does not have enough rules for
> naturals.
> 
> 
> Also, as I'm not even conscious about what exactly to ask, is this possible
> to just give me random important hints about good strategies and common
> biases related to proving similar things:
> 
> 
> I would like to define the following properties to numbers:
> 
> Collatz itself, is this OK:
> 
> fun
>   collatzNext :: "int \<Rightarrow> int"
> where
>   "collatzNext n =
>    (if (n \<in> even) then (n div (2::int)) else
>    (if (n \<in> odd) then ((3::int) * n) + (1::int) else
>    1))"
> 
> I am somewhat worried about this last else clause - it should not be "1",
> but undefined. Such output is not possible as I'm considering only the
> typical version of Collatz with naturals. I would like to do in one step:
> create class that collatz(i) or smth. is positive natural so that I could
> use it in definitions (instead of writing everywhere the clause >0) and
> prove that thus, it's output is also positive natural (I imagine that this
> proof will be automatically asked from me when defining such function?) I
> wasn't able to prove this trivial thing - actually I wasn't able to even
> prove that things belonging to my class of positive naturals are always
> bigger than zero. Thus, maybe the class was totally wrong? I haven't done
> classes with Haskell, I am only tried Haskell for a few days as my
> girlfriend learns it (sometimes) and I do not want to take the fun away by
> knowing better. Anyway, I am now stuck with Isabelle classes - or do I need
> a class at all?
> 
> Second, I would like to define such things:
> "follows a b" for a comes after b in series.
> "nextto a b" for b is right after a.
> I would better like to use something like a \<before> b and a \<rightbefore>
> b.
> 
> I would like to have everything after a available as sequence for this class
> of rules:
> head (collatzSequence a) \<in> even.
> first (collatzSequence a) \<in> even. - how to argument about concrete
> position, for example that third element is first even element and thus,
> second element is last odd element in this series?
> 
> 
> I would also like to (check and) prove the following lemmas:
> 
> 
> I am playing with Coq and Isabelle now :) Formalizing the following:
> 
> 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 - how to use that and mix with
> other parts?
> 
> 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.
> 
> Which classes and other stuff I should use for all that?
> 
> Tambet
> 
> 
> 
> Brute-force (python) check for those lemmas follows:
> 
> # -*- coding: utf-8 -*-
> 
> def iterCollatz(number, included=False):
>   if number == 0:
>     return
>   if included:
>     yield number
>   while number != 4:
>     while number % 2 == 0:
>       number /= 2
>       yield number
>     number *= 3
>     number += 1
>     if number != 4:
>       yield number
>     else:
>       return
> 
> def pow(number, p):
>   # For integers
>   if p == 0:
>     return 1
>   r = 1
>   for a in range(0,p):
>     r *= number
>   return r
> 
> def maxp2(number):
>   # Count the zeros at end of number
>   a = number
>   p = 0
>   while a % 2 == 0 and a > 1:
>     a /= 2
>     p += 1
>   return p
> 
> def nextp2(number):
>   b = 1
>   while b < number:
>     b *= 2
>   return b
> 
> def simulate(number):
>   times = maxp2(number+1)
>   result = pow(3, times) * (number + 1) / pow(2, times) - 1
>   # print "Guess: " + str(result)
>   for b in iterCollatz(number):
>     if b == result:
>       # print "Guess correct"
>       return
>   print "Guess wrong"
> 
> def pattern(start, length, highlight=-1):
>   s = ""
>   for a in range(start, start+length):
>     if a < 0:
>       n = "-"
>     elif maxp2(a) == 0:
>       n = "o"
>     elif maxp2(a) > 9:
>       n = "+"
>     else:
>       n = "%1d" % maxp2(a)
>     if a == highlight:
>       n = "*%s" % n
>     elif highlight != -1:
>       n = " %s" % n
>     s += n
>   return s
> 
> def patternDiff(start, start2, length, highlight=-1):
>   s = ""
>   for a in range(0, length):
>     d = maxp2(a+start) - maxp2(a+start2)
>     if a+start < 0 or a+start2 < 0:
>       n = "-"
>     if d == 0:
>       n = "o"
>     if d == -1:
>       n = "A"
>     if d == -2:
>       n = "B"
>     if d == -3:
>       n = "C"
>     elif d < 0:
>       n = "!"
>     elif d > 9:
>       n = "+"
>     else:
>       n = "%1d" % (maxp2(a+start) - maxp2(a+start2))
>     if a+start == highlight:
>       n = "*%s" % n
>     elif highlight != -1:
>       n = " %s" % n
>     s += n
>   return s
> 
> def patternShiftSeq(start, length, count):
>   print "Init: %8d %s" % (start, pattern(start, length))
>   for i in range(0, count):
>     print "Diff: %8d %s %d" % (start + length*i, patternDiff(start +
> length*i, start, length), start)
>     print "Self: %8d %s" % (start + length*i, pattern(start + length*i,
> length))
> 
> def patternMulSeq(number, length, count):
>   print "Init: %8d %s" % (number, pattern(number, length))
>   for i in range(0, count):
>     print "Diff: %8d %s %d" % (number * pow(2, i), patternDiff(number *
> pow(2, i), number, length), number)
>     print "Self: %8d %s" % (number * pow(2, i), pattern(number * pow(2, i),
> length))
> 
> def patternMul3Seq(start, length, count, shift, difp=-1):
>   if shift % 2 == 0:
>     print "Error: there is no 3n for even value"
>   for i in range(1 + shift, count * length + shift, length):
>     print "Diff: %8d %s %d" % (((start + i)*3+1)/2, patternDiff(((start +
> i)*3+1)/2, start + i, length), start + i)
>     print "Prev: %8d %s" % (start + i, pattern(start, length))
>     if difp != -1:
>       print "Dif+: %8d %s %d" % (((start + i)*3+1)/2, patternDiff(((start +
> i)*3+1)/2, start + difp, length), start + difp)
>       print "Pre+: %8d %s" % (start + difp, pattern(start + difp, length))
>     print "Next: %8d %s" % (((start + i)*3+1)/2, pattern(((start +
> i)*3+1)/2, length))
> 
> def collatzPattern(number):
>   for b in iterCollatz(number):
>     print "%4d %s" % (b, pattern(b-25, 25, b))
> 
> def Series(a):
>   s = ""
>   d = []
>   while a != 1:
>     a = a + 1
>     p = 0
>     while a % 2 == 0:
>       #s += " "
>       d += [1]
>       a = a / 2
>       p += 1
>     s += str(p)
>   return s
> 
> def Collatz1(a):
>   t = 0
>   b = a / pow(2, maxp2(a))
>   c = a / pow(2, maxp2(a))
>   for a in iterCollatz(a):
>     if a % 2 == 1:
>       if t == 0:
>         c = a
>       if t > 1 and b % 2 == 0:
>         print "Error"
>       if t > 1 and c+1 < a == 0:
>         c = a
>       if t > 1 and b < a:
>         print "Error"
>       #print t, b > a
>       #print "%10d %30s" % (a, Series(a)), b
>       t = 0
>       b = a
>     else:
>       t += 1
> 
> for a in range(1, 100000):
>   Collatz1(a)





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.