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

All times shown according to UTC.

Time Nick Message
08:39 gal_bolle joined #darcs-theory
09:51 kowey joined #darcs-theory
10:50 gal_bolle joined #darcs-theory
11:35 jnaimard joined #darcs-theory
12:38 tux_rocker joined #darcs-theory
14:28 Igloo jnaimard: OK, I see what you're saying re the axiom rewrites, I think
14:28 Igloo jnaimard: It looks to me that we should avoid using exists in axioms/lemmas, except in the conclusions
14:29 Igloo jnaimard: Using them in the assumptions just makes it harder to use the axiom/lemma
14:41 jnaimard yes
14:43 gal_bolle and i think that my geometric intuition at the end could be formalized into something useful
15:05 Igloo Ah, it does mean we lose the <-> for UnnamedPatchCommuteConsistent though
15:06 Igloo But I don't think that that is important
15:11 gal_bolle i think you get it back by using inverses everywhere
15:12 gal_bolle Lemma commute_consistent_mirror:
15:12 gal_bolle forall a b c d e f g
15:12 gal_bolle (p : Patch b a) (q : Patch b c) (r: Patch c d)
15:12 gal_bolle (q'': Patch a e) (r'': Patch e f) (p': Patch d f)
15:12 gal_bolle (p'': Patch c e) (r': Patch b g) (q': Patch g d),
15:12 gal_bolle <<q,r>> <~> <<r',q'>> ->
15:12 gal_bolle <<q,p''>> <~> <<p,q''>> ->
15:12 Igloo No, it's just pointless in that lemma
15:12 gal_bolle <<p'',r''>> <~> <<r,p'>> ->
15:12 gal_bolle exists f, exists r3: (Patch a f), exists p3, exists q3,
15:12 Igloo You just need to flip the <<q, r>> <~>u <<r', q'>>
15:12 gal_bolle <<r',p3>> <~> <<p,r3>> /\ <<p3,q3>> <~> <<q',p'>> /\
15:12 gal_bolle <<r3,q3>> <~> <<q'',r''>>
15:12 gal_bolle .
15:12 gal_bolle ah ok
15:12 Igloo The interesting opposite case is when p starts /after/ qr, not before it
15:13 * gal_bolle has thought too much about this in terms of flipping cubes
15:14 Igloo :-)
15:15 gal_bolle the axiom is for when the vertices adjacent to the three faces has two incoming edges and one outgoing
15:15 gal_bolle and the lemma is useful in the opposite case
15:16 gal_bolle but if p is before q and r, and you invert everyone, p^ ends up after q^ and r^
15:19 Igloo Right, although we don't have all the lemmas we'd need for that yet
15:20 Igloo Well, maybe we do for these lemmas
15:34 gal_bolle we have it more or less
15:35 gal_bolle after much pondering i did implement inversion of sequences
16:28 arjanb joined #darcs-theory
17:02 gal_bolle left #darcs-theory