Re: [isabelle] Problem with Int.int_ge_induct



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", so it can be discharged by simp.

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
proof (induct x rule: Int.int_ge_induct)
  case base then show ?case by simp
next
  case (step i) then show ?case by simp
qed

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

Even if you don't want your students to use the induct method, I would
still suggest to use a structured proof:

lemma
  fixes x :: int
  assumes "0 â x"
  shows "x â x * x"
  using assms
proof (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

Which looks almost the same here as the one using the induction method.
But this will change once the goals get more complex.

> P. S. Might there be a problem with Int.int_ge_induct having a
> variable called ?i and a (presumably different) bound variable called
> i? -WDM
No :)

  -- Lars




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