# IRC log for #darcs-theory, 2009-04-30

All times shown according to UTC.

Time Nick Message
09:32 arjanb joined #darcs-theory
09:58 tux_rocker joined #darcs-theory
10:42 kowey joined #darcs-theory
14:58 gal_bolle joined #darcs-theory
15:00 Igloo gal_bolle: I've added the remaining lemmas to patch_universes, and proved the final "contradiction" lemma using them now
15:00 Igloo Most of the lemmas are still just admit'ted, though
15:00 gal_bolle ok
15:01 gal_bolle i'm in the converse situation…
15:01 Igloo But I think they're all fairly easily provable...
15:01 gal_bolle i've got most of the lemmawork done
15:01 gal_bolle but i'm not sure if my lemmas
15:01 gal_bolle would be useful for your proof
15:02 Igloo I don't think so. Most of my lemmas are to do with the "commutes left out of" relation
15:03 tux_rocker joined #darcs-theory
15:03 Igloo Or they're silly things, like if ([] :+> r :> s :> []) can be transitively commuted to (us :+> r' :> s' :> vs) then us = vs = []
15:06 Igloo (which requires far more proving than I feel it ought!)
15:10 gal_bolle i now have a haskell program to turn my goals into dot graphs
15:10 gal_bolle this is going too far
15:11 Igloo Do you mean it shows the patch graph of them?
15:11 Igloo Can I see an example?
15:11 gal_bolle one second
15:11 gal_bolle it's really dirty, though
15:12 Igloo Dirty? I imported Classical_Prop yesterday. I can't get any dirtier.
15:12 gal_bolle ok
15:13 gal_bolle look in your mailbox
15:14 Igloo So the circles are types and the lines are values?
15:14 Igloo What are the colours?
15:15 gal_bolle yes, the circles are states
15:15 gal_bolle the lines are patches
15:15 gal_bolle and i'm following q in red and p in green in that graph
15:16 gal_bolle if you squeeze your eyes, you can see an hypercube in the middle
15:16 Igloo Heh
15:17 Igloo That's cool. I sometimes draw those pictures by hand in the gimp
15:17 gal_bolle i got tired when they got too complex
15:17 Igloo Although with fewer lines and circles  :-)
15:17 Igloo Right, I wouldn't want to do it for that case  :-)
15:18 gal_bolle do you know if there's a dot viewer which allows to move the nodes?
15:18 Igloo dotty
15:18 gal_bolle thanks a lot
15:18 Igloo Although I've never got on with it particularly well
15:20 gal_bolle no it seems a bit primitive
15:21 gal_bolle and it has refreshment bugs
15:49 * gal_bolle just discovered it was possible to tell dot to make graphs go from right to left
15:49 gal_bolle dual cases get so much easier
15:49 gal_bolle (i know they should really be in lemmas, but well…)