*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Problem with Int.int_ge_induct*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Thu, 16 Apr 2015 09:27:02 +0200*In-reply-to*: <a06200707d15488d4faa5@[192.168.1.6]>*References*: <mailman.33897.1429007609.13101.cl-isabelle-users@lists.cam.ac.uk> <a06200707d15488d4faa5@[192.168.1.6]>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Icedove/31.6.0

On 16.04.2015 04:41, W. Douglas Maurer wrote: >> Message: 7 >> Date: Tue, 14 Apr 2015 07:40:33 +0200 >> From: Lars Noschinski <noschinl at in.tum.de> >> Subject: Re: [isabelle] Problem with Int.int_ge_induct >> To: cl-isabelle-users at lists.cam.ac.uk >> Message-ID: <552CA851.7000501 at in.tum.de> >> Content-Type: text/plain; charset=UTF-8 >> >> On 14.04.2015 06:40, W. Douglas Maurer wrote: >>> From my previous posts you may be aware that I am still looking for >>> the best possible way to do the kind of mathematical induction that is >>> typically taught first in a course on discrete mathematics. After >>> looking over the various replies I have gotten, I would like very >>> much, for most of this, to use Int.int_ge_induct: "?k <= ?i ==> ?P ?k >>> ==> (!!i. ?k <= i ==> ?P i ==> ?P (i + 1)) ==> ?P ?i". >>> This assumes that the induction variable is an int, not a nat, so >>> inductions starting at negative numbers can be covered, as well as >>> numbers greater than zero. It can also be applied to course-of-values >>> induction. >>> Having made this decision, I now tried a very simple case, namely >>> proving by induction that if x >= 0, then x <= x*x. Most of what >>> Int.int_ge_induct is supposed to be doing seems to be working fine, >>> but, at the end, I am getting the message: "Failed to finish proof: >>> goal (1 subgoal): 1. 0 <= 0". Well, it's true that (0::int) <= 0 would >>> be true by simp, but 0 <= 0 is not (and it makes sense to me that it >>> is not, since 0 might be a label, for instance). >> By default, Isabelle does not print the types (and in 2014, it also does >> not show them on hovering in the output, unfortunately), but your goal >> is indeed "(0 :: int) <= 0", > > How can I tell that the rule involves (0 :: int)? Is there some > construction in Isar that I can use, to find this out? In Isabelle 2015, you will be able to see the types of constants by hovering over them. In Isabelle 2014, this is hard to see. To get a hint, replace by (rule ...) by apply (rule ...) using [[show_consts]] This will give you a list of all constants with their types. > >> so it can be discharged by simp. > > I tried discharging this by writing: > have 5: "(0 :: int) <= 0" by simp > I tried this just before, and also just after, the step starting with > "from 1 and 2 and 3". In both cases I still get the same message on > "by (rule Int.int_ge_induct)", namely > Failed to finish proof: goal (1 subgoal): 1. 0 <= 0 > Am I misunderstanding what "discharged" means? You are misunderstanding how "rule" works, I think. When used with chained facts (this is what "from 1 and 2 and 3" does -- it chains the facts 1, 2, 3), it uses the first fact to discharge the first premise of the rule, the second for the second and so on. When you use a fact "A1 ==> ... ==> Am ==> B" to discharge a premise "C1 ==> ... ==> Cn ==> B", you will get m new subgoals, you need to prove: "C1 ==> ... ==> Cn ==> A1" ... "C1 ==> ... ==> Cn ==> Am". Let's have a look at your proof again: assume "x >= (0::int)" then have 1: "(0::int) <= x" by simp have 2: "[|(0::int) <= (0::int)|] ==> (0::int) <= (0::int)*(0::int)" by simp have 3: "!!i. (0::int) <= i ==> (i::int) <= i*i ==> (i::int)+1 <= (i+1)*(i+1)" sorry from 1 and 2 and 3 show "(x::int) <= x*x" by (rule Int.int_ge_induct) The rule Int.int_ge_induct has three premises, you are chaining in three facts. The first fact has no premise, so no new subgoal arises for that. The second fact has one premise, "(0::int) <= (0::int)" and the second premise of Int.int_ge_induct has no premises. This gives you one new subgoal (0::int) <= (0::int) (which Isabelle prints as 0 â 0) Similarly, from the third fact and premise arise the subgoals âi. 0 â i â i â i * i â 0 â i âi. 0 â i â i â i * i â i â i * i Rule is a basic tool and does nothing more then combining the chained facts with the given rule in the way I described above and apply this to the goal. In particular, it does not pick up any other facts you may have proven before. You can see these three subgoals if you write "apply (rule Int.int_ge_induct)" instead of "by (rule Int.int_ge_induct)". So, why does your proof "by (rule Int.int_ge_induct)" complain only about the subgoal "0 â 0" and not the other subgoals? This is because the "by" tries to solve any remaining subgoals with "assumption" and this obviously succeeds for the subgoals 2 and 3. So, that being explained, how can you fix your proof (without rewriting it completely)? "by" can take two proof methods: an initial step to transform the goal and a second step to finish the remaining subgoals. In your case, simp (or simp_all) suffices: by (rule Int.int_ge_induct) simp_all >> You get these goals, because of the way rule works, you still need to >> discharge the assumptions of 2, 3 after rule application. As you don't >> need the assumption in 2, just get rid of it. BTW, 3 is easily proved by >> simp. >> >>> theory IntInduct imports Main begin >>> lemma "[|x >= (0::int)|] ==> (x::int) <= x*x" proof- >>> assume "x >= (0::int)" >>> then have 1: "(0::int) <= x" by simp >>> have 2: "[|(0::int) <= (0::int)|] ==> (0::int) <= (0::int)*(0::int)" >>> by simp >>> have 3: "!!i. (0::int) <= i ==> (i::int) <= i*i ==> (i::int)+1 <= >>> (i+1)*(i+1)" sorry >>> from 1 and 2 and 3 show "(x::int) <= x*x" by (rule Int.int_ge_induct) >>> qed >>> end >> The standard way of applying this induction rule would be: >> >> lemma >> fixes x :: int >> assumes "0 <= x" >> shows "x <= x * x" >> using assms > > I've never needed "using assms" before, and its position in this proof > confuses me. "Programming and Proving in Isabelle/HOL" (prog_prove) > states (p. 43): "There are two further linguistic variations: > (have|show) prop using facts = from facts (have|show) prop...The > 'using' idiom de-emphasizes the used facts by moving them behind the > proposition." This, however, is for "using" within a proof, not before > the word "proof." Then (pp. 43-44), fixes-assumes-shows is introduced, > with the meaning of assms; but there is no reference here to "using" > immediately after fixes-assumes-shows and before "proof." No further > occurrences of "using" in prog_prove involve "using" before the word > "proof." Is there a better writeup which explains this? While these usages may look different, they are exactly the same. All of "have", "show" and "lemma" switch into proof mode. In proof mode, you can * do one-line proofs ("by ..."), * structured proofs ("proof ... qed"), * apply-style proofs ("apply ..."), or * add additional chained facts "using ...")- Both "apply" and "using" modify the proof state and leave you in proof mode. > >> proof (induct x rule: Int.int_ge_induct) >> case base then show ?case by simp > > In this particular proof, the base case is the case "x=0". However, > Int.int_ge_induct also works for proofs with other base cases. If I > were to prove something with base case "x=1", would I still be able to > write "case base then show" here? Yes. This is determined by the single fact you chained in. Int.int_ge_induct is ?k <= ?i ==> ?P ?k ==> (!!i. ?k <= i ==> ?P i ==> ?P (i + 1)) ==> ?P ?i so resolving this with "0 <= x" leaves you with "?P 0 ==> (!!i. 0 <= 0 ==> ?P i ==> ?P (i + 1)) ==> ?P ?i Had you chained in "1 <= x", base would refer to 1 instead. > You appear, here, to be making use of "base" and "step" as what I > believe are called minor keywords within the case construction. Where > are minor keywords (if that's what they're called) defined? These are no keywords, it is just what the author of the induction rule thought the cases ought to be called. The induction method sets up cases according to some additional information stored in the induction rule. To see which cases are there, you can type "print_cases" (or select "cases" in the "print context" tab of the "Query" panel) after the initial "proof (induct ...)" step. Basically, a case is a shortcut for the fix/assume I did manually in my example below and sets up "?case" to refer to the correct goal. -- Lars

**References**:**Re: [isabelle] Problem with Int.int_ge_induct***From:*W. Douglas Maurer

- Previous by Date: Re: [isabelle] Isabelle2015-RC0 available for testing
- Next by Date: [isabelle] 2 new AFP entries
- Previous by Thread: Re: [isabelle] Problem with Int.int_ge_induct
- Next by Thread: [isabelle] error encountered while parsing in autocorres
- Cl-isabelle-users April 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list