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

All times shown according to UTC.

Time Nick Message
08:52 arjanb joined #darcs-theory
11:25 Igloo_ joined #darcs-theory
14:04 gal_bolle joined #darcs-theory
14:05 gal_bolle hi igloo, if you're still intrested in getting the axioms as small as possible, commute-square should be an implication, not an equivalence
14:05 gal_bolle since you can get one side from the other by using commute-self-invert
14:07 Igloo OK, ta
14:08 Igloo I think I'm close to the proof that 2 patches commute consistently anywhere in a sequence, BTW
14:08 Igloo The hard bit is done, it's just all the lemmas etc I need to finish
14:09 kowey joined #darcs-theory
14:25 gal_bolle looks great
14:26 gal_bolle be aware that semtimes «all the lemmas can be quite long»
14:26 * gal_bolle has been doing «all the lemmas» for a while
14:26 Igloo Yes, that's the problem  :-)
14:27 Igloo Oh, I haven't actually done the end bit either, but hopefully that won't be too bad
14:27 Igloo I'm up to:
14:27 Igloo TransitiveCommuteRelates p p'
14:27 Igloo -> (exists r  : namedPatchSequence mid to, <<q, r>>  <~ <<p>>)
14:27 Igloo -> (exists r' : namedPatchSequence mid to, <<q, r'>> <~ <<p'>>).
14:27 gal_bolle what kind of lemmas do you need?
14:28 Igloo I think it's all in the repo
14:28 gal_bolle ok i'll have a look
14:28 gal_bolle what is that <~ ?
14:29 Igloo I was trying to prove NamedPatchCommutePreservesCommute in the other direction, based on the other lemmas rather than from first principles, but I think I ended up going round in a circle or something. I'll try again later
14:29 Igloo the other direction meaning starting with qrp rather than pqr
14:29 Igloo <~ is "commutes out of"
14:29 Igloo Given a sequence p, we can directly commute q out to the left, leaving r
14:32 Igloo The final proof might actually only want
14:32 Igloo <<p>> <~~> <<p'>>
14:32 Igloo -> (exists r  : namedPatchSequence mid to, <<q, r>>  <~ <<p>>)
14:32 Igloo -> (exists r' : namedPatchSequence mid to, <<q, r'>> <~ <<p'>>).
14:32 Igloo Where <~~> is non-transitive
14:33 Igloo The idea is to show things by contradiction. Suppose f p holds. Then f r holds, where we commute q out of p at every step. But f [] doesn't hold. Contradiction.
14:34 gal_bolle i'm not sure it's the simplest way to go in coq
14:34 gal_bolle but i might be wrong
14:35 Igloo So might I  :-)
14:35 gal_bolle in particular i'm not sure how easy it is to show the f p -> f r bit
14:36 Igloo I haven't done that bit yet; maybe I should ignore the lower lemmas for now and do that first.
14:39 kowey_ joined #darcs-theory
14:39 gal_bolle what i like in the proof that i'm doing (i sent you the argument on monday) is that i don't need any proof by absurd
14:40 gal_bolle by the way, do you use the fact that the sequence of commute is minimal?
14:40 gal_bolle i seem to remember you did in the paper
14:43 Igloo I'm not sure what you mean
14:45 Igloo Oh, you mean that the fewest commutes are used to get from the start to end states? I don't use that in the paper or the coq
14:45 gal_bolle does your proof start by "let p <~~> p' be a minimal sequence of transitions between p and p'"?
14:45 gal_bolle ok, i misremembered
14:48 Igloo It's possible an earlier proof attempt did, I tried lots of things
14:49 gal_bolle ah ok
14:54 gal_bolle haha, i have a "patch sequence" instance of my patch module types, yay
14:55 gal_bolle now ba
14:55 Igloo :-)
14:55 gal_bolle now back to the crazy proof
14:55 Igloo Is the module type stuff in the dic repo?
14:57 gal_bolle it's coming
14:57 gal_bolle it's halfway there
14:57 Igloo OK  :-)
15:47 Igloo gal_bolle: BTW, if you're looking at my stuff in coq, I think you need the trunk coq
15:48 gal_bolle same of mine ;-)
15:48 Igloo heh
20:23 tux_rocker joined #darcs-theory