Camelia, the Perl 6 bug

IRC log for #darcs-theory, 2009-03-25

| Channels | #darcs-theory index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
09:56 kowey joined #darcs-theory
11:01 gal_bolle joined #darcs-theory
11:22 gal_bolle joined #darcs-theory
12:23 gal_bolle joined #darcs-theory
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 function-based 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 function-based 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/hp​aste.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 over-zealous
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/hp​aste.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 #darcs-theory
17:41 arjanb joined #darcs-theory
18:07 semka joined #darcs-theory
18:11 semka joined #darcs-theory

| Channels | #darcs-theory index | Today | | Search | Google Search | Plain-Text | summary