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:45 

wagle joined #isabelle 
04:41 

mal`` joined #isabelle 
05:35 

tokenrove joined #isabelle 
06:30 
pruvisto 
xJCI don't know 
06:30 
pruvisto 
JCaesar: I don't know 
06:30 
pruvisto 
I don't see any dangerous equations there 
06:31 
pruvisto 
But the splitter shouldn't really do anything here either, I think 
06:31 
pruvisto 
Have you tried simptracing it? 
06:32 
pruvisto 
(the obvious solution is to prove intro/dest rules for Hintikka and do an Isar proof using them instead of unfolding the entire definition) 
06:33 
pruvisto 
Unfolding a complicated definition like this can sometimes make the automation go haywire 
06:40 
JCaesar 
pruvisto: Since I already found a different way of proving it, I didn't bother with it much further… 
06:43 
larsrh 
remember the ABC of Isabelle 
06:43 
larsrh 
Always 
06:43 
larsrh 
Be 
06:43 
larsrh 
Cleaning up 
06:43 
JCaesar 
*sobs softly* 
06:45 
JCaesar 
the simp trace just stops after a few dozen messages. 
07:38 

ertes joined #isabelle 
08:46 

silver joined #isabelle 
14:20 

aneas joined #isabelle 
14:26 
aneas 
i'm writing applystyle proofs and can't find a way to explicitly reference goal premises. say i'm using induction on a datatype like list. deep inside the proof i want isabelle to apply the induction hypothesis, which often is stated as the first premise. in cases where simp cannot proof all premises of the IH, i cannot fall back on using subst, because the first premise has no name i can use. is there any way i can do this without usin 
14:26 
aneas 
g isar style proofs? 
14:39 
inte 
there's the subgoal command, which can also extract premises subgoal premises IH 
14:39 
inte 
though typically I use this for exploration and switch to isar style in the end. 
14:42 
aneas 
holy shit 
14:43 
aneas 
this would have saved me days! 
14:43 
aneas 
thank you very much! 
14:45 
pruvisto 
aneas: I haven't quite understood what you want, but there is also "goal_cases" 
14:45 
pruvisto 
which is a proof method that assigns names to goals 
14:45 
pruvisto 
e.g. "proof (rule A, rule B, goal_cases)" 
14:46 
pruvisto 
then you can do "case (1 …)", "case (2 …)" etc. 
14:46 
pruvisto 
you can also do "goal_cases A B C" to choose other names than the default ones (1, 2, 3) 
14:47 
aneas 
pruvisto, i guess this is useful for isar style proofs? can those names be used in apply style proofs? 
14:48 
pruvisto 
Oh, yes, I think this is only useful for Isar 
14:48 
pruvisto 
if you only want to do applystyle proofs, I don't think it'll help you at all 
14:48 
pruvisto 
on the other hand, if you are doing applystyle proofs that are this complicated, you might want to think about whether it'd be a good idea to use Isar instead anyway 
14:50 
inte 
http://downthetypehole.de/paste/gJNFrs3z < I find that often the Isar style, besides being more readable, is shorter simply because one can easily pick out specific subgoals and leave the easy ones to auto. 
14:50 
inte 
(the example is artificial of course, induct auto would suffice) 
14:51 
pruvisto 
I don't think I've ever used subgoal 
14:51 
pruvisto 
would have been quite useful a few years ago ^^ 
14:51 
pruvisto 
(but it didn't exist back then) 
14:51 
inte 
didn't exist then :P 
14:51 
aneas 
hm, I see. so far every isar proof I tried was significantly longer than applys 
14:53 
aneas 
i'm afraid my usage of isabelle is very clumsy and overly complicated. just as an example: i just finished the "main" proof of my theory. its ~600 lines of applies and subgoals. horrible 
14:53 
pruvisto 
Quite possibly, but shortness isn't everything 
14:53 
aneas 
but this is totally my fault 
14:53 
pruvisto 
Isar tends to be much more explicit and verbose than applystyle scripts, and therefore often longer 
14:53 
pruvisto 
but it's more understandable and maintainable 
14:54 
pruvisto 
you can still make a mess of things in Isar (and I frequently do), but it's a lot better than apply scripts 
14:54 
pruvisto 
I'm not saying that /whatever/ you do, you should always prefer Isar to applyscripts, but you should at least consider it. 
14:54 
aneas 
i'll try using it more 
14:55 
pruvisto 
And, re: your fault, well, Isabelle is far from perfect. There are lots of things that could be improved (and are being improved). 
14:55 
pruvisto 
And I don't think anyone is satisfied with the documentation (and particularly the introductory material for beginners) that we have 
14:56 
aneas 
something that would help me greatly would be a way to break down simple apply proofs to isar style, even if its only restating all intermediate subgoal states 
14:56 
aneas 
i have found the documentation to be quite good, if you know what you're looking for 
14:57 
aneas 
the isar ref, however, didn't help me very much to discover important and helpful things 
14:58 
aneas 
its more like a encyclopedia, which doesn't priorities, or provide many examples 
14:59 
pruvisto 
Yes. 
14:59 
aneas 
oh, and working with jedit is a pain for programmers like me :) 
15:00 
pruvisto 
How so? 
15:03 
aneas 
some issues are small. for example, i still haven't figured out how to get a nonblock cursor, so after months of usage i still have problems selecting things 
15:06 
aneas 
i love the continuous verification, but i would prefer it if it just assumed everything with qed, done, and sorry to be correct, and prove everything in parallel. if something fails to prove later on, jedit should indicate that separately. sometimes, when adding a trivial lemma in a different theory, i have to wait minutes before i can continue using it, and i think tthis could be improved greatly 
15:07 
aneas 
and then there are many missed opportunities. quite often, isabelle displays me the current state, and i just want to click on a specific subexpression and apply a rule there 
15:08 
JCaesar 
isar proofs do thend to parallelize better than apply. 
15:08 
aneas 
oh, ok. that explains a lot 
15:08 
JCaesar 
and isabelle does assume that things are done as soon as you write by foo. 
15:08 
JCaesar 
(and will run the prover in background.) 
15:09 
aneas 
oh, and for large expressions, the pretty printed output is still unreadable. a simple parenthesishighlighting on mouse over would help me very much 
15:09 
JCaesar 
oh yes… btw, wasn't there some nonjedit thing recently? electron, or so? 
15:10 
pruvisto 
Visual Studio Code 
15:10 
pruvisto 
but it'll need more work before it's actually usable 
15:11 
pruvisto 
there's a good chance that it will become the "default" editor for Isabelle in the future 
15:11 
pruvisto 
Makarius is pushing it quite a bit 
15:11 
aneas 
is it worth a try in its current state? 
15:11 
pruvisto 
aneas: as JCaesar has already said, there is quite a bit of parallelisation already 
15:12 
pruvisto 
every "by" forks the proof to a background thread 
15:12 
JCaesar 
hm, subgoal, does, too… 
15:12 
pruvisto 
and I think "lemma" is a kind of "checkpoint" as well 
15:12 
aneas 
then i'm doing something wrong. because i've never seen isabelle proving two subgoals simultaneously 
15:12 
pruvisto 
but if you change something somewhere, Isabelle will have to reprocess everything after that 
15:13 
pruvisto 
because the entire "theory" may have changed 
15:14 
aneas 
pruvisto, yes, because isabelle stays in the realm of constant correctness. however, sometimes i just want to continue working with the outdated state, and have isabelle catch up later 
15:15 
JCaesar 
that's very likely… just going to be weird. what the provers do does depend on what comes before them, after all… 
15:15 
aneas 
what i mean is that almost always  by that i mean after almost all keypresses  nothing of any significance changed 
15:16 
aneas 
maybe, i don't know 
15:16 
JCaesar 
Well, knowing what is significant is… tricky, at best. 
15:17 
aneas 
yes 
15:17 
aneas 
anyway, isabelle is still amazing 
18:12 

