Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-06-24

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

All times shown according to UTC.

Time Nick Message
01:47 ilbot3 joined #isabelle
01:47 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/
08:09 fracting joined #isabelle
08:30 silver joined #isabelle
08:30 silver_ joined #isabelle
08:30 silver__ joined #isabelle
11:01 silver_ joined #isabelle
12:47 fracting joined #isabelle
12:50 fracting joined #isabelle
14:01 int-e Is there a deep reason why  simp only:  exists but  elim only:   and  intro only:  don't?
14:01 int-e (and  dest only: ... I keep forgetting about dest)
15:14 fracting joined #isabelle
15:48 popinman322 joined #isabelle
15:49 tautologico joined #isabelle
16:48 JCaesar int-e: Because dest/intro/elim aren't applied eagerly, maybe?
16:51 larsrh int-e: try just "del:"
16:54 int-e background: I had an application of 'auto' that took 3 seconds and it's 6 times faster with  simp only: (no rules; no simplification steps were performed anyway, as far as I could see), which led me to wonder how fast it would be if only the relevant intro and elim rules were present.
16:55 int-e it's not a big deal.
16:57 JCaesar int-e: Well, you can always build your own stuff with apply(intro foo|elim bar)+ or so…
16:57 JCaesar Btw, what should I fill in for X: rule<->intro; erule<->elim; drule<->X ?
17:00 larsrh JCaesar: drules are the odd one out; they're translated to erules internally anyway
17:01 int-e JCaesar: well, elim foo.cases  tends to not terminate.
17:02 larsrh yeah, because generated case rules are not conditional
17:05 int-e JCaesar: so I'm heavily relying on auto's backtracking there
17:10 JCaesar Hmm… metis, then?
17:11 JCaesar But no, that's not good stlye…
17:17 fracting joined #isabelle
17:23 larsrh metis is fine
18:09 int-e The full proof looks somewhat like this, http://lpaste.net/1640249187163439104 ... the 'clarify' involves rewriting using existing equations and reasoning about constructors (Foo a b = Foo c d <--> a = b /\ c = d)... metis won't find this in reasonable time. I'm actually fairly happy with auto (respectively force) here.
18:12 int-e datatype puts unnamed facts into claset ... I don't like unnamed facts.
18:12 int-e hmm, or are they named but hidden?
18:51 JCaesar putting a print_theorems right behind the datatype declaration should show all their names… (iirc)
19:51 fracting joined #isabelle
20:51 fracting joined #isabelle
20:55 fracting joined #isabelle
21:46 fracting joined #isabelle
22:13 fracting joined #isabelle
22:16 fracting joined #isabelle
22:43 fracting joined #isabelle
23:13 fracting joined #isabelle
23:39 fracting joined #isabelle
23:41 fracting joined #isabelle
23:44 fracting joined #isabelle

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