Time 
Nick 
Message 
08:52 

arjanb joined #darcstheory 
11:25 

Igloo_ joined #darcstheory 
14:04 

gal_bolle joined #darcstheory 
14:05 
gal_bolle 
hi igloo, if you're still intrested in getting the axioms as small as possible, commutesquare should be an implication, not an equivalence 
14:05 
gal_bolle 
since you can get one side from the other by using commuteselfinvert 
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 #darcstheory 
14:25 
gal_bolle 
looks great 
14:26 
gal_bolle 
is it already in your repository? 
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 nontransitive 
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 #darcstheory 
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 #darcstheory 