Time 
Nick 
Message 
08:39 

gal_bolle joined #darcstheory 
09:51 

kowey joined #darcstheory 
10:50 

gal_bolle joined #darcstheory 
11:35 

jnaimard joined #darcstheory 
12:38 

tux_rocker joined #darcstheory 
14:28 
Igloo 
jnaimard: OK, I see what you're saying re the axiom rewrites, I think 
14:28 
Igloo 
jnaimard: It looks to me that we should avoid using exists in axioms/lemmas, except in the conclusions 
14:29 
Igloo 
jnaimard: Using them in the assumptions just makes it harder to use the axiom/lemma 
14:41 
jnaimard 
yes 
14:43 
gal_bolle 
and i think that my geometric intuition at the end could be formalized into something useful 
15:05 
Igloo 
Ah, it does mean we lose the <> for UnnamedPatchCommuteConsistent though 
15:06 
Igloo 
But I don't think that that is important 
15:11 
gal_bolle 
i think you get it back by using inverses everywhere 
15:12 
gal_bolle 
Lemma commute_consistent_mirror: 
15:12 
gal_bolle 
forall a b c d e f g 
15:12 
gal_bolle 
(p : Patch b a) (q : Patch b c) (r: Patch c d) 
15:12 
gal_bolle 
(q'': Patch a e) (r'': Patch e f) (p': Patch d f) 
15:12 
gal_bolle 
(p'': Patch c e) (r': Patch b g) (q': Patch g d), 
15:12 
gal_bolle 
<<q,r>> <~> <<r',q'>> > 
15:12 
gal_bolle 
<<q,p''>> <~> <<p,q''>> > 
15:12 
Igloo 
No, it's just pointless in that lemma 
15:12 
gal_bolle 
<<p'',r''>> <~> <<r,p'>> > 
15:12 
gal_bolle 
exists f, exists r3: (Patch a f), exists p3, exists q3, 
15:12 
Igloo 
You just need to flip the <<q, r>> <~>u <<r', q'>> 
15:12 
gal_bolle 
<<r',p3>> <~> <<p,r3>> /\ <<p3,q3>> <~> <<q',p'>> /\ 
15:12 
gal_bolle 
<<r3,q3>> <~> <<q'',r''>> 
15:12 
gal_bolle 
. 
15:12 
gal_bolle 
ah ok 
15:12 
Igloo 
The interesting opposite case is when p starts /after/ qr, not before it 
15:13 
* gal_bolle 
has thought too much about this in terms of flipping cubes 
15:14 
Igloo 
:) 
15:15 
gal_bolle 
the axiom is for when the vertices adjacent to the three faces has two incoming edges and one outgoing 
15:15 
gal_bolle 
and the lemma is useful in the opposite case 
15:16 
gal_bolle 
but if p is before q and r, and you invert everyone, p^ ends up after q^ and r^ 
15:19 
Igloo 
Right, although we don't have all the lemmas we'd need for that yet 
15:20 
Igloo 
Well, maybe we do for these lemmas 
15:34 
gal_bolle 
we have it more or less 
15:35 
gal_bolle 
after much pondering i did implement inversion of sequences 
16:28 

arjanb joined #darcstheory 
17:02 

gal_bolle left #darcstheory 