Time 
Nick 
Message 
09:07 

gal_bolle joined #darcstheory 
11:15 

gal_bolle joined #darcstheory 
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 3line 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 commutepreservescommute and commuteconsistent 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 gutsout 
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 nonexistant) 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 commutepreservescommute, 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)) /\ viceversa 
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 commuteconsistent 
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 email me what you think the axiom should be, please? 
13:48 
gal_bolle 
it's in the email 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://patchtag.com/repo/dic/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 #darcstheory 
17:33 

arjanb joined #darcstheory 
20:20 

Heffalump joined #darcstheory 
20:21 

tux_rocker joined #darcstheory 
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 userdetermined order, in the case of a hunkhunk 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? 
20:29 
Igloo 
Suppose you start with a 2line file 
20:29 
Igloo 
A and B each add a line between those 2 lines 
20:29 
Igloo 
C removes the line A added and the last line 
20:29 
Igloo 
If you resolve it with A's line added first, then C would have to remove lines 2 and 4 
20:30 
Heffalump 
not all Cs will work 
20:31 
Igloo 
So you'd have to work out if commuting C' past R^ should turn C' back into a nonconflictor 
20:31 
Heffalump 
ok 
20:31 
Igloo 
In a similar way to how you can make A A^ + B give you A A^ B, rather than B being a conflictor 
20:33 
* Igloo 
is dubious, though 
20:33 
Igloo 
The reason A A^ is OK is that you can always keep the patch and its inverse together (or rather, the sequences of patches and their inverses can be kept together) 
20:35 
Heffalump 
this is because we don't have conflictors that support arbitrary commutes, right? 
20:35 
Igloo 
Yup 
20:36 
Heffalump 
most annoying, that :( 
20:39 

kowey joined #darcstheory 