Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-04-06

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

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 "well-formedness" 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 int-e it can be proved by (auto simp: less_vec_def less_eq_vec_def)
18:22 int-e 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 int-e: thanks any idea why sledgehammer couldnt find anything ?
18:31 int-e Not really. Perhaps it does not know that 2 has only two elements.
18:34 int-e (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 int-e no. there's no relation between the z and u
18:43 int-e (where "the z" refers to the z that one gets when elminating the existential quantifier in f7)
18:43 int-e 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 int-e hmm, what do you mean by "clean"...
22:10 int-e lemma dup: "X ⟹ X ⟹ X" by simp ... lemma "1 = 1" proof (rule dup, goal_cases)
22:21 int-e 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 int-e 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 int-e I guess I'd put the second proof in an unnamed lemma and leave a comment about why it's there.

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary