Time 
Nick 
Message 
01:47 

ilbot3 joined #isabelle 
01:47 

Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html  Now with logging: http://irclog.perlgeek.de/isabelle/ 
04:05 

chindy_ joined #isabelle 
07:29 
larsrh 
can we just kill proof terms please ... 
08:02 

dave24 joined #isabelle 
10:41 
pruvisto 
larsrh: that is starting to sound like a very intriguing idea 
10:41 
pruvisto 
I get the tourches, you get the pitchforks? 
10:41 
pruvisto 
*torches 
10:48 
JCaesar 
Yay! 
10:48 
JCaesar 
And I'll get some popcorn… 
10:48 
pruvisto 
In all honesty, proof terms are a nice thing to have. In theory. 
10:49 
JCaesar 
(I'm not entirely sure I know what a proof term is… It's a datatype that encodes the entire proof, with every derivation step?) 
10:49 
pruvisto 
I don't know much about them; I've only seen this from the side lines, but it is starting to seem like they are causing a lot of engineering problems with no pay off, considering that they are still completely unusable for anything other than tiny toy examples. 
10:49 
pruvisto 
JCaesar: pretty much 
10:50 
pruvisto 
The idea is that you could check such a proof term independently so that you don't have to trust the Isabelle kernel 
10:50 
JCaesar 
kek 
10:50 
pruvisto 
And depending on what kind of stuff you've used in the proof, you can use them for code extraction 
10:51 
pruvisto 
i.e. if you've proven some existential statement, you can derive an actual executable function that computes a witness 
10:51 
pruvisto 
of course, that doesn't work when you use classical reasoning 
10:51 
pruvisto 
it's a bit like what the Coq people do, but they do that much more excessively and not only on small examples 
11:12 
dave24 
hello, I'm new to HOL and Isabelle and trying to understand how I would go about writing specifications for programs. 
11:13 
pruvisto 
dave24: can you be more concrete? 
11:14 
dave24 
In particular I'm trying to write a verified implementation of a binary message format and I am not sure how I would write a spec which could be used to prove an implementation correctly translates native types into binary message strings 
11:15 
dave24 
pruvisto: sorry, irc client would not let me send the whole thing in one go. 
11:17 
pruvisto 
what program? 
11:17 
pruvisto 
i.e. in what language? 
11:18 
dave24 
I was going to use isabelle code generation, because it seemed the easiest 
11:18 
dave24 
But it does not have to be 
11:18 

silver joined #isabelle 
11:36 
pruvisto 
dave24: if you're okay with using the code generation, that makes it a lot easier 
11:36 
pruvisto 
so probably you want to write something like "encode" and "decode" functions and prove that "decode (encode x) = x" 
11:37 
pruvisto 
assuming that your encodings are bit strings 
11:37 
pruvisto 
if it's more like a bit stream, things might get a bit more complicated 
11:37 
pruvisto 
because I'm not sure how one would best encode the property that your decode function doesn't read "too much" from the input stream 
11:38 
pruvisto 
as for how to encode binary stuff, I you can either do "bool list" if you /really/ want to operator on single bits 
11:38 
pruvisto 
but something like "8 word list" (i.e. a list of bytes) would probably be more reasonable 
11:39 
dave24 
yes, I found the Word theory and was panning to use that 
11:40 
dave24 
and "decode (encode x) = x" is nice and easy, but that does not gurantee that the format it creates is actually correct 
11:41 
dave24 
s/panning/planning 
11:47 
dave24 
so should I just start with lemmas for each type, for example one lemma for integers that can be encoded as a single byte given that the integer is smaller than a certainnumber? 
11:48 
larsrh 
dave24: is the idea that each type has exactly one decoding/encoding function? 
11:49 
larsrh 
if so I'd recommend using a type class 
11:49 
dave24 
can I still generate SML if I use type classes? 
11:50 
dave24 
or only haskell? 
11:50 
larsrh 
the code generator will translate it to use records in SML 
11:52 
pruvisto 
dave24: well in that case you'll have to specify your format somehow 
11:52 
pruvisto 
i.e. some "wellformedness" predicate, and prove that "encode x" always fulfils it 
11:52 
pruvisto 
What this predicate will look like depends on your specific use case 
11:53 
pruvisto 
but you can write down such a predicate using "fun" or "inductive" 
11:54 
dave24 
larsrh: ok, thanks I will have a closer look at type classes 
11:54 
dave24 
pruvisto: Thanks. I will try using inductive. 
11:55 
pruvisto 
type classes are kind of orthogonal to this, I think 
11:55 
pruvisto 
the constants you'll define and the theorems you'll prove will be the same 
11:55 
pruvisto 
type classes would just allow you to write things down a bit more uniformly 
11:55 
dave24 
I'll try both and see which one takes me further 
14:40 
dave24 
datatype a = AMap "(a, a) map" 
14:40 
dave24 
this does not work, is there some way of achieving some sort of equivalent? 
14:41 
larsrh 
Are you sure you want a map with a as keys _and_ values? 
14:42 
dave24 
I think so, I'm using a datatype to represent my binary format which allows having maps as keys of maps 
14:42 
dave24 
its much like json in structure 
14:43 
dave24 
oh json doesent allow that, correction: aside from maps as keys, its much like json 
14:43 
larsrh 
are these maps finite? 
14:44 
larsrh 
If so you might be able to get away with "(a \<times> a) list" 
14:47 
larsrh 
note: recursive occurrence in negative positions are highly suspicious 
14:48 
dave24 
hm ok, thanks 
16:48 

