Email Gateway (Aug 18 2022 at 15:45): Email Gateway (Aug 18 2022 at 15:45):From: Tambet <qtvali@gmail.com>
I'm still stuck with inductive proofs. I did seek manuals of inductive
functions, searched Google about induction etc., but they all seem to lack
something.
Case 1:
(* If someone would hint, how to make this a subclass of nat so that lemmas
about nat would be used and I could use it in fix part of lemmas, it would
be nice *)
definition cnat :: "nat => bool" where "cnat n = (0 < n)"
(* This one is already proven - thanks to Lawrence and Rafal *)
lemma cn_is_cnat: "cnat n ==> cnat (cn n)"
(* This defines the following function - an ordered list, which will go to
infinite cycle at end. This would be nice to have a constructor for list,
which contains those elements, but currently this basic syntax should be
enough? *)
inductive cf :: "nat => nat => bool" where
cnf[intro!]:
"cnat n ==> cf (cn n) n" |
cff[intro!]:
"cf m n ==> cf (cn m) n"
(* This follows directly from cf_def and cn_is_cnat. *)
lemma cf_is_cnat: "cnat n ==> cf m n ==> cnat m"
I did try strategies described in
http://www.mkm-ig.org/meetings/mkm06/Presentations/Wenzel.pdf
For example, this:
lemma cf_is_cnat:
assumes "cnat n"
assumes f: "cf m n"
shows "cnat m"
using f
proof (induct n fixing: m)
I would read it as that if I fix m, then I can prove general statements,
which hold for any m. Then I could have case with cnf followed by case with
cff and it would be proven.
Anyway, what I get is that I actually could not fix m:
*** method "HOL.induct": bad arguments
*** : m
*** At command "proof".
lemma cf_is_cnat:
assumes "cnat n"
assumes "cf m n"
shows "cnat m"
proof -
fix x
show "cf (cn x) x ==> cnat (cn x)"
*** Local statement will fail to refine any pending goal
*** Failed attempt to solve goal by exported rule:
*** cf (cn (?x2::nat)) ?x2 ==> cnat (cn ?x2)
*** At command "show".
Now, how could I extract the cases of definition - first case
(non-inductive) is the case "cf (cn x) x"; second case is the inductive case
"cf (cn y) x", where y is resulting "cn ?" from first or second case. It
should be proven if I show that first case gives me number with property
cnat and inductive case gives me number with property cnat if it's given
number with property cnat.
Anyway, I am unable to close such circle. I am unable to define that these
are the cases and all cases.
This is the pattern from isar-overview I also tried:
lemma cf_is_cnat:
assumes "cnat n"
assumes f: "cf m n"
shows "cnat m"
using f
proof (induct m)
fix x
case "cnat n ==> cf (cn n) n"
case "cnat n"
case "cn n"
case cnf
That last list of cases is all kinds of things I tried to use to point out
that I mean the first, noninductive case there.
I can understand that the best way to prove something about recursive
function is:
- Show that the parts of function, which are not recursive ("entry
points") will be True if values given have property x (and False otherwise).
- Show that the parts of function, which are recursive and call those
parts will be True if values given have property x (and False otherwise).
This could be extended by having properties x, y and z and paths, which have
this property. This is finite task to create all possible paths from one to
another and show that iff given values have property x, y or z, then all
calls they make have property z, y or x (for example) and thus, all paths
lead to True if input has any of such properties; then to show that some
such property is assumed.
Anyway, I am probably lacking some critical bit of knowledge to actually
create such path and show about those properties ...manuals give this rather
by example, but my current tries to generalize them to my case do not meet
some constraint if any of them is interpreted as meant at all.
How to solve such cases - example for concrete examples would be nice, link
to general manual not needing too much foreknowledge would be also very
nice. Because this is totally critical for me to have such things proven to
continue - I can already handle the simple non-recursive proofs in many
cases, but I do not catch the logic(s?) behind cases.
Tambet
Email Gateway (Aug 18 2022 at 15:45):From: Tobias Nipkow <nipkow@in.tum.de>
Tambet wrote:
I'm still stuck with inductive proofs. I did seek manuals of inductive
functions, searched Google about induction etc., but they all seem to lack
something.Case 1:
(* If someone would hint, how to make this a subclass of nat so that lemmas
about nat would be used and I could use it in fix part of lemmas, it would
be nice *)
definition cnat :: "nat => bool" where "cnat n = (0 < n)"(* This one is already proven - thanks to Lawrence and Rafal *)
lemma cn_is_cnat: "cnat n ==> cnat (cn n)"(* This defines the following function - an ordered list, which will go to
infinite cycle at end. This would be nice to have a constructor for list,
which contains those elements, but currently this basic syntax should be
enough? *)
inductive cf :: "nat => nat => bool" where
cnf[intro!]:
"cnat n ==> cf (cn n) n" |
cff[intro!]:
"cf m n ==> cf (cn m) n"(* This follows directly from cf_def and cn_is_cnat. *)
lemma cf_is_cnat: "cnat n ==> cf m n ==> cnat m"
lemma cf_is_cnat: "cf m n ==> n>0 ==> m>0"
apply(induct rule: cf.induct)
apply (metis cn_is_cnat)
by (metis cn_is_cnat)
You can easily turn into a structured proof.
I have eliminated cnat - I don't see the point of it. More importantly,
your whole approach is overly complicated. You want to iterate function
cn. Well, simply use function iteration: (cn^^k)(n) is the result of the
k-fold application of cn to n. See compower in theory Nat.thy.
Tobias
I did try strategies described in
http://www.mkm-ig.org/meetings/mkm06/Presentations/Wenzel.pdfFor example, this:
lemma cf_is_cnat:
assumes "cnat n"
assumes f: "cf m n"
shows "cnat m"
using f
proof (induct n fixing: m)I would read it as that if I fix m, then I can prove general statements,
which hold for any m. Then I could have case with cnf followed by case with
cff and it would be proven.Anyway, what I get is that I actually could not fix m:
*** method "HOL.induct": bad arguments
*** : m
*** At command "proof".lemma cf_is_cnat:
assumes "cnat n"
assumes "cf m n"
shows "cnat m"
proof -
fix x
show "cf (cn x) x ==> cnat (cn x)"
*** Local statement will fail to refine any pending goal
*** Failed attempt to solve goal by exported rule:
*** cf (cn (?x2::nat)) ?x2 ==> cnat (cn ?x2)
*** At command "show".Now, how could I extract the cases of definition - first case
(non-inductive) is the case "cf (cn x) x"; second case is the inductive case
"cf (cn y) x", where y is resulting "cn ?" from first or second case. It
should be proven if I show that first case gives me number with property
cnat and inductive case gives me number with property cnat if it's given
number with property cnat.Anyway, I am unable to close such circle. I am unable to define that these
are the cases and all cases.This is the pattern from isar-overview I also tried:
lemma cf_is_cnat:
assumes "cnat n"
assumes f: "cf m n"
shows "cnat m"
using f
proof (induct m)
fix x
case "cnat n ==> cf (cn n) n"
case "cnat n"
case "cn n"
case cnfThat last list of cases is all kinds of things I tried to use to point out
that I mean the first, noninductive case there.I can understand that the best way to prove something about recursive
function is:- Show that the parts of function, which are not recursive ("entry
points") will be True if values given have property x (and False otherwise).
- Show that the parts of function, which are recursive and call those
parts will be True if values given have property x (and False otherwise).This could be extended by having properties x, y and z and paths, which have
this property. This is finite task to create all possible paths from one to
another and show that iff given values have property x, y or z, then all
calls they make have property z, y or x (for example) and thus, all paths
lead to True if input has any of such properties; then to show that some
such property is assumed.Anyway, I am probably lacking some critical bit of knowledge to actually
create such path and show about those properties ...manuals give this rather
by example, but my current tries to generalize them to my case do not meet
some constraint if any of them is interpreted as meant at all.How to solve such cases - example for concrete examples would be nice, link
to general manual not needing too much foreknowledge would be also very
nice. Because this is totally critical for me to have such things proven to
continue - I can already handle the simple non-recursive proofs in many
cases, but I do not catch the logic(s?) behind cases.Tambet
Last updated: Apr 25 2024 at 20:15 UTC