Time 
Nick 
Message 
07:31 

kowey joined #darcstheory 
12:57 

Guest934 joined #darcstheory 
15:00 
gal_bolle 
igloo: where have you gotten to with coq? 
15:01 
gal_bolle 
it would be nice to have a consensus on one version before/during the sprint 
15:12 
Igloo 
gal_bolle: I am stuck at two points: 
15:12 
Igloo 
Lemma NamedPatchCommutePreservesCommute 
15:13 
Igloo 
I don't think this is hard, it's just big, and I need to invert the right things and give them sensible names that match a picture so that I can follow what's going on 
15:13 
Igloo 
Lemma Foo 
15:14 
Igloo 
This I need to get the right induction pattern for 
15:14 
Igloo 
My aim for the Hackathon is to get NamedPatchCommutePreservesCommute done, and any other lemmas that I've skipped over up to now 
15:15 
Igloo 
And then to be able to describe better why Foo is true 
15:15 
Igloo 
Then hopefully you and/or Eelis (who's also said he's interested in this stuff) can tell me if/where I'm going wrong 
15:16 
Igloo 
gal_bolle: You won't be physically at the Hackathon, right? 
15:19 
Igloo 
gal_bolle: Oh, I was going to compare what we have after you modularised yours, but I completely forgot about it 
15:20 
gal_bolle 
ok, you can pull, i pushed everything 
15:20 
gal_bolle 
why does NamedPatchCommutePreservesCommute get so big? 
15:21 
gal_bolle 
ok, that's one point where having names as a construction rather than an axiom hits you 
15:21 
gal_bolle 
i think i have a middle ground for this. 
15:21 
Igloo 
http://urchin.earth.li/~ian/NamedPatchCommutePreservesCommute.png is the image 
15:22 
gal_bolle 
(note that i don't have any named patches stuff yet) 
15:22 
Igloo 
For each of those patches you have a named patch and an unnamed patch (plus various other bits and pieces), and when coq assigns them random names it's impossible to see what's going on 
15:22 
gal_bolle 
yes, that's the drawback of inversion 
15:23 
Igloo 
I was doing things like 
15:23 
Igloo 
inversion p1 as [? np ? ? ? up1]. 
15:23 
gal_bolle 
you can try "rename toto into titi" to unconfuse things too 
15:23 
Igloo 
but I don't think that works, because coq doesn't consistently apply that everywhere 
15:23 
gal_bolle 
ok, so i'd like to talk about the big picture for a moment 
15:23 
gal_bolle 
is that ok with you 
15:23 
gal_bolle 
? 
15:24 
gal_bolle 
or should i send a mail on the darcsusers list? 
15:24 
Igloo 
So I think I need to invert the p1andq1invert hypothesis instead, and give names to everything that comes out of that. Maybe. 
15:24 
Igloo 
Here is fine 
15:24 
Igloo 
Mail is also fine, if you prefer that 
15:24 
Igloo 
Although the camp list might be better 
15:24 
gal_bolle 
there is a camp list? 
15:25 
* gal_bolle 
feels very stupid 
15:25 
Igloo 
http://projects.haskell.org/cgibin/mailman/listinfo/camp 
15:25 
Igloo 
Don't worry, you haven't been missing much :) 
15:25 
Igloo 
Just some random status updates, I think 
15:25 
gal_bolle 
ok 
15:26 
* Igloo 
wonders if "Contacting us" is the wrong link text for the mailing list page 
15:26 
gal_bolle 
it's absolutely wrong 
15:26 
gal_bolle 
in my opinion 
15:26 
Igloo 
What's right, and also covers IRC? 
15:27 
gal_bolle 
forums is ugly but conveys the right message 
15:27 
gal_bolle 
(fora for additionned pedantism) 
15:27 
gal_bolle 
or discussions 
15:27 
Igloo 
Maybe there should be a "Mailing list" and "IRC" link to the same page 
15:27 
Igloo 
Anyway, big picture! 
15:27 
gal_bolle 
yes 
15:28 
gal_bolle 
so the big point of camp is names 
15:28 
gal_bolle 
do we agree? 
15:28 
Igloo 
No. The big point is correctness. 
15:28 
Igloo 
And simplicity 
15:28 
gal_bolle 
i mean the main innovation with respect to darcs 
15:29 
Igloo 
The main design choice difference is names 
15:29 
gal_bolle 
i agree about your two points wholly 
15:29 
gal_bolle 
ok, we agree 
15:29 
gal_bolle 
so my opinion is that we should introduce them as late as possible, with _one_ axiom 
15:30 
Igloo 
Would you want to do that if darcs didn't exist? 
15:30 
gal_bolle 
yes 
15:30 
gal_bolle 
it's orthogonal 
15:30 
gal_bolle 
let me explain why 
15:31 
gal_bolle 
picture yourself proving some theorem about named patches 
15:31 
gal_bolle 
you'll get a lot of patches on your sheet, which came from different part of your proof 
15:32 
gal_bolle 
and at a moment, you take p and q and say "either their names are different or they are equal" 
15:32 
Igloo 
assuming they have the same context 
15:32 
gal_bolle 
no, assuming nothing 
15:32 
Igloo 
OK, so not equal in the coq = sense then 
15:33 
gal_bolle 
no, they referred to the names 
15:33 
Igloo 
Oh, I see. Yes. 
15:33 
gal_bolle 
generally, the differentnames branches will be easy, it's the case you are expected 
15:34 
gal_bolle 
that the names happen to be equal will be an "exceptional case" 
15:34 
gal_bolle 
s/expected/expecting/ 
15:34 
gal_bolle 
so in the equal case, you want as much information as possible 
15:35 
Igloo 
There's a third case where the names are inverses, incidentally 
15:36 
gal_bolle 
that's why (in coqland) i'd like to have a reasonably big base of lemmas fo unnamed patches, and one axioms that says if (name p) = (name q) then R p q. 
15:36 
Igloo 
What is R? 
15:36 
gal_bolle 
yes, i consider this first case treated by "consider p^" (or "consider q^") 
15:36 
gal_bolle 
that's the point: what should R be? 
15:37 
Igloo 
You would still need to prove that (same name AND same context => some patch representation), for example 
15:37 
gal_bolle 
not necessarily 
15:37 
Igloo 
FWIW, here are the reasons I like my approach: 
15:37 
gal_bolle 
that's what my marked shuffles come from 
15:37 
Igloo 
Proving the named patch proofs is good practice for proving catch proofs 
15:37 
Igloo 
When proving catch proofs, we won't ever have to take apart named patches, so th 
15:37 
Igloo 
e fact that they are distinct from unnamed patches is irrelevant 
15:37 
Igloo 
I think that building named patches from unnamed patches and names is the right 
15:37 
Igloo 
mental model 
15:38 
Igloo 
Sigh, that pasted badly, sorry 
15:38 
gal_bolle 
it's ok 
15:38 
gal_bolle 
i agree with the premisses but not with the conclusion 
15:39 
gal_bolle 
my idea for R would be something a bit more involved like: 
15:39 
gal_bolle 
for every sequences (_:p:_) (_:p':_) such that name(p) = name(p') 
15:40 
gal_bolle 
there is a sequence (_:p'':_) from which the two above can be obtained 
15:40 
gal_bolle 
by commutation and patch deletion 
15:40 
gal_bolle 
(and maybe addition of qq^ pairs in the middle 
15:40 
gal_bolle 
) 
15:40 
gal_bolle 
with name p'' = name p 
15:41 
Igloo 
I don't think that you can make that an axiom 
15:41 
gal_bolle 
and patch addition 
15:41 
gal_bolle 
sorry 
15:41 
Igloo 
I think it's too complex 
15:42 
gal_bolle 
well, the sequence _:p'':_ is the context where (name p) was recorded 
15:42 
gal_bolle 
so it's in fact natural 
15:42 
gal_bolle 
if you look at it the other way, it says that every name was recorded once 
15:43 
Igloo 
I guess so 
15:43 
gal_bolle 
and every instance of that name comes from that record + commutation and legal addition of patches 
15:43 
Igloo 
But you might have to invent patches that have been unpulled in order to actually compute p'' 
15:43 
Igloo 
In order to compute it by retracing your steps, I mean 
15:44 
gal_bolle 
yes, that's what the right part of p'' is for 
15:44 
gal_bolle 
it's also why i'm not sure about the final form of this R relation 
15:44 
* Igloo 
is unconvinced that that's going to be easier to work with 
15:45 
gal_bolle 
well, i find myself thinking «these patches come from the same record» 
15:45 
gal_bolle 
and i want a coq way to say that 
15:46 
Igloo 
I'm not sure I see why you're thinking that 
15:46 
Igloo 
Or rather, I'm not sure how that's different from "these patches have the same name" (when you're in a patch universe) 
15:47 
gal_bolle 
it's because i don't find that having "these patches have the same name" is a very good information to have 
15:48 
gal_bolle 
once you have that information, the only way to use it is to say "when the last of the two was recorded, the first existed already, so they were in fact recorded at the same time" 
15:48 
Igloo 
Do you want \start{lemma}{patchinuniversehasminimalcontext}? 
15:49 
gal_bolle 
rather patchinuniversehasoriginalcontext 
15:49 
gal_bolle 
but minimal would do equally well 
15:49 

kowey joined #darcstheory 
15:49 
gal_bolle 
hi kowey 
15:49 
gal_bolle 
you've come at a historic moment… 
15:49 
kowey 
hi gal_bolle... ooh? 
15:49 
gal_bolle 
historical? 
15:49 
kowey 
ahistorical? 
15:49 
gal_bolle 
hysterical? 
15:49 
Igloo 
patchinuniversehasminimalcontext is a lemma in the latex, can will be in the coq once we can prove it 
15:50 
gal_bolle 
moment 
15:50 
Igloo 
And you can prove your axiom given the properties a patch universe satisfies 
15:50 
gal_bolle 
one second (moment as a phrase is german, isn't it?) 
15:50 
gal_bolle 
igloo: it's equivalent 
15:50 
Igloo 
It's not an unheard of phrase in English 
15:50 
gal_bolle 
just like i prefer f a = f b > a = b as a way to state injectivity 
15:51 
Igloo 
Although "one moment" is far more common 
15:51 
kowey 
erm... so I don't understand what you guys are saying, but sounds like a very good thing 
15:51 
gal_bolle 
rather than a <> b > f a <> f b 
15:52 
Igloo 
The difference is, in that case I agree with you :) 
15:52 
Igloo 
I just didn't know how to use the former with coq 
15:52 
gal_bolle 
ok, then i just have to convince you that your current way of stating it is the doublenegative one 
15:52 
gal_bolle 
and convince you to use my positive way 
15:53 
gal_bolle 
(newage proof theory, eminced pepper mint…) 
15:53 
gal_bolle 
the never changing coq 
15:53 
gal_bolle 
the ever changing goal 
15:53 
Igloo 
My axioms are simpler than yours and can prove yours, so you'll have a tough job persuading me I think :) 
15:54 
gal_bolle 
my answers to those claims are: my axiom is _one_ axiom, hence it is simpler 
15:54 
gal_bolle 
and it can also prove yours 
15:55 
Igloo 
OK, which would you rather prove for Primitive unnamed patches, my axioms or yours? 
15:55 
gal_bolle 
they only differ on states versus sensible sequences, don't they 
15:56 
Igloo 
In fact, I don't even know how one could prove yours. You'd need something like the patch universe concept to stop me recording 2 patches with the same name 
15:56 
gal_bolle 
that's the point 
15:56 
gal_bolle 
that's exactly the point, thanks for pinning it down 
15:57 
gal_bolle 
i suppose that i have a magical way to prevent collisions 
15:57 
gal_bolle 
prove that with that magical device, everything is good 
15:57 
Igloo 
Whereas I don't need one (as far as the person providing unnamed patches is concerned) 
15:57 
gal_bolle 
sorry, i misread you 
15:57 
gal_bolle 
i don't need one either 
15:58 
gal_bolle 
we are discussing unnamed patches only 
15:58 
gal_bolle 
aren't we 
15:58 
* gal_bolle 
is getting a bit confused 
15:58 
Igloo 
Your axiom uses names 
15:58 
gal_bolle 
no, it uses states 
15:58 
Igloo 
"for every sequences (_:p:_) (_:p':_) such that name(p) = name(p'), ..." 
15:58 
gal_bolle 
yes, it's the nameseliminationaxiom 
15:59 
gal_bolle 
everybody there is a named patch within a patch universe 
15:59 
gal_bolle 
i'm really getting confused 
16:00 
gal_bolle 
claim 1/ our formalisations of unnamed patches only marginally differ, with me using states and you sensible sequence, do you agree? 
16:01 
Igloo 
Yes, I have no opinions on unnamed patch representation in coq yet 
16:01 
gal_bolle 
ok 
16:01 
Igloo 
(or in the latex for that matter) 
16:01 
gal_bolle 
so my point is that currentcamp is not a correct patchuniverse 
16:02 
gal_bolle 
because the names are only in finite number 
16:02 
Igloo 
Do you mean the code isn't? 
16:02 
Igloo 
The set of names isn't required to be infinite 
16:02 
gal_bolle 
what i mean is that in a fully distributed system, we can't have a guaranteed way to have foolproof freshnames generation 
16:03 

DanielC joined #darcstheory 
16:04 
gal_bolle 
so you can't avoid namesclash 
16:04 
gal_bolle 
that's a fact we have to deal with 
16:04 
Igloo 
Ah, so you're saying that name clash avoidance needs to be an axiom? 
16:04 
gal_bolle 
how do you plan not to require it? 
16:04 
DanielC 
Question about patch theory: The only reason patches include context is so we know which patches to commute when we do a merge, but context does not actually affect the commutation rules at all, right? 
16:05 
Igloo 
Well, in order to use "record" in a patch universe you need to provide a name that isn't already used in that PU 
16:05 
gal_bolle 
ok, so it's an axiom of record that someone provides you with such a name 
16:05 
Igloo 
That's technically impossible in reality, of course, but we can wave our hands a bit 
16:05 
gal_bolle 
we agree on that course of axiom 
16:05 
gal_bolle 
of action sorry 
16:06 
Igloo 
It's not an axiom so much as a requirement of the operation 
16:06 
gal_bolle 
ok 
16:06 
Igloo 
record takes a mutable PU and a name not used in that PU, and mutates the PU. Or something. 
16:06 
gal_bolle 
ok 
16:06 
gal_bolle 
then i think i see where we disagree 
16:06 
Igloo 
Or you can sequence PUs like the IO monad. This is the unpleasant bit where we interact with the real world. 
16:07 
gal_bolle 
which is the first step towards agreement 
16:07 
Igloo 
:) 
16:07 
gal_bolle 
and smiling is the second step 
16:07 
gal_bolle 
so :) too 
16:07 
* Igloo 
picks up his shovel for step 3 
16:08 
gal_bolle 
if shovelpicking is step three, is it zeno's paradox? 
16:08 
gal_bolle 
so, i think you take a very algorithmic view of the proofs 
16:08 
gal_bolle 
you want to prove that this system with a mutable PU works 
16:09 
gal_bolle 
whereas i want something axiomatic (or descriptive, if you want) 
16:09 
Igloo 
It's PU manipulation where I think things become algorithmic 
16:09 
gal_bolle 
yes, i want to separate that algorithmic part from the logic part 
16:09 
gal_bolle 
so i have to separate two questions 
16:09 
Igloo 
Actually, maybe it doesn't have to be after all, as far as the theory is concerned 
16:10 
gal_bolle 
1/ What's a working PU, what does it buy us? 
16:10 
Igloo 
Because we can freely copy PUs in theory 
16:10 
gal_bolle 
2/ How do we get one 
16:10 
Igloo 
A PU is a set of repositories. It provides guarantees about the patches in these repositories 
16:11 
gal_bolle 
let me make that clearer 
16:11 
Igloo 
For example, every patch name has a unique minimal context in a PU 
16:11 
gal_bolle 
the crucial component of a PU is a Unique Name Generator 
16:12 
gal_bolle 
in fact, PUs are a tentative to encode unique name genarators, and one i'm not entirely satisfied with 
16:13 
gal_bolle 
do we agree on that (not on the satisfaction bit) 
16:14 
Igloo 
It's not really a generator as such, but OK 
16:14 
gal_bolle 
what i propose is to axiomatise this unique name generator with this Raxiom 
16:14 
Igloo 
record is something like: 
16:15 
Igloo 
If (N, repos@(repo:_), U) is a PU, n \in N, n \notin repos, u \in U, then (N, ((n, u):repo):repos, U) is a PU 
16:16 
Igloo 
where N is the set of names and U is the set of unnamed patches 
16:17 
Igloo 
And you can then prove that given you have a patch named n in two repos in that PU, that they share the same minimal context 
16:17 
gal_bolle 
ok 
16:17 
gal_bolle 
one moment 
16:17 
Igloo 
And that you can commute them directly to that context in the obvious way 
16:18 
gal_bolle 
what i don't like is the "n \notin repos" bit 
16:19 
gal_bolle 
that means that patch universes form an inductive type 
16:19 
gal_bolle 
with record, commute, merge as operations? 
16:19 
Igloo 
Yes 
16:19 
gal_bolle 
and unrecord 
16:20 
Igloo 
Yup 
16:21 
gal_bolle 
now if you have an hypothesis H: name p = name q 
16:21 
gal_bolle 
you'll need heavy inversion of the universe to find out how they are related 
16:22 
Igloo 
You'll have a lemma saying that they have the same minimal context 
16:22 
gal_bolle 
i want to see the proof of that lemma 
16:22 
gal_bolle 
it starts with "they come from the same record, and then, stuff happened" 
16:23 
gal_bolle 
and that's what i'm afraid of 
16:23 
gal_bolle 
and things i'm afraid of, i like to turn into axioms 
16:24 
Igloo 
OK, so the way I think it'll actually work is that there will be a property that is part of the inductive type that makes up a PU, and there will be a proof that record etc maintain the property 
16:24 
gal_bolle 
that's a kind of cowardness that's quite useful 
16:24 
gal_bolle 
ok, and that property will be my axiom, and the rest of the inductive construction won't see any use 
16:25 
Igloo 
Yes, but I think that we need to prove it, not axiomatise it 
16:25 
gal_bolle 
i halfagree 
16:26 
Igloo 
Incidentally, your lemma is false for darcs1 in theory and implementation, and the darcs2 implementation 
16:26 
Igloo 
Oh, I take that back, your lemma is true 
16:26 
Igloo 
But minimal contexts is false 
16:26 
gal_bolle 
aha 
16:26 
gal_bolle 
why? 
16:26 
Igloo 
And darcs can't actually use your lemma directly, because it might require patches that have been unpulled 
16:27 
gal_bolle 
of course 
16:27 
gal_bolle 
it's a lemma that should be used in proofs, not in code 
16:27 
Igloo 
s/lemma/axiom/g 
16:27 
gal_bolle 
goes without saying 
16:27 
Igloo 
See appendix B of the camp paper 
16:28 
Igloo 
I can dig up the script if you want to see the bug in action 
16:28 
gal_bolle 
oh yes, that's right 
16:28 
gal_bolle 
no it's ok 
16:28 
gal_bolle 
one moment 
16:28 
gal_bolle 
i thought that my axiom implied minimal context 
16:29 
gal_bolle 
it implies the record behaviour, doesn't it? 
16:30 
Igloo 
No, given PQR, your axiom allows a definition of commute that can give you PRQ and QRP but not RPQ 
16:30 
Igloo 
What do you mean by "the record behaviour"? 
16:31 
gal_bolle 
my axiom does not say anything about commute 
16:31 
Igloo 
http://hpaste.org/fastcgi/hpaste.fcgi/view?id=3787 is your axiom, right? 
16:32 
gal_bolle 
i keep commutepreservescommute and commuteconsistent 
16:32 
Igloo 
It says "by commutation" 
16:32 
gal_bolle 
yes 
16:34 
gal_bolle 
ok let me take it slowl 
16:34 
gal_bolle 
slowly 
16:34 
gal_bolle 
we have pqr 
16:34 
gal_bolle 
how do you apply my axiom? 
16:35 
Igloo 
If you take your axiom together with the other axioms then it will imply minimal contexts, but the other axioms imply that by themselves 
16:36 
Igloo 
But your axiom alone doesn't imply minimal contexts 
16:36 
gal_bolle 
no, that's right 
16:36 
gal_bolle 
i keep all axioms 
16:36 
gal_bolle 
and i replace the inductive definition of patch universes with my axiom 
16:37 
gal_bolle 
(the notion of patch universe goes out through the window@ 
16:37 
Igloo 
So surely it's better to not have an extra axiom? 
16:37 
gal_bolle 
so surely it's better to not have an extra inductive type? 
16:37 
Igloo 
When we extent the proofs downwards, we'll have to prove it anyway 
16:38 
Igloo 
But the extra inductive type doesn't make the theorem/proof weaker 
16:38 
gal_bolle 
yes, like you'll have to prove it upward if you don't have it 
16:38 
Igloo 
Yes, but the whole goal is to prove these things 
16:38 
gal_bolle 
it's a question of where we cut through the sandwich between implementation and specification 
16:39 
gal_bolle 
my point is that 
16:39 
Igloo 
What we're currently calling axioms I'll want to prove for primitive patches at some point 
16:39 
gal_bolle 
i agre 
16:39 
gal_bolle 
agree 
16:39 
gal_bolle 
but slicing at the right place and isolating components is important 
16:39 
gal_bolle 
it can save us a lot of work 
16:41 
gal_bolle 
do you agree that either my axiom appears as a lemma in proving minimal context, or that (an implementation of) patch universes appear in proving my axiom 
16:41 
gal_bolle 
? 
16:41 
gal_bolle 
? 
16:41 
gal_bolle 
? 
16:41 
gal_bolle 
sorry, that was a bit of lag 
16:41 
Igloo 
Also, the same proof that patches have minimal context will work for catches, because both of them form patch universes 
16:42 
Igloo 
I use something similar to your axiom, yes, in that I induct over a commuteRelates relation 
16:43 
gal_bolle 
ok 
16:44 
gal_bolle 
in my opinion the second alternative is better 
16:45 

arjanb joined #darcstheory 
16:45 
gal_bolle 
because it allows one to use different ways to find unique names 
16:45 
* Igloo 
is lost  what's "the second alternative"? 
16:46 
gal_bolle 
maybe we could prove that some cryptographical scheme for name is cryptographically sure 
16:46 
gal_bolle 
stating my proposition as an axiom rather than a lemma 
16:46 
Igloo 
So how are you going to prove that catches have minimal contexts? 
16:47 
gal_bolle 
and having to prove that a global name dealer satisfies my axiom 
16:47 
gal_bolle 
by proving that going from patches to catches preserves my axiom 
16:47 
gal_bolle 
(that having my axioms on patches yields it as a theorem on catches) 
16:47 
gal_bolle 
i don't see how else _you_ are going to do 
16:47 
Igloo 
I think we'll have to agree to disagree :) 
16:48 
gal_bolle 
ok, i'll try to make that clear and in email form, i have to go 
16:48 
Igloo 
I prove that minimal contexts follows from the other axioms, so I don't need to show that catches satisfy your extra axiom 
16:48 
Igloo 
OK 
16:49 
gal_bolle 
yes, but you need an implementation of record that works in the presence of catches 
16:49 
gal_bolle 
see you 
19:56 

tux_rocker joined #darcstheory 
21:25 

DanielC joined #darcstheory 
21:53 

DanielC joined #darcstheory 