Camelia, the Perl 6 bug

IRC log for #darcs-theory, 2009-04-19

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

All times shown according to UTC.

Time Nick Message
05:46 gal_bolle joined #darcs-theory
08:08 tux_rocker joined #darcs-theory
08:13 Igloo gal_bolle: I'm not following you
08:15 gal_bolle on what subject?
08:15 gal_bolle i didn't say anything yet, i must have deep zen mysterious silence abilities
08:15 gal_bolle cool
08:17 Igloo gal_bolle: http://www.hpaste.org/fastc​gi/hpaste.fcgi/view?id=3911
08:19 gal_bolle oh i was just a very big tactic invocation i needed in my goal
08:20 gal_bolle i'm teaching coq what it means to "consider the shortest sequence of commutations between two patch sequences"
08:20 gal_bolle and it's a bit of an hairy proof
08:21 Igloo Ah, right, yes
08:29 arjanb joined #darcs-theory
08:31 kowey joined #darcs-theory
08:46 gal_bolle joined #darcs-theory
08:56 arjanb_ joined #darcs-theory
09:35 gal_bolle http://www.cis.upenn.edu/~plclub/popl0​8-tutorial/code/coqdoc/Metatheory.html
09:36 gal_bolle igloo : you might want to look at this eventually
09:37 Igloo gal_bolle: For NameSets, you mean?
09:37 gal_bolle yup
09:39 Igloo gal_bolle: Is that related to my club post? Do you think it would solve that verbosity?
09:40 gal_bolle i saw taht by musing
09:41 gal_bolle and saw your club post after i had given you the link
09:41 gal_bolle so i don't kno
09:41 gal_bolle w
09:42 Igloo OK
09:42 Igloo Is the verbosity in my post what you were worried would happen?
09:43 Igloo Or is it something else you were worrying about?
09:44 gal_bolle no it's just that i thought it could be useful to have a tactic to discharge all these trivial subgoal you had trouble with
09:44 gal_bolle s/trivial/boring/
09:45 Igloo gal_bolle: So were you worrying that things about NameSets would be unprovable?
09:46 gal_bolle no, just very verbose
09:47 gal_bolle and that they might make some things unprovable if they showed up in types (but this does not seem to have happened)
09:50 kowey joined #darcs-theory
09:52 Igloo OK
09:52 Igloo Hopefully someone on the list will be able to provide some magic, anywya
10:39 Igloo gal_bolle: We may have another miscommunication about finite vs infinit sets, BTW
10:47 gal_bolle ok tell me
10:49 * gal_bolle wishes he had came to utrecht, face to face communication is so much easier
10:50 Igloo I'll talk to someone here who understands this stuff first
10:50 Igloo BTW, hte link above says that set equality is proper = equality: http://www.cis.upenn.edu/~plclub/popl0​8-tutorial/code/coqdoc/FiniteSets.html
10:51 gal_bolle it only works in the ordered case
10:51 gal_bolle i think
10:52 gal_bolle which you can add without problems to the names axioms anyway (real axioms, here)
10:53 gal_bolle saying "to make list processing with them easier, we assume names are ordered"
10:53 gal_bolle since they are Strings anyway, it's a valid assumption
10:56 Igloo OK, I take back what I said about finite/infinite
10:56 Igloo I was misunderstanding "Atoms are structureless objects such that we can always generate one fresh from a finite collection."
10:57 Igloo I don't see why it only works in the ordered case
10:58 Igloo Well, that definition clearly does, but you could write the same thing without requiring ordered values
10:59 kowey joined #darcs-theory
10:59 gal_bolle because if you have no order, how do you decide that {p,q} is [p,q] rather than [q,p]?
10:59 gal_bolle s/is/is represented by/
11:00 gal_bolle so you without order, you're bound to have {p,q} <> {q,p}
11:01 Igloo It doesn't matter whether there's [p,q] or [q,p] in the FSet internals
11:01 Igloo You can still have = relate the FSets themselves
11:02 gal_bolle no, = is really =
11:02 gal_bolle you can't define it
11:02 gal_bolle it's primitive, it's not a notation
11:03 gal_bolle do you want a shocking revelation?
11:03 gal_bolle forall f g x, f x = g x -> f g is not true in coq
11:03 Heffalump you mean f = g?
11:03 gal_bolle (it's a separate axiom form the base axioms)
11:03 Igloo It's defined as:
11:03 Igloo Inductive eq (A:Type) (x:A) : A -> Prop := refl_equal : x = x :>A
11:03 Igloo where "x = y :> A" := (@eq A x y) : type_scope.
11:03 Igloo In http://coq.inria.fr/V8.2/doc/h​tml/stdlib/Coq.Init.Logic.html
11:04 Igloo But that's besides the point; you cna say that Equal FSets are = as an axiom
11:04 gal_bolle Heffalump: yes
11:05 gal_bolle yes, but you cannot have an implementation of this axiom without an order on the elements of the set
11:06 gal_bolle so if you want to use that, you have to add an order on names as an axiom (real axiom)
11:06 gal_bolle which is reasonable
11:06 gal_bolle or use Ensembles
11:06 Igloo Right, I mean a proper axiom axiom
11:06 Igloo But yes, you could also say that Ord Names, and actually prove it
11:07 gal_bolle yup, it does not matter much in the end
11:08 gal_bolle the question is whether you hard-code the implementation of finite sets you use, and we absolutely don't care about that
11:08 gal_bolle so go for whatever's simpler for you
11:44 gal_bolle left #darcs-theory
17:03 gal_bolle joined #darcs-theory
19:25 arjanb joined #darcs-theory

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