Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-12-12

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

All times shown according to UTC.

Time Nick Message
09:48 seafood joined #isabelle
10:29 seafood joined #isabelle
11:54 silver joined #isabelle
16:49 chindy joined #isabelle
17:36 chindy can someone help me with this thy? http://pastebin.com/6PpQkiAy \n i am unable to show associativity
17:39 larsrh chindy: 1) aux_lem1 is oriented the wrong way; 2) aux_lem2 is needless and makes the simplifier loop
17:41 chindy ahh..
17:42 chindy larsrh, the problem with aux_lem2 makes sense but how did you see that aux_lem1 was the wrong way?
17:46 chindy ^nvm
17:47 larsrh chindy: a healthy dose of experience :-)
17:47 larsrh most of the time the idea is to "bubble up" the constructors
17:48 larsrh unfortunately I can't provide you with a more coherent explanation
17:48 larsrh btw, you should prefer induct over induct_tac
17:48 larsrh where'd you pick up induct_tac anyway?
17:51 chindy larsrh, the isabelle tutorial from the isabelle website
17:51 chindy whats the difference between induct and induct_tac ?
17:53 larsrh that's what I feared ... the "tutorial" is sadly outdated
17:54 larsrh Please use prog-prove instead
17:54 larsrh just a couple of hours ago the 2016-1 release has been cut; there, the tutorial is not listed as prominently as before
17:55 chindy ahh i see
17:55 larsrh "induct_tac" is what we call "old style"; it does a couple of things in the wrong way
17:55 larsrh e.g. how it deals with assumptions is not as expected
17:55 larsrh rule of thumb: if it ends with "_tac", don't use it unless you know exactly what you're doing
17:55 larsrh the "tutorial" itself is not wrong, it's just describing an outdated style of using the system
17:56 larsrh here's the more modern one: http://isabelle.in.tum.de/dist/Isabelle2016-1/doc/prog-prove.pdf
17:57 chindy thanks a lot
18:37 larsrh you're welcome :-)
18:55 chindy larsrh, could you just help me out again... this is from the exercise in the tutorial you posted (http://pastebin.com/G69FaUc0) i see that isabelle needs som kind of distributive property of listsum/contents but how can give the correct lemma ?
19:32 ThreeOfEight chindy: you probably want something like "lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys""
19:32 ThreeOfEight doesn't have anything to do with contents
19:33 ThreeOfEight you just need the fact that listsum distributes over concatenation of lists
19:34 larsrh your aux_lem1 is not general enough
19:34 larsrh (to be proven directly via induction, that is)
19:34 ammbauer joined #isabelle
19:34 larsrh but it follows directly from listsum_append
19:34 larsrh and with it Ex2_6 goes through as expected
19:34 julian__ joined #isabelle
19:36 ThreeOfEight chindy: out of curiosity, why are you doing Isabelle stuff? Is it for a university course?
19:39 julian__ ThreeOfEight, not really for a course, but its for University. Basically my prof told me is should learn isabelle for my bachelor thesis. But frankly, i dont really wanna bother him with these "basics"
19:39 chindy joined #isabelle
19:41 chindy @ThreeOfEight, yea thanks that worked
19:43 ThreeOfEight chindy: that wouldn't be Rene Thiemann, by any chance?
19:43 chindy no, why ?
19:44 ThreeOfEight Just wondering who else does Isabelle in Austria.
19:46 chindy ThreeOfEight, are you from Amsterdam or Uterecht ?=
19:46 ThreeOfEight chindy: no, Munich.
19:47 ThreeOfEight Right from the main center of activity. (larsrh, too)
19:47 chindy ah... i see
19:47 ThreeOfEight (activity wrt. Isabelle)
19:47 ThreeOfEight So what are you doing in your thesis?
19:49 chindy formalizing some (not too difficult) game theory (hopefully)
19:50 chindy @ThreeOfEight, but why does your ip say you are from amsterdam ???
19:52 ThreeOfEight chindy: because that's where my vserver is
19:52 ThreeOfEight on which my tmux is running
19:53 chindy ahh ... that makes sense ;)
19:53 ThreeOfEight Ah, Game Theory. Very interesting.
19:53 ThreeOfEight I worked on Social Choice Theory in the past.
19:53 ThreeOfEight I even thought about doing some game theory at some point myself. What results are you interested in in particular?
20:11 chindy @ThreeOfEight, well i dont know yet, im gonna have to read up on that over the holidays
22:44 silver_ joined #isabelle

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