Time 
Nick 
Message 
02:48 

ilbot3 joined #isabelle 
02:48 

Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html  Now with logging: http://irclog.perlgeek.de/isabelle/ 
06:01 

fracting joined #isabelle 
06:55 
pruvisto 
JCaesar: a locale sounds cleaner 
06:55 
pruvisto 
providing something like a function "fresh :: 'v set => 'v" 
06:56 
pruvisto 
working with the infinity of the type and Hilbert choice (I presume that's what you were going to do) has its drawbacks 
06:56 
pruvisto 
for one, it'll be tricky to get executable code from this 
06:57 
pruvisto 
the "proper" way to do something like this would be to be completely nondeterministic about the choice of a fresh variable, but that would either require very modular theorems or a nondeterministic monad 
06:57 
pruvisto 
but I'm not sure it's worth the effort 
07:26 
larsrh 
I have a "fresh" monad that's executable 
10:29 
AtnNn 
Is there a better way to prove `f (A x) ==> B x' by induction than this? 
10:30 
AtnNn 
`{ fix a x have "f a ==> a = A x ==> B x" proof (induction f.induct) ... qed } then show "f (A x) ==> B x" by simp' 
10:31 
pruvisto 
AtnNn: I find this a bit confusing 
10:31 
pruvisto 
do you have a more concrete example? 
10:32 
AtnNn 
pruvisto: yes, thanks. Let me upload it somehwere 
10:32 
pruvisto 
Ah I think I'm starting to understand it 
10:32 
pruvisto 
You can do have "f (A x) ==> B x" proof (induction "A x" arbitrary: x rule: f.induct) 
10:33 
pruvisto 
I think the proof obligations in the induction will look the same as with what you did 
10:33 
pruvisto 
but it's easier to give stylistic advice with a concrete example, I suppose 
10:34 
AtnNn 
pruvisto: I'll try that 
10:34 
AtnNn 
https://gist.github.com/AtnNn/dc6def74ab66c2d793077894d7b951e1#filechatper4thyL222 
10:39 
AtnNn 
Thanks, your tip seems to work for me by doing `proof (induction "x @ y" arbitrary: x y rule: S.induct)' 
10:45 
AtnNn 
Another question: on line 319 of that file, I want to assume that "n = 0" (because of the corresponding definition on line 178) but Isabelle doesn't seem to agree with me. What am I doing wrong? 
10:50 
pruvisto 
I don't get why it should be 0 
10:50 
pruvisto 
even if it were, you'd have to prove that (probably by induction using balanced.induct) 
10:50 
pruvisto 
but if I write down 
10:50 
pruvisto 
lemma assumes "balanced n (b # xs)" shows "n = 0" 
10:50 
pruvisto 
then QuickCheck immediately finds a counterexample: 
10:51 
pruvisto 
n = 1, xs = [] 
10:51 
pruvisto 
i.e. "balanced 1 [b]" holds 
11:07 
AtnNn 
what confuses me is that the assumption that isabelle gives me (balanced n (b # xs)) corresponds to "balanced 0 (b # _) = False" 
11:08 
pruvisto 
but that is the last equation! 
11:09 
pruvisto 
that will only match if none of the preceding equations match 
11:09 
pruvisto 
"fun" without extra arguments works in "sequential mode" 
11:09 
pruvisto 
i.e. if several equations match, the first one that matches will be taken 
11:09 
pruvisto 
just like e.g. in Haskell and pretty much every other functional programming language I know of 
11:10 
pruvisto 
if you look at the rules balanced.simps, you can see that the "fun" command did a few case splits to accommodate this 
11:12 
AtnNn 
ok. so in this case n is always 0 if it gets to the last case. how can i use that information when doing induction proofs? 
11:13 
AtnNn 
in haskell, 'f 0' 'f ~0' and 'f _' are all different 
11:14 
AtnNn 
maybe that's why i'm confused 
11:40 
JCaesar 
Uh, is there some other way than [[simp_trace]] to debug the simplifier? I'm in a spot where apply simp loops, and the trace is just 20 linesâ¦ 
11:44 
JCaesar 
Hm, it says simp_trace_depth_limit exceededâ¦ 
11:46 
JCaesar 
Ah, that can just be declared, too. nvm. 
12:24 

silver joined #isabelle 
12:49 
pruvisto 
AtnNn: I'm not sure what you mean 
15:55 
AtnNn 
pruvisto: Isabelle still doesn't give me "n = 0" if I switch from fun to function and change the order of the equations (none of which overlap) 
16:00 
pruvisto 
AtnNn: please show the actual code 
16:00 
pruvisto 
you may have to do a case distinction 
16:00 
pruvisto 
(which should be trivial if the situation is as you say) 
16:00 
pruvisto 
If there is no overlap, there should also be no reason to use "function" instead of "fun" 
16:06 
chindy 
I am trying to define a set where {x \in R^2  p*x <= p*w} where w and p are given. I got the following 3 defintions, are they correct, which one is preferable? or is there another way ? http://downthetypehole.de/paste/Q8NnfMsK 
16:07 
larsrh 
chindy: I'd prefer the first one 
16:07 
larsrh 
if you're not doing recursion or pattern matching there's no point in fun 
16:07 
larsrh 
whether you want a predicate or a set depends on how you're planning to use it 
16:09 
chindy 
larsrh: so whats the difference between fun and function ? 
16:09 
chindy 
and what are the advantages of using something as set or as predicate? 
16:10 
larsrh 
if you're new to Isabelle you should almost always prefer fun over function 
16:10 
larsrh 
fun = function + automagic 
16:11 
chindy 
ahh so termination etc is not proven automatically? 
16:11 
larsrh 
(automagic = proving termination + sequential pattern matching) 
16:11 
larsrh 
yes 
16:11 
larsrh 
fun uses the "lexicographic_order" tactic to automatically find a, well, lexicographic order 
16:11 
larsrh 
*termination order, that is 
16:21 
chindy 
and what are the advantages of using something as set or as predicate? 
16:26 
chindy 
larsrh: ^ 
17:06 

tautologico joined #isabelle 
17:23 
AtnNn 
pruvisto: I was using the induction tactic wrong. I was doing "induction arbitrary: n rule: f.induct", but this seems to work instead: "induction n w rule: f.induct" 
17:32 

logicmoo joined #isabelle 
17:32 
larsrh 
chindy: depends on your use case, really 
17:32 
larsrh 
if you're going to use stuff like f ` S (image of a function) often, use sets 
17:33 
larsrh 
or if you often have to describe subset relationships 
17:33 
larsrh 
instead if you pass it to higherorder functions, use predicates 
17:40 
pruvisto 
larsrh: actually, I think "fun" can do even more if you import the Multiset order 
17:40 
pruvisto 
but I don't think I ever needed that for anything 
17:41 
pruvisto 
AtnNn: yes, it take some practice to see what variables you have to make arbitrary during induction 
17:41 
pruvisto 
if you choose too few variables, your induction steps might be unprovable even though the overall goal is provable 
17:46 
AtnNn 
thanks a lot for your help. that was the last exercise of the Programming and Proving book. I'm going to start on Concrete Semantics now 
17:47 
AtnNn 
https://github.com/AtnNn/isabellelearn/tree/master/programmingandproving 
17:50 
pruvisto 
if you choose too many, everything will still be provable, but automation might get confused 
17:50 
pruvisto 
and you might, too ^^ 
17:51 
pruvisto 
because more arbitrary variables = more choices 
17:51 
pruvisto 
and one of the secrets for short and easy induction proofs is choosing the right induction rule in order to minimise the amount of wrong choices the automation could make 
17:55 
AtnNn 
I'm getting the hang of that. I just tried two induction proofs from that exercise using all permutations of the induction tactic that I could find 
18:14 
pruvisto 
Concrete Semantics is an excellent way of learning Isabelle 
18:14 
pruvisto 
it's how I got started, more or less 
18:14 
pruvisto 
(I took the lecture upon which the book is based) 
18:15 
pruvisto 
the main "problem" is that that way of learning it is very much on the computer science side of things 
18:15 
pruvisto 
and you don't learn how to do maths in Isabelle 
18:15 
pruvisto 
but it's probably better to do it that way round anyway, because I think computer science/programmingrelated things tend to be more amenable to theorem proving, at least for beginners 
18:15 
pruvisto 
anyway, chindy, I have no idea what the third definition is supposed to mean 
18:16 
pruvisto 
note that that predicate does /not/ check whether the given set is that which contains all x for which P*x â¤ E*P 
18:17 
pruvisto 
it just checks whether that inequality holds for all values that /are/ in the set 
18:17 
pruvisto 
e.g. the predicate would also return "True" for the empty set 
18:17 
pruvisto 
not sure whether that is the way you intended it 
19:07 

stoopkid joined #isabelle 
19:19 
ammbauer 
soooo, how do you do that? http://stackoverflow.com/questions/42532826/findlemmasusedbysimpautoclarify 
19:23 
pruvisto 
simp trace, I guess 
19:23 
pruvisto 
for classical reasoning, I don't think you can trace that 
19:24 
pruvisto 
but I don't know really 
19:24 
pruvisto 
that's why I didn't answer yet 
20:09 
larsrh 
*hushed voice* proof terms *scurries away* 
21:15 
pruvisto 
larsrh: go away 
22:20 

fracting joined #isabelle 
22:41 
chindy 
So that that: "budget_set P E â¡ {x . (P*x) â¤ (E*P)}" return a set with all elements x where (P*x) â¤ (E*P) evaluates to true ? 
23:18 

ezyang joined #isabelle 