Time 
Nick 
Message 
13:22 

gal_bolle joined #darcstheory 
13:27 
gal_bolle 
hi all 
13:28 
Igloo 
Yo 
13:28 
gal_bolle 
how's Czar 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 Czar 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 '90haskell, without even the IO monad 
13:31 
gal_bolle 
where C=Ltac and prehistoric haskell=Czar 
13:31 
Igloo 
I think the problem isn't the immaturity of Czar, 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 illdefined 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 Czar 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 Czar 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/pipermail/coqclub/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 Czar 
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/pipermail/coqclub/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/hpaste.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/hpaste.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/hpaste.fcgi/view?id=2638#a2642 
14:17 
Igloo 
Hmm, I get "Error: No product even after headreduction." 
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 
proofgeneral + Czar 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 Ltac 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/hpaste.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 Ltac 
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 Czar proof is going to be a bigger obstacle than Ltac'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 Czar 
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 bugfree Czar I would hope to be able to prove it with http://hpaste.org/fastcgi/hpaste.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/hpaste.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/hpaste.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 Czar 
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 #darcstheory 
19:15 

gal_bolle joined #darcstheory 
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 