# IRC log for #isabelle, 2017-04-08

All times shown according to UTC.

Time Nick Message
01:48 ilbot3 joined #isabelle
01:48 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/
02:02 ertes joined #isabelle
05:35 cmr joined #isabelle
05:35 cmr joined #isabelle
05:53 cmr joined #isabelle
05:53 cmr joined #isabelle
06:00 cmr joined #isabelle
06:00 cmr joined #isabelle
06:11 cmr joined #isabelle
06:11 cmr joined #isabelle
09:56 larsrh I should stop being so unreasonably irked by failing builds
10:07 silver joined #isabelle
10:17 pruvisto larsrh: you should
10:17 pruvisto I would have fixed Random_BSTs soon-ish
10:18 pruvisto but I'm working on my long term project "Do more work during working hours, do less work during free time"
10:24 larsrh Let's say I have a relation {(a1, a2). ∃junk1 x xs. a1 = (junk1, xs) ∧ a2 = (junk1, x # xs)}
10:25 larsrh is it true that there is an injective f s.t. R = map_prod f f ` {(a1, a2). ∃x xs. a1 = xs ∧ a2 = x # xs}
10:25 larsrh I feel like this is true but I can't seem to get a hold of _the_ "junk1"
10:26 larsrh wait, no. This is wrong.
10:27 larsrh R contains all possible junks, so there's no single one
10:27 larsrh R is more of a union of {(a1, a2). ∃x xs. a1 = xs ∧ a2 = x # xs} joined with all possible junks
10:27 larsrh To phrase it differently. I know that R' = {(a1, a2). ∃x xs. a1 = xs ∧ a2 = x # xs}  is wf. I want to prove that R is wf as well
10:31 int-e R is the lexicographic product of = and R'.
10:32 int-e (err, the empty relation, not =)
10:34 larsrh int-e: how can I express that in Isabelle?
10:34 int-e lemma "{(a1, a2). ∃junk1 x xs. a1 = (junk1, xs) ∧ a2 = (junk1, x # xs)} = {} <*lex*> {(xs, x # xs)|x xs. True}" by auto
10:35 int-e (is there a better way to write "{(xs, x # xs)|x xs. True}"? The "True" is a bit awkward)
10:37 larsrh splendid
10:37 larsrh this looks highly relevant
10:39 larsrh now the only problem I have left is that R is tupled in slightly the wrong way
10:39 larsrh it's more like (junk1, (junk2, x)) instead of ((junk1, junk2), x)
10:40 int-e so use the same trick twice?
10:40 larsrh but this can be solved by giving an injective f that maps it the right way
10:40 larsrh or that
10:43 larsrh wooo, that actually works
10:58 larsrh int-e: you have just secured yourself a spot in the acknowledgements of my thesis
11:20 int-e . o O ( uh-oh )
11:25 JCaesar Because you helped with lars' junk.
11:29 pruvisto int-e: int-e I can't think of a better way to write that really
11:29 pruvisto this sort of thing can sometimes be expressed nicely with the dependent sum operator (SIGMA)
11:29 pruvisto but you can't get rid of the "True" that way, I think
11:35 int-e it's a small price to pay to get rid of the existential quantifiers anyway
11:37 larsrh the existential quantifiers come from the function package
11:37 larsrh little I can do about them
11:39 larsrh *walk into the function package like* ᕕ( ᐛ )ᕗ
11:39 larsrh (* FIXME: broken by design *)
11:39 larsrh (ಠ_ಠ)
13:02 tautologico joined #isabelle
14:32 larsrh ok so the good news is that I have narrowed down the spot in the function package where f_rel is defined
14:32 larsrh the bad news is that if I change that all hell breaks loose
17:30 chindy I have a proof with a general outline of this http://downthetypehole.de/paste/YHkbP5an I know that f1 is true and i can obtain y. but using those why cant i derive false ?
17:33 larsrh chindy: you need "False" in upper case
18:11 chindy :P i have that... i figured modus ponens or sth like that would suffice
18:13 ertesx joined #isabelle