Time 
Nick 
Message 
09:56 

kowey joined #darcstheory 
11:01 

gal_bolle joined #darcstheory 
11:22 

gal_bolle joined #darcstheory 
12:23 

gal_bolle joined #darcstheory 
13:05 
Igloo 
gal_bolle: I've been experimenting with Ltac; did you say you have a proof of this lemma, so I can compare? http://hpaste.org/fastcgi/hpaste.fcgi/view?id=2848 
13:31 
gal_bolle 
this lemma does not correspond to my formalisation 
13:32 
gal_bolle 
i have commute as a Prop of 4 patches 
13:32 
gal_bolle 
but i'll look anyway 
13:32 
gal_bolle 
it's in your repo? 
13:32 
gal_bolle 
(i need your axioms) 
13:33 
Igloo 
Everything but those proofs is in my repo, so you can paste those proofs into named_patches.v 
13:33 
gal_bolle 
and names are a function of named patches to names for me 
13:33 
gal_bolle 
which means i don't even need this proof 
13:33 
gal_bolle 
(i have an axiom saying that the name function is preserved by commute) 
13:33 
gal_bolle 
ok 
13:33 
Igloo 
This isn't saying the name is preserved 
13:34 
Igloo 
This is <p, q> <> <q', p'> <=> <q', p'> <> <p, q> 
13:34 
Igloo 
Do you think your formalisation will make things easier? 
13:34 
gal_bolle 
ok, but for me the <> is the same for named as unnamed patch 
13:34 
gal_bolle 
patches 
13:35 
gal_bolle 
in my formalisation, unnamed patches are a particular case of named patches 
13:35 
gal_bolle 
the converse sorry 
13:35 
Igloo 
Hmm, but <p, q> doesn't commute if name p = name q or inv (name q) 
13:35 
gal_bolle 
named patches \subset patches 
13:35 
gal_bolle 
that's not a problem 
13:35 
Igloo 
OK 
13:36 
gal_bolle 
so any theorem of unnamed patches is true for named patches too 
13:36 
gal_bolle 
which means a whole lot of boring proofs don't even need to exist 
13:36 
gal_bolle 
but i think you can prove that in your formalisation 
13:36 
gal_bolle 
forall 
13:37 
Igloo 
The fact that my second lemma has an uglier proof than my first one makes me think that your (more mathematical) formalisation might have uglier proofs than a functionbased formalisation 
13:37 
gal_bolle 
ok, one second 
13:38 
gal_bolle 
it's because your second lemma is in the middle of the road 
13:38 
gal_bolle 
you want: 
13:38 
gal_bolle 
forall p q p' q', Commute p q q' p' > Commute q' p' p q. 
13:39 
gal_bolle 
with Commute: NamedPatch > NamedPatch > NamedPatch > NamedPatch > Prop 
13:40 
gal_bolle 
i'll try to make the proof and see 
13:42 
gal_bolle 
i don't understand your repo atm 
13:42 
Igloo 
How so? 
13:42 
gal_bolle 
that's because i have an exponential conflict pulling from you 
13:43 
gal_bolle 
and darcs is not finished applying 
13:43 
Igloo 
Oh, you probably have local changes to the coq stuff you never sent me? 
13:43 
gal_bolle 
so i'm looking at the wrong version of the files 
13:43 
gal_bolle 
yep 
13:43 
Igloo 
So they'll all conflict with me removing them 
13:43 
gal_bolle 
ok 
13:43 
gal_bolle 
i didn't think about that 
13:43 
gal_bolle 
i thought it would be ok since you had put it into another repo 
13:44 
Igloo 
Oh, I added a link to your stuff on http://projects.haskell.org/camp/ BTW; let me know if you want the text changed or anything 
13:44 
Igloo 
I don't understand that 
13:45 
gal_bolle 
s/repo/file/ sorry 
13:45 
gal_bolle 
where it = your own coq 
13:45 
gal_bolle 
(with all my respect) 
13:46 
Igloo 
Ah, no, the problem is that when I removed your coq file, darcs records a hunk patch that removes all your content and replace it with "" 
13:46 
Igloo 
So that hunk conflicts with any other hunks in your coq file 
13:46 
gal_bolle 
yes, but i forgot it'd do so 
13:46 
gal_bolle 
anyway, now i have a copy 
13:47 
Igloo 
I think that's something we should think about doing better. I think there should be a way to delete that behaves more like mv foo old_files_ignore_me/foo 
13:47 
Igloo 
But I haven't thought about what problems that might cause 
13:53 
gal_bolle 
having commute as a function returning a maybe is bad 
13:53 
Igloo 
Why? 
13:54 
Igloo 
That's what I meant by a functionbased formalisation 
13:55 
Igloo 
It seems to give nice proofs, and is suited to code extraction or tieing proofs to the Haskell code 
13:55 
gal_bolle 
yes, but it's pretty painful to have to case reason on the value of the function and rewriet everytime 
13:55 
gal_bolle 
you want commute : Patch > Patch > Patch > Patch > Prop 
13:56 
gal_bolle 
and commute_dec: forall p q, {not exists q' p', commute p q q' p'}+{q' p' commute p q q' p'} 
13:56 
gal_bolle 
and you extract commute_dec 
13:57 
gal_bolle 
modulo syntax for the type of commute_dec 
14:04 
Igloo 
Hmm, OK, I think that's going to give a much shorter proof 
14:04 
* Igloo 
dithers 
14:08 
gal_bolle 
look at my code 
14:08 
gal_bolle 
it's what i did 
14:08 
gal_bolle 
except i didn't mandate the existence of commute_dec in my axioms 
14:08 
gal_bolle 
(i don't have any reason to yet) 
14:14 
Igloo 
OK, so http://hpaste.org/fastcgi/hpaste.fcgi/view?id=2851 is what I came up with 
14:14 
gal_bolle 
new version pasted 
14:14 
gal_bolle 
for me 
14:14 
gal_bolle 
ok, i paste my version 
14:15 
gal_bolle 
i assure you it removes the need for all these stupid lemmas 
14:16 
gal_bolle 
http://hpaste.org/fastcgi/hpaste.fcgi/view?id=2851#a2853 
14:17 
* Igloo 
likes the separation of named and unnamed patches 
14:17 
Igloo 
The person supplying the type names and the unnamed patches shouldn't need to prove commute_preserves_names 
14:18 
Igloo 
Why do you use unfold rather than compute? 
14:19 
gal_bolle 
what this person will do is take your definition of the named patches and prove commute_preserves_name by compute. Qed. 
14:19 
gal_bolle 
because compute can be overzealous 
14:19 
gal_bolle 
and replace some function by its definition 
14:19 
gal_bolle 
which makes the goal unreadable 
14:20 
gal_bolle 
(i don't think it'd have applied here, though) 
14:22 
gal_bolle 
i tried and it does make things worse 
14:22 
Igloo 
Heh, OK 
14:31 
Igloo 
Even simpler proof, FWIW: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=2848#a2855 
14:32 
gal_bolle 
yes, it's good to use trivial 
14:33 
Igloo 
I feel like I should be able to use UnnamedPatchCommuteSelfInverse more directly, without asserting the result first 
14:35 
gal_bolle 
have you tried generalizing it? 
14:35 
gal_bolle 
generalize (UnnamedPatchCommuteSelfInverse p q p' q' Hunnamedcommute); intro Hq'p'. 
14:35 
gal_bolle 
or maybe destruct (UnnamedPatchCommuteSelfInverse p q p' q' Hunnamedcommute). 
14:36 
gal_bolle 
as Hq'p' 
14:37 
gal_bolle 
if you had Implicit Arguments, destruct (UCSI commute) would be enough 
14:40 
Igloo 
Hmm, will play more with that later 
14:40 
Igloo 
Thanks for your help! 
14:43 
gal_bolle 
you're welcome 
14:43 
gal_bolle 
please have a look at my code 
14:43 
gal_bolle 
tell me what you don't understand 
14:44 
gal_bolle 
i really think my formalisation makes things simpler, as it's more comfortable to manipulate Props than functions 
14:44 
Igloo 
I had a look for this lemma, but couldn't find it. Which I now know is because it doesn't exist :) 
14:44 
gal_bolle 
and not having one more level of constructors is very nice 
14:44 
Igloo 
Yes, you may well be right. I just needed to try things out to get the hang of how it works 
15:05 
gal_bolle 
please repull, i did some cleaning, it should start to be readable now 
15:06 
gal_bolle 
except for shuffle_preserves_closable, which is not ready yet 
17:26 

semka joined #darcstheory 
17:41 

arjanb joined #darcstheory 
18:07 

semka joined #darcstheory 
18:11 

semka joined #darcstheory 