IRC log for #isabelle, 2016-03-10

All times shown according to UTC.

Time Nick Message
00:50 ammbauer joined #isabelle
02:47 ilbot3 joined #isabelle
02: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/
03:08 andromeda-galaxy I'm new to Isabelle and have been tryign to go through prog-prove.pdf, but I'm a little bit confused by Exercise 4.6: I assume that the proof should be by induction of some sort, but can't figure out how to use case on induction with the elems.induct rule.  Can anyone provide a few tips on that exercise?
04:10 JCaesar How did you define your elems function?
04:13 JCaesar (I'm not really sure what that exercise wants and all the pros aren't gonna wake up for at least another 3 hoursâ¦)
04:19 JCaesar andromeda-galaxy: Hint: Don't try prooving this in apply style.
04:22 JCaesar and about the case distinction: You just go proof(induction â¦) case (Cons a as) show ?case proof(cases â¦) case True â¦
04:22 JCaesar (I hope I didn't say too much.)
04:26 andromeda-galaxy JCaesar: I've not be doing it in apply style
04:26 andromeda-galaxy JCaesar: elems is defined the relatively straightforward recursive way with [] = {} and (x#xs) = {x} U elems xs
04:26 JCaesar kk. (so it's just the set functionâ¦)
04:26 andromeda-galaxy JCaesar: it's the Nil case that I'm having trouble with right now...
04:26 JCaesar uhâ¦ that should go by simp.
04:27 JCaesar what are you inducting over?
04:27 andromeda-galaxy JCaesar: that's the problem.  right now, "induction rule: elems induct"
04:27 andromeda-galaxy I mean, elems.induct
04:28 andromeda-galaxy the problem is that "case Nil" results in undefined case
04:29 JCaesar Oh.
04:29 JCaesar Well, in this case, elems.induct should just be the same as induction over a list.
04:30 andromeda-galaxy JCaesar:that's what I thought....
04:30 JCaesar and then case Nil will be defined.
04:31 andromeda-galaxy JCaesar: that's what I thought, but for some reason it doesn't seem to be..
04:31 JCaesar you have to take out the rule: for that to happen.
04:31 JCaesar If you really want to use rule induction, try a print_cases to see what your cases are named.
04:32 JCaesar (and yes, case (2 a as) will work)
04:32 andromeda-galaxy JCaesar: ahh... that helps.  they look unnamed right now.
04:32 andromeda-galaxy so "proof (induction) case Nil" still gives me "Undefined case: "Nil""
04:33 JCaesar Yeah, you need something to induct over.
04:33 JCaesar a variableâ¦
04:34 andromeda-galaxy JCaesar: oh, why didn't I think of that?  I tried induction voer the function and "cases xs" but not "induction xs"...
04:35 JCaesar :)
04:37 andromeda-galaxy JCaesar: thanks!
04:38 JCaesar np
04:39 andromeda-galaxy JCaesar: on general strategy, is the second case something that you would handle with "obtain"?
04:40 JCaesar I guess so. (You could also use guess in this case. ;))
04:41 JCaesar Oh, and btw, it's also possible to do without the case names for the induction. The proper way is to fix all the variables ("fix a as something") and then make all the assumptions (e.g. assume "xs = []" in the base case). The dirty way is to use goal1, goal2, â¦
04:42 andromeda-galaxy JCaesar: right, that makes sense, prog-prove mentioned that  "case ..."  was mostly sugar, it's just nice not to have to restate the ?case.  I've been trying to avoid the "improper" methods...
04:46 andromeda-galaxy JCaesar: sorry, one more question: would it be good to break the second one up into cases again for when a = x and when a /= x?
04:47 JCaesar I don't think there's a way around that.
04:47 JCaesar by second one, you mean the inductive case, I assume?
04:47 andromeda-galaxy JCaesar: I do
04:47 andromeda-galaxy JCaesar: I was just wondering because I don't remember prog-prove having mentioned anything about how to do that
04:48 JCaesar proof(cases "a = x") case True â¦ next case False qed essentially.
04:49 andromeda-galaxy ohhh... that makes sense now.
04:50 JCaesar or proof cases assume "a = x" â¦ next assume "a â  x" â¦ qed
04:50 JCaesar It's mentioned in 4.2
04:50 andromeda-galaxy right, that also makes sense.
04:53 andromeda-galaxy JCaesar: oh, I see, that's what the first one meant.
04:53 ThreeOfEight joined #isabelle
04:53 andromeda-galaxy JCaesar: how does ?case get bound with nested cases?
04:54 JCaesar eheheheâ¦
04:54 JCaesar I think for induction, it's ?case and for case it's ?thesis.
04:54 JCaesar But I honestly have no idea.
04:55 andromeda-galaxy JCaesar: oh right, now I remember.  Isabelle has a lot of cases to learn in one day...
04:56 JCaesar Yup. (Which is why I like goal1. It's always ?case there.)
04:56 andromeda-galaxy JCaesar: goal1?
04:58 andromeda-galaxy JCaesar: sorry for all the questions, thanks for all your help.  What exactly does "using True by force" mean?
04:59 JCaesar You sledgehammered. :)
04:59 JCaesar when saying case True, that defines the assumption you get from the case split and names it True.
05:00 andromeda-galaxy ah, of course, I forgot it makes those named assumptions.  I did try sledgehammer, I was curious (after I got it working by reordering the statements)
05:00 JCaesar I'm not sure what exactly using does, but essentially, it adds it to the list of assumptions. (There are two such lists, look at the difference of using True by force and using True apply - by force. And I don't really know the meaning of the two.)
05:02 andromeda-galaxy JCaesar: ah, that kind of makes sense.  what was that goal1 that you mentioned by the way?
05:02 JCaesar just try case goal1 instead of case True
05:03 andromeda-galaxy Hmm, okay.  I get: "Legacy feature!  Bad case "goal1" <unicode pentagon> -- use proof method "goal cases" instead"
05:04 andromeda-galaxy I'll look that up...
05:04 JCaesar :O
05:05 JCaesar Isabelle 2016?
05:05 andromeda-galaxy yes, I just installed it yesterday
05:05 JCaesar They finally deprecated it, noooooooo!
05:07 andromeda-galaxy sorry if this was already explained in prog-prove, I'm having a little trouble remembering/compartmentalizing everything, but: how do I reference the exists. variables from the IH in the obtain cases, for the second case (a /= x) of the inductive step?
05:16 JCaesar either with obtain or guess.
05:16 andromeda-galaxy JCaesar: right, but how do you refer to it in the "where" part of obtain?
05:17 JCaesar assume "âx. P x" then obtain x where "P x" by blast
05:17 JCaesar (it doesn't have to be the same name)
05:17 JCaesar alternatively: assume "âx. P x" then guess x ..
05:18 andromeda-galaxy JCaesar: sorry, I'm not understanding something... how do you formulate the "P"?
05:19 JCaesar P is that condition that describes the x that exists.
05:19 andromeda-galaxy JCaesar: of course!  but in this case, how do I formulate that?  just making it the same as the thesis condition doesn't help much
05:20 JCaesar waitâ¦ do you want to obtain something that you know exists by assumption, or do you want to show the existence of something?
05:20 andromeda-galaxy JCaesar: we know that the propositoin h olds for as/ys/zs, so now we need to find new ys/zs for (a#as) where a != x.  Then ys = a # <old ys> and zs = <old zs>
05:21 JCaesar Yes.
05:21 andromeda-galaxy I can't figure out how to formulate the references to <old ys> and <old zs>
05:22 JCaesar Well, you have Cons.IH that has a precondition. x â as, probably. You first need to show that.
05:22 andromeda-galaxy JCaesar: why do we need that just for obtaining the new ys/zs?
05:22 JCaesar because we don't know that they exist unless we show that precondition.
05:23 JCaesar that's what Cons.IH states. if x â elems as then they must exist, otherwise, you know nothing.
05:23 andromeda-galaxy do I ineed to show x : as or x : (a#as)?
05:23 andromeda-galaxy oh I see, I need that to apply the IH. right...
05:23 JCaesar x : (a#as) should be Cons.prems
05:24 JCaesar (You know about print_theorems, right?)
05:24 andromeda-galaxy whow, prog-prove really left a lot out
05:25 JCaesar If you know what to do, you can probably do without. And the one who wrote it definitely knows.
05:26 JCaesar Old problem of tutorialsâ¦
05:26 andromeda-galaxy indeed...
05:27 andromeda-galaxy JCaesar: thanks for all the help!
05:31 andromeda-galaxy JCaesar: sorry, I still am not clear on how to, once the IH premises are done, use the xs and ys from it...
05:32 andromeda-galaxy all the proofs that I remember only really use the IH sort of implicitly
05:32 JCaesar now you can write obtain ys zs where "â¦"
05:32 JCaesar and for the â¦ you write exactly what is said about ys and zs in the freeed IH.
05:34 andromeda-galaxy JCaesar: so I use that to get the old ys/zs and then another obtain to get the "new" ones?
05:34 JCaesar you only use it to get the old ones.
05:35 JCaesar for the onew ones, youâ¦ wait a second.
05:35 JCaesar it is forbidden to use obtained variables in thesis proofs. gotta try somethingâ¦
05:40 JCaesar okay, so the usual way would be to say show ?thesis (* here you get some âfoo. P foo *) proof (* Now you get "P ?foo" which means you can just show P for something arbitrary: *) show "P 42" â¦
05:40 JCaesar But I'm not sure that works hereâ¦
05:41 andromeda-galaxy JCaesar: hmm...
05:41 andromeda-galaxy JCaesar: why can't you use obtained variables in thesis proofs?
05:41 JCaesar You could show non-theorems.
05:41 JCaesar Professor Nipkow once explained to me how, I forgot. :(
05:42 andromeda-galaxy ah, okay.  I'll look into it more later...
05:44 andromeda-galaxy JCaesar: alright, so I have the "old" ys/zs...
05:45 JCaesar and I'm too stupid to go on from there on in a proper manner. (I can proove it with some apply(rule_tac x="a # ys" in exI) magic, but bahâ¦)
05:46 andromeda-galaxy JCaesar: this is even more different from both fp and informal proofs on paper than I expected
05:47 JCaesar Wellâ¦
05:47 JCaesar Technically, what you should do now is a witness proof as shown in 4.2
05:48 andromeda-galaxy right, but that requires finding witnesses...
05:48 JCaesar that is the same as on paper. :)
05:49 JCaesar The problem that I have is that I can't write those witnesses down so Isabelle/Isar will accept it.
05:49 andromeda-galaxy true, but I'm not sure how to do it in isabelle, since I can't just do "obtain ys where ys = a # yso"...
05:49 andromeda-galaxy (well, I can, but that makes "thus ?thesis' result in "failde to refine any pending goal")...
05:50 JCaesar hm? okay, that shouldn't happenâ¦
05:50 andromeda-galaxy wait no, never mind
05:50 andromeda-galaxy that was something else, that's why it was so confusing, sorry
05:50 JCaesar look at section 4.2 of prog-proove, that shows a witness-proof.
05:50 andromeda-galaxy to be exact: I can do it, but then I can't use that witness
05:52 JCaesar forget about what I said about using obtained variables in show, it doesn't apply in this case (since the ?free variables only appear after you obtain, so I think that's why its fineâ¦)
05:53 JCaesar Try the following: (in case False write) show ?thesis proof(intro exI) (* the exI is so you don't need two sub-proofs for the two things that exist *)
05:54 JCaesar and then write show "a # as = wittness_ys @ x # witness_zs & x â elems witness_ys"
05:54 JCaesar That should work. But it doesn't, for me at least. :(
05:54 JCaesar I'll go fetch some food since I'm out of ideas why.
05:54 andromeda-galaxy JCaeser: I'll be done for now as well, thanks so much for all the other help
05:54 JCaesar The simple solution for this whole task is to show that elems is equal to the predefined set and then the lemma is trivial.
05:55 JCaesar (set as in the function called set)
05:55 andromeda-galaxy JCaesar: ah, that makes sense...
05:55 andromeda-galaxy JCaesar: this seems more educational, though.  Thanks for all the help so far, I'll probably show up again thinking about this sometime tomorrow
08:43 kyagrd joined #isabelle
09:11 JCaesar btw, is there a nice combination of case and exists?
09:12 larsrh JCaesar: not sure what you mean there
09:12 JCaesar Ã  la if âx. P x then F (THE x. P x) else foo
09:13 larsrh I don't see what you're getting at
09:13 larsrh Could you propose a hypothetical syntax and what it'd translate to?
09:16 JCaesar CASETHE P OF x => F x | NOTHING => foo. (P F and foo just as above.)
09:17 ThreeOfEight you could define something like "The_option P = (if â!x. P x. then Some (THE x. P x) else None)
09:17 ThreeOfEight (note that for THE, you need â!, i.e. "there exists a unique"; if you only have â you can use SOME, but you don't get uniqueness)
09:18 JCaesar oh, rightâ¦
09:19 larsrh JCaesar: oh, I get it. No, I don't think it exists in HOL
09:19 larsrh something like Set.collect but for option
09:20 ThreeOfEight larsrh: option?
09:21 JCaesar If it's not defined yet I think I have better options that defining it myself.
09:28 larsrh ThreeOfEight: Set.collect :: ('a => bool) => 'a set
09:28 larsrh The_option :: ('a => bool) => 'a option
09:28 ThreeOfEight larsrh: why option?
09:28 ThreeOfEight ah
09:29 ThreeOfEight well that sounds like a bit of  a stretch
09:29 ThreeOfEight anyway
09:29 larsrh You used option :p
09:29 ThreeOfEight step back, I know syntax translations!
09:29 ThreeOfEight http://downthetypehole.de/paste/XwgDVAbv
09:29 larsrh [60,0,60,60,100] 60
09:29 larsrh That's numberwang
09:31 ThreeOfEight Yeah don't ask me where I got those numbers from
09:56 larsrh Copy-pasted from somewhere else, I presume
09:58 JCaesar classic syntax translationâ¦
09:59 JCaesar ThreeOfEight: btw, you set the background color in that paste service, but not the foreground color.
10:00 JCaesar (Which is a bit annoying if you have white as the default font color and grey as the default background.)
10:01 larsrh ... why would you do such a thin
10:01 larsrh *thing
10:02 JCaesar I chose a dark theme some point and ages later firefox decided to honor it. and now I'm too lazy to fix it.
10:03 ammbauer https://xkcd.com/1172/
10:13 ThreeOfEight larsrh: copy-pasted and then adapted
10:13 ThreeOfEight JCaesar: yeah I might change that, I suppsoe
10:15 JCaesar ammbauer++
15:58 ammbauer joined #isabelle
19:35 andromeda-galaxy hmmm... can anyone provide a hint on what the correct variable to induct on is for prog-prove?  Induction on n seems the most natural to me, but I've got induct/case proofs three deep now..
19:41 int-e andromeda-galaxy: which exercise are you doing?
19:45 andromeda-galaxy int-e: oops, I it ctrl+w at the wrong time.  4.7, the last one
19:45 andromeda-galaxy lemma "S (replicate n a @ w) ==> balanced n w"
21:38 andromeda-galaxy anyone?