chindy joined #isabelle 
16:49 
chindy 
So did you get a cake pruvisto ? 
17:45 
chindy 
Can anyone explain, why this seems to be so difficult t proof ? 
17:45 
chindy 
lemma "(u::real) > 0 ⟹ ((x::real^2) + u *⇩R 1) > x" sorry 
18:07 
pruvisto 
what if x=0.5 and u =0.1 ? 
18:08 
pruvisto 
or is x a vector 
18:08 
pruvisto 
no cant be 
18:12 

ertesx joined #isabelle 
18:22 
inte 
it can be proved by (auto simp: less_vec_def less_eq_vec_def) 
18:22 
inte 
but I spent what felt like half an hour on finding the names of these definitions. sigh. 
18:25 
chindy 
pruvisto: x:: reall^2 
18:25 
chindy 
inte: thanks any idea why sledgehammer couldnt find anything ? 
18:31 
inte 
Not really. Perhaps it does not know that 2 has only two elements. 
18:34 
inte 
(I don't even know how that ^<n> stuff works... maybe I'll find out another day) 
18:35 
chindy 
(real , 2) vec == real ^2 
18:35 
chindy 
and afaik with vectors its "hardcoded" types 
18:35 
chindy 
so 2 is not a nat but a type 2 
18:35 
chindy 
but i bet pruvisto can explain better 
18:37 
chindy 
wouldn't step f5 in combination with f7 be enough proof the last open proof ( resolve sorry) http://downthetypehole.de/paste/2q3Ajhfn 
18:41 
inte 
no. there's no relation between the z and u 
18:43 
inte 
(where "the z" refers to the z that one gets when elminating the existential quantifier in f7) 
18:43 
inte 
eliminating. 
18:49 
chindy 
i see ... 
20:57 

silver joined #isabelle 
21:23 
JCaesar 
Hm, btw, is there a nice way of writing down two proofs for something, and have both checked? 
21:23 
JCaesar 
(I mean, I can just state the thing twice (even with (is ?foo) if it's long), but i'd like something clean. 
22:07 

ammbauer joined #isabelle 
22:10 
inte 
hmm, what do you mean by "clean"... 
22:10 
inte 
lemma dup: "X ⟹ X ⟹ X" by simp ... lemma "1 = 1" proof (rule dup, goal_cases) 
22:21 
inte 
But why, are you having a beauty context? > http://downthetypehole.de/paste/K4C5bDzH 
22:21 
JCaesar 
no, more like a replacement for lemma foo by(fact bla) lemma foo by(fact blubb) 
22:24 
inte 
well, lemma foo by (rule dup, fact bla, fact blubb) would do the trick? I really don't quite see the use case. 
22:28 
JCaesar 
Oh, that's what you planned. 
22:29 
JCaesar 
Didn't get that there… 
22:29 
JCaesar 
The use case is that I have two proofs, and I don't know which is more likely to break in a future version. 
22:33 
inte 
I guess I'd put the second proof in an unnamed lemma and leave a comment about why it's there. 