Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-01-09

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

All times shown according to UTC.

Time Nick Message
03:04 lispy_ joined #isabelle
10:51 ThreeOfEight the function package is probably the best way, yes.
10:51 ThreeOfEight someone should really write an ML command to use the function package to just generate an induction scheme without actually declaring a function
10:52 ThreeOfEight Any volunteers? larsrh, I heard you have a lot of spare time at your hands.
11:03 JCaesar Don't bash the dead horse…
12:33 larsrh ThreeOfEight: not sure whether I should laugh or cry about this
12:33 larsrh Because actually I needed such a thing on more than one occasion already
12:33 larsrh *would've needed
12:47 JCaesar So did I.
12:47 JCaesar larsrh: You gave us the wrong topics for our practikum. :P
13:11 ThreeOfEight maybe I'll do it at some point
13:11 ThreeOfEight I've worked on the function package before, after all
17:31 mal`` joined #isabelle
18:27 JCaesar Just me having fun: lemma "0 ≠ 1" … auto Quickcheck found a counterexample: (empty output)
18:28 JCaesar (I'm just wonderin why it's empty.)
18:31 JCaesar (Nothing to output I guess.)
18:31 int-e because there are no free variables... it's be helpful to display the chosen types though
18:32 int-e lemma "0 = (1 :: Enum.finite_1)" by simp
18:32 int-e (I tricked it: lemma "0 * x ≠ 1"  gives an assignment for x with that type)
18:33 int-e or rather, quickcheck gives the assignment
18:36 tangentstorm joined #isabelle
18:36 tangentstorm fun dub :: "nat ⇒ nat" where "dub 0 = 0" | "dub (Suc m) = add (Suc m) (Suc m)"
18:36 tangentstorm ^ the background turns purple on this for me, but there's no output or tooltip to explain what it means.
18:36 tangentstorm what does it mean? :)
18:40 tangentstorm ah, because i had this: theorem add_commut [simp]: "add x y = add x y"
18:40 tangentstorm .. which was sending it into an infinite loop. removing the [simp] fixed it.
18:47 larsrh ThreeOfEight: purple means "processing"
18:47 larsrh sorry
18:47 larsrh tangentstorm: purple means "processing"
18:48 larsrh The "fun" package employs the simplifier for some internal tactics, which means it's particularly dependent on a good [simp] setup
18:48 tangentstorm yeah, thanks. i should have googled a bit more before asking :)
18:49 * tangentstorm is working through "concrete semantics"
18:49 larsrh no worries
18:50 JCaesar (And here I was under the impression that googling doesn't help with Isabelle…)
18:55 ThreeOfEight it doesn't help much
19:01 tangentstorm https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-January/msg00017.html  <- it turned up a mailing list discussion that pointed me in the right direction.
19:02 tangentstorm it doesn't help that all the docs are in PDF though. :/
19:02 ThreeOfEight I think they are generated from .thy files
19:03 tangentstorm that's probably true. i meant for googling though. you get a result and it's just somewhere in a 50-page book. :)
19:04 tangentstorm but there seem to be plenty of great docs, plus stackoverflow ... so it's not like there's a shortage of info.
19:05 larsrh tangentstorm: Makarius is working on better document preparation
19:05 larsrh So there's a chance the docs will be available as multi-page HTML docs at some point
19:05 tangentstorm nice :)
19:28 tangentstorm hrm.  i want to prove that `sum range(n)` = `n * (n+1) / 2`  for natural numbers, but nat doesn't have / defined. I see Divides.thy, but how would I use it?
19:28 tangentstorm oh just 'div' i guess
19:28 larsrh tangentstorm: div
19:28 larsrh yeah, exactly :-)
19:29 larsrh Don't need to import anything, just plain old 'Main'
20:10 tangentstorm well i think i made my proof but i can't figure out how to cap it off
20:10 tangentstorm https://gist.github.com/tangentstorm/4ccb13968414437da36b
20:13 tangentstorm hrm. hold up. i removed the 'fix n::nat assume n>0' and was able to get isabelle to accept it. any thoughts on how i could make it better?
20:20 larsrh tangentstorm: un-quantified variables in the lemma statement are automatically fixed, so no need to fix them again
20:21 larsrh You can still 'assume "n > 0"', that way you don't have to repeat your assumption all the time
20:24 larsrh tangentstorm: I commented on the Gist
21:15 tangentstorm very nice. thank you, larsrh
22:04 ammbauer for fucks sake, in einer funktion ∧ statt ∨ benutzt... auf einmal sind die beweise soviel einfacher... kopf -> tisch.
22:08 larsrh ammbauer: I think you picked the wrong channel
22:13 ammbauer larsrh: ohh, sorry. well, it's isabelle related :D
22:59 tangentstorm is there any way to make jEdit save as unicode instead of latex? (like for \<LongArrow>)
23:29 tangentstorm fun qsort :: "'a::ord list ⇒ 'a list" where "qsort [] = []" | "qsort x#xs = qsort (filter (λy. y≤x) xs)"
23:29 tangentstorm ^ why does this give me type problems? "no type arity list::ord"  ...  op ≤ y :: ??'a ⇒ bool
23:32 int-e qsort x#xs  should be  qsort (x#xs)
23:33 tangentstorm aha. thank you
23:33 int-e as written, (qsort x) # xs  is a list, and that leads to the odd ord requirement for list.
23:34 int-e err. the x in (qsort x) # xs  is a list.
23:34 tangentstorm gotcha. i keep forgeting how tightly function application binds.
23:34 tangentstorm thanks
23:42 larsrh tangentstorm: I don't think there's a way
23:47 tangentstorm oh, to save as unicode? yeah, i went through like every line in the settings and couldn't find anything. no big deal.
23:49 tangentstorm i've moved on to trying to prove that my quicksort actually sorts. :) i think i have a decent setup, but i haven't learned enough to know where to go next: https://gist.github.com/tangentstorm/c23f572bf7ed9771b667
23:53 larsrh tangentstorm: not to curb your enthusiam, but qsort is not trivial, even for advanced users
23:54 larsrh A simpler sorting function you could try to tackle would be selectionsort
23:54 larsrh err, I meant insertionsort
23:55 larsrh If you want to cheat, you can look here: https://github.com/larsrh/sorted/blob/master/Insertion_Sort.thy and check if that looks doable to you
23:57 tangentstorm hrm. that's a lot more work than i expected. thanks for the warning.

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