IRC log for #isabelle, 2017-03-09

All times shown according to UTC.

Time Nick Message
00:02 rollary could someone point me to an example of how to do proofs by contradiction in isar using "proof contradiction"?
00:02 rollary my proof state has the following two subgoals: 1. ¬ ?P  2. ?P
00:03 rollary how can i specify them? this might be more of an isar question
00:09 JCaesar proof(rule ccontr)
00:10 JCaesar show "¬ something" show "something" (possibly with a next in between.)
00:10 JCaesar (I'd be worried about the thing you're showing, though.)
00:12 JCaesar You can do the same thing with assumptions, btw. if you have goals 1. "?P ==> asdf" 2. "¬ ?P ==> asdf", you can do an assume foo show asdf next assume "¬ foo" show asdf.
00:12 rollary ah, thanks
00:13 rollary why are you worried about what i'm showing? the types notP and P appear in my assumptions
00:13 JCaesar That's okay. But if you have to show ?P and ¬ ?P, I'd be worried.
00:13 rollary i see
00:18 rollary sorry, another question
00:18 JCaesar Oh, btw, there's a nice section in the isar manual that explains how to do all the usual derivations in natural deduction in isar. If you have a bit of a logic background, that might help.
00:19 rollary my theorem looks like this: P -> notP -> Q
00:19 rollary i can't see how to use proof (rule ccontr) to show Q
00:19 JCaesar that might be due to how the facts are… available…
00:20 JCaesar I can't explain this very well.
00:20 JCaesar The rule method doesn't like it if you have facts lying around the way you get then when you use "using".
00:21 JCaesar You can try an apply - before the proof(rule ccontr). If that helps, that was the case.
00:21 rollary ah so would you recommend not using isar for this then?
00:21 JCaesar I wouldn't say that.
00:21 JCaesar I have to ask, though… what's notP?
00:21 JCaesar You said, it was a type, earlier?
00:22 rollary just an assertion?
00:22 rollary i'm sorry, i'm quite new to isabelle
00:22 rollary it's just a statement
00:22 JCaesar did you say anything like lemma "P ==> ¬ P ==> Q"?
00:23 rollary yup
00:23 JCaesar then, a simple by blast should solve the goal.
00:23 JCaesar The assumptions are contradictory, after all.
00:24 JCaesar (if you write "try" instead of apply or proof, it should directly tell you that.)
00:24 JCaesar ("try", and nothing after it.)
00:25 rollary sure, trying (hah)
00:26 rollary ah so it suggests notE
00:26 rollary how do i use it?
00:26 JCaesar Much of the stuff has funny names. There's proof methods called force (so you'll write "apply force"), and a command called sledgehammer.
00:26 JCaesar Oh, it comes back with auto-solve direct?
00:26 rollary yup
00:27 JCaesar Meh, right, that's actually a bit annoying. It's telling you that what you want to prove has already been proved (maybe in a more general way).
00:28 JCaesar In theory, it should be possible to use by(rule notE) as a proof, but I'm not sure that always works.
00:28 JCaesar Try writing try0 instead of try, that will give you concrete instructions.
00:29 JCaesar (I'm not a big fan of try. sometimes it will take ages and you have no idea what it's doing. I usually use try0 and sledgehammer instead.)
00:29 rollary hm, it shows no proof found :/
00:29 rollary why is this so (seemingly) difficult?
00:30 JCaesar issues with unification.
00:30 JCaesar (I'm assuming. No idea.)
00:30 rollary aha, so sledgehammer has done the trick
00:32 rollary i'd like to bother you about another thing now. suppose i have lemma "A ==> B ==> P ==> Q" and I know that A & B ==> not(P)
00:32 rollary how can I prove this new lemma?
00:49 JCaesar proof - assume "A" "B" hence "¬ P" by … moreover assume "P" ultimately show "Q" by … qed
00:53 rollary ah, brilliant, trying it out now - thanks
00:56 rollary what should the last ... be?