Camelia, the Perl 6 bug

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

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

All times shown according to UTC.

Time Nick Message
13:22 gal_bolle joined #darcs-theory
13:27 gal_bolle hi all
13:28 Igloo Yo
13:28 gal_bolle how's C-zar going
13:28 gal_bolle ?
13:29 Igloo Looks like I'll have to put it on ice: "I'll try to make a fix before the summer."
13:29 gal_bolle I think I now see how to phrase my doubts about it more clearly
13:30 gal_bolle imagine we're in 1990
13:30 Igloo I might spend some time reading up on coqdoc, sections, modules, etc, and see how C-zar or Ltac should be glued together and integrated into the latex
13:30 gal_bolle would you rather program darcs/camp in C or in '90-haskell, without even the IO monad
13:31 gal_bolle where C=L-tac and prehistoric haskell=C-zar
13:31 Igloo I think the problem isn't the immaturity of C-zar, so much as having to wait 6 months for a fix each time I run into a problem
13:31 gal_bolle it's not immaturity as in being ill-defined or unstable
13:32 gal_bolle it's just that it doesn't have enough features (yet?) to allow one to work correctly
13:32 Igloo I think it has the features, but they don't work correctly
13:32 Igloo I currently have 3 problems:
13:32 gal_bolle the fact that induction in C-zar is much less powerful than in Ltac is really crippling
13:32 Igloo "consider foo from bar" doesn't add the knowledge that "bar = MkBar foo"
13:33 Igloo "per cases on foo. suppose it is X" doesn't add the knowledge that "foo = X"
13:33 Igloo And the knowledge "a = b" doesn't allow C-zar to realise that "match a with ... = match b with ..."
13:34 Igloo AFAICS, frmo my naive user standpoint, none of these should be hard to fix
13:34 gal_bolle for the two first ones, you can try reconsidering P x as (forall y, y = x -> P y) beforehand
13:34 gal_bolle the third one is actually a little deeper
13:35 gal_bolle it's a separate axiom in code
13:35 Igloo Pierre sent a workaround for the third oen
13:35 gal_bolle coq
13:35 Igloo You probably saw it on the list?
13:35 gal_bolle not yet
13:35 Igloo http://pauillac.inria.fr/piper​mail/coq-club/2009/004638.html
13:36 Igloo Basically you just "define C x as (match x with ...)" and use that definition instead
13:36 Igloo Which of course adds a few more lines to the proof
13:38 Igloo I didn't follow your reconsider suggestion
13:38 Igloo Currently I have "consider u:U from n."
13:38 gal_bolle if you have to prove P u by cases on u
13:38 Igloo where "n : N" and "Inductive N : Set := MkN : U -> N."
13:38 gal_bolle then say "suffices to have (forall y:N, y = u -> P y)"
13:39 gal_bolle (i don't know the exact syntax in C-zar
13:39 Igloo Ah, OK, so you're talking about the second problem, I think
13:39 gal_bolle yes
13:39 gal_bolle but the same idea would work on the first too i think
13:39 Igloo I don't see how
13:39 gal_bolle i'm just translating what one had to do before case_eq existed
13:40 gal_bolle oh right
13:40 gal_bolle it's a bit more involved
13:40 gal_bolle but it's the same idea
13:40 Igloo http://pauillac.inria.fr/piper​mail/coq-club/2009/004636.html is the script, FWIW
13:40 gal_bolle you need to have two instances of u, one of which is going to be deconstructed and the other not
13:41 Igloo I don't see what I can reconsider n as, though
13:41 Igloo (it's the line before the first "THIS IS NOT ACCEPTED")
13:42 gal_bolle ok, i step through your code
13:42 gal_bolle 5 minutes
13:42 Igloo OK, thanks!
13:44 gal_bolle what does the from … part mean in consider u from n ?
13:44 gal_bolle oh ok, I misread n as N
13:44 gal_bolle sorry
13:46 Igloo It just destructs the n, and names its components, AIUI
13:50 gal_bolle yes
13:50 gal_bolle i can get to your second THIS IS NOT ACCEPTED
13:50 Igloo But doesn't remember that it has done so  :-)
13:50 gal_bolle but i don't know if i have sufficient hypothesis anymore
13:50 Igloo You mean you have fixed the first one?
13:51 gal_bolle i'll see if my idea works, and if so i'll explain it to you
13:51 gal_bolle i'm not sure
13:51 gal_bolle i can get coq to step over it
13:51 Igloo Can you paste what you have?
13:51 gal_bolle but i'm not sure my goal is solvable
13:51 gal_bolle sure
13:52 gal_bolle http://hpaste.org/fastcgi/hp​aste.fcgi/view?id=2638#a2638
13:52 gal_bolle here you are
13:53 gal_bolle the line     then (f u = None).
13:54 gal_bolle is useless
13:54 gal_bolle since you overwrite it with g … = g …
13:55 gal_bolle and the goal is not solvable with my modification
13:56 Igloo Right, you have no evidence that there is an n'' such that "n'' = MkN u"
13:56 Igloo (why can't I copy from the top right window in coqide properly? Grr)
13:56 Igloo Oh, wait, you don't need to show that there is such an n''
13:57 Igloo So you can then say "let n'' be such that (n'' = MkN u)."
13:58 gal_bolle i think i'm on the right track
14:00 Igloo OK, everything but the "thus thesis by H1, H4" goes green for me now
14:02 gal_bolle can you paste your code?
14:02 gal_bolle i'm stuck before that
14:02 Igloo Hmm, I think we need to do a similar trick with n'
14:02 gal_bolle (at your second "THIS IS NOT ACCEPTED")
14:02 gal_bolle yes, i did that
14:03 Igloo http://hpaste.org/fastcgi/hp​aste.fcgi/view?id=2638#a2639
14:03 gal_bolle and i can get to  your second problem
14:04 Igloo Ah, I think I see how
14:05 Igloo Oh, no, I don't
14:06 Igloo So we have    g n = Some _
14:07 Igloo g n'' = None
14:08 Igloo And no way to connect the two, AFAICS
14:09 gal_bolle yes, seems a bit desperate
14:12 gal_bolle n : N
14:12 gal_bolle n' : N
14:12 gal_bolle H1 : g n = Some n'
14:12 gal_bolle n'' : N
14:12 gal_bolle H2 : n'' = n
14:12 gal_bolle u : U
14:12 gal_bolle Hun : MkN u = n
14:13 gal_bolle ============================
14:13 gal_bolle thesis :=
14:13 gal_bolle g n' = Some (MkN u)
14:13 gal_bolle this smells good
14:13 gal_bolle look at Hun
14:13 Igloo Ah, yes. How'd you get there?
14:14 gal_bolle you have to deconstruct n'' rather than n
14:15 gal_bolle http://hpaste.org/fastcgi/hp​aste.fcgi/view?id=2638#a2642
14:17 Igloo Hmm, I get "Error: No product even after head-reduction."
14:17 Igloo On the assume Hun line
14:18 gal_bolle yes
14:18 gal_bolle now that i reloaded it's what i get
14:18 gal_bolle hum
14:18 Igloo Argh!  :-)
14:20 gal_bolle ok
14:20 gal_bolle proof-general + C-zar seems a bit inconsistent
14:20 gal_bolle but i'm almost there
14:20 gal_bolle it's ugly
14:20 gal_bolle far uglier than the equivalent L-tac in my opinion
14:20 Igloo "inconsistent" isn't a nice word to throw around when talking about theorem provers  :-)
14:20 Igloo Oh, yes, but that's because Ltac isn't buggy
14:21 gal_bolle http://hpaste.org/fastcgi/hp​aste.fcgi/view?id=2638#a2643
14:22 gal_bolle ok
14:23 gal_bolle just the other case is not done
14:23 gal_bolle so your problem is solved
14:24 gal_bolle btw, it would really be three lines in L-tac
14:24 Igloo Woo!
14:24 Igloo Thanks!
14:24 gal_bolle and it's typically the kind of things where you don't want to see the proof
14:24 Igloo So what did you change? Just the order of the equality?
14:25 gal_bolle i repeated it twice
14:25 Igloo Yes, but I need to know how to do these things for cases where I do want to see the proof
14:25 Igloo Ah, I see
14:25 Igloo No, I don't see
14:25 Igloo What did you repeat twice?
14:26 gal_bolle i think that in these cases, the sheer size of the C-zar proof is going to be a bigger obstacle than L-tac's obscurity
14:26 gal_bolle here i had to obfuscate the proof and it was a simple case
14:26 gal_bolle which defeats the purpose of C-zar
14:26 gal_bolle i needed one exemplary in the hypotheses
14:26 gal_bolle and one in the goal
14:27 gal_bolle so that when i deconstruct n, only one gets touched
14:27 gal_bolle i use the n'' in the goal as a bridge between the n in the hypothesis and the one in the goal
14:27 gal_bolle it needs two pillars: one in the hypothesis and one in the goal
14:28 gal_bolle maybe we can be smarter and do away with the n''
14:28 gal_bolle yes
14:29 gal_bolle you don't need that dance
14:29 gal_bolle just consider u before you assume H1
14:30 gal_bolle and n' too before you assume H1
14:30 Igloo gal_bolle: In a bug-free C-zar I would hope to be able to prove it with http://hpaste.org/fastcgi/hp​aste.fcgi/view?id=2638#a2645
14:31 Igloo And without the NoneOrSome lemma
14:32 gal_bolle have you tried considering before you assume in that proof too?
14:32 * Igloo fails to understand the difference between
14:32 Igloo assume Hun : (MkN u = n).
14:32 Igloo assume Hun : (MkN u = n'').
14:34 Igloo Just moving the assume later doesn't work: "Error: Incorrect change of the type of H1."
14:36 gal_bolle ok, i paste what i have
14:37 gal_bolle it's pasted
14:38 gal_bolle igloo: do you have n = n'' in the context?
14:39 Igloo gal_bolle: In what context?
14:40 Igloo Oh, in the assume Hun thing?
14:40 gal_bolle YES
14:40 gal_bolle sorry, yes
14:41 Igloo This is your http://hpaste.org/fastcgi/hp​aste.fcgi/view?id=2638#a2643 - I have "H2 : n'' = n"
14:41 Igloo Oh, I see why
14:41 Igloo It's because the thesis is   MkN u = n -> ...
14:42 gal_bolle http://hpaste.org/fastcgi/hp​aste.fcgi/view?id=2638#a2647
14:42 gal_bolle you don't need n'' at all
14:42 gal_bolle nor n3
14:43 gal_bolle i think the end can be made more elegant
14:43 gal_bolle but i don't know how to say «by contradiction» in C-zar
14:43 gal_bolle and that we're doing by hand what inversion does automatically
14:43 Igloo "by H1, H2" where H1 and H2 are contradictory certainly works
14:44 gal_bolle ok
14:47 Igloo So this works:
14:47 Igloo =~ None.
14:47 Igloo then H2 : (g (MkN u) = None).
14:47 Igloo thus thesis by H1, H2.
14:48 gal_bolle but not giving a name to H2 and doing thus thesis by H1 does not work?
14:48 gal_bolle strange
14:49 Igloo Ah, I see, so doing the consider's earlier means they're still in the thesis, so get altered
14:50 Igloo Oh, you don't need to mention H2 if you say "then thesis"
14:50 * Igloo doesn't really understand the difference between then, thus, hence, etc
14:51 gal_bolle neither do I
14:51 Igloo This is looking much nicer now, thanks!
14:52 gal_bolle you should give hypothesis more explicit names btw
14:53 Igloo Makes sense. I assume starting with H is just a convention?
14:53 * Igloo tends to be lazy when naming things, as I keep having to change them so often  :-)
14:58 gal_bolle yes, it's only a convention
15:01 Igloo Oh, "then thesis by H1" doesn't actually show thesis, you need to use "thus" for that
15:50 Igloo gal_bolle: If you're interested, here's a complete proof: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=2651
15:50 Igloo Haven't looked to see if it can be simplified further yet
15:55 gal_bolle my Ltac version is 19 lines long and does not need NoneOrSome
15:55 gal_bolle and i didn't even try to optimize it
15:55 * Igloo wonders if n' should actually be existentially quantified
15:57 gal_bolle the two versions are equivalent
15:57 gal_bolle because of the g n = Some n' constraint
16:00 Igloo Right, but I think the proof might be shorter
16:00 Igloo I think my (u' = u'') proof would probably disappear
16:07 Igloo Oh, actually, it's fiddly with an exists, isn't it, because things don't scope how you want
16:07 Igloo forall n, (exists n' . g n = Some n') -> (g n' = Some n), but n' isn't in scope there
18:49 arjanb joined #darcs-theory
19:15 gal_bolle joined #darcs-theory
20:28 Igloo gal_bolle: Do your sequences still go from one context to another, BTW?
20:28 Igloo gal_bolle: I was wondering if actually they should have the set of names they add to the context instead
20:28 Igloo Oh, no, because we also need to know what context they apply in. Ignore that
20:30 gal_bolle anyway my contexts are just an abstract type
20:30 gal_bolle so you can put whatever you want inside
20:30 Igloo *nod*
20:31 gal_bolle you might want to quotient by some equivalence at each step, but that would be overkill
20:39 * Heffalump wonders if gal_bolle will be hackathoning
20:42 gal_bolle no i wont
20:43 gal_bolle when is the hackathon?
20:43 gal_bolle it's later than i thought
20:43 gal_bolle so maybe i will, but then by irc

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