Time 
Nick 
Message 
05:46 

gal_bolle joined #darcstheory 
08:08 

tux_rocker joined #darcstheory 
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/fastcgi/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 #darcstheory 
08:31 

kowey joined #darcstheory 
08:46 

gal_bolle joined #darcstheory 
08:56 

arjanb_ joined #darcstheory 
09:35 
gal_bolle 
http://www.cis.upenn.edu/~plclub/popl08tutorial/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 #darcstheory 
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/popl08tutorial/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 #darcstheory 
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/html/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 hardcode 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 #darcstheory 
17:03 

gal_bolle joined #darcstheory 
19:25 

arjanb joined #darcstheory 