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

All times shown according to UTC.

Time Nick Message
09:07 gal_bolle joined #darcs-theory
11:15 gal_bolle joined #darcs-theory
11:47 gal_bolle hi all
11:49 Igloo Hey
11:50 Igloo gal_bolle: fsetdec is shiny, although I do need to clear any unused hypotheses or it just makes my CPU get hot
11:50 gal_bolle hehe
11:51 gal_bolle great
11:51 gal_bolle look in your mailbox
11:53 Igloo OK, great. I will read it properly later
11:55 gal_bolle it's really an innocent remark
11:55 gal_bolle for once…
11:56 Igloo I've skimmed it, but can't think about what 3-line formulae mean right now  :-)
11:57 gal_bolle do the drawing i describe in the end, it was enlightening for me
12:31 gal_bolle btw, is it true that (p^)^=p Q
12:31 gal_bolle p^^ = p
12:31 gal_bolle otherwise, i think we need some more axioms
12:32 gal_bolle a version of commute-preserves-commute and commute-consistent with p going in the other direction
12:32 Igloo Someone pointed out that nameInverseInverse makes namesInverseInjective incidentally
12:32 Igloo p^^ = p, yes
12:33 gal_bolle thanks
12:33 gal_bolle yay for coq catching missing axioms
12:33 Igloo boo for coq not catching redundant axioms  :-)
12:34 gal_bolle it can give hint at them, though
12:35 Igloo How do you mean?
12:35 gal_bolle its for constructors rather than axioms
12:36 gal_bolle but if you make a structure closed by some redundant operation
12:36 gal_bolle by adding too many constructors to an inductive
12:36 gal_bolle then inverting that inductive will quickly show you that there is some overlap
13:13 gal_bolle Theorem shuffle_preserves_comm_seq_patch:
13:13 gal_bolle forall a b b' c
13:13 gal_bolle (s: FL Patch a b) (s': FL Patch a b) (p: Patch b c)
13:13 gal_bolle (s'': FL Patch b' c) (p': Patch a b'),
13:13 gal_bolle s =~= s' ->
13:13 gal_bolle comm_seq_patch s p p' s'' ->
13:13 gal_bolle exists s3, comm_seq_patch s' p p' s3.
13:13 * gal_bolle would never have thought that one would be tricky
13:16 Igloo It should just be induction on s =~= s', shouldn't it?
13:24 gal_bolle yes
13:24 gal_bolle but then you need to invert everythings guts-out
13:25 gal_bolle there's nothing hard
13:25 gal_bolle just a lot of little drawings to do
13:25 gal_bolle and it took me a moment to notice that i was lacking an axiom
13:26 Igloo The ^^p = p one?
13:27 * Igloo doesn't see why that should be necessary
13:27 Igloo (in this proof)
13:31 gal_bolle because i need a commute consistent with p in the wrong direction
13:31 Igloo Ah, OK
13:31 gal_bolle that took a bit to spot
13:32 gal_bolle i doubted my internal implementation of unification
13:32 gal_bolle until i remembered that i had to put arrows and not just lines on my drawings
13:32 Igloo In lemmas like NamedPatchCommutePreservesCommute I've been wondering if the <- direction should just be some (currently non-existant) lemma and the -> direction
13:32 Igloo Heh
13:32 gal_bolle yes
13:33 gal_bolle i think the axioms should be just the -> direction
13:33 gal_bolle too
13:33 gal_bolle (cf my mail)
13:34 Igloo Well, I think better would be to split them into -> and <- separate axioms, and a tiny => <-> axiom
13:35 gal_bolle if it's commute-preserves-commute, then given ->, <- is just the axiom instantiated the other way
13:35 Igloo With various refactoring polished off by mattam's reverse tip, the proof is looking more succinct, BTW: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=4018
13:35 Igloo You mean by inverting all the patches?
13:35 Igloo (and sequences)
13:35 gal_bolle no by exchanging q and r with q' and r'
13:36 Igloo I don't follow; the result is ((q1 <~?~> r1) <-> (q3 <~?~> r3))
13:36 gal_bolle yes, but that is equivalent to:
13:37 Igloo And the assumption <p, qr1> <~> <qr3, p> make it directional
13:37 gal_bolle (forall q4 r4, <q1,r1> <~> <r4,q4> -> (q3 <~?~> r3)) /\ vice-versa
13:38 Igloo right
13:38 gal_bolle then you can take that forall q4 r4 out of the /\
13:38 gal_bolle no sorry, the other way around
13:38 gal_bolle you can take the /\ to the top level
13:39 Igloo Oh, wait, do you mean that you can repeat the whole proof a second time?
13:39 gal_bolle yup
13:39 gal_bolle just instantiating the variables differently
13:40 Igloo Right, agreed, but I'm suggesting you could have a much smaller proof, where you translate the <- with pqr into -> with their inverses
13:40 Igloo Well, maybe it wouldn't actually be that much smaller by the time you've inverted everything
13:41 gal_bolle ok, i was just looking for a small axiom
13:42 gal_bolle and making the case that it was equivalent by manipulating the formula rather than doing a real proof
13:42 Igloo YM the axiom has only -> but the lemma has <->?
13:43 gal_bolle yup
13:43 Igloo OK, I see
13:45 gal_bolle and then if you take the forall q4 r4 to the toplevel, it has the same hypothesis as commute-consistent
13:45 gal_bolle so you can make that one axiom
13:45 gal_bolle which is good because otherwise, both axioms introduce the same context in different ways
13:46 gal_bolle so you don't have the information that it _is_ the same context (when you used the named version)
13:46 gal_bolle of course, there, the axioms are actually lemmas, but you see why it's preferable
13:47 Igloo Hmm, you mean they can be sensibly combined into 1 axiom? If so, can you e-mail me what you think the axiom should be, please?
13:48 gal_bolle it's in the e-mail i sent you this morning
13:48 gal_bolle i'll send you a graphical version
13:49 Igloo Ah, I hadn't realised you'd merged them. OK.
14:33 gal_bolle igloo: http://patch-tag.com/repo/d​ic/browse/commute_cube.pdf
14:33 gal_bolle this is the graphical version
14:37 Igloo gal_bolle: Ta
14:59 gal_bolle is the drawing clear?
15:28 kowey joined #darcs-theory
17:33 arjanb joined #darcs-theory
20:20 Heffalump joined #darcs-theory
20:21 tux_rocker joined #darcs-theory
20:21 Heffalump Igloo: if you have patches A and B which conflict, and C which depends on A (only), and a repo with A+B+resolutionpatch, is it a necessary property of current camp theory that C is in conflict if pulled into that repo?
20:23 Igloo It's a necessary property of any theory that works along the same lines as camp/darcs, isn't it?
20:23 Heffalump why?
20:23 Igloo You'd need a theory where resolution meant cancelling a patch or a branch or something to not make it a conflict
20:23 Igloo Well, the effect of A is not in AB'R, so you can't apply the effect of C
20:24 Heffalump I'm imagining a hypothetical kind of resolution patch that applies A's effect in some way - e.g. by concatenating the conflicting text of A and B in a user-determined order, in the case of a hunk-hunk conflict
20:25 Heffalump i.e. I can give a commutation rule for C and the resolution patch (for at least some possible Cs)
20:26 Heffalump sorry, I mean the difference between the resolution patch and A, or something. Hmm.
20:27 Heffalump anyway, the question is does the rest of the theory, e.g. conflictors, break down nastily if this kind of thing is allowed to happen?
20:27 Igloo OK, then you might be able to make that work
20:28 Igloo It is very hairy, though
20:28 Heffalump as in the conflictor stuff will be hairy?