Re: [isabelle] Problem with Int.int_ge_induct



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



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