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 
andromedagalaxy 
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 
andromedagalaxy 
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 
andromedagalaxy 
(rev_induct?) 
03:51 

fracting joined #isabelle 
04:14 
larsrh 
andromedagalaxy: Why can't you make it arbitrary? You can make any variable arbitrary 
04:14 
larsrh 
andromedagalaxy: yes, that's rev_induct 
04:26 
andromedagalaxy 
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 
andromedagalaxy 
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 
andromedagalaxy 
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 referredto theorems in each case are slightly different 
04:49 
andromedagalaxy 
(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 
andromedagalaxy 
(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 setup 
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 

andromedagalaxy joined #isabelle 
10:02 

fracting joined #isabelle 
11:09 

fracting joined #isabelle 
12:32 

fracting joined #isabelle 
13:55 

fracting joined #isabelle 
14:45 
andromedagalaxy 
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 
andromedagalaxy 
isarref 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 
andromedagalaxy 
ThreeOfEight: okay, just curious. Do you know why iserref says it's = moreover from calculation but it appears to be somewhat different? 
16:52 
andromedagalaxy 
(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 
andromedagalaxy 
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 
andromedagalaxy 
(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 
andromedagalaxy 
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 
andromedagalaxy 
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 
andromedagalaxy 
larsrh: hmm, okay... 
17:22 
andromedagalaxy 
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 
andromedagalaxy 
are you saying that it would be more idiomatic to forget abou that and just name everything 
17:23 
andromedagalaxy 
? 
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 
andromedagalaxy 
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 thingsprogprove doesn't touch on everything, and isarref 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 
andromedagalaxy 
larsrh: thanks for the reassurance! Well, I'lj 
17:28 
andromedagalaxy 
just have to try to keep proving and hope that at some point I manage to get to relatively succint & humanreadable proofs 
17:43 
ThreeOfEight 
In my experience, most Isar proofs are far from "humanreadable". 
17:43 
ThreeOfEight 
(However, neither are most penandpaper proofs) 
17:44 
ThreeOfEight 
In a wellwritten 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 
andromedagalaxy 
Anyone know of a pastebin with isar syntax highlighting support? 
22:50 
andromedagalaxy 
I just finished my first notentirelytrivial proof in Isabelle; I'd really appreciate any comments/feedback/suggestions on it: http://paste.lisp.org/display/316340 