# IRC log for #isabelle, 2015-11-21

All times shown according to UTC.

Time Nick Message
01:42 barrucadu I've got this proof I've been working on down to one missing component, which feels like I'm doing the induction wrong: https://gist.github.com/barrucadu/b5fc0b3f440b354cca34 (see the "sorry")
01:43 barrucadu There's also a sledgehammer-generated proof I don't really understand the complexity of
01:43 barrucadu Hopefully this'll be the last question for a while…
01:52 int-e barrucadu: without trying to understand that in full detail: should the  proof (induct trace)  be a  proof (induct trace arbitrary: por)? Right now the induction hypothesis fixes `por` to the original one.
01:54 barrucadu int-e: Possibly, let me try
01:57 int-e you'll then have to use Cons(2) instead of assms(1)
02:01 barrucadu Everything but the 'have "por_well_formed newPor"' works, still not sure how to approach that :(
02:04 int-e a first step would be  unfolding `newPor = grow_por p xs` apply (intro Cons(1)) ... but then you'll have to show that  trace_por_agree xs p  and I'm not sure that actually holds.
02:18 ThreeOfE1ght joined #isabelle
03:10 barrucadu Hmm, I'll stare at this some more in the morning. Thaqnks for the suggestion.
08:24 ski joined #isabelle
09:34 ThreeOfE1ght barrucadu: I haven't looked at your proof in detail, but the first thing I noticed: why don't you do "proof (induction por trace rule: grow_por.induct)"?
09:35 ThreeOfE1ght When doing induction over a function definition, it is usually a good idea to use the induction rule of the function package
09:35 ThreeOfE1ght because that follows the definition of the function precisely
09:40 int-e Ah I should've seen that... that's what I get for not really thinking about what's supposed to be proved.
09:52 ThreeOfE1ght well your approach would probably also have worked, but only with the "arbitrary:" that int-e suggested
10:07 ThreeOfEight it would be easier to prove things with it if you could formulate it with just 2 cases
12:58 barrucadu It's kind of doing two things at once, and I'm not sure it needs to do both those things… so I can throw away the singleton case and make the nil case be True
13:41 ThreeOfEight I tried to complete your proof but got very stuck at one point and couldn't really proceed because I had no idea what "trace_por_agree" actually does
13:41 ThreeOfEight keeping things separate and modular whenever possible is one of the things that tend to make one's life a lot easier in theorem proving
13:42 ThreeOfEight oh, and, by the way "obtain x where "x = …"" is kind of an antipattern
13:42 ThreeOfEight just write "def x ≡ "...""
13:42 ThreeOfEight then you get a theorem called x_def to unfold the definition
13:43 ThreeOfEight and if you only want an input abbreviation without defining a new constant, you can also use "let ?x = "...""
17:48 mbrcknl joined #isabelle