# IRC log for #isabelle, 2016-05-11

All times shown according to UTC.

Time Nick Message
01:47 ilbot3 joined #isabelle
01:47 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/
03:44 cmr joined #isabelle
10:25 ammbauer Can I specify what file Isabelle/jedit opens up by default on startup (instead of ~/Scratch.thy)?
10:38 silver joined #isabelle
11:22 ThreeOfEight joined #isabelle
11:24 ThreeOfEight cocreature: apply assumption
11:28 cocreature ThreeOfEight: I tried that but I only got "Failed to apply proof method". maybe I simplified the example a bit too much to illustrate the problem, here’s the actual state http://lpaste.net/163003. fwiw I was able to solve it using subgoal premises prems and then apply (rule prems) but that seems a bit weird
11:28 larsrh cocreature: "subgoal" is kinda cheating :-)
11:29 ThreeOfEight cocreature: I'm afraid this isn't terribly useful; people cannot really reproduce your problem if you just post the proof state
11:29 ThreeOfEight Can you post enough definitions etc. to actually reproduce this in Isabelle?
11:30 ThreeOfEight Anyway, I think the best answer these days is "Either let the automation do it for you or write it in Isar"
11:30 int-e (presumably  sorted (x # xs)  implies  sorted xs, and that'll prove the first subgoal)
11:31 ThreeOfEight but it is, of course, sometimes useful to know how to use low level tactic scripts
11:31 cocreature ThreeOfEight: sorry, I think this should be enough http://lpaste.net/163004
11:31 cocreature sorry for the german comments
11:31 ThreeOfEight no problem
11:31 int-e the subgoal command is *very* useful in proof exploration
11:31 ThreeOfEight it's fine, I would imagine a significant portion of this channel is German ;)
11:31 ThreeOfEight (like me)
11:31 cocreature larsrh: cheating in what way?
11:31 ThreeOfEight and, yes, there is sorted_Cons, for instnace
11:32 cocreature int-e: yep it does
11:32 ThreeOfEight I was a bit puzzled about what "subgoal" even is
11:33 larsrh cocreature: subgoal introduces a structured Isar proof, and you said you wanted to use a tactic :-)
11:33 ThreeOfEight I should read the change logs more carefully
11:33 cocreature larsrh: ah good point :)
11:33 ThreeOfEight cocreature: KIT?
11:34 cocreature ThreeOfEight: yep :)
11:34 larsrh cocreature: Small world, both ThreeOfEight and me are TUMmies
11:34 ThreeOfEight How utterly surprising for two Isabelle users to be connected to TUM :P
11:35 cocreature also don’t worry about solving my exercises for me. we don’t need to use manual tactics and I have it solved in other ways already
11:35 cocreature heh :)
11:37 larsrh cocreature: who's teaching that course?
11:37 ThreeOfEight Who do you think
11:37 ThreeOfEight Joachim Breitner of course
11:37 cocreature yep
11:37 cocreature and dennis lohner
11:37 ThreeOfEight I still know that name from the Haskell competition
11:37 cocreature eh *denis
11:38 ThreeOfEight he's the one who always solved /every/ problem by throwing GLPK at it
11:38 larsrh Denis "linear programming" Lohner :D
11:38 ThreeOfEight cocreature: btw, referring to "trotz meiner manuellen Tactichacks…"
11:38 ThreeOfEight long-winded apply scripts actually tend to be slower than Isar proofs in many cases
11:38 larsrh cocreature: who told you about case_tac and rule_tac?
11:38 ThreeOfEight because when you write "by", the proof gets forked to the background and processing can resume immediately
11:38 larsrh I'd like to have a word with that person
11:39 ThreeOfEight whereas with an apply script, all of it is done in a single thread
11:39 cocreature ThreeOfEight: ah ok, I thought it would at least be faster than just using auto
11:39 ThreeOfEight depends
11:39 ThreeOfEight if auto has a lot of proof space to search, then yes, it may be faster
11:39 larsrh If auto solves it in <1 second, just use auto, that's the way I do it usually
11:39 cocreature larsrh: the manual :P
11:40 ThreeOfEight I do wonder why this is so horribly slow though
11:40 larsrh cocreature: most, if not all methods ending with _tac should not be used unless you know exactly what you're doing
11:41 cocreature yeah the manual told me that as well :)
11:41 larsrh ...
11:42 larsrh We need to implement that jEdit plays some sound when you use such a method
11:42 larsrh or flashes a biohazard sign or something
11:42 int-e uh this is so low-level. how does one turn (A ==> B) ==> C ==> B into C ==> A (i.e., use an assumption as an intro rule?)
11:42 ThreeOfEight int-e: well, "assumption" should do the trick
11:43 ThreeOfEight but it will probably solve it as well
11:43 ThreeOfEight oh it can't solve it
11:43 ThreeOfEight yeah well then…
11:45 cocreature wait so what am I doing wrong that it doesn’t solve it for me?
11:45 int-e subgoal apply (subst (asm) sorted.simps(2)) apply (erule conjE) apply assumption done  solves the first subgoal
11:45 int-e the assumptions don't fit.
11:45 ThreeOfEight cocreature: it only does that when the precondition of the implication is litteraly there in the premises
11:46 int-e "litteraly" is cute.
11:46 ThreeOfEight I couldn't find any tactic that applies an assumption like an intro rule
11:47 int-e ThreeOfEight: I doubt that is ever a problem in practice... it certainly hasn't come up for me. But thanks for looking!
11:47 ThreeOfEight Well, if it /is/ a problem in practice, then you probably shouldn't solve it this way
11:47 ThreeOfEight but write Isar instead
11:48 cocreature ThreeOfEight: ok, thanks for your help
11:59 ThreeOfEight int-e: You /can/ do this: http://downthetypehole.de/paste/gS54gXg9
11:59 ThreeOfEight allows you to write e.g. "apply (intro_asm 2)" to apply the second assumption as an intro rule
12:00 int-e cocreature: more usefully, perhaps: letrans is a very expensive simp rule, so I wouldn't declare it as simp. lemerge and sortmerge are actually good, safe, intro rules, so one may mark them as [intro!]
12:00 larsrh everyone: disregard what ThreeOfEight wrote, use Isar :p
12:00 ThreeOfEight pff
12:00 ThreeOfEight let me have my fun
12:00 int-e cocreature: with lemerge marked as intro! and letrans not marked at all, the last proof goes throuh fairly quickly using  by (induction xs ys rule: merge.induct) (auto, auto simp: letrans)
12:01 int-e though.
12:01 int-e (the two stage auto actually helps :-/)
12:06 int-e ThreeOfEight: thanks, I almost certainly won't use the tactic but I'll probably try to understand the ML code at some point.
12:07 cocreature int-e: ah great. what’s the criteria for something to be a safe intro rule?
12:07 int-e cocreature: an intro rule is safe if the premises follow from the conclusion.
12:08 cocreature int-e: alright, thanks again!
12:08 int-e (so it's an if and only if, P and Q iff R, expressed in the shape of an introduction rule, "P ==> Q ==> R")
12:09 chuchucorny what is the most simple way to get some sort of well-formndness constraint into a datatype. I have "datatype 'a foo = Foo 'a set  'a set" and want to enforce that for "Foo a b" b is a subset of a. And this should be in the type definition (I don't want additional assumptions in my lemmas)
12:12 int-e cocreature: The premises should also be "simpler" than the conclusion, so that applying the intro rules terminates. But that's also true in your case.
12:41 chuchucorny (okay, dlists seem to be a nice exaple for what I'm looking for)
13:07 ThreeOfEight chuchucorny: probably define a datatype foo_rep, then a well-formedness predicate on the datatype, and then a typedef that enforces the definition
13:08 ThreeOfEight and use lifting/transfer to define functions on that type and transfer lemmas
13:08 ThreeOfEight cocreature: I for one would be careful about declaring things as intro!
13:08 ThreeOfEight because when these things do get you into trouble, it's difficult to find out why
13:09 ThreeOfEight (there is tracing for classical methods, but it's not very nice to use)
13:10 ThreeOfEight and another good rule (in my opinion): don't write simp rules where there are variables in the premises that do not occur in the goal (like in le trans)
13:10 ThreeOfEight you can maybe declare this as dest or something like that, but I wouldn't recommend it
13:10 larsrh tools are in general not very good with transitivity rules
13:11 ThreeOfEight but a simp/intro rule with variables in the premises that do not occur in the goal are basically guaranteed to blow up in your face
13:11 ThreeOfEight *is
13:13 cocreature thank I’ll keep that in mind
13:15 ThreeOfEight also, two consecutive autos are a bad idea
13:16 ThreeOfEight if you want a fast one-line proof, you can do something like this:
13:16 ThreeOfEight by (induction xs ys rule: merge.induct) (auto intro!: lemerge dest: letrans less_imp_le simp: not_le)
13:17 cocreature why are two consecutive autos a bad idea?
13:17 ThreeOfEight (after removing all the simp annotations from those rules)
13:17 ThreeOfEight because "auto" does a lot of things
13:17 ThreeOfEight and the exact things that it does may change with every new Isabelle release
13:17 ThreeOfEight and unlike blast, force, etc., auto doesn't fail when it can't solve the goal
13:17 ThreeOfEight it just leaves the remaining proof obligations behind
13:18 ThreeOfEight but if the behaviour of auto changes, what it leaves behind also changes
13:18 ThreeOfEight and then the subsequent proof methods will suddenly be used on a different proof state and might not work anymore
13:18 ThreeOfEight and the person who will have to fix it will have a hard time figuring out what went wrong and what to do
13:19 ThreeOfEight so it is considered good style to use auto only as the very last proof method
13:19 ThreeOfEight two consecutive autos may still work more or less
13:19 ThreeOfEight it's not great, but it can work fine in practice
13:19 ThreeOfEight however, I've seen people do "proof auto", or "apply auto proof"
13:20 ThreeOfEight and /that/ is pure evil
13:20 fracting joined #isabelle
13:24 cocreature makes sense
13:39 fracting joined #isabelle
14:21 fracting joined #isabelle
19:11 ammbauer "Linear arithmetic should have refuted the assumptions.
19:11 ammbauer Please inform Tobias Nipkow."
19:11 ammbauer ... halp
19:54 ThreeOfEight haha
19:54 ThreeOfEight yeah that happens occasionally
19:54 ThreeOfEight unless you were actively hoping to use linear arithmetic there, I would just ignore that
19:55 ThreeOfEight but you can inform him if you want
20:31 tautologico joined #isabelle
21:39 ammbauer joined #isabelle