Email Gateway (Aug 18 2022 at 12:36): Email Gateway (Aug 18 2022 at 12:36):From: "M. Baksys" <mb2412@cam.ac.uk>
Dear all,
I am writing this to ask about an induction argument, which generalizes the
type in its induction hypothesis. My current use case for this is Kneser's
theorem and more specifically, formalisation of its proof, which can be found
on arXiv here: https://arxiv.org/pdf/1303.3539.pdf. In the proof, the argument
inducts over all abelian groups and passes to the quotient group in one of the
cases during the induction step. This creates a type issue even if
generalizing the group itself since the types of elements of the quotient
group and the original group is different. Searching on the internet, I have
found this related StackOverflow question:
https://stackoverflow.com/questions/41002312/free-type-variables-in-proof-by-induction?answertab=trending#tab-top.
It is claimed that a general approach to do this is to "prove instances for
fixed types first" and "then derive a proof generalized in the type itself",
which I can't quite parse myself. Therefore, I would appreciate any help with
this issue.
Note: It is not sufficient to split the argument into an auxiliary lemma
dealing with when the stabilizer is trivial because the proof of that case
uses the induction hypothesis for not necessarily trivial stabilizers.
Last updated: Apr 23 2024 at 20:15 UTC