# IRC log for #darcs-theory, 2009-05-05

All times shown according to UTC.

Time Nick Message
09:30 gal_bolle joined #darcs-theory
10:13 Igloo gal_bolle: Woo! (see camp list mail)
10:18 gal_bolle congratulations
10:18 gal_bolle my constructive proof is not yet ready, but it's coming
10:18 gal_bolle i may have one painful lemma to do though
10:19 gal_bolle your proof is going to be smaller, but i won't have to import Classical logic
10:20 Igloo I'm pretty sure I can get rid of classical logic, by making commutability of unnamed patches decidable and then proving decidability of named patches
10:21 gal_bolle it's possible
10:21 Igloo Will my proof still be smaller when I've provied the other direction too?
10:22 gal_bolle i don't know
10:22 * Igloo isn't actually sure how much stuff ends up getting duplicated
10:22 gal_bolle the thing is that i'll have two lemmas with ridiculously big proofs
10:22 gal_bolle but they are of general use
10:22 Igloo Oh, I ended up using your combined axioms, BTW
10:22 gal_bolle aren't they nice?
10:23 Igloo Yup; I think they were even essential in one case, but I could be wrong
10:23 gal_bolle the geometric interpretation is really helpful to me
10:23 gal_bolle i have one such case too
10:23 Igloo I think I needed the knowledge that the two results gave you /the same/ patches, not just separately existing patches
10:24 gal_bolle yup
10:24 Igloo It's possible that was provable anyway, but combining the lemmas was easiest
10:24 gal_bolle exactly
10:24 Igloo Hopefully they won't be too hard to prove for primitive patches
10:25 gal_bolle so my fat lemma is if start p tail commutes to start' p' tail' (with name(p) = name(p') ), then in fact one can start by sorting start into start_to_start +> start_to_tail
10:25 gal_bolle then tail into tail_to_start +> tail_to_tail
10:25 gal_bolle then commute these guys where they belong
10:25 Igloo Actually, I don't see why they should be. For the prim patch proofs we'll know what the answer is, so we can just (exists _) it and then split
10:25 gal_bolle yes
10:26 gal_bolle this is the "shortest sequence of commutes" argument
10:26 Igloo start_to_start is the intersectino of start and start'?
10:26 gal_bolle yes
10:27 gal_bolle modulo shuffling
10:27 Igloo Have you proven that yet?
10:27 gal_bolle yes
10:27 gal_bolle now i need to prove the same thing
10:27 gal_bolle but with sequences where i track two patches
10:28 Igloo Interesting. It sounds harder than "minimal context exists", which I was going to use this lemma to prove
10:28 gal_bolle i think you can extract an algorithm to make an optimal sequence of commutes from one sequence to another using that
10:28 gal_bolle something like quick-sort
10:28 Igloo Oh, with just 1 patch it's roughly the same as "minimal context exists"
10:28 gal_bolle is it?
10:29 gal_bolle maybe i just got carried away
10:29 gal_bolle my starting intuition was that we should prove minimal context exists from names
10:29 Igloo Well, I don't know if you can make the leap in coq
10:29 gal_bolle then everytthing from minimal context exists
10:30 gal_bolle i had even made minimal context exists an axiom at some point (when i didn't want to deal with names and finite sets)
10:30 gal_bolle (* Given two sequences ending with two patches with the same name n,
10:30 gal_bolle we can commute them into a common part ending with a patch with name
10:30 gal_bolle n, and the rest of each. That is, we can get back to the context in
10:30 gal_bolle which a patch named n was first recorded, except for patches which
10:30 gal_bolle were unpulled in either s or s'. Is this too strong an assumption? *)
10:30 gal_bolle Hypothesis name_original_context : forall a b c d e
10:31 gal_bolle (s: FL Patch a b)
10:31 gal_bolle (s': FL Patch a c)
10:31 gal_bolle (p: Patch b d)
10:31 gal_bolle (p': Patch c e),
10:31 gal_bolle patchname p = patchname p' ->
10:31 gal_bolle exists f: State, exists g:State,
10:31 gal_bolle exists ctx: FL Patch a f, exists p'' : Patch f g,
10:31 gal_bolle exists rest : FL Patch g d, exists rest' : FL Patch g e,
10:31 gal_bolle patchname p'' = patchname p /\
10:31 gal_bolle (s +> p :> NilFL) =~= (ctx +> p'' :> rest) /\
10:31 gal_bolle (s' +> p' :> NilFL) =~= (ctx +> p'' :> rest').
10:31 Igloo Ah, Hypothesis = Axiom, right?
10:31 gal_bolle yes
10:32 Igloo OK
10:32 Igloo so that would still need to be proven
11:10 gal_bolle yes, but i thought it summed up what names give
11:11 Igloo It'll definitely need to be proven for catches
11:16 gal_bolle so my plan is/was to use that hypothesis to isolate names from the rest of the proofs
11:16 gal_bolle maybe it's worth going that way for catches
11:17 gal_bolle the dic repo is now up to date, if you want to take a look
11:17 gal_bolle but it's not very readable i'm afraid
12:34 jnaimard joined #darcs-theory
12:39 jnaimard joined #darcs-theory
13:37 gal_bolle joined #darcs-theory
15:03 gal_bolle Module Import Shmo := Shmorf.Shmo.
15:03 gal_bolle Module Import Shu := Shmo.Shu.
15:03 gal_bolle sorry
15:05 Igloo Did you have Thundercats in France?
15:06 gal_bolle maybe
15:07 gal_bolle let me wikipedia out the french name
15:07 Igloo Sounds like module names Snarf would use, anyway  :-)
15:07 gal_bolle cosmocats they were
15:07 gal_bolle but i didn't watch it
15:08 Igloo Oh well, not important  :-)
15:12 Igloo In what way?
15:13 gal_bolle scholarness
15:13 Igloo Ah  :-)
15:41 gal_bolle The term "middle_left" has type "FL Patch c x"
15:41 gal_bolle while it is expected to have type
15:41 gal_bolle "Shmor.Shmo.Shu.Seq.SequenceAsPatch.Patch d ?14304".
15:41 gal_bolle i love these error messages
15:43 Igloo :-)
15:43 Igloo Would Shmor.Shmo.Shu make more sense if I spoke French?
15:44 gal_bolle nope
15:44 gal_bolle maybe in hebrew
15:44 gal_bolle or yiddish
15:44 gal_bolle sounds a bit like it
15:45 gal_bolle Shmor is "Shuffle mark one rectify"
15:45 gal_bolle Shmo is "Shuffle mark one"
15:45 gal_bolle and Shu is shuffle
15:46 Igloo Aha
15:46 Igloo I went the other way, with NamesAsLongAsYourScreenIsWide  :-)
15:46 * Igloo doesn't have a feel for what is best yet
15:46 gal_bolle yes, but these name don't appear explicitely in my code
15:47 gal_bolle it's modules which are imported
15:47 gal_bolle so i don't care for their names
15:47 Igloo Ah, OK
15:47 gal_bolle the other names are sometimes baroque but as explicit as possible
15:47 Igloo I was wondering if patch sequences could be moved inside PatchUniverse, so we only need one sequence type
15:47 gal_bolle though i sometimes would like to say wiggle_the_patch_down
15:47 Igloo Then it could just use unqualified Cons and Nil
15:47 gal_bolle or some such
15:48 Igloo *nod*
15:48 gal_bolle i'm not sure what you mean
15:48 Igloo Well, currently I have
15:48 gal_bolle my patch sequence types (and all the theorems about it) are parametric in the patches
15:48 Igloo namedPatchSequence = NilNamedPatchSequence | ConsNamedPatchSequence x xs
15:49 gal_bolle so i only have one cons and one nil
15:49 Igloo Right, that's what I mean
15:49 Igloo The only thing is, unnamed patches are different as they don't have sets of names as parameters
15:49 Igloo But I'm not sure that we actually use unnamed patch sequences any more
15:50 gal_bolle my approach is to give them paramaters anyway
15:50 gal_bolle but not say what the parameters are
15:50 gal_bolle then later we can say parameter_type = unit
15:50 gal_bolle and we're done
15:50 Igloo We used to use them for the "p commutes past (q r)" pemmas, but now the lemmas explicitly commute past q and r separately anyway
15:50 gal_bolle yes
15:51 gal_bolle (this suppose that the sequence treat the parameters as opaque, but it's good for sanity anyway)
15:51 Igloo I'm not sure if generalising the type will work for my proofs
15:51 Igloo As the sets are actually used in the proof
15:51 Igloo Maybe it would be fine anyway
15:52 Igloo No, I think it must be fine. There are no properties about the sets in teh actual sequence, only that the two midpoints match
15:53 gal_bolle in the worst case, i think there's a way in coq's module system to have sequence use a type opaquely, then use sequence with the constraint that this type is in fact some transparent type we know
15:53 gal_bolle but it shouldn't be necessary
17:17 arjanb joined #darcs-theory