Time 
Nick 
Message 
09:30 

gal_bolle joined #darcstheory 
10:13 
Igloo 
gal_bolle: Woo! (see camp list mail) 
10:18 
gal_bolle 
congratulations 
10:18 
gal_bolle 
my constructive proof is not yet ready, but it's coming 
10:18 
gal_bolle 
i may have one painful lemma to do though 
10:19 
gal_bolle 
your proof is going to be smaller, but i won't have to import Classical logic 
10:20 
Igloo 
I'm pretty sure I can get rid of classical logic, by making commutability of unnamed patches decidable and then proving decidability of named patches 
10:21 
gal_bolle 
it's possible 
10:21 
Igloo 
Will my proof still be smaller when I've provied the other direction too? 
10:22 
gal_bolle 
i don't know 
10:22 
* Igloo 
isn't actually sure how much stuff ends up getting duplicated 
10:22 
gal_bolle 
the thing is that i'll have two lemmas with ridiculously big proofs 
10:22 
gal_bolle 
but they are of general use 
10:22 
Igloo 
Oh, I ended up using your combined axioms, BTW 
10:22 
gal_bolle 
aren't they nice? 
10:23 
Igloo 
Yup; I think they were even essential in one case, but I could be wrong 
10:23 
gal_bolle 
the geometric interpretation is really helpful to me 
10:23 
gal_bolle 
i have one such case too 
10:23 
Igloo 
I think I needed the knowledge that the two results gave you /the same/ patches, not just separately existing patches 
10:24 
gal_bolle 
yup 
10:24 
Igloo 
It's possible that was provable anyway, but combining the lemmas was easiest 
10:24 
gal_bolle 
exactly 
10:24 
Igloo 
Hopefully they won't be too hard to prove for primitive patches 
10:25 
gal_bolle 
so my fat lemma is if start p tail commutes to start' p' tail' (with name(p) = name(p') ), then in fact one can start by sorting start into start_to_start +> start_to_tail 
10:25 
gal_bolle 
then tail into tail_to_start +> tail_to_tail 
10:25 
gal_bolle 
then commute these guys where they belong 
10:25 
Igloo 
Actually, I don't see why they should be. For the prim patch proofs we'll know what the answer is, so we can just (exists _) it and then split 
10:25 
gal_bolle 
yes 
10:26 
gal_bolle 
this is the "shortest sequence of commutes" argument 
10:26 
Igloo 
start_to_start is the intersectino of start and start'? 
10:26 
gal_bolle 
yes 
10:27 
gal_bolle 
modulo shuffling 
10:27 
Igloo 
Have you proven that yet? 
10:27 
gal_bolle 
yes 
10:27 
gal_bolle 
now i need to prove the same thing 
10:27 
gal_bolle 
but with sequences where i track two patches 
10:28 
Igloo 
Interesting. It sounds harder than "minimal context exists", which I was going to use this lemma to prove 
10:28 
gal_bolle 
i think you can extract an algorithm to make an optimal sequence of commutes from one sequence to another using that 
10:28 
gal_bolle 
something like quicksort 
10:28 
Igloo 
Oh, with just 1 patch it's roughly the same as "minimal context exists" 
10:28 
gal_bolle 
is it? 
10:29 
gal_bolle 
maybe i just got carried away 
10:29 
gal_bolle 
my starting intuition was that we should prove minimal context exists from names 
10:29 
Igloo 
Well, I don't know if you can make the leap in coq 
10:29 
gal_bolle 
then everytthing from minimal context exists 
10:30 
gal_bolle 
i had even made minimal context exists an axiom at some point (when i didn't want to deal with names and finite sets) 
10:30 
gal_bolle 
then i decided i should start with something weaker 
10:30 
gal_bolle 
(* Given two sequences ending with two patches with the same name n, 
10:30 
gal_bolle 
we can commute them into a common part ending with a patch with name 
10:30 
gal_bolle 
n, and the rest of each. That is, we can get back to the context in 
10:30 
gal_bolle 
which a patch named n was first recorded, except for patches which 
10:30 
gal_bolle 
were unpulled in either s or s'. Is this too strong an assumption? *) 
10:30 
gal_bolle 
Hypothesis name_original_context : forall a b c d e 
10:31 
gal_bolle 
(s: FL Patch a b) 
10:31 
gal_bolle 
(s': FL Patch a c) 
10:31 
gal_bolle 
(p: Patch b d) 
10:31 
gal_bolle 
(p': Patch c e), 
10:31 
gal_bolle 
patchname p = patchname p' > 
10:31 
gal_bolle 
exists f: State, exists g:State, 
10:31 
gal_bolle 
exists ctx: FL Patch a f, exists p'' : Patch f g, 
10:31 
gal_bolle 
exists rest : FL Patch g d, exists rest' : FL Patch g e, 
10:31 
gal_bolle 
patchname p'' = patchname p /\ 
10:31 
gal_bolle 
(s +> p :> NilFL) =~= (ctx +> p'' :> rest) /\ 
10:31 
gal_bolle 
(s' +> p' :> NilFL) =~= (ctx +> p'' :> rest'). 
10:31 
Igloo 
Ah, Hypothesis = Axiom, right? 
10:31 
gal_bolle 
yes 
10:32 
Igloo 
OK 
10:32 
Igloo 
so that would still need to be proven 
11:10 
gal_bolle 
yes, but i thought it summed up what names give 
11:11 
Igloo 
It'll definitely need to be proven for catches 
11:16 
gal_bolle 
so my plan is/was to use that hypothesis to isolate names from the rest of the proofs 
11:16 
gal_bolle 
maybe it's worth going that way for catches 
11:17 
gal_bolle 
the dic repo is now up to date, if you want to take a look 
11:17 
gal_bolle 
but it's not very readable i'm afraid 
12:34 

jnaimard joined #darcstheory 
12:39 

jnaimard joined #darcstheory 
13:37 

gal_bolle joined #darcstheory 
15:03 
gal_bolle 
Module Import Shmo := Shmorf.Shmo. 
15:03 
gal_bolle 
Module Import Shu := Shmo.Shu. 
15:03 
gal_bolle 
sorry 
15:05 
Igloo 
Did you have Thundercats in France? 
15:06 
gal_bolle 
maybe 
15:07 
gal_bolle 
let me wikipedia out the french name 
15:07 
Igloo 
Sounds like module names Snarf would use, anyway :) 
15:07 
gal_bolle 
cosmocats they were 
15:07 
gal_bolle 
but i didn't watch it 
15:08 
Igloo 
Oh well, not important :) 
15:12 
gal_bolle 
i'm impressed by the wikipedia page on thundercats anyway 
15:12 
Igloo 
In what way? 
15:13 
gal_bolle 
scholarness 
15:13 
Igloo 
Ah :) 
15:41 
gal_bolle 
The term "middle_left" has type "FL Patch c x" 
15:41 
gal_bolle 
while it is expected to have type 
15:41 
gal_bolle 
"Shmor.Shmo.Shu.Seq.SequenceAsPatch.Patch d ?14304". 
15:41 
gal_bolle 
i love these error messages 
15:43 
Igloo 
:) 
15:43 
Igloo 
Would Shmor.Shmo.Shu make more sense if I spoke French? 
15:44 
gal_bolle 
nope 
15:44 
gal_bolle 
maybe in hebrew 
15:44 
gal_bolle 
or yiddish 
15:44 
gal_bolle 
sounds a bit like it 
15:45 
gal_bolle 
Shmor is "Shuffle mark one rectify" 
15:45 
gal_bolle 
Shmo is "Shuffle mark one" 
15:45 
gal_bolle 
and Shu is shuffle 
15:46 
Igloo 
Aha 
15:46 
Igloo 
I went the other way, with NamesAsLongAsYourScreenIsWide :) 
15:46 
* Igloo 
doesn't have a feel for what is best yet 
15:46 
gal_bolle 
yes, but these name don't appear explicitely in my code 
15:47 
gal_bolle 
it's modules which are imported 
15:47 
gal_bolle 
so i don't care for their names 
15:47 
Igloo 
Ah, OK 
15:47 
gal_bolle 
the other names are sometimes baroque but as explicit as possible 
15:47 
Igloo 
I was wondering if patch sequences could be moved inside PatchUniverse, so we only need one sequence type 
15:47 
gal_bolle 
though i sometimes would like to say wiggle_the_patch_down 
15:47 
Igloo 
Then it could just use unqualified Cons and Nil 
15:47 
gal_bolle 
or some such 
15:48 
Igloo 
*nod* 
15:48 
gal_bolle 
i'm not sure what you mean 
15:48 
Igloo 
Well, currently I have 
15:48 
gal_bolle 
my patch sequence types (and all the theorems about it) are parametric in the patches 
15:48 
Igloo 
namedPatchSequence = NilNamedPatchSequence  ConsNamedPatchSequence x xs 
15:49 
gal_bolle 
so i only have one cons and one nil 
15:49 
Igloo 
Right, that's what I mean 
15:49 
Igloo 
The only thing is, unnamed patches are different as they don't have sets of names as parameters 
15:49 
Igloo 
But I'm not sure that we actually use unnamed patch sequences any more 
15:50 
gal_bolle 
my approach is to give them paramaters anyway 
15:50 
gal_bolle 
but not say what the parameters are 
15:50 
gal_bolle 
then later we can say parameter_type = unit 
15:50 
gal_bolle 
and we're done 
15:50 
Igloo 
We used to use them for the "p commutes past (q r)" pemmas, but now the lemmas explicitly commute past q and r separately anyway 
15:50 
gal_bolle 
yes 
15:51 
gal_bolle 
(this suppose that the sequence treat the parameters as opaque, but it's good for sanity anyway) 
15:51 
Igloo 
I'm not sure if generalising the type will work for my proofs 
15:51 
Igloo 
As the sets are actually used in the proof 
15:51 
Igloo 
Maybe it would be fine anyway 
15:52 
Igloo 
No, I think it must be fine. There are no properties about the sets in teh actual sequence, only that the two midpoints match 
15:53 
gal_bolle 
in the worst case, i think there's a way in coq's module system to have sequence use a type opaquely, then use sequence with the constraint that this type is in fact some transparent type we know 
15:53 
gal_bolle 
but it shouldn't be necessary 
17:17 

arjanb joined #darcstheory 