# IRC log for #isabelle, 2016-01-10

All times shown according to UTC.

Time Nick Message
00:02 tangentstorm i guess i'll stick with the exercises in concrete semantics for the time being.
01:21 int-e wow, one can make qsort look deceptively simple... http://sprunge.us/KCJa
01:23 int-e (this is a bit shorter than I expected, but it took quite a few detours to get there...)
01:26 int-e Isabelle's own definition of 'sorted' turns out to be more convenient than tangentstorm's; it's fairly easy to show that for linear orders, they are equivalent.
01:58 tangentstorm cool, int-e :)
02:00 tangentstorm i was trying to make something work by saying if (max(list a)) < (min(list b)) and both a and b are sorted, then a @ b is sorted.
02:00 tangentstorm i'm stuck just trying to prove that   x <= y   ==>   x = (min x y)   though :/
02:09 tangentstorm lemma assumes "x ≤ y" shows "(min x y) = x" using assms by (simp only: min_def; auto)
02:09 tangentstorm surely there's a better way?
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:10 tangentstorm :(
04:10 tangentstorm lemma "(x ≤ y) ∧ (y ≤ z) ⟹ (x ≤ z)" sorry
04:11 tangentstorm why wouldn't ≤ work like that?
04:18 tangentstorm lemma lt_trans: fixes x y z assumes "(x ≤ y) ∧ (y ≤ z)" shows "(x ≤ z)" sorry
04:18 tangentstorm still doesn't work but i guess that's better.
05:27 spacekitteh joined #isabelle
05:28 spacekitteh how can i find the documentation for proof method "HOL.step"?
10:17 JCaesar tangentstorm: I'm guessing your missing a type (class).
10:21 JCaesar I can show a lemma fixes x y z :: "'a :: preorder" shows "x ≤ y ⇒ y ≤ z ⇒ x ≤ z" by(rule_tac y = y in order_trans, simp_all), but that's kind of more ugly than I would expect.
10:21 JCaesar Hm, using order_trans also does it with blast and a few others.
10:22 JCaesar (And It's just re-showing order_trans anyway.)
11:08 ThreeOfEight larsrh: wait what?
11:08 ThreeOfEight quicksort is difficult?
11:10 ThreeOfEight well, as int-e has shown, it is not.
11:10 larsrh ThreeOfEight: it isn't if you use 'sorted' from the library and its setup
11:10 larsrh I was under the impression tangentstorm wanted to define everything himself
11:10 ThreeOfEight hm
11:11 ThreeOfEight yeah it might require a few auxiliary lemmas
11:11 ThreeOfEight but unlike insertion sort and bubble sort etc., you don't need any auxiliary functions and complicated invariants
11:12 ThreeOfEight actually, yeah, insertion sort is probably really easy
11:13 ThreeOfEight tangentstorm: are you using your own definition of min?
11:13 ThreeOfEight because if you're using the built-in one, there is min_absorb1
13:32 int-e tangentstorm: Oh, I should have brought up type classes... I defined qsort for 'a::linorder instead of 'a::ord (ord just says that the type 'a comes with relations <= and <); one needs a preorder to ensure that the result of qsort is always sorted; a partial order to prevent that elements of the list are duplicated; and a total order (linorder) to prevent that list elements are dropped by qsort.
14:38 JCaesar ThreeOfEight: It's not entirely simple, is it? Termination is a bit of a problem, no?
14:43 larsrh JCaesar: for qsort? No, don't think so
14:43 larsrh For bubblesort, probably yes
14:50 JCaesar Oops, bubblesort is what I meant, yes…
16:01 ThreeOfEight yeah I think you have to define the number of inversions in the list and show that that decreases with every step
17:22 JCaesar I did that for my Semantics christmas homework, but I don't remember how…
17:22 JCaesar Anyway, does Isabelle have a type like Either?
17:41 larsrh JCaesar: yes, 'a + 'b
17:41 larsrh constructors being Inl and Inr
17:43 JCaesar ty
17:58 JCaesar joined #isabelle
18:08 JCaesar joined #isabelle
18:50 spacekitteh joined #isabelle
23:25 spacekitteh-work joined #isabelle