IRC log for #isabelle, 2016-05-19

All times shown according to UTC.

Time Nick Message
01:03 fracting joined #isabelle
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/
02:24 tautologico ammbauer: the new Lean theorem prover also uses a proof language that was clearly inspired by Isar
03:59 fracting joined #isabelle
04:56 fracting joined #isabelle
05:13 fracting joined #isabelle
05:46 ThreeOfEight andromeda-galaxy: mine does: http://downthetypehole.de/paste/
05:46 ammbauer andromeda-galaxy: http://downthetypehole.de/paste/BHgFaITD
05:46 ammbauer ThreeOfEight: oh, you were faster.
05:51 ThreeOfEight The highlighting is afar from perfect (Isabelle highlighting is really complicated) and it's done by some ugly JavaScript
05:51 ThreeOfEight but it works reasonably well
05:52 ThreeOfEight (and it even expands Isabelle symbol codes like \<and> server-side, so you can directly paste a .thy file)
05:53 ThreeOfEight andromeda-galaxy: First tip: use records instead of tuples. They're typically easier to handle, especially when you get more components.
05:53 ThreeOfEight Second, type names are usually not capitalised in Isabelle by convention
05:58 ThreeOfEight Third, "by" accepts two methods: an initial method and a terminal method. The initial method is meant to "refine" the goal, i.e. pre-process the goals; the terminal method then solves them
05:59 ThreeOfEight by A B is more or less an abbreviation of proof A qed B
05:59 ThreeOfEight so something like "by (cases x; cases y; auto)" would more idiomatically be written as "by (cases x; cases y) auto"
07:42 fracting joined #isabelle
08:22 fracting joined #isabelle
10:23 fracting joined #isabelle
10:53 dmiles joined #isabelle
12:11 tautologico joined #isabelle
13:35 fracting joined #isabelle
14:14 fracting joined #isabelle
16:40 fracting joined #isabelle
17:37 andromeda-galaxy ThreeOfEight: great, I'll try using it next time
17:37 andromeda-galaxy ThreeOfEight: thanks for the feedback! I'll try incorporating those suggestions now...
17:58 andromeda-galaxy Any more suggestions would be welcome, here's a version 2 that (I think) incorporates those suggestions: http://downthetypehole.de/paste/vzinAOj9
17:59 andromeda-galaxy (one particular question: I'm making a pretty big leap of reasoning at the end of the second case in the main theorem, that uses a bunch of facts and simplification rules to jump straight to the proof of the main statement; would it be better to add a few more reasoning steps that aren't necessary for the proof to check but help illustrate what's happening?)
18:10 ThreeOfEight Well, that is a common problem
18:10 ThreeOfEight Since I often work on really big proofs, I try to use automation as much as possible
18:10 ThreeOfEight I do add additional intermediate steps if the resulting proof looks fragile to me
18:11 ThreeOfEight but using too many intermediate steps just gets tedious in the end
18:11 ThreeOfEight if there's something that needs more explanation, you can always add a comment and explain it there
18:12 andromeda-galaxy ThreeOfEight: okay, that gives me a better sense of the tradeoffs involved (& alternatives)
18:12 andromeda-galaxy why would you prefer adding a comment?
18:13 ThreeOfEight Don't know; I just do that occassionally, especially for stuff that goes in the AFP
18:14 andromeda-galaxy ah okay, that makes sense
18:14 ThreeOfEight I think it's more important to give the reader a high-level idea of why certain things are proven and how they connect with one another than to have every little step of the individual proofs annotated
18:15 ThreeOfEight if the automation can solve it in a single step, it's probably not really an interesting proof anyway
18:15 ThreeOfEight just a lot of case distinctions and simplification
18:15 andromeda-galaxy hmm, I hadn't considered that before, but that makes sense now---it's hard for me to decide if it's interesting or not, because I've spent a bunch of time trying to figure out how to make it work at all
18:15 larsrh except for Cantor :-)
18:15 andromeda-galaxy but that makes sense
18:15 ThreeOfEight larsrh: yeah but that's cheating and we all know it :P
18:17 andromeda-galaxy well, I'm glad that the rest of the proof looks reasonable overall! Thanks again to everyone for all the suggestions/answers
18:18 ThreeOfEight also, there are cases where automation takes a very long time because it does a lot of needless case distinctions
18:18 ThreeOfEight and you can make a faster and more stable proof with Isar
18:18 ThreeOfEight but that doesn't happen too often
18:18 ThreeOfEight I recall one example related to IPv4 addresses
18:19 ThreeOfEight and in my Bachelor's thesis, there's an instance of some linear inequalities where linarith, despite being a complete decision procedure, just takes much to long
18:19 ThreeOfEight (would probably take several million years)
18:19 ThreeOfEight but smt can solve it in a fraction of a second
18:19 andromeda-galaxy that's interesting!
18:19 ThreeOfEight and an Isar proof can do reasonably well, too
18:20 ThreeOfEight well the problem with linarith is that if it sees a disjunction, it just makes a case distinction for both cases
18:20 ThreeOfEight and if it sees 60 disjunctions, it makes 2^60 case distinctions
18:20 ThreeOfEight which is a really terrible idea
18:20 ThreeOfEight whereas smt uses Z3, and Z3, like alls SMT solver, does a very sophisticated SAT-like thing
18:21 andromeda-galaxy right, I can see why that would be much faster
18:21 ThreeOfEight but SMT proofs are not allowed in the AFP, and they're kind of opaque, so it's not so easy to convince a mathematician that you really have a proof
18:21 ThreeOfEight so I spent half a week developing that into a 500 line Isar proof
18:22 ThreeOfEight well, proofs using the smt method are no less trustworthy than any other Isabelle proofs
18:23 ThreeOfEight it calls Z3, Z3 returns a proof object and the smt method translates that proof object into an Isabelle proof and puts it through the kernel like any other Isabelle proof
18:23 andromeda-galaxy Why doesn't the AFP allow them?
18:23 ThreeOfEight you can even cache the Z3 proof object in a text file and then you're completely independent from Z3 after the first time
18:24 ThreeOfEight That's an interesting question and it is still shrouded in mystery
18:24 ThreeOfEight I made some attempt to clear this up by asking the person who developed smt
18:24 ThreeOfEight You'd have to cache certificates, because otherwise, AFP proofs will depend on Z3, which is an external tool that is not under our control and may not be developed in the future
18:24 ThreeOfEight so we don't want that
18:25 ThreeOfEight however, there have been some issues with cached certificates in the past, but no one remembers quite what they were
18:25 ThreeOfEight I'm pretty sure that in my case, it wouldn't have been a problem because I only used linear arithmetic
18:25 ThreeOfEight but some people claimed that, in the general case, there may be some issues with Isabelle lemmas being used and then renamed
18:26 ThreeOfEight And that that may break the cached certificates. I don't know. smt's developer hasn't commented on it yet.
18:26 ThreeOfEight (note however that there are "not-so-trustworthy" Isabelle proofs as well, namely those using oracles, like the code generation oracle)
18:26 andromeda-galaxy that is interesting... I guess stearing clear of smt is probably the safest route for now...
18:26 andromeda-galaxy code generation oracle?
18:26 ammbauer joined #isabelle
18:27 ThreeOfEight Isabelle has a code generator
18:27 ThreeOfEight that allows you to export executable code (ML, Haskell, Scala, etc.) for your functions
18:27 andromeda-galaxy (right, I've tried using that with my automata)
18:27 ThreeOfEight that's also what the "value" command does
18:27 ThreeOfEight and there's a proof method called "eval" which essentially takes your proof goal, compiles it to ML and runs it
18:27 andromeda-galaxy How does that work when all the names in the expresion aren't resolved?
18:28 ThreeOfEight and if it gets "true" as a result, it accepts it as a theorem
18:28 ThreeOfEight this is done by an oracle
18:28 andromeda-galaxy That does sound dangerous
18:28 ThreeOfEight an oracle is essentially something that can create theorems bypassing the Isabelle kernel
18:28 ThreeOfEight it is
18:28 ThreeOfEight the code generator is reasonably trustworthy, but certain people (like me) do consider such proofs to be less trustworthy
18:28 ThreeOfEight in some cases, it may be the only viable option though
18:29 ThreeOfEight (e.g. when you have to do heavy numerical computation)
18:29 andromeda-galaxy that's unlike e.g. sledgehammer or smt which have the isabelle core check the proof object after it's found?
18:29 ThreeOfEight and what do you mean, unresolved names?
18:29 ThreeOfEight sledgehammer isn't a proof method itself, but it generates calls to proof methods
18:29 ThreeOfEight like simp, blast, force, auto, metis, smt
18:29 ThreeOfEight and all of those go through the Isabelle kernel, yes
18:30 andromeda-galaxy (right of course, but I thouhgt that I had read that it also checked them before suggesting them?)
18:30 ThreeOfEight which checks the proofs down to the axioms of the logic
18:30 ThreeOfEight well I think it checks them by just running the proof methods and seeing if they can prove it
18:30 ThreeOfEight so, yes
18:30 ThreeOfEight (there is an option [[smt_oracle]] for smt that also bypasses the kernel, that's useful for speed)
18:31 andromeda-galaxy by unresolved names I meant something like this: value "foldl (op +) 0 [5, 3, foo]" => "0 + (1 + 1 + (1 + 1) + 1) + (1 + 1 + 1) + foo"
18:31 ThreeOfEight (proof reconstruction usually takes much longer than the actual proof search, so when you're still experimenting, switching that on might make sense)
18:31 ThreeOfEight ah, that doesn't use the code generator
18:32 ThreeOfEight value can use three different backends: code generation, normalisation by evaluation, and the simplifier with a special setup
18:32 ThreeOfEight if there are free variables in the term, it can't use code generation and falls back on one of the other two
18:32 ThreeOfEight you can do value [code] "…" and that will probably fail
18:32 andromeda-galaxy okay, that explains it
18:32 ThreeOfEight whereas value [nbe] "…" and value [simp] "…" will probably work
18:33 andromeda-galaxy by the way, what's a good reference/introduction to all the available proof methods?  isar-ref seems to just be about the isar syntax
18:33 ThreeOfEight I don't think there is one
18:33 mbrcknl joined #isabelle
18:34 ThreeOfEight simp, auto, force, blast, linarith, metis, smt are pretty much the ones I use
18:34 ThreeOfEight and of course the more low-level ones like rule, drule, frule, erule, intro, elim, clarify, safe
18:34 andromeda-galaxy Thanks for the rough list. How is linarith different from arith?
18:35 ThreeOfEight I think arith does more stuff
18:35 ThreeOfEight http://stackoverflow.com/questions/28644151/whats-the-difference-between-arith-and-presburger-in-isabelle/28678826#28678826
18:35 ThreeOfEight ^I answered this question here
18:36 andromeda-galaxy Thanks for the link, sorryI missed it earlieri
18:37 ThreeOfEight Earlier? No, I answered that was a long time ago.
18:37 andromeda-galaxy (earlier => when I tried to find out if that question had been answered before)
18:38 larsrh andromeda-galaxy: To me, it's also very disappointing when I wrote a long, detailed Isar proof which can subsequently refactored into a single 'auto' invocation. It happens, and I always do it if I can
18:40 andromeda-galaxy larsrh: well, that's just what happened here! The consensus seems to be that auto can't usually prove anything huge enough to need explanation (although a comment explaining roughly what it does with relation to the other parts might be useful), and that it's often less fragile/better, although that doesn't necessarily always apply.
18:40 andromeda-galaxy Thanks for all the explanations, I'll keep refactoring my proofs down until 2 days of trying to understand something result in 2 lines of isar
19:24 fracting joined #isabelle
21:30 fracting joined #isabelle
21:57 andromeda-galaxy Is there a way to make something like "by (cases as) (auto simp add: ...)" automatically add the case information to the context for each application of the "auto simp add: "?
21:58 andromeda-galaxy e.g. I'm seeing that form work if the long-form proof looks like "proof (cases as) case 1 have ... by (auto simp add: ...)" but not when it looks like "proof (cases as) case 1 then have ... by (auto simp add: ...)"
22:01 andromeda-galaxy wait sorry, that's not quite it; the problem occurs when the (auto) needs to be "using" some other fact---the combined by doesn't seem to provide a way to pass them through...
22:03 andromeda-galaxy oh wait, never mind, sorry for the noise, it's just simp vs. simp_all