Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-03-23

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

All times shown according to UTC.

Time Nick Message
00:23 silver_ joined #isabelle
06:49 dmiles joined #isabelle
07:12 pruvisto JCaesar: if it's just milliseconds, it's probably too short to be measured reliably anyway
07:13 pruvisto better set up some ML code that runs longer and benchmark that
07:13 pruvisto there's something like Timing.start() etc. do do that sort of stuff
10:12 ertes joined #isabelle
11:24 silver joined #isabelle
12:17 chindy how do you assign a "variable" or synonym to an expression in an isar proof, so that i dont have to constantly type it out
12:17 chindy so let-in or sth
12:41 JCaesar let ?foo = "blargh"
12:42 JCaesar there's also def baz == "hrrrng", but that's deprecated and I don't like the new define command.
12:43 JCaesar let creates an input abbreviation, def/definition really create a new local definition which you might have to unfold in a proof.
12:44 ammbauer joined #isabelle
12:54 pruvisto JCaesar: what's the problem with "define"?
12:54 pruvisto It works great
12:55 pruvisto "define" is great because 1. big proof states get more readable 2. you can hide unnecessary detail from the automation
12:55 pruvisto and the only overhead you have w.r.t. let is that you may have to unfold the definition equations a few times
12:55 pruvisto which isn't really a big deal
12:56 JCaesar can you define [simp]: btw?
12:56 JCaesar But hm, I don't remember why I didn't like it…
12:56 int-e pruvisto: the obligatory "where" is annoying for "define" in proofs.
12:57 int-e define foo where "foo = 42"  vs.  def foo == "42"
13:03 pruvisto JCaesar: I think so, but I'm not sure.
13:04 pruvisto when I define something, I usually do /not/ want Isabelle to unfold the definition automatically
13:04 pruvisto making terms smaller through definitions can make automation much more effective
13:04 pruvisto int-e: can't say that bothered my very much really
13:04 pruvisto but it is, arguably, unnecessary
13:06 int-e it's a nuisance mainly because I have already grown used to 'def'.
13:08 pruvisto I think Makarius does not like the idea that a variable is fixed implicitly
13:10 int-e . o O ( I should send a bug report to the isabelle mailing list. *runs* *ducks* )
14:04 aneas why is it that sometimes apply (subst xyz) works but apply (simp add: xyz) doesn't?
14:05 pruvisto aneas: I can think of two reasons
14:05 pruvisto 1. simp is unable to prove the pre-conditions of the rule
14:05 pruvisto 2. the rule contains existential variables (i.e. variables that appear in the premises, but not in the conclusion)
14:06 pruvisto so applying it would introduce schematic variables in the premises and the simplifier doesn't do that
14:06 JCaesar 3. simp thinks the thing is too dangerous and wraps it in a ?P = True.
14:06 pruvisto Huh?
14:07 aneas pruvisto, does 1. imply that subst tries harder to prove pre-conditions than simp?
14:07 pruvisto aneas: no, subst does not try to prove anything at all
14:07 pruvisto it just applies the rule and adds the pre-conditions to your goal
14:07 pruvisto so you have to deal with them
14:08 aneas oh, right
14:08 pruvisto "simp" never adds new goals (except possibly through splitting)
14:09 JCaesar pruvisto: The I've had a simplifier 'bug' like that.
14:10 JCaesar it thought that some ?a = ?b was not usabel, and instead of adding that it added (?a = ?b) = True to the simpset…
14:10 JCaesar *ble
14:11 aneas ok, i think i understand my problem now, thanks!
14:13 pruvisto JCaesar: That is odd
14:13 pruvisto I've never heard of such a thing
14:13 pruvisto but quite possible
14:24 aneas in a case where apply simp fails to apply a rule that was declared simp, is there any way to find out why? maybe by running apply (simp only: xyz) with additional debugging flags?
14:25 pruvisto well, there is the simp trace
14:25 pruvisto and the new simp trace
14:25 aneas its frustrating to do thing manually, when a simple glue-lemma would enable simp to do its job...
14:25 pruvisto but I've never actually used either of them in a fruitful way
14:26 pruvisto it's a continuing source of embarrassment for us and someone will try to improve things soon
14:26 JCaesar declare[[simp_trace]] outside of a proof, note[[simp_trace]] inside.
14:27 aneas ok, i'll try that. wish me luck :D
14:27 JCaesar I've pulled some useful information out of there on two occasions, but mostly, it's just… too much.
18:12 ertesx joined #isabelle

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