Email Gateway (Aug 18 2022 at 18:52): Email Gateway (Aug 18 2022 at 18:52):From: Lars Hupel <hupel@in.tum.de>
I'd like to prove a theorem which looks like that:
theorem "P i (i+k) ⟹ Q i (i+k)"
I use induction over k for an arbitrary i which works fine for case
0. However, in Suc, I get some assumptions:
P ?i (?i + k) ⟹ Q ?i (?i + k)
P ?i (?i + Suc k)
This is useless so far. What I'd like to have is:
P ?i (?i + ?k) ⟹ ?k < k ⟹ Q ?i (?i + ?k)
At the moment, I am using
theorem
"(⋀k. ⟦ k < n; P i (i+k) ⟧ ⟹ Q i (i+k)) ⟹ P i (i+n) ⟹ Q i (i+n)"
This seems to be rather convoluted, though. What is the usual approach here?
Email Gateway (Aug 18 2022 at 18:52):From: Lars Hupel <hupel@in.tum.de>
I should add that I have no idea whether this works, as I'm still in the
process of figuring out how my proof should look like.
Email Gateway (Aug 18 2022 at 18:52):From: Tobias Nipkow <nipkow@in.tum.de>
I think you need less_induct, induction where you can assume the
property holds for all smaller values. It is used like this:
(induction k arbitrary: i rule: less_induct).
Regards
Tobias Nipkow
Email Gateway (Aug 18 2022 at 18:52):From: Lars Hupel <hupel@in.tum.de>
Thanks, that worked. Now I have a question regarding the recommended
style: Is it better to make a proof without less_induct but rather
with an explicit premise and then prove the proposition as a corollary
using
by
(induct n arbitrary: i nt rule: less_induct)
(fact cyk_correct_helper)
or by stating it as a single theorem, where the structure would look like
proof (induct n arbitrary: i nt rule: less_induct)
case (less n' i nt)
thus ?case
proof (cases n')
case 0
thus ?thesis sorry
next
case (Suc n)
thus ?thesis sorry
qed
qed
The more general question is whether it is good style to nest case
distinction proofs.
Email Gateway (Aug 18 2022 at 18:52):From: Tobias Nipkow <nipkow@in.tum.de>
I don't think there are hard and fast rules. Nesting is certainly not a
crime. I try to avoid auxiliary lemmas and split a proof up only if it
becomes too long or too indented.
Tobias
Last updated: Apr 26 2024 at 08:19 UTC