# IRC log for #isabelle, 2016-05-18

All times shown according to UTC.

Time Nick Message
01:48 ilbot3 joined #isabelle
01:48 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:19 andromeda-galaxy What's a reasonable way to induct on a list but actually look at the cases xs = [] and xs = as@[a] (instead of xs = a#as)?
02:20 andromeda-galaxy for the program about which I'm trying to prove something, what is done when encountering "later" states is dependent on earlier states, so it makes more sense to append symbols one at a time than to prepend them
02:39 andromeda-galaxy (rev_induct?)
03:51 fracting joined #isabelle
04:14 larsrh andromeda-galaxy: Why can't you make it arbitrary? You can make any variable arbitrary
04:14 larsrh andromeda-galaxy: yes, that's rev_induct
04:26 andromeda-galaxy larsrh: I can't make it arbitrary because the base case proof needs it to be a certain value (because it is a sort of "state" that is used when "processing" "later" items)
04:27 andromeda-galaxy larsrh: rev_induct seems to be working, so far!  What's the best practice for finding this sort of thing?  I stumbled on rev_induct by chance..
04:49 andromeda-galaxy I have an (auxilary) proof that right now is by cases on two variables: (proof (cases v1) case 1 <p1> proof (cases v2) case 1 <p2> next case 2 <p3> qed next case 2 <p4> proof (cases v2) case 1 <p5> next case 2 <p6> qed qed.  <p1> and <p4> are completely identical, and the statements proved in <p2>/<p3>/<p5>/<p6> are also all identical, although the referred-to theorems in each case are slightly different
04:49 andromeda-galaxy (as those proofs actually refer to the case assumptions).  Since each of these blocks is several lines, I'd like to reduce the duplication but am not sure how (except that <p1>/<p4> could maybe be moved out of the case altogether), could anyone recommend strategies for this sort of thing?
04:54 fracting joined #isabelle
04:56 andromeda-galaxy (e.g. is there a way to say something like "use this procedure to prove each case"?)
05:06 mal``` joined #isabelle
05:08 chuchuco1ny joined #isabelle
05:11 andromeda_galaxy joined #isabelle
05:51 ThreeOfEight andromeda_galaxy: you may have to generalise your induction statement
05:52 ThreeOfEight and if I recall correctly, it is always possible to make variables arbitrary (unless they appear in the induction rule); it may just not help
05:52 ThreeOfEight but it shouldn't make your goals any less provable, that's what larsrh probably meant
05:53 ThreeOfEight as for the cases: first of all, you can do two case splits at the same time using either case_prod
05:53 ThreeOfEight (I think the usage was something like "apply (cases nat.cases[case_prod nat.cases])"
05:53 ThreeOfEight or you can use the ";" tactical (e.g. "apply (cases a; cases b)"
05:55 ThreeOfEight not entirely sure what your exact situation is, but you may be able to then just solve /all/ the goals by calling auto with the right set-up
05:55 ThreeOfEight if not, I suggest you pull out the identical cases as an auxiliary lemma, or you show it in Isar before the induction and then just use the lemma.
05:55 ThreeOfEight As always, I can give more concrete suggestions if you give me actual code to work with
07:15 dmiles joined #isabelle
07:48 fracting joined #isabelle
08:43 kyagrd_ joined #isabelle
08:44 chuchucorny joined #isabelle
08:46 cocreature joined #isabelle
08:46 cocreature joined #isabelle
08:47 andromeda-galaxy joined #isabelle
10:02 fracting joined #isabelle
11:09 fracting joined #isabelle
12:32 fracting joined #isabelle
13:55 fracting joined #isabelle
14:45 andromeda-galaxy ThreeOfEight: thanks for the suggestions!  When I finish my main theorem I was planning on pastebinning it here & asking for any/all feedback on improving my proof style
16:39 andromeda-galaxy isar-ref says that ultimately = moreover from calculation, but it also seems to reset calculation.  Is there a form that appends to calculation the same way that moreover does, but automatically uses the other calculation results (so that it's not necessary to put "using calculation" everywhere)?
16:44 ThreeOfEight ~I don't think so
16:52 andromeda-galaxy ThreeOfEight: okay, just curious.  Do you know why iser-ref says it's = moreover from calculation but it appears to be somewhat different?
16:52 andromeda-galaxy (e.g. using moreover from calculation -> works, using ultimately -> doesn't work)
16:52 ThreeOfEight I think that's more of a rough approximation
16:54 andromeda-galaxy ah, okay. By the way, is it (easily) possible to define a new command/keyword/etc that really is an abbreviation for moreover from calculation?
16:57 andromeda-galaxy (I'm guessing that it would require using the ML interface?)
17:08 ThreeOfEight should be pretty easy, but you'd have to use ML, yes
17:14 andromeda-galaxy ThreeOfEight: thanks for the confirmation, after I finish this proof maybe I'll think about doing that..
17:15 ThreeOfEight not quite as easy as I thought
17:15 ThreeOfEight you'd have to know a thing or two about how Isar works
17:15 ThreeOfEight and, in any case, I would say doing something like that is heavily discouraged
17:19 andromeda-galaxy ThreeOfEight: okay, I was thinking of it as a learning project for figuring out more about isar.  why would it be heavily discouraged?
17:20 larsrh You're not really supposed to use 'calculation' yourself
17:20 larsrh it's an implementation detail
17:21 larsrh nothing wrong with giving your facts custom names
17:21 andromeda-galaxy larsrh: hmm, okay...
17:22 andromeda-galaxy I feel like in this particular proof I've been running into lots of proofs that need show a, show b, show c, show d using a b c, show e, show f, show g using c f, etc., which seemed like a good fit for calculational reasoning at first but then seemed to not be because after the first "ultimately" none of the early facts are left
17:23 andromeda-galaxy are you saying that it would be more idiomatic to forget abou that and just name everything
17:23 andromeda-galaxy ?
17:23 larsrh not everything, but the stuff you need
17:23 larsrh you can certainly mix and match
17:24 larsrh moreover have c: ... ultimately have ... from c have ...
17:26 andromeda-galaxy larsrh: well, I'll try rewriting things in that style, thanks for the suggestions (also, sorry for asking so many questions in here, I'm just having a hard time figuring out the most idiomatic ways of doing things---prog-prove doesn't touch on everything, and isar-ref just sort of drops everything on you at once)
17:27 larsrh don't worry
17:27 larsrh Getting questions answered is what this channel is here for :-)
17:27 larsrh Keep in mind that many advanced users also still haven't figured out style yet
17:28 larsrh To quote a particular Isabelle dev when looking at my Isar proofs, "this is shit"
17:28 andromeda-galaxy larsrh: thanks for the reassurance!  Well, I'lj
17:28 andromeda-galaxy just have to try to keep proving and hope that at some point I manage to get to relatively succint & human-readable proofs
17:43 ThreeOfEight In my experience, most Isar proofs are far from "human-readable".
17:43 ThreeOfEight (However, neither are most pen-and-paper proofs)
17:44 ThreeOfEight In a well-written Isar proof, someone who is familiar with the domain and the background theory /and/ with Isabelle and Isar has a reasonable change of finding out what is happening
17:44 ThreeOfEight but that's about it
18:00 ammbauer are there theorem provers which offer something similiar to Isar?
18:05 fracting joined #isabelle
18:17 larsrh ammbauer: Mizar
18:17 larsrh (in fact Mizar inspired the design of Isar)
19:14 fracting joined #isabelle
22:40 andromeda-galaxy Anyone know of a pastebin with isar syntax highlighting support?
22:50 andromeda-galaxy I just finished my first not-entirely-trivial proof in Isabelle; I'd really appreciate any comments/feedback/suggestions on it: http://paste.lisp.org/display/316340