Time 
Nick 
Message 
11:10 

arjanb joined #darcstheory 
11:38 

gal_bolle joined #darcstheory 
16:52 

gal_bolle joined #darcstheory 
16:53 

gal_bolle joined #darcstheory 
17:27 
gal_bolle 
igloo: i can't get your coq to compile 
17:30 
Igloo 
gal_bolle: Hmm, with an uptodate copy of my repo? 
17:35 
gal_bolle 
yes I think so 
17:35 
gal_bolle 
yes 
17:35 
Igloo 
gal_bolle: What error do you get, and with which file? 
17:35 
gal_bolle 
it's my fau 
17:35 
gal_bolle 
my fault sorry 
17:36 
gal_bolle 
i did not respect the order of the loads 
17:36 
Igloo 
Doesn't it do that itself? 
17:37 
gal_bolle 
hmm 
17:37 
Igloo 
I just load the file I'm interested in in coqide, and it takes care of it, anyway. Maybe proof general is different 
17:37 
gal_bolle 
unnamed_patches gets duplicated with the Load patch_sequences.v on top of foo.v 
17:37 
gal_bolle 
i don't really know 
17:37 
gal_bolle 
i don't use load 
17:37 
gal_bolle 
Require is cleaner in my understanding 
17:38 
Igloo 
I think require was loading .vo files rather than .v files 
17:38 
gal_bolle 
it's ok 
17:38 
gal_bolle 
but i think Load is Require Export 
17:39 
gal_bolle 
whereas Require Import is more often what you want 
17:39 
gal_bolle 
but my experience with such things is low 
17:39 
gal_bolle 
ok, so your commute_relate is my shuffle 
17:39 
gal_bolle 
stated differently 
17:40 
Igloo 
Require Import "patch_sequences.v". says "Error: Can't find file patch_sequences.v.vo on loadpath" 
17:40 
gal_bolle 
Require Import patch_sequences. 
17:40 
gal_bolle 
and yes, you need to have a .vo 
17:41 
gal_bolle 
so that means changing your Makefile 
17:41 
Igloo 
OK. Well, it also means changing how I work 
17:41 
gal_bolle 
yes, so not worth the bother 
17:41 
gal_bolle 
I was just surprised 
17:41 
Igloo 
I'd need to run "make" before opening something in coqide to be sure I'm using the code I think I am 
17:41 
Igloo 
It's already a pain having to restart coqide when I change a dep 
17:42 
Igloo 
Anyway, commute_relates == shuffle, yes 
17:42 
gal_bolle 
ok 
17:42 
gal_bolle 
and commuteOutLeft q r s says "I can take some patch with the same name as r at the head of q, and I get r:>s" 
17:43 
Igloo 
commute_relates + swap, actually, I think 
17:43 
gal_bolle 
yes, of course, commute_relates alone does not make sense 
17:43 
Igloo 
r is the actual patch that you get out, not just one with the same name, but yes 
17:44 
gal_bolle 
yes, that's what I tried to formulate 
17:44 
gal_bolle 
i think it would be good style in coq to make a distinction between variables which are sequences and those which are patches 
17:45 
Igloo 
Do you mean "ps" vs "p"? 
17:45 
* Igloo 
is also hideously inconsistent with capitals 
18:08 

gal_bolle joined #darcstheory 
18:15 

gal_bolle left #darcstheory 
18:15 

