IRC log for #isabelle, 2016-03-11

All times shown according to UTC.

Time Nick Message
00:11 int-e andromeda-galaxy: 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 andromeda-galaxy int-e: ah, okay, that makes sense, thanks for looking into it!
00:16 andromeda-galaxy 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 andromeda-galaxy I figure I should do at least one tedious proof while trying to learn from all the exercises...
00:30 andromeda-galaxy int-e: how did you tackle the aSb case?
01:07 int-e by thinking about when  balanced n (x @ [b])  holds
01:08 andromeda-galaxy int-e: where did you get "x"
01:08 andromeda-galaxy ?
01:09 int-e nowhere in partiuclar, it's just a string.
01:10 andromeda-galaxy int-e: ah. so balanced n1 x ==> balanced (Suc n) (x @ [b]), right?
01:11 int-e except for the typo
01:11 andromeda-galaxy right, sorry "balanced n x"
01:13 andromeda-galaxy int-e: so after "case (aSb w1)" the idea so to prove "w1 = replicate n a w ==> balanced n (a # w @ [b])", right?
01:13 andromeda-galaxy I'm trying to make sure that I'm correctly interpreting all of the different variables after that statement
01:14 andromeda-galaxy (replicate n a @ w, not replicate n a w)
01:17 int-e I need to sleep but I used the  append_eq_append_conv2  lemma quite a bit.
01:17 andromeda-galaxy int-e: okay, I'll try that.  thanks for all the help!
04:05 andromeda-galaxy 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 andromeda-galaxy int-e: that wasn't too bad, actually... I used a couple of extra balance_* lemmas, and it only came out to 4-5 lines in each case
04:23 andromeda-galaxy now for the other direction...
05:29 andromeda-galaxy 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 andromeda-galaxy: 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 andromeda-galaxy ThreeOfEight: ah, okay, that makes sense.  any thoughts on the other proof problems?
07:21 ThreeOfEight the one with the balanced thing?
07:25 andromeda-galaxy 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 andromeda-galaxy: 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 int-e andromeda-galaxy: 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 int-e: you don't need the universal quantifiers in the definition of the inductive
11:10 int-e right, thanks. (I haven't done any cleanups at all, but I probably would have missed that)
11:11 int-e Well, that's a lie. I've done the usual exploration-then-clean-up-the-messy-apply-script pass for the proof.
11:23 dmiles joined #isabelle
11:38 int-e 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 int-e 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 andromeda-galaxy int-e: 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 prog-prove didn't mention, I'll look into them...
16:43 int-e I really hate resorting to tricks like  using S.intros(2)[of "_ @ _ @ _"]  just to work around problems with associativity
16:51 andromeda-galaxy int-e: ah, so that's what that does...
16:52 andromeda-galaxy 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 andromeda-galaxy 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 andromeda-galaxy int-e: 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 int-e hmm, what's your definition of S?
17:09 int-e 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 andromeda-galaxy int-e: I have Isabelle2016 too.  S is:
17:11 andromeda-galaxy (oh wait, I just realized the problem: your S has the last two equations swapped from mine)
17:11 int-e okay.
17:12 int-e yeah I don't know why I chose that order... the order in the exercise is different from mine.
17:12 andromeda-galaxy int-e: 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 int-e 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 int-e But there's quite a bit of pattern matching going on, i.e. experience resulting from practice.
17:15 andromeda-galaxy int-e: ah, that makes sense
17:16 andromeda-galaxy int-e: 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 andromeda-galaxy (at least while new to Isabelle, I find the more explicit style a lot easier to read...)
17:17 int-e 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 int-e 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 andromeda-galaxy That makes sense, thank you for all the explanations.  I guess the tradeoff between compactness and understanding-why-they-work really depends a lot on what you want to do with the proof..
17:21 andromeda-galaxy I'll keep practicing in both styles for now
17:24 int-e basically I try to keep proofs clean near the root, and allow them to become messier (and more fragile) towards the leaves...
17:26 andromeda-galaxy 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