# IRC log for #isabelle, 2017-03-24

All times shown according to UTC.

Time Nick Message
02:48 ilbot3 joined #isabelle
02: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/
04:33 wagle joined #isabelle
10:53 silver joined #isabelle
11:50 JCaesar Uh, am I missing something? Does finite (dom S) ==> finite (ran S) hold?
12:08 pruvisto JCaesar: I guess so?
12:09 JCaesar I'm proving it in very weird ways right now, e.g. first proving finite (dom M) ==> ∃m. M = map_of m…
12:12 pruvisto JCaesar: http://downthetypehole.de/paste/015sbvqU
12:14 int-e http://sprunge.us/XCVd ?
12:14 int-e *compares*
12:15 JCaesar narf.
12:16 JCaesar auto3++ auto4++
12:19 int-e why didn't I know about -`
12:34 larsrh JCaesar: I have this proof somewhere
12:34 JCaesar larsrh: auto3 already applied…
15:11 JCaesar the irony of my theories: if there's apply, that is by me. if there's an isar proof… sledgehammer.
15:13 pruvisto olol
15:13 pruvisto I'm sure that Isar proof is very readable
15:13 JCaesar Uh, actually… this one is kinda good…
15:13 JCaesar for sledgehammer standards.
15:13 pruvisto I actually have almost no "apply"s anywhere
15:14 pruvisto the only exception is coinduction-related stuff
15:15 pruvisto which accounts for like 5 or 6 applies in about 10 kLOC of proofs
15:15 pruvisto but to be fair, I sometimes put quite a bit of stuff into a "by"
15:15 pruvisto by (rule foo, rule bar, rule narf) (insert A, simp_all)
15:15 pruvisto by (rule A, simp, force)+
15:15 pruvisto things like that
15:16 JCaesar that's actually worse than apply style…
15:16 JCaesar much more annoying to fix.
15:16 JCaesar (speaking from experience…)
15:16 pruvisto Well, depends on what the rules look like and where they come from.
15:17 pruvisto and those are some of the more extreme examples
15:17 JCaesar my favourite is: you used that one magic Multiset rule, which has now been removed, and you can, for the life of it, not remember what it did.
18:08 silver_ joined #isabelle
18:12 ertesx joined #isabelle
19:37 int-e joined #isabelle
19:39 int-e joined #isabelle
19:42 int-e joined #isabelle
19:42 int-e joined #isabelle