gal_bolle joined #darcstheory 
18:15 
gal_bolle 
Igloo: back 
18:16 
gal_bolle 
i think you need marked sequences in order to prove your lemma 
18:16 
gal_bolle 
s/need/probably want/ 
18:16 
Igloo 
gal_bolle: Marked in what way? Have a list of names with them? 
18:17 
gal_bolle 
as in either that or more or less my shuffle_marked1 
18:17 
gal_bolle 
your commuteOutLeft is a subcase of my shuffle_marked1 
18:18 
gal_bolle 
commuteOutLeft r s1 s2 is equivalent to: 
18:18 
gal_bolle 
commuteOutLeft r (s1+>r':>s2) s3 is equivalent to: 
18:18 
Igloo 
I'll look at your code in more detail later 
18:19 
gal_bolle 
s1#>r'>#s2 =~~= NilFL#>r>#s3 
18:19 
Igloo 
But yeah, I'm not sure about details like exposing the names in sequences differently, or giving sequences a nat containing their length, etc, will be helpful or a hinderance 
18:19 
gal_bolle 
you're constraining one of the arguments to be NilFL 
18:20 
gal_bolle 
(ie, you only consider the case where you pull to the end) 
18:20 
gal_bolle 
but i think you need an induction on all the places you can pull to in order to conclude 
18:20 
gal_bolle 
if you go to the Admitted. in foo.v, there you need to do something with n 
18:21 
gal_bolle 
if it's 0 it's ok, you can conclude by commuteOutLeftSwap 
18:22 
gal_bolle 
but in the other case, there's a step of commute which you need to do, but which I don't know how to express with the NilFL constraint 
18:23 
gal_bolle 
maybe I'm confused and induction n with a suitably generalized goal works 
18:24 
Igloo 
*nod*, thanks for the ideas. I'll see what I can make of it 
18:45 
gal_bolle 
i think you have a problem in commuteOutLeft[Swap] 
18:46 
gal_bolle 
in the commuteOutLeftSwap constructor 
18:46 
gal_bolle 
s' is not constrained 
18:46 
gal_bolle 
there's probably not enough information in that predicate 
18:49 
Igloo 
Oh, yes. I think s' = Cons p' s or something 
18:50 
gal_bolle 
k 
18:50 
Igloo 
thanks! 
18:51 
gal_bolle 
i caught that by adding Implicit Arguments commuteOutLeftSwap. 
18:51 
gal_bolle 
Then Print commuteOutLeft. 
18:51 
gal_bolle 
s' did not get implicited 
18:51 
gal_bolle 
which was not normal 
18:52 
Igloo 
Ah, cunning 
18:55 
gal_bolle 
i'm a bit lost in that proof 
18:57 
gal_bolle 
i'm not sure if you should start with induction H or H0 
18:59 
Igloo 
I think it needs a subproof that commuteOutLeft p q r /\ commuteOutLeft p q r' > r = r' or something 
18:59 
Igloo 
Anyway, I didn't expect you to start trying to prove it. I was just letting you know where I was :) 
19:01 
gal_bolle 
yes, you probably need that 
19:01 
gal_bolle 
i'm proving these kinds of lemma for shuffles myself 
19:01 
gal_bolle 
so we're at the same point 
19:01 
gal_bolle 
still, I'm worried about how you plan to tackle the axiomatisation of sensible sequences 
19:02 
Igloo 
You mean how I plan to do the contexts? 
19:02 
gal_bolle 
i'm not sure if that's it 
19:02 
Igloo 
I think I'll put an abstract context type on unnamed patches 
19:02 
gal_bolle 
ok 
19:03 
* Igloo 
isn't thinking about that ATM, though 
19:03 
gal_bolle 
it's reassuring to see your code slowly converging to a cleaner version of mine ;) 
19:05 
gal_bolle 
btw, i think that sensibility is underspecified in the paper 
19:05 
gal_bolle 
section 12.1 
19:06 
gal_bolle 
Explanation 
19:06 
gal_bolle 
What we’re saying here is that if we have two repos that diﬀer in only their last patch then 
19:06 
gal_bolle 
we can always merge them. The two (equal up to commutation) results of the repo merge 
19:06 
gal_bolle 
are cde 
19:06 
gal_bolle 
′ 
19:06 
gal_bolle 
and ced 
19:06 
gal_bolle 
′ 
19:06 
gal_bolle 
. 
19:06 
gal_bolle 
this is a problem: we don't prove that we do that sensibly 
19:13 
Igloo 
There might be a theorem missing, but it is true 
19:14 
* Igloo 
is mostly away, sorry 
19:14 
gal_bolle 
I don't doubt it's true 
19:14 
gal_bolle 
i just think there's also a definition missing 
19:17 
gal_bolle 
we don't have an axiom that says : if spp^q is sensible, then so is sq ? 
19:19 
Igloo 
I don't think you can make both of those sequences unless p^ and q commute 
19:20 
gal_bolle 
hmm 
19:21 
gal_bolle 
sorry, it's if sp and sq are sensible, so is spp^q 
19:21 
gal_bolle 
(assuming p and q are not equal or inverts) 
19:22 
gal_bolle 
(with unnamed abstract contexts, this says that if p: Patch a b, then p^: Patch b a) 
19:22 
Igloo 
Ah, yes, OK, I think you are right 
19:23 
gal_bolle 
you may also want if s and s' are sensible, so is ss' 
19:24 
Igloo 
That's not true 
19:24 
gal_bolle 
sp and ps' 
19:24 
gal_bolle 
so is sps' 
19:24 
Igloo 
addfile "x"; addfile "x" isn't sensible, but the two subsequences are 
19:24 
gal_bolle 
(p is a patch, s and s' are sequences) 
19:24 
* arjanb 
is wary of adding axioms containing patches and their inverses 
19:25 
gal_bolle 
why? 
19:25 
gal_bolle 
this one really is the definition of the inverse 
19:25 
gal_bolle 
if you don't have it, then the inverse is any arbitrary patch 
19:26 
gal_bolle 
(as i said, it just says that if p goes from a to b, then p^ goes from b to a) 
19:27 
arjanb 
it's very easy to get to the point of the old conflictors where arbitrarily commutation is needed 
19:28 
gal_bolle 
i'm not convinced that arbitrary commute is not the solution (JP Bernardy's solution) 
19:28 
Heffalump 
I never quite understood his representation of them 
19:29 
gal_bolle 
his patch types, or what happens when you force commutation? 
19:29 
Heffalump 
the latter 
19:29 
Heffalump 
I should read that paper again 
19:29 
gal_bolle 
you get conflict markers (poor ones at the moment, afaik) 
19:30 
Heffalump 
but how does he guarantee the same result after different orderings? 
19:30 
gal_bolle 
the markers won't be the same 
19:31 
Heffalump 
that's no good, though 
19:31 
gal_bolle 
but the internal representation will 
19:31 
Heffalump 
oh, right 
19:31 
gal_bolle 
(same as in darcs, i think) 
19:32 
gal_bolle 
although in more cases 
19:32 
gal_bolle 
in the case of failed dependencies in addition to conflicts 
19:32 
gal_bolle 
and duplicated patches too 
19:33 
gal_bolle 
but there's no reason you can't add a dependency layer on top of that 
19:37 
* Heffalump 
is rereading their paper and can't actually find any detail of this 
19:37 
gal_bolle 
the last line is my idea 
19:37 
Heffalump 
IM of the conflict representation at all 
19:37 
Heffalump 
I think there was a bit more in the emails but not much 
19:38 
gal_bolle 
can't remember 
19:38 
gal_bolle 
more than this, that is 