Time 
Nick 
Message 
08:34 

gal_bolle joined #darcstheory 
08:34 
gal_bolle 
hi 
09:40 
Igloo 
Hey 
09:42 
gal_bolle 
seen my mail? 
09:43 
Igloo 
Yup. This one looks like it doesn't have scary things like <q,r> <~> <q'',r''> :) 
09:43 
gal_bolle 
well, they are properly enclosed in coq code 
09:43 
gal_bolle 
but they're still there 
09:43 
Igloo 
I mean the variable names 
09:44 
gal_bolle 
ok, i 
09:44 
gal_bolle 
i'm not sure what i've made simpler on this front 
09:45 
Igloo 
You don't see why <<q,r>> <~> <<r'',q''>> is easier to understand? 
09:45 
gal_bolle 
no 
09:45 
Igloo 
q and r'' are "the same patch" in the first example 
09:45 
gal_bolle 
oh yes 
09:46 
gal_bolle 
that was an embarassing typo 
09:46 
Igloo 
I wasn't sure what you actually meant, so got confused :) 
09:46 
gal_bolle 
coq has a tendency to autocorrect me with these things than 
09:46 
gal_bolle 
ks to using states everywhere 
09:47 
gal_bolle 
so i tend to be sloppy when it's not there to check 
09:47 
Igloo 
Grr, why do people keep spamming camp ticket #13? 
09:49 
* Igloo 
removes anonymous's ticket create/modify permissions. It's not like camp has any users anyway 
09:59 
gal_bolle 
by the way, do you know about stuff like 2categories? 
10:00 
Igloo 
Doesn't ring a bell 
10:00 
gal_bolle 
i think there might be a way to state patch theory within a known algebraic framework 
10:07 
Igloo 
That would certainly be nice, especially if it gave us theorems for free 
11:20 

tux_rocker joined #darcstheory 
12:17 

gal_bolle joined #darcstheory 
12:23 
Igloo 
gal_bolle: I have a problem 
12:24 
Igloo 
Ignoring the fact that http://hpaste.org/fastcgi/hpaste.fcgi/view?id=4244 can't be written as is, it's also not true 
12:24 
Igloo 
All I can prove is that (NameSet.Equal mid' mid'') 
12:27 
gal_bolle 
that's normal 
12:27 
gal_bolle 
that's all what holds 
12:28 
gal_bolle 
if you have built mid' and mid'' using different set operations they're not equal 
12:28 
gal_bolle 
one moment 
12:28 
gal_bolle 
did you add the assumptions that names were ordered or not? 
12:29 
gal_bolle 
if you didn't, then one can build a counterexample of your goal by building mid' and mid'' in such a way that they are not =, only NameSet.Equal 
12:30 
gal_bolle 
otherwise, you have the assumption that a `Set.Equal` b > a = b somewhere in one of the FSetSomethings modules 
12:30 
gal_bolle 
FsetFacts, I thin 
12:30 
gal_bolle 
k 
12:31 
gal_bolle 
damened typematrix keyboard, my return key is where my 'k' key used to be 
12:31 
Igloo 
:) 
12:32 
* gal_bolle 
has a southernfrench accent on irc: "damened" 
12:32 
gal_bolle 
cong 
12:34 
Igloo 
I don't think FSetFacts does it, unless Add Relation t Equal ... as EqualSetoid does it somehow 
12:34 
gal_bolle 
nope 
12:34 
gal_bolle 
this would allow you to use setoid_rewrite i believe 
12:34 
gal_bolle 
do you use a FSet or a FWeakSet? 
12:35 
Igloo 
I use FSetWeakList 
12:35 
gal_bolle 
ok, then your theorem only holds with NameSet.Equal, not with = 
12:36 
gal_bolle 
= is real equality, you can't overload it 
12:36 
gal_bolle 
and extensionality does not hold for FSetWeakLists 
12:37 
gal_bolle 
ie, you can have two sets with the same elements whose representations are not the same 
12:37 
Igloo 
Maybe I should just make names ordered. Mutter grumble abstraction. 
12:37 
gal_bolle 
if you want to mumble grumble abstraction, then just make NameSet abstract as a whole 
12:37 
gal_bolle 
make NamedPatches a functor 
12:38 
gal_bolle 
and NameSet an argument of this functor 
12:38 
Igloo 
Ah, you mean let it take any nonweak FSet? 
12:39 
gal_bolle 
and in the type of that argument, have module type NameSet: [some stuff] … Axiom extensional: forall a b, a has the same elements as b > a = b 
12:39 
gal_bolle 
yes 
12:39 
Igloo 
Maybe I should use an ordered set for now, and do clever stuff like that later 
12:39 
Igloo 
Thanks for your advice! 
12:39 
gal_bolle 
yup 
12:39 
gal_bolle 
having an order on names is really an innocent axiom on the other hand 
12:40 
Igloo 
But it's the /principle/ of the thing :) 
12:43 
Igloo 
Are you sure that one of the FSet modules defines Equal => =? I can't find it 
12:44 
Igloo 
s/defines/proves/ 
12:45 
gal_bolle 
maybe it's somewhere else 
12:45 
gal_bolle 
i think i saw it somewhere 
12:45 
Igloo 
I think it was in that metatheory thing you showed me 
12:46 
gal_bolle 
ah yes, probably 
12:47 
Igloo 
Yes, http://www.cis.upenn.edu/~plclub/popl08tutorial/code/coqdoc/FiniteSets.html has it 
12:48 
Igloo 
But that's essentially the same as making it an axiom, isn't it? 
12:49 
gal_bolle 
yes 
12:49 
gal_bolle 
i think so 
12:50 
gal_bolle 
but why aren't you happy with an Equal in the conclusion of that theorem? 
12:50 
gal_bolle 
oh because then those NameSets creep into the types 
12:50 
Igloo 
Because it doesn't allow me to show that q' = q'' 
12:51 
gal_bolle 
yes, so add the axiom 
12:51 
Igloo 
(admittedly that's not technically true, but it morally is :) ) 
12:51 
Igloo 
*nod*, OK, thanks again 
13:22 

tux_rocker joined #darcstheory 
13:48 

tux_rocker_ joined #darcstheory 
14:36 

gal_bolle joined #darcstheory 
16:49 

arjanb joined #darcstheory 
19:26 

tux_rocker joined #darcstheory 
20:51 

tux_rocker joined #darcstheory 