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 
andromedagalaxy 
I'm new to Isabelle and have been tryign to go through progprove.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 
andromedagalaxy: 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 
andromedagalaxy 
JCaesar: I've not be doing it in apply style 
04:26 
andromedagalaxy 
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 
andromedagalaxy 
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 
andromedagalaxy 
JCaesar: that's the problem. right now, "induction rule: elems induct" 
04:27 
andromedagalaxy 
I mean, elems.induct 
04:28 
andromedagalaxy 
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 
andromedagalaxy 
JCaesar:that's what I thought.... 
04:30 
JCaesar 
and then case Nil will be defined. 
04:31 
andromedagalaxy 
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 
andromedagalaxy 
JCaesar: ahh... that helps. they look unnamed right now. 
04:32 
andromedagalaxy 
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 
andromedagalaxy 
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 
andromedagalaxy 
JCaesar: thanks! 
04:38 
JCaesar 
np 
04:39 
andromedagalaxy 
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 
andromedagalaxy 
JCaesar: right, that makes sense, progprove 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 
andromedagalaxy 
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 
andromedagalaxy 
JCaesar: I do 
04:47 
andromedagalaxy 
JCaesar: I was just wondering because I don't remember progprove having mentioned anything about how to do that 
04:48 
JCaesar 
proof(cases "a = x") case True … next case False qed essentially. 
04:49 
andromedagalaxy 
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 
andromedagalaxy 
right, that also makes sense. 
04:53 
andromedagalaxy 
JCaesar: oh, I see, that's what the first one meant. 
04:53 

ThreeOfEight joined #isabelle 
04:53 
andromedagalaxy 
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 
andromedagalaxy 
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 
andromedagalaxy 
JCaesar: goal1? 
04:58 
andromedagalaxy 
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 
andromedagalaxy 
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 
andromedagalaxy 
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 
andromedagalaxy 
Hmm, okay. I get: "Legacy feature! Bad case "goal1" <unicode pentagon>  use proof method "goal cases" instead" 
05:04 
andromedagalaxy 
I'll look that up... 
05:04 
JCaesar 
:O 
05:05 
JCaesar 
Isabelle 2016? 
05:05 
andromedagalaxy 
yes, I just installed it yesterday 
05:05 
JCaesar 
They finally deprecated it, noooooooo! 
05:07 
andromedagalaxy 
sorry if this was already explained in progprove, 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 
andromedagalaxy 
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 
andromedagalaxy 
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 
andromedagalaxy 
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 
andromedagalaxy 
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 
andromedagalaxy 
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 
andromedagalaxy 
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 
andromedagalaxy 
do I ineed to show x : as or x : (a#as)? 
05:23 
andromedagalaxy 
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 
andromedagalaxy 
whow, progprove 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 
andromedagalaxy 
indeed... 
05:27 
andromedagalaxy 
JCaesar: thanks for all the help! 
05:31 
andromedagalaxy 
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 
andromedagalaxy 
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 
andromedagalaxy 
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 
andromedagalaxy 
JCaesar: hmm... 
05:41 
andromedagalaxy 
JCaesar: why can't you use obtained variables in thesis proofs? 
05:41 
JCaesar 
You could show nontheorems. 
05:41 
JCaesar 
Professor Nipkow once explained to me how, I forgot. :( 
05:42 
andromedagalaxy 
ah, okay. I'll look into it more later... 
05:44 
andromedagalaxy 
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 
andromedagalaxy 
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 
andromedagalaxy 
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 
andromedagalaxy 
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 
andromedagalaxy 
(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 
andromedagalaxy 
wait no, never mind 
05:50 
andromedagalaxy 
that was something else, that's why it was so confusing, sorry 
05:50 
JCaesar 
look at section 4.2 of progproove, that shows a witnessproof. 
05:50 
andromedagalaxy 
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 subproofs 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 
andromedagalaxy 
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 
andromedagalaxy 
JCaesar: ah, that makes sense... 
05:55 
andromedagalaxy 
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 
Copypasted 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: copypasted 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 
andromedagalaxy 
hmmm... can anyone provide a hint on what the correct variable to induct on is for progprove? Induction on n seems the most natural to me, but I've got induct/case proofs three deep now.. 
19:41 
inte 
andromedagalaxy: which exercise are you doing? 
19:45 
andromedagalaxy 
inte: oops, I it ctrl+w at the wrong time. 4.7, the last one 
19:45 
andromedagalaxy 
lemma "S (replicate n a @ w) ==> balanced n w" 
21:38 
andromedagalaxy 
anyone? 