Paolo Giarrusso (Jun 18 2020 at 22:38): Paolo Giarrusso (Jun 18 2020 at 22:38):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: Apr 20 2024 at 13:01 UTC