# IRC log for #isabelle, 2017-03-01

All times shown according to UTC.

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 non-deterministic 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#file-chatper4-thy-L222
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 higher-order 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/isabelle-learn/tree/master/programming-and-proving
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/programming-related 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/find-lemmas-used-by-simp-auto-clarify
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