Stream: Coq users

Topic: Mutual fixpoints and duplication


view this post on Zulip 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: Jan 28 2023 at 08:02 UTC