Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-07-19

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

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/
03:57 keep_learning joined #isabelle
07:50 larsrh joined #isabelle
08:03 chindy I wonder why Isabelle has no find theory or "find file" feature or something like this such that one does not have to grep in /opt or afp directory
08:03 chindy its probably one of things quite easy to implement and increasing usability by quite a bit
08:21 larsrh are you looking for file names or file content?
08:21 larsrh Because for file content it's trivial, use HyperSearch in jEdit
08:26 chindy larsrh: I basically want this in Isabelle instead of the command line: grep -r "asdf" /opt/Isabelle-version/src/chosen_theory or the afp directory
08:27 larsrh chindy: yeah, jEdit can do that
08:27 larsrh press Ctrl-F, select search in directory
08:37 ammbauer there's also the query panel and then "find_theorems" command
08:43 int-e I believe this is about finding theories that have not yet been loaded but may contain relevant lemmas for your own work...
08:44 ammbauer yeah, something like hoogle for the distribution + AFP would be nice
08:44 int-e Once a theory is loaded, find_theorems is great, of course.
08:58 pruvisto well, according to his ERC grant, Larry Paulson is on it.
09:11 larsrh I should tell Larry about libisabelle
09:13 chindy ammbauer: yea what int-e said
09:14 ammbauer larsrh: or get an erc grant for libisabelle :D
09:15 chindy can someone help me with that lemma http://downthetypehole.de/paste/uOlddAhB
09:15 pruvisto chindy: have you tried "apply (auto simp: arg_max_set_def is_arg_max_def)"?
09:15 pruvisto and perhaps then sledgehammer on what's left
09:17 chindy yea... but sledgehammer couldn't find anything
09:17 pruvisto I'll look at it later
09:29 JCaesar just asking: you did not forget the using assms? (i do that a lot.)
09:30 int-e it's missing something like  fixes f :: "'a ⇒ ('b :: linorder)"
09:30 int-e chindy: ^^
09:31 JCaesar hm, why is that necessary, btw?
09:32 int-e hmm
09:32 ammbauer JCaesar: Otherwise nitpick finds a counterexample :P
09:32 int-e well, order is enough
09:33 int-e and so is preorder
09:33 JCaesar meh. is there isabelle-for-phone?
09:34 JCaesar (not that mine could run that...)
09:34 int-e But by default it will use just 'ord' which comes with no properties at all.
09:35 int-e so, http://downthetypehole.de/paste/gwiP4FVF
09:36 int-e oh, le_less_trans even works as a simp rule here
09:36 int-e that's rare
09:47 chindy int-e: ahh thanks i guess it needed some kind of transitivity, right?
09:49 int-e yes, you need that if z > f y and f y >= f x then z > f x, to obtain a contradiction
09:50 int-e (hmm, perhaps I should write f z rather than z)
10:58 JCaesar int-e: Is it possible that the simplifier recently got a bit stronger with things like that?
11:01 int-e I don't know.
11:03 pruvisto I doubt it
11:04 pruvisto I don't think there have been significant changes to the simplifier lately
11:04 pruvisto any non-trivial change to the simplifier will likely result in a lot of broken proofs
11:04 pruvisto which the person making the change would have to fix
11:04 pruvisto and ain't nobody got time for that
11:11 int-e The default simpset is evolving though, so indeed the simplifier can "get better" in certain areas.
11:13 int-e Though I don't see any such changes mentioned for just ord. But Isabelle2016-1 included some changes around ordered rings, for example.
11:24 pruvisto oh I thought w.r.t. working for rules like "le_less_trans
11:24 pruvisto but even default simpset for "general" stuff like orders is very difficult to change
11:24 pruvisto and results in a lot of breaking stuff
11:25 int-e . o O ( let's just change sets back to predicates, shall we... )
11:30 pruvisto don't you dare :P
11:30 pruvisto I'm getting flashbacks
11:56 logicmoo joined #isabelle
13:03 silver joined #isabelle
13:40 chindy whats the difference between let ?xy = "adf" and define xy where "xy = adf"
13:46 int-e The most visible change is that "let" is an abbreviation.
13:48 int-e err, difference, not change.
15:15 pruvisto the main difference is that "xy" introduces a new fixed variable
15:15 pruvisto whereas "?xy" is just a syntactic abbreviation for the term
15:15 pruvisto so when you write "?xy", after parsing, you still have the same term as before
15:15 pruvisto whereas "define" will give you a fixed free variable "xy" that you can unfold to the original thing
15:16 pruvisto "define" can be used to make goals more readable and more easily processed by automation
15:16 pruvisto whereas "let" only lets you write down terms in a shorter way
15:25 larsrh for all practical purposes "define" behaves like a local definition (i.e. constant)
15:25 larsrh you'll get a "constant" x and a theorem x_def
15:26 larsrh these days I prefer define over let
15:26 pruvisto Me, too, usually.
15:26 larsrh although I would really like local abbreviations instead of local definitions
15:26 larsrh anything that doesn't print the unfolded output, really
15:26 pruvisto larsrh: um, just use "write"?
15:27 larsrh err
15:27 larsrh TIL
15:27 larsrh brb, refactoring my proofs
15:28 larsrh disregard that, "write" is "notation" not "abbreviation
15:30 pruvisto hm yeah, write is a lot less useful than I thought
15:31 pruvisto probably why no one ever uses it
15:31 pruvisto I think I used it like once in my life
17:15 dmiles joined #isabelle
18:51 chindy this is only a small excerpt of the whole proof so its proably not very helpful but does someone have an idea why this is not simply the application fo commutativy and therefore trivially true: http://downthetypehole.de/paste/vYKxWUYH
18:59 int-e well, (∑f∈firms. ∑i∈agents. Θ[i,f] *⇩R Price ∙ Y[f]) = (∑f∈firms. (∑i∈agents. Θ[i,f]) *⇩R Price ∙ Y[f])  needs linearity of *⇩R and possibly ∙ (not sure about precedence) in their first argument
19:00 int-e iow, you're doing more than just swapping the two sums
19:11 ezyang joined #isabelle
23:53 silver_ joined #isabelle

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary