Email Gateway (Aug 18 2022 at 15:40): Email Gateway (Aug 18 2022 at 15:40):From: Tambet <qtvali@gmail.com>
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:
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 + lengthi, pattern(start + lengthi,
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)
Email Gateway (Aug 18 2022 at 15:40):From: Lawrence Paulson <lp15@cam.ac.uk>
I took a quick look at your problem and attach a small theory file, in which I define your collatzNext function and prove a trivial property of it. To undertake the project you describe, you just have to do one step at a time, and your first step should be to read the tutorial: http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf
It will take a while before you can become proficient enough to do a challenging project.
Larry Paulson
theory Collatz
imports Parity
begin
definition
collatzNext :: "nat \<Rightarrow> nat"
where
"collatzNext n = (if even n then (n div 2) else 3*n + 1)"
lemma "0<n \<Longrightarrow> 0 < collatzNext n"
apply (auto simp add: collatzNext_def)
apply (metis Suc_n_div_2_gt_zero lemma_even_div2)
done
Email Gateway (Aug 18 2022 at 15:40):From: Tobias Nipkow <nipkow@in.tum.de>
If you do not need negative numbers, I suggest to use nat instead of int.
Tobias
Tambet schrieb:
Last updated: Apr 26 2024 at 20:16 UTC