IRC log for #isabelle, 2017-03-30

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: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 apply-style 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 int-e there's the subgoal command, which can also extract premises   subgoal premises IH
14:39 int-e 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 apply-style proofs, I don't think it'll help you at all
14:48 pruvisto on the other hand, if you are doing apply-style 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 int-e 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 int-e (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 int-e 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 apply-style 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 apply-scripts, 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 re-stating 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 non-block 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 parenthesis-highlighting on mouse over would help me very much
15:09 JCaesar oh yes… btw, wasn't there some non-jedit 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 re-process 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 int-e 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 non-empty sets›
22:34 int-e "F A = the (Finite_Set.fold (λx y. Some (case y of None ⇒ x | Some z ⇒ f x z)) None A)"
22:34 int-e 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 int-e 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 int-e JCaesar: yes, and I copied that so I could navigate further, until I found that definition of F.
22:38 int-e (which is used in  Min = Min.F  and Max = Max.F)
22:40 int-e (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 int-e 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 int-e I would speculate that non-empty finite sets is about the only class for which you can define maximum /as a function/ in a reasonable way.
22:44 int-e I'm a bit irritated that it doesn't seem to exist as a predicate though.
22:45 int-e (I'm only looking at Main though)
22:45 chindy yea JCaesar 's definition sounds quite good
22:46 int-e 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 int-e 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 int-e 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 int-e 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)