Time 
Nick 
Message 
00:11 
inte 
andromedagalaxy: proof (induct "replicate n a @ w" arbitrary: n w rule: S.induct) [...] works for me... but it's quite tedious to push through to the end. 
00:15 
andromedagalaxy 
inte: ah, okay, that makes sense, thanks for looking into it! 
00:16 
andromedagalaxy 
I have the first case working with "induction n arbitrary: w" (which then uses induction on S.induct internally) but can't get that to work very well for the second case. I'll try it with "replicate n a @ w" arbitrary: n w rule: S.induct, thanks for the suggestion 
00:17 
andromedagalaxy 
I figure I should do at least one tedious proof while trying to learn from all the exercises... 
00:30 
andromedagalaxy 
inte: how did you tackle the aSb case? 
01:07 
inte 
by thinking about when balanced n (x @ [b]) holds 
01:08 
andromedagalaxy 
inte: where did you get "x" 
01:08 
andromedagalaxy 
? 
01:09 
inte 
nowhere in partiuclar, it's just a string. 
01:10 
andromedagalaxy 
inte: ah. so balanced n1 x ==> balanced (Suc n) (x @ [b]), right? 
01:11 
inte 
except for the typo 
01:11 
andromedagalaxy 
right, sorry "balanced n x" 
01:13 
andromedagalaxy 
inte: so after "case (aSb w1)" the idea so to prove "w1 = replicate n a w ==> balanced n (a # w @ [b])", right? 
01:13 
andromedagalaxy 
I'm trying to make sure that I'm correctly interpreting all of the different variables after that statement 
01:14 
andromedagalaxy 
(replicate n a @ w, not replicate n a w) 
01:17 
inte 
I need to sleep but I used the append_eq_append_conv2 lemma quite a bit. 
01:17 
andromedagalaxy 
inte: okay, I'll try that. thanks for all the help! 
04:05 
andromedagalaxy 
by the way, is there a way to specify a fact that should be used by all further "have.."? after "case (SS w1 w2)", it's a little bit annoying to have to write "using SS" all the time... 
04:09 
andromedagalaxy 
inte: that wasn't too bad, actually... I used a couple of extra balance_* lemmas, and it only came out to 45 lines in each case 
04:23 
andromedagalaxy 
now for the other direction... 
05:29 
andromedagalaxy 
Also, does anyone have any thoughts on how to prove "S (x @ y) ==> S (x @ a # b # y)" (from above) or how to get away without it in the (Suc m) case of the 3rd case of "balanced n w ==> S (replicate n a @ w)" relatively neatly? 
06:43 
ThreeOfEight 
andromedagalaxy: you can do "note [simp] = …" 
06:43 
ThreeOfEight 
that adds the facts "…" to the simp set, so the simplifier will use them 
06:43 
ThreeOfEight 
the same works for intro, dest, etc. 
06:43 
ThreeOfEight 
but you can't chain it in automatically (which is what from/using do) 
07:05 
andromedagalaxy 
ThreeOfEight: ah, okay, that makes sense. any thoughts on the other proof problems? 
07:21 
ThreeOfEight 
the one with the balanced thing? 
07:25 
andromedagalaxy 
ThreeOfEight: yes, I have the S (replicate n a @ xs) => balanced n xs direction done, but the other direction is proving more annoying, specifically that supporting lemma that I mentioned most recently 
07:43 
ThreeOfEight 
andromedagalaxy: no idea; this is a pretty difficult exercise 
07:43 
ThreeOfEight 
it would take me to much time right now 
07:45 
ThreeOfEight 
in Exercise 3.5 you proved the equivalence of S and T – perhaps you can use that somewhere? 
10:15 
inte 
andromedagalaxy: http://sprunge.us/hWic is a generalized version of "S (x @ y) ==> S (x @ a # b # y)" with proof... could be worse. (And I think that lemma is needed.)... however I have not thought about using T at all. 
10:33 
ThreeOfEight 
inte: you don't need the universal quantifiers in the definition of the inductive 
11:10 
inte 
right, thanks. (I haven't done any cleanups at all, but I probably would have missed that) 
11:11 
inte 
Well, that's a lie. I've done the usual explorationthencleanupthemessyapplyscript pass for the proof. 
11:23 

dmiles joined #isabelle 
11:38 
inte 
regarding using T, I suspect one would like to work with T' which is defined in the dual fashion: T' > [] and T' > a T' b T', so that one can match the 'a' with an 'a' coming from replicate more easily... but I suspect even that wouldn't make the proof noticably simpler. 
11:41 
inte 
ironically, if one is only interested in proving that S x ==> balanced 0 x, there's a much nicer generalization that can be proved far more easily: "S x ==> balanced n (x @ y) = balanced n y" 
16:29 
andromedagalaxy 
inte: wow, that's a lot more succinct than my attempt, probably at least partly due to the generalization. Thanks for looking into it! that Isar proof uses some features that progprove didn't mention, I'll look into them... 
16:43 
inte 
I really hate resorting to tricks like using S.intros(2)[of "_ @ _ @ _"] just to work around problems with associativity 
16:51 
andromedagalaxy 
inte: ah, so that's what that does... 
16:52 
andromedagalaxy 
I'm practicing writing out the same proof in a somewhat more verbose style (e.g. "thus ?case proof (cases x1)") so that I can make sure I understand what everything there means 
16:53 
andromedagalaxy 
What would be good reading for understanding "best practices" about how condensed to make proofs (e.g. how many steps to explicitly show in Isar)? 
17:03 
andromedagalaxy 
inte: by the way, on your proof, in the (aSb z x1 x2) case, this line gives me a unification error: S.intros(2)[OF S.intros(3), of "z @ x" "[]", OF S.intros(2)] 
17:07 
inte 
hmm, what's your definition of S? 
17:09 
inte 
hmm and I'm using Isabelle2016, though I don't see how this would make a difference (and if you had a different version, "consider" would cause you trouble already) 
17:10 
andromedagalaxy 
inte: I have Isabelle2016 too. S is: 
17:11 
andromedagalaxy 
(oh wait, I just realized the problem: your S has the last two equations swapped from mine) 
17:11 
inte 
okay. 
17:12 
inte 
yeah I don't know why I chose that order... the order in the exercise is different from mine. 
17:12 
andromedagalaxy 
inte: how do you get to proofs that compact? e.g. I'm trying to learn by working out another version of it (using the induction rule and generalization from yours), and the "simple" way of doing that seems to end up with something like this (so far): 
17:14 
inte 
tricky. I tend to stare at the output of "auto" and try figure out what next step would move the proof forward... and add that as a rule to auto or as a fact with "using". 
17:14 
inte 
But there's quite a bit of pattern matching going on, i.e. experience resulting from practice. 
17:15 
andromedagalaxy 
inte: ah, that makes sense 
17:16 
andromedagalaxy 
inte: are compact proofs like that considered "better" than ones that spell out the intermediate results (kind of like http://lpaste.net/4428694916691918848, my progress on it)? 
17:17 
andromedagalaxy 
(at least while new to Isabelle, I find the more explicit style a lot easier to read...) 
17:17 
inte 
No, I wouldn't say they're better... the disadvantage is that with such compact proofs it's often not really obvious why they work. 
17:19 
ThreeOfEight 
one should avoid unnecessary intermediate steps 
17:19 
ThreeOfEight 
but one should attempt to keep the proofs understandable 
17:19 
ThreeOfEight 
but in my experience, that is very difficult to achieve 
17:20 
inte 
I think your proofs will just become more compact over time, as you become more familiar with Isabelle/HOL, existing lemmas and a couple of tricks of the trade. 
17:20 
ThreeOfEight 
one should definitely avoid doing so much automation/apply script reasoning in a single step that the proof becomes fragile 
17:20 
ThreeOfEight 
it's not a huge issue if you're just doing it for yourself 
17:20 
ThreeOfEight 
but once your stuff goes into the AFP or the Isabelle distribution, fragile proofs are very annoying 
17:21 
ThreeOfEight 
also, metis/smt proofs are notoriously fragile 
17:21 
andromedagalaxy 
That makes sense, thank you for all the explanations. I guess the tradeoff between compactness and understandingwhytheywork really depends a lot on what you want to do with the proof.. 
17:21 
andromedagalaxy 
I'll keep practicing in both styles for now 
17:24 
inte 
basically I try to keep proofs clean near the root, and allow them to become messier (and more fragile) towards the leaves... 
17:26 
andromedagalaxy 
I see, that does seem like a good idea 
17:34 
ThreeOfEight 
I think I've just stopped caring at this point :P 
17:35 
ThreeOfEight 
On the other hand, whenever I think my proofs are ugly, I look at chuchucorny's proofs and everything is fine again. 
17:35 
ThreeOfEight 
(No offence chuchucorny, but, you know… bloody hell… :P) 
18:57 

dmiles joined #isabelle 
19:45 

dmiles joined #isabelle 
23:42 

mbrcknl joined #isabelle 