Email Gateway (Aug 19 2022 at 17:29): Email Gateway (Aug 19 2022 at 17:29):From: "W. Douglas Maurer" <maurer@gwu.edu>
I sent this once before and the first line didn't come through, so it
got bounced. I'm sending it again now, as follows. -WDMaurer
I have to teach a unit on mathematical induction to students in my
high-level algorithms class. Many of them were undergraduate
mechanical engineering or electrical engineering majors who switched
in graduate school to being computer science majors, so their
exposure to mathematical induction, during their undergraduate years,
was sketchy at best. One of the books we use presents the basic
principle of mathematical induction to be induction starting from 1
instead of from zero. The first example in that book is
factorial(n) >= 2^(n-1), which, if I try to do it on type nat, makes
no sense for n = 0. All of the examples I have been able to find in
Isar manuals and tutorials are for induction starting from 0. How do
I do induction starting from 1 in Isar?
P. S. While I was still in graduate school I co-wrote a paper
containing an inductive proof in which the inductive step, P(k-1)
implies P(k), depended on the fact that k >= 3. Therefore I needed
two basis steps, one for k = 1, which was trivial, and one for k = 2,
which my co-author supplied. How would you do something like that in
Isar?
Email Gateway (Aug 19 2022 at 17:29):From: Mathias Fleury <mathias.fleury12@gmail.com>
Hello,
On Tuesday 24 March 2015 15:37:40 W. Douglas Maurer wrote:
I sent this once before and the first line didn't come through, so it
got bounced. I'm sending it again now, as follows. -WDMaurerI have to teach a unit on mathematical induction to students in my
high-level algorithms class. Many of them were undergraduate
mechanical engineering or electrical engineering majors who switched
in graduate school to being computer science majors, so their
exposure to mathematical induction, during their undergraduate years,
was sketchy at best. One of the books we use presents the basic
principle of mathematical induction to be induction starting from 1
instead of from zero. The first example in that book is
factorial(n) >= 2^(n-1), which, if I try to do it on type nat, makes
no sense for n = 0.
Actually it makes sense for n = 0, since 0 - 1 = 0 (over natural numbers,
not integers).
All of the examples I have been able to find in
Isar manuals and tutorials are for induction starting from 0. How do
I do induction starting from 1 in Isar?
The easiest way is probably to use a case distinction :
lemma "(fact n :: nat) ≥ 2^(n-1)"
proof (induct n)
case 0
thus ?case by auto
next
case (Suc n) note IH = this
{ assume "Suc n = 1"
hence ?case by auto
}
also {
assume "Suc n > 1"
have ?case sorry
}
ultimately show ?case by arith
qed
If you prefer, the 0 case can be the result of the assumption "n > 0".
P. S. While I was still in graduate school I co-wrote a paper
containing an inductive proof in which the inductive step, P(k-1)
implies P(k), depended on the fact that k >= 3. Therefore I needed
two basis steps, one for k = 1, which was trivial, and one for k = 2,
which my co-author supplied. How would you do something like that in
Isar?
There might be a better solution, but using nat_less_induction rule
(instead of the default nat_induct) associated with case distinctions (k=0,
k=1, k=2, k>=3) like the above should work. If you need often such kind of
induction, proving another induction principle that does the case
distinction might be useful.
Regards,
Mathias Fleury
Email Gateway (Aug 19 2022 at 17:29):From: Joachim Breitner <breitner@kit.edu>
Dear Douglas,
remember that inductions schemes are just regular lemmas, so you can
always define precisely the induction rule that you need, and use that:
lemma ind_from_2[case_names 0 1 2 many]:
assumes "P 0"
assumes "P 1"
assumes "P 2"
assumes "⋀ k. k ≥ 2 ⟹ P k ⟹ P (Suc k)"
shows "P n"
proof(induction n)
case 0 thus ?case by fact
next
case (Suc k)
have "k = 0 ∨ k = 1 ∨ k ≥ 2" by auto
with Suc.IH assms
show ?case by (auto simp add: numeral_eq_Suc)
qed
And later
lemma "foo n"
proof(induction n rule: ind_from_2)
case 0 show ?case...
next
case 1 show ?case...
next
case 2 show ?case...
next
case many show ?case...
qed
I find this separation of concerns makes your proofs much easier to read
and understand.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 17:30):From: Michael Norrish <michael.norrish@nicta.com.au>
Similarly, you might prove induction lemmas like
⊢ P 2 ∧ (∀n. 2 ≤ n ∧ P n ⇒ P (Suc n)) ⇒ (∀n. 2 ≤ n ⇒ P n)
where the 2 ≤ n part has been factored out of the P. I don’t know how to best
apply this theorem in Isabelle; perhaps it would not be as easy as a regular
induction because of the more complicated pattern under the ∀ in the conclusion.
(Clearly it could be cast as an introduction rule.)
Michael
signature.asc
Email Gateway (Aug 19 2022 at 17:30):From: Johannes Hölzl <hoelzl@in.tum.de>
In Isabelle one would write:
lemma nat_induct2[consumes 1]:
"2 <= n ==> P 2 ==> (!!n. 2 <= n ==> P n ==> P (Suc n)) ==> P n"
with the consumes attribute it's stated that 2 <= n is not a induction
step but an assumption for the induction itself.
Email Gateway (Aug 19 2022 at 17:30):From: Christian Sternagel <c.sternagel@gmail.com>
Maybe this is a good point to remind us all of the very nice
"induction_schema" method that comes with the function package by Alex
Krauss (and the automatic "termination" methods that also come with it,
like "lexicographic_order").
lemma ind_from_2 [case_names 0 1 2 many]:
fixes P :: "nat ⇒ bool"
assumes "P 0"
and "P 1"
and "P 2"
and "⋀k. k ≥ 2 ⟹ P k ⟹ P (Suc k)"
shows "P n"
using assms
apply (induction_schema)
apply (case_tac n, force, force)
apply (lexicographic_order)
done
the 2nd line of the proof script is a bit awkward in this case, but can
often be replaced by "apply (pat_completeness)" (which raises an
exception on this specific example).
cheers
chris
Last updated: Apr 19 2024 at 20:15 UTC