Email Gateway (Aug 18 2022 at 12:09): Email Gateway (Aug 18 2022 at 12:09):From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
Hi,
induction over a nested datatype usually involves two statements being
given to the induct method simultaneously. However, if the inductive
hypotheses for the constructors with the nested recursion are not
needed, the statement about the nested case is not needed.
For example:
datatype dt = A
| B dt "dt list"
| C dt
inductive foo :: "dt => nat => bool"
and foos :: "dt list => nat => bool"
where
"foo A 0"
| "[| foo dt n; foos dts n |] ==> foo (B dt dts) n"
| "foo dt n ==> foo (C dt) n"
| "foos [] n"
| "[| foo dt n; foos dts m |] ==> foos (dt # dts) m"
lemma "foo dt 1 ==> False"
apply(induct dt)
apply(auto elim: foo.cases)
done
Here, induct automatically figures out the approriate induction rule and
leaves the induction hypothesis for the list case open. However, this
does not give the cases as nicely as the induction rule provided by the
inductive package, in particular if foo/foos has far more cases.
However, if I want to prove the lemma with the induction rule for foo
and foos, I was only able to prove the lemma with a senseless second
statement
lemma "foo dt 1 ==> False"
and "foos dts n ==> True"
apply(induct dt n=="1::nat" rule: foo_foos.inducts)
apply(auto)
done
So, is there an induction rule for foo/foos with which the second
statement does not have to be written or a trick to tell induct that
only one statement is relevant and the other is supposed to be left open?
Andreas
Email Gateway (Aug 18 2022 at 12:09):From: Makarius <makarius@sketis.net>
The "induct" method merely uses the provided rules in a uniform way. To
get the desired effect you need to produce a rule where the unwanted
branches are specialized to "True", and maybe redundant occurences of such
trivial statements are simplified. For larger inductive definitions this
is quite tedious. In fact the inductive package could do it for you, and
probably will so in the future.
At the moment your example already represents the usual way to do it:
merely state additional statements that will be ignored in the final
result. Inserting "x : A ==> True" in the goal is much shorter than
writing down long induction rule statements for this special case, unless
you do that projected induction very often.
Makarius
Last updated: May 03 2024 at 08:18 UTC