Email Gateway (Aug 22 2022 at 09:10): Email Gateway (Aug 22 2022 at 09:10):From: "W. Douglas Maurer" <maurer@gwu.edu>
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). But my
question now is: Why am I getting 0 <= 0 in that form? Here is my
proof, in which I have replaced every occurrence of 0 by (0::int), in
order to try (unsuccessfully) to stop generating a subgoal involving
0 rather than 0::int:
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
I have also tried this starting with lemma fixes x::int assumes 4:
"x >= (0::int)" shows "x <= x*x" proof- from 4 have 1: "(0::int) <=
x" by simp
with the same result. -Douglas
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
Email Gateway (Aug 22 2022 at 09:10):From: Lars Noschinski <noschinl@in.tum.de>
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
Email Gateway (Aug 22 2022 at 09:12):From: "W. Douglas Maurer" <maurer@gwu.edu>
Message: 7
Date: Tue, 14 Apr 2015 07:40:33 +0200
From: Lars Noschinski <noschinl@in.tum.de>
Subject: Re: [isabelle] Problem with Int.int_ge_induct
To: cl-isabelle-users@lists.cam.ac.uk
Message-ID: <552CA851.7000501@in.tum.de>
Content-Type: text/plain; charset=UTF-8On 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
Email Gateway (Aug 22 2022 at 09:12):From: Lars Noschinski <noschinl@in.tum.de>
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@in.tum.de>
Subject: Re: [isabelle] Problem with Int.int_ge_induct
To: cl-isabelle-users@lists.cam.ac.uk
Message-ID: <552CA851.7000501@in.tum.de>
Content-Type: text/plain; charset=UTF-8On 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 assmsI'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 simpIn 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
Last updated: Apr 24 2024 at 16:18 UTC