Consider a set of N mutually inductive types (say N = 6) and a definition/proof by mutual recursion/induction (using
Fixpoint... with...with, not a mutual induction scheme). Can the definition be represented internally without N-way duplication, and does this multiply typechecking costs by N times? Is this another argument for using induction principles for such proofs?
I ask because I don't see how to avoid it, by looking at Gallina terms: While I write the recursive definition/proof once, there doesn't seem to be a way to _represent it_ in-kernel once — with actual fixpoints, I must replicate the body N times, and in each copy I must select a different member — from
fix a1 ... with aN for a1 to
fix a1 ... with aN for an.
Last updated: Sep 23 2023 at 08:01 UTC