Re: [isabelle] Problem with Int.int_ge_induct



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?

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 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?

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? Or would I write something slightly different? Or would I have to spell out assumptions and conclusions, as you have done below?

next
  case (step i) then show ?case by simp
qed

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?


or -- if you prefer to spell out assumptions and conclusions (which I
guess makes sense for teaching):

lemma
  fixes x :: int
  assumes "0 ? x"
  shows "x ? x * x"
  using assms
proof (induct x rule: Int.int_ge_induct)
  show "(0 :: int) ? 0 * 0" by simp
next
  fix i :: int
  assume "0 ? i" "i ? i * i"
  then show "i + 1 ? (i + 1) * (i + 1)"
    by simp
qed

(snip)


  -- Lars


Thanks! -Douglas
--
Prof. W. Douglas Maurer                Washington, DC 20052, USA
Department of Computer Science         Tel. (1-202)994-5921
The George Washington University       Fax  (1-202)994-4875




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.