ertesx joined #isabelle 
19:22 
chindy 
"XY::set = argmax (SOME func . property func Z) SET" is there some way of expressing an argument as a return value? so for example given the argmax function that takes a function and a SET i want to give it a function that is defined as a propertiy of type "(nat>nat) => nat set => bool" 
19:23 
chindy 
well the function is defined as having to have the property 
19:27 
chindy 
so basically is there some standard way of wrapping a predicate of type "'func => Set => bool" into "Set => func" given that 
20:25 
chindy 
given obvsl hat such an object exists 
20:54 
pruvisto 
chindy: I think you're looking for the choice operators 
20:54 
pruvisto 
there's "SOME x. P x" and "THE x. P x" 
20:55 
pruvisto 
they do have their uses, but if you can avoid using them, I would suggest that you do 
20:58 

larsrh joined #isabelle 
21:51 

silver joined #isabelle 
22:29 
chindy 
ah thanks 
22:30 
chindy 
Can someone tell me what i am missing? or why sledgehammer has so much trouble proving: lemma assumes "S ≠ {}" shows"(Max S ∈ S)" 
22:31 
inte 
hmm, what is Max. 
22:31 
chindy 
...i was hoping it is the max element of set S 
22:32 
chindy 
Latices_Big.thy 
22:32 
chindy 
defines it 
22:32 
chindy 
subsection ‹Minimum and Maximum over nonempty sets› 
22:34 
inte 
"F A = the (Finite_Set.fold (λx y. Some (case y of None ⇒ x  Some z ⇒ f x z)) None A)" 
22:34 
inte 
so it'll only work for finite sets, I'm afraid. 
22:34 
chindy 
uuh... :/ 
22:35 
JCaesar 
There's also Sup, maybe that works for you… 
22:36 
JCaesar 
hm, but wasn't there a saner max definition? 
22:36 
chindy 
also that... explains a lot... why so many lemmas with Max dont seem to work 
22:36 
inte 
Sup comes from a syntactical class, hmm 
22:36 
chindy 
i couldn't find anyhting 
22:37 
chindy 
other than Max 
22:37 
JCaesar 
wait… if I say "term Max" and follow the click, I just land in some locale in Lattices_Big.thy… 
22:37 
chindy 
yea i said that somewhere above 
22:38 
inte 
JCaesar: yes, and I copied that so I could navigate further, until I found that definition of F. 
22:38 
inte 
(which is used in Min = Min.F and Max = Max.F) 
22:40 
inte 
(I suppose `f` will be `min` and `max`, respectively) 
22:40 
JCaesar 
anyway, why is it not defined like "Max S = THE x. ∀y ∈ S. y <= x", or so… 
22:41 
chindy 
what is `f` 
22:41 
inte 
chindy: there's an `f` used in the definition of `F` earlier. I'm using `...` to quote identifiers, perhaps a bad habit in the Isabelle context. 
22:44 
inte 
I would speculate that nonempty finite sets is about the only class for which you can define maximum /as a function/ in a reasonable way. 
22:44 
inte 
I'm a bit irritated that it doesn't seem to exist as a predicate though. 
22:45 
inte 
(I'm only looking at Main though) 
22:45 
chindy 
yea JCaesar 's definition sounds quite good 
22:46 
inte 
But it'll give you seemingly random values if S doesn't have a maximum. 
22:46 
chindy 
I was also quite surprised that i wasnt able to find an argmax definition 
22:46 
inte 
JCaesar's definition is incomplete: it needs to assert x : S as well. 
22:47 
chindy 
well it probably only makes sense to define max in closed sets, right 
22:48 
JCaesar 
Oh, right, forgot about that… 
22:49 
inte 
for real numbered sets I would expect that people use Sup and have lemmas that Sup is a member of the set if the set is closed and bounded. 
22:49 
inte 
ugh. subsets of the reals, I should write 
22:51 
chindy 
well im screwed i guess, since i need some defintion for Euclidean space :/ 
22:53 
chindy 
but wouldnt it be possible to define it over every set that has a total order is convex (and maybe some other stuff) 