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

All times shown according to UTC.

Time Nick Message
06:48 kowey joined #darcs-theory
08:49 galbolle joined #darcs-theory
09:53 galbolle joined #darcs-theory
09:56 gal_bolle joined #darcs-theory
10:31 kowey joined #darcs-theory
10:48 gal_bolle joined #darcs-theory
11:40 gal_bolle joined #darcs-theory
11:49 gal_bolle i'm not sure your lemma (in foo.v) is provable
11:49 Igloo Is that NamedPatchCommutePreservesCommute?
11:49 gal_bolle yes
11:50 Igloo Why not?
11:50 gal_bolle i think you need an axiom somewhere that says that if the contexts of p and q are NameSet.Equal, and p and q are otherwise equal
11:50 gal_bolle then they are equal
11:50 gal_bolle but maybe i'm worrying too early
11:50 Igloo why?
11:51 gal_bolle because you might end up using different sequences of Set.Add with the same names
11:52 * Igloo can't see a problem
11:52 gal_bolle (if you happen to commute the same patch by two different ways to the same place)
11:52 gal_bolle modulo syntax
11:53 Igloo Those are NameSet.Equal
11:53 Igloo Which is why we need (NameSet.Equal to (NameSet.add n from)) rather than (to = NameSet.add n from)
11:54 gal_bolle yes, but the problem is that you will have unequalities between patches
11:54 gal_bolle you need to define patches modulo equivalence of contexts (with respect to NameSet.Equal)
11:54 gal_bolle that's a no-go for me
11:55 gal_bolle let me just make sure i'm not worrying for nothing
11:55 gal_bolle i might be jumping to conclusions
11:55 gal_bolle thing is, suppose i have up an unnamed patche
11:55 gal_bolle patch
11:55 gal_bolle m and n names
11:56 gal_bolle x a name set
11:57 Igloo OK, I think I see what you're saying
11:57 Igloo But I don't think we'll ever create two patches in the same context without already knowing that they're equal
11:57 gal_bolle then i can't prove they are equal (they are not, they don't even have the same type)
11:58 Igloo We'll use lemmas like named-patch-commute-consistent which tell us that they're equal already
11:58 gal_bolle yes, but i think we won't be able to prove named-patch-commute-consistent because of that
11:58 Igloo We will, because we construct the NamedPatch while proving that lemma
11:58 gal_bolle i'm in that proof, and i see that problem coming at me with the slow but unavoidable pace of a freight train loaded with uraniuw
11:59 gal_bolle uranium
11:59 Igloo So we can build the   (NameSet.Equal to (NameSet.add n from))
11:59 gal_bolle ok, i'll try
12:00 gal_bolle i think named-commute-consistent will be fun
12:01 gal_bolle i think we're in trouble: when i construct such a NameSet.Add, it gets used twice
12:01 gal_bolle hence i can't make sure it will be right for both branches
12:01 gal_bolle let's pray…
12:05 * Igloo didn't follow that
12:16 jnaimard joined #darcs-theory
12:36 jnaimard have you ever used setoid_rewrite?
12:39 jnaimard you need to declare an instance of Setoid for Names under Names.Equal, otherwise it's unusably complex
12:41 jnaimard why do you export the result of Raw and not Make in NameSet?
12:45 Igloo Raw is the first thing I found that worked
12:45 jnaimard ok
12:45 jnaimard well, i'm not sure how to, but you need to have an instance of setoid for namesets
12:46 jnaimard otherwise it's incredibly tedious to prove anything about them
12:46 Igloo What's the advantage of Make?
12:47 jnaimard i don't know
12:48 jnaimard but it's the usage to give the name Make to the functor you want to see people use
12:48 jnaimard and Raw to the one you don't want them to see
12:48 jnaimard to use
12:50 Igloo Yeah, I'm sure you're right, it's just nto clear to me what the difference is
13:39 DanielC joined #darcs-theory
14:02 DanielC joined #darcs-theory
14:15 jnaimard igloo: did you get a mail from me?
14:15 jnaimard i thought i sent it to the list, but i don't see it there
14:19 jnaimard it's ok, of course my asking the question here made it appear
15:25 gal_bolle joined #darcs-theory
15:53 gal_bolle joined #darcs-theory
16:40 arjanb joined #darcs-theory
16:41 gal_bolle left #darcs-theory
18:43 tux_rocker joined #darcs-theory
20:04 tux_rocker is shuffling (in gal_bolle's mail) the same as